CODEWITHSUNDEEP
recursionfunctional-programminglambda-calculusy-combinator
dumdum
dumdum

Reputation: 23

Recursive lambda calculus function

I would like to create a lambda calculus function P such that (P x y z) gives ((x y)(x P)(P z)). I have tried using variants of the Y-combinator/Turing combinator, i.e. functions of the form λg.(g g), since I need to reproduce the function itself, but I can't see any way forward. Any help would be greatly appreciated.

Upvotes: 2

Views: 1510

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15404

Basically you want to solve "β-equation" P x y z = (x y) (x P) (P z). There is a general method of solving equations of the form M = ... M .... You just wrap the right-hand side in a lambda, forming a term L, where all occurrences of M are replaced by m:

L = λm. ... m ...

Then using a fixed-point combinator you get your solution. Let me illustrate it on your example.

L = λp. (λxyz. (x y) (x p) (p z)),
    where λxyz. is a shorthand for λx. λy. λz.

Then, P = Y L, unfolding Y and L we get:

P = (λf. (λg. f (g g)) (λg. f (g g))) (λp. (λxyz. (x y) (x p) (p z)))
  ->β
(λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g))
// the previous line is our "unfolded" P

Let's check if P does what we want:

P x y z
    =   // unfolding definition of P
(λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) x y z
    ->β
((λp. (λxyz. (x y) (x p) (p z))) ((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)))) x y z
    ->β
(λxyz. (x y) (x ((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)))) (((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g))) z)) x y z
    ->β
(x y) (x ((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)))) (((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g))) z)
    =   // folding 1st occurrence of P
(x y) (x P) (((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g))) z)
    =   // folding 2nd occurrence of P
(x y) (x P) (P z)

Q.E.D.

Upvotes: 3

Mulan
Mulan

Reputation: 135187

U-combinator should help you create a self-referential lambda abstraction.

Here is Ω, the smallest non-terminating program that exhibits the U-combinator nicely.

((λf. (f f))
 (λf. (f f)))

If you can give it a name

Ω := λf.(f f)

Here's what it might look like with your abstraction

((λP. (P P x y z))
 (λP. λx. λy. λz. ((x y) (x P) (P z))))

Or using Ω

λx. λy. λz. Ω (λP. λx. λy. λz. ((x y) (x P) (P z))) x y z

Upvotes: 2

Related Questions