sml - Lambda 演算 (SML) - 将一个教堂号码应用于另一个

Question

我试图了解 Church 数字的幂函数：

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

如果您的计算结果是一个教堂编号，您可以通过传递一个后继函数和零来计算它的 int 值：

(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!