Search code examples
recursionfunctional-programminglambda-calculusy-combinator

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.


Solution

  • 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.