如何解决如何迭代或重复无类型函数 n 次？
我正在使用 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>
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
