Pairs and Y

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 definition
= (λ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

Armed with that, and the definition of the Y combinator below, can you show what happens to this recursive tuple:

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))
?

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