Lecture Notes 
Programming Languages and Types

October 29, 2009
Instructor: Tillmann Rendel


The Y Combinator
----------------


We can write recursive programs without supporting recursion directly in our
language. As a first step, consider the following program.

  {{fun {x} {x x}} {fun {x} {x x}}}

Evaluating the application (in a substitution-based interpreter) yields:

  {{fun {x} {x x}} {fun {x} {x x}}}
  
which is the program itself. Therefore, the execution of this program never
terminates. We have written a nonterminating program without using recursion or
loops or any other language constructs usually associated with non-termination.

We can build upon this nonterminating program to simulate recursion. But first,
we need a recursive function to test it. Lets write a function sum which adds
the first n integers, but without using recursion. To do so, we assume that we
have already defined sum, and can take it as a parameter.

  {fun {sum}
    {fun {n}
      {if0 n
           0
           {add n {sum {add n -1}}}}}}

Lets call this function F. Note that it returns sum, if given sum. In other
words, sum is a fixed point of F. 

  {F sum} = sum

We can now write a function which computes the fixed point of a function. We
will call it Y. In other words, Y is a fixed point combinator. Then, we will
be able to calculate sum as follows.

  sum = {Y F}

We can adapt the nonterminating program from above to apply F everytime it
copies itself.

  Y = {fun {f} {{fun {x} {f {x x}}} {fun {x} {f {x x}}}}}

Is (Y F) really a fixed point of F?

Lets check {F {Y F}} = {Y F}.

The left-hand-side is:

    {F {Y F}}
  = {F {{fun {f} {{fun {x} {f {x x}}} {fun {x} {f {x x}}}}} F}} ; definition of Y
  = {F {{fun {x} {F {x x}}} {fun {x} {F {x x}}}}}               ; application

and the right-hand-side is:

    {Y F}
  = {{fun {f} {{fun {x} {f {x x}}} {fun {x} {f {x x}}}}} F}     ; definition of Y
  = {{fun {x} {F {x x}}} {fun {x} {F {x x}}}}                   ; application
  = {F {{fun {x} {F {x x}}} {fun {x} {F {x x}}}}}               ; application

Since {F {Y F}} = {Y F}, we know that {Y F} is the fixed point of F, so Y is
indeed a fixed point combinator.