Lambda calculus (SML) - 将一个教会编号应用于另一个教会编号

Question

我试图理解教会数字上的幂函数：

fun power m n f = n m f;

在其中，我看到了乘法。我知道这是错误的，因为乘法是：

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

我想已经理解了。

问题是我无法理解什么功能产生了教会数字对另一个教会数字的应用。

例如，此表达式产生什么？

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

谢谢

Answer 1

如果你的计算结果是一个教会数字，你可以通过传递一个后继函数和零来计算它的整数值：

(fn x=> x+1) 0

在您的示例中：

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

结果是：

val it = 9 : int

所以你计算了 3^2

术语

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

减少到

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

但是sml不能简化为这个术语，它需要参数才能计算出一个具体的值。

使用Lambda演算的更好语言是Haskell，因为它使用惰性求值。

您可以减少期限

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

由你自己：

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!