问题描述
我正在使用 OCaml 编译器练习,我正在做一个小作业,我们必须实现定义为的教堂数字:
zz = pair c0 c0; ss = λp. pair ( snd p) ( plus c1 (snd p)); prd = λm. fst (m ss zz );
并计算我想要实现的 ss 加:
plus = λm. λn. λs. λz. m s (n s z)
所以我的问题是,如何实现功能加,比如 n 次成功 0?
我试过了
plus = lambda m. lambda n. lambda s. lambda z. m s (n s z);
但它在编译器中是不正确的。
我注意到我在 OCaml 编译器中工作并将所有函数写入 func.f 文件而不是 .ml 文件
https://www.cis.upenn.edu/~bcpierce/tapl/ 代码来自那里,完整的文件夹
解决方法
与 lambda 演算中的 lambda
不同,您使用 fun
在 OCaml 中对 Church 数字进行编码。您将数字定义为采用一元函数(名为 s
表示“后继”)和基值(z
表示“零”)的函数。例如,三是:
# let three = fun s z -> (s (s (s z)));;
val three : ('a -> 'a) -> 'a -> 'a = <fun>
如果您想将此表示转换为 OCaml 整数,您可以定义:
# let int_succ x = x + 1;;
然后你可以通过像这样调用它来获得 three
的 OCaml 整数表示:
# three int_succ 0;;
- : int = 3
它有效地在 0、最里面的结果(即 1)等上连续调用 int_succ
,直到得到 3。
但是您可以按如下方式在其 Church 表示中操纵这些数字。例如,要计算任意 Churn 数 n 的后继 Church 数:
# let succ n = fun s z -> (s (n s z));;
我们必须返回一个教堂数,结果是两个参数 s
和 z
的函数。它还需要一个输入,一个教堂编号 n
。结果是在 s
上调用 (n s z)
,即数字 n
的后继者。例如:
# (succ three) int_succ 0;;
- : int = 4
同样,我们可以定义add
:
# let add x y = (fun s z -> (x s (y s z)));;
val add : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun>
这里,函数需要两个数字。表达式(y s z)
表示对数y
进行的计算,在x
中应用(x s (y s z))
时将其用作基值。如果您将 int_succ
和 0 用于 s
和 z
,您可以看到 (y s z)
将从 0 递增与 y
编码的次数相同,然后递增来自该值的次数与由 x
编码的次数相同。
例如:
# let two = fun s z -> (s (s z)) ;;
val two : ('a -> 'a) -> 'a -> 'a = <fun>
那么:
# let five = add two three;;
val five : ('_weak4 -> '_weak4) -> '_weak4 -> '_weak4 = <fun>
请注意类型是弱,您不必担心太多,但这意味着一旦您使用给定的 s
和 z
调用 5 ,您将无法对不同类型重复使用 five
。
# five int_succ 0;;
- : int = 5
现在,类型是完全已知的:
# five;;
- : (int -> int) -> int -> int = <fun>