Lambda 演算 (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!

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

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

sml

ml

lambda-calculus

church-encoding