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.
Add a comment
|
2 Answers
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.
Comments
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
