What do the lambdas?
An expression is one of the following:
- <identifier> (variable reference)
- λ<identifier>.<exp> (function abstraction, but sometimes we’ll just call it a “lambda”)
- <exp> <exp> (function application)
Is like tree. Variable references are leaves. Function application branches into two sub-trees, one for function and one for argument.
Function application is left associative. So a b c and (a b) c works out the same.
For example, can take a look at expression (λa.a (foo a)) bar and its sub-expressions:
- (λa.a (foo a)) bar is a function application with a function (λa.a (foo a)) and an argument bar
- λa.a (foo a) is a function abstraction with a parameter x and a body a (foo a).
- a (foo a) is a function application with a function a and argument foo a
- foo a is a function application with a function foo and argument a
And we can do like a little tree-drawing, like maybe like this:
(So really, syntax is mostly like in an ML family language or a Haskell or something. Only instead of like, fn x => foo or fun x -> foo or \x -> foo), we do λx.foo. Andalso there’s never any infix stuff for function application.)
Evaluation goes mostly like so: (λx.B) A ⟶ [A/x]B.
Meaning something like, a “reducible expression” (the bit to the left of the arrow) is:
- a function application
- with a function-part that is a function abstraction, with some identifier x as its parameter and some expression B as its body
- and with an argument-part that is some expression A
And if we have a reducible expression, then we can do “beta reduction”: Substitute the argument A for every free occurence of the parameter x in the body B, and replace the whole function application with the result of that.
(The part that goes [A/x]B means that substitution thing: B but with every free x replaced with A. So (λx.B) A ⟶ [A/x]B is a bit like a pattern match on the syntax of an expression. Like, the expression to the left of the arrow binds the variables x and B and A, and the expression to the right uses them.)
Can try. With the expression (λz.z bar) foo, the parameter x is z, the body B is z bar, and the argument A is foo. So for this “instance” of (λx.B) A ⟶ [A/x]B we get (λz.z bar) foo ⟶ [foo/z]z bar. It should evaluate to the body z bar with every free z replaced by the argument foo: foo bar. (ctrl+enter below)
A variable reference is free if it is not bound by a parameter in a function abstraction. With the expression (λz.z (λz.bar z) bar) foo, the parameter x is z, the body B is z (λz.bar z) bar, and the argument A is foo. Here, only the first z in the body z (λz.bar z) bar is free, so only that one is replaced with foo.
(In maybe more programmy jargon, we could maybe say that the inner z shadows the outer.)
Sometimes we have to change the names of some variables before doing beta reduction, in order to avoid having “variable capture” change the meaning of our expression. With the expression (λx.λy.y x) y, the parameter x is x, the body B is λy.y x, and the argument A is y. If we just replace the x in λy.y x with y, we get λy.y y. Our argument-y becomes like bound (“captured”) by the parameter of the lambda within the body. Is no good. We should be able to keep refering to some outer y. So, we change the name of the parameter of the lambda (and all references to it) before we do beta reduction. (ctrl+enter two times, since the first one will just rename the parameter)
That’s mostly it. We:
- look through our expression-tree in some order
- maybe find a reducible expression
- rename things if necessary
- and do the substitution thing
The order we look through the expression-tree is “normal order”. We check the outermost expression first, and then the function-parts of applications before the argument-parts. If we can’t find any reducible expression, then the expression is on “normal form”.
Typically we want to evaluate something down to normal form. So we run through those steps over and over until it is. (If we’re unlucky that takes actually forever. But that’s cool too.)
Can do (ctrl+shift+enter) to evaluate the foillowing until it’s on normal form: