sml - 如何获得教堂数字的前身

Question

我正在练习 SML，我正在做一个小任务，我们必须实现教堂数字，定义为：

datatype 'a church = C of ('a -> 'a) * 'a  -> 'a

示例值

ZERO = C(fn (f,x) => x)

我已经实现了以下功能：

create: int -> 'a church  
churchToInt: 'a church -> int  

并SUC返回 Church 数字的后继。

现在我必须实现该功能

PRED: 'a church -> 'a church * 'a church  

它返回 (predecessor, current numeric) 的元组。我不允许使用churchToInt，我应该直接使用 Church 数字。显然，这可以通过传递特定参数在一行中解决。

我一直在考虑SUC一遍又一遍地使用，直到我们找到正确的数字，但我无法比较 2 个 Church 数字。我完全坚持这一点。

Answer 1

假设您要构建为您提供N的 pred 的函数。你必须在这样的数字上使用对 (0,1) (1,2) ....(n,n+1) 并构造succPair函数从 (n-1,n) 到 (n,n+ 1）然后你在（0,1）上应用succPair N次，最后一步你只应用snd我描述的最后一个结果然后繁荣！你得到你的预测N 看这里得到图片http://m2-info-upmc.blogspot.fr/2012/11/predecesseur-sur-les-entiers-de-church.html

Answer 2

您必须通过 subPred 中的 int 强制它。