While preparing Subtleties of Instance Variable Initialization and Recursive Records and Instance Variable Initialization, I wanted to work out what actually happens in lambda calculus to recursive records. I decided to settle for recursive pairs as an equivalent but more practical endeavor.

Pairs get constructed:

pair = λx.`λy.``λz.z x y`

And destructed:`fst = λp.``p(λx.``λy.x)``snd = ``λp.``p(λx.``λy.y)`

How does this pair constructor work? Give it the first and second elements, and it returns a "visitor" function, if you will:`p1 = pair 1 2 = ``λz. z 1 2`

Now p1 is a function (of course) taking a visitor z. The function z is written so as to get both values of p1 to do with whatever it needs. The destructors are example visitors:

fst p1 Replace fst with its definitionArmed with that, and the definition of the Y combinator below, can you show what happens to this recursive tuple:

= (λp.p(λx.λy.x)) p1 Beta reduce, replacing p with p1 in λ body

= p1(λx.λy.x) Replace p1 with its definition

= (λz. z 1 2)(λx.λy.x) Beta reduce, replacing z with p1 in λ body

= (λx.λy.x) 1 2 Beta reduce, replacing x with 1 in λ body

= (λy.1) 2 Beta reduce is trivial since y never occurs

= 1

`Given Y =`

`λf.`

`(`

`λx.`

`f(λy.x x y`

`)`

`)`

`(`

`λx.`

`f(λy.x x y`

`)`

`)`,

what happens to

Y (λthis. pair 1 (+ (fst this) 1))

Y (λthis. pair 1 (+ (fst this) 1))

?

If you don't know, try whipping up these encodings (including Church numerals for the ints) in your favorite language and evaluating the example.

## No comments:

Post a Comment