Search code examples
smlmllambda-calculuschurch-encoding

Lambda calculus (SML) - Apply a church number to another

I'm trying to understand the exponentiation function on Church numerals:

fun power m n f = n m f;

In it, I see a multiplication. I know that it's wrong, because the multiplication is:

fun times m n f = m ( n f );

and I think to have understood it.

The problem is that I'm not able to understand what function produces the application of a church number to another.

For example, what does this expression produce?

( fn x => fn y => x ( x y ) ) ( fn x => fn y => x ( x ( x y ) ) );

Thanks

Solution

  • if the result of your calculation is a church number, you can calculate its int-value by passing a successor-function and zero: 

    (fn x=> x+1) 0

    In your example:

    ( fn x => fn y => x ( x y ) ) ( fn x => fn y => x ( x ( x y ) ) ) (fn x=> x+1) 0;

    the result is:

    val it = 9 : int

    so you calculated 3^2

    The Term

    ( fn x => fn y => x ( x y ) ) ( fn x => fn y => x ( x ( x y ) ) )

    reduces to

    ( fn x => fn y => x ( x ( x ( x ( x ( x ( x ( x ( x y ) ) ) ) ) ) ) ) )

    But sml can not reduce to this term, it needs the parameters so it can calculate a concrete value.

    A better language for playing with Lambda Calculus is Haskell, because it uses lazy evaluation.

    You can reduce the term 

    ( fn x => fn y => x ( x y ) ) ( fn x => fn y => x ( x ( x y ) ) )

    by yourself:

    fn x => fn y => x (x y) (fn x => fn y => x (x (x y) ) )
reduce x with (fn x => fn y => x (x (x y) ) ):
fn y => (fn x => fn y => x (x (x y) ) ) ( (fn x => fn y => x (x (x y) ) ) y)
rename y to a in the last (fn x => fn y => x (x (x y) ) )
and rename y to b in the first (fn x => fn y => x (x (x y) ) ):
fn y => (fn x => fn b => x (x (x b) ) ) ( (fn x => fn a => x (x (x a) ) ) y)
reduce x in (fn x => fn a => x (x (x a) ) ) with y:
fn y => (fn x => fn b => x (x (x b) ) ) ( fn a => y ( y (y a) ) )
reduce x in (fn x => fn b => x (x (x b) ) ) with ( fn a => y ( y (y a) ) ):
fn y => fn b => ( fn a => y ( y (y a) ) ) ( ( fn a => y ( y (y a) ) ) ( ( fn a => y ( y (y a) ) ) b) )
we reduce a with b in the last term:
fn y => fn b => ( fn a => y ( y (y a) ) ) ( ( fn a => y ( y (y a) ) ) ( y ( y (y b) ) ) )
we reduce a with ( y ( y (y b) ) ) in the last term:
fn y => fn b => ( fn a => y ( y (y a) ) ) ( y ( y (y ( y ( y (y b) ) ) ) ) )
we reduce a with ( y ( y (y ( y ( y (y b) ) ) ) ) ) in the last term:
fn y => fn b => y ( y (y ( y ( y (y ( y ( y (y b) ) ) ) ) ) ) )
we are done!