context of the lambda calculus can be found here:
[Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
Sestoft also provides a lovely on-line lambda evaluator:
context of the lambda calculus can be found here:
[Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
Sestoft also provides a lovely on-line lambda evaluator:
which allows you to select multiple evaluation strategies,
and to see reductions happen step by step.
which allows you to select multiple evaluation strategies,
and to see reductions happen step by step.
Using a Continuation Passing Style transform to control order of evaluation
---------------------------------------------------------------------------
Using a Continuation Passing Style transform to control order of evaluation
---------------------------------------------------------------------------
using a Continuation Passing Style transform (CPS), then we'll explore
what the CPS is doing, and how.
using a Continuation Passing Style transform (CPS), then we'll explore
what the CPS is doing, and how.
beta reduction: beta reduction does not occur underneath a lambda.
That is, `(\x.y)z` reduces to `z`, but `\w.(\x.y)z` does not, because
the `\w` protects the redex in the body from reduction.
beta reduction: beta reduction does not occur underneath a lambda.
That is, `(\x.y)z` reduces to `z`, but `\w.(\x.y)z` does not, because
the `\w` protects the redex in the body from reduction.
After using the following call-by-name CPS transform---and assuming
that we never evaluate redexes protected by a lambda---only the first
After using the following call-by-name CPS transform---and assuming
that we never evaluate redexes protected by a lambda---only the first
Both xforms make the following guarantee: as long as redexes
underneath a lambda are never evaluated, there will be at most one
Both xforms make the following guarantee: as long as redexes
underneath a lambda are never evaluated, there will be at most one
That is, all choice is removed from the evaluation process.
Questions and excercises:
That is, all choice is removed from the evaluation process.
Questions and excercises:
type form = Var of char | Abs of char * form | App of form * form;;
3. What happens (in terms of evaluation order) when the application
rule for CBN CPS is changed to `[MN] = \k.[N](\n.[M]nk)`? Likewise,
type form = Var of char | Abs of char * form | App of form * form;;
3. What happens (in terms of evaluation order) when the application
rule for CBN CPS is changed to `[MN] = \k.[N](\n.[M]nk)`? Likewise,
CBN xform of a variable appears to be an exception, but instead of
writing `[x] => x`, we can write `[x] => \k.xk`, which is
eta-equivalent. The `k`'s are continuations: functions from something
CBN xform of a variable appears to be an exception, but instead of
writing `[x] => x`, we can write `[x] => \k.xk`, which is
eta-equivalent. The `k`'s are continuations: functions from something
-to a result. Let's use $sigma; as the result type. The each `k` in
-the transform will be a function of type `ρ --> σ` for some
+to a result. Let's use σ as the result type. The each `k` in
+the transform will be a function of type ρ --> σ for some