Slide 12.4: Syntax of the lambda calculus (cont.) Slide 12.6: Curried functions Home |
λx y z . E means ( λx . ( λy . ( λz . E ) ) )
define <name> = <expression>
For example, given define Twice = λf.λx.f(f x)
, it follows that
( Twice (λn.(add n 1)) 5 ) = 7Imagine that
Twice
is replaced by its definition as with a macro expansion before the lambda expression is reduced.
( λn . λf . λx . f ( n f x ) ) ( λg . λy . g y )
We first identify the lambda abstractions, using the rule that the scope of lambda variable extends as far as possible.
Observe that the lambda abstractions in the first term are ended by an existing set of parentheses.
( λx . f ( n f x ) ) ( λy . g y ) ( λf . ( λx . f ( n f x ) ) ) ( λg . (λy . g y ) ) ( λn . ( λf . ( λx . f ( n f x ))))Then grouping the combinations by associating them to the left yields the completely parenthesized expression:
( (λn.(λf.(λx.(f(( n f ) x ))))) (λg.(λy.( g y ))) )