寻找一个使用 Church 编码（λ演算）来定义 <、> 和 != 的方法。

Question

我需要创建一些Lambda函数来处理 >, < 和 !=，但我不知道该如何操作，是否有人能帮助我？PS：我们刚开始学习Lambda演算，请不要假设任何先前的知识。谢谢提前！

编辑 - 我的意思是使用lambda演算实现Lambda演算中的算术运算

编辑2 - 更准确地说：寻找一个Church编码（lambda演算）来定义<、>和!=。

---

编辑者注： 我认为这就是OP所尝试询问的内容：

我正在尝试使用Church编码在无类型 lambda 演算中实现以下操作：

1. 大于 (GT 或 >)。
2. 小于 (LT 或 <)。
3. 不等于 (NE 或 !=)。

我已经知道如何实现以下内容：

1. 布尔值 true (TRUE 或 λx.λy.x)。
2. 布尔值 false (FALSE 或 λx.λy.y)。
3. 逻辑 AND (AND 或 λp.λq.p q p)。
4. 逻辑 OR (OR 或 λp.λq.p p q)。
5. 逻辑 NOT (NOT 或 λp.λa.λb.p b a)。

你会如何在无类型 lambda 演算中编写 GT、LT 和 NE 函数？

- Blnpwr

---

“为>创建Lambda函数”是什么意思？一个只包装操作符的Lambda函数？那有什么意义呢？ - Sebastian Redl

一个表示“>”的Lambda函数：(\a b -> a > b)。您现在能创建另外两个吗？ - Will Ness

@user2938633 哦，我们非常清楚什么是lambda。但你到底在问什么？ - Bartek Banachewicz

没错，非常感谢 Chris Taylor。 - Blnpwr

a > b == (a-b) > 0. 那有帮助吗？ - Will Ness

Answer 1

使用 Greg Michaelson 的 "通过 Lambda 演算介绍函数式编程"

从以下开始

第4.8.3节。比较

有许多定义数字相等的方法。一种方法是注意到两个相等数之间的差为零。但是，如果我们从一个较小的数字中减去另一个数字，我们也会得到零，因此我们需要找到它们之间的绝对差异；无论比较顺序如何，都是不变的差异。要找到两个数字之间的绝对差异，请将第一个和第二个之间的差异加上第二个和第一个之间的差异：

def abs_diff x y = add (sub x y) (sub y x)

如果它们都相同，则绝对差异将为零，因为从一个数字中减去另一个数字的结果将为零。如果第一个数字大于第二个数字，则绝对差异将是第一个减去第二个，因为第二个减去第一个将为零。同样，如果第二个数字大于第一个数字，则差异将是第二个减去第一个，因为第一个减去第二个将为零。

因此，我们可以定义：

def equal x y = iszero (abs_diff x y)

我们还可以使用减法来定义算术不等式。例如，如果从第二个数字中减去第一个数字得到非零结果，则一个数字大于另一个数字：

def greater x y = not (iszero (sub x y))

Less是在后面的练习解决方案部分中定义的。

def less x y = greater y x

现在只需使用链接中的书籍查找所有下属函数，您将拥有=、>和<。虽然该书没有定义!=，但这应该很明显。

编辑

根据WillNess的评论，请注意：

4.8.2. 减法

要找出两个数字之间的差异，请在减少两个数字后找到它们之间的差异。一个数字与零之间的差异就是这个数字：

rec sub x y =
if iszero y
then x
else sub (pred x) (pred y)

请注意 "现在只需使用链接中的书籍查找所有下属函数"。

我不打算追寻所有下属函数并在此列出它们，因为这会导致重新创建许多函数。我已经阅读并完成了该书的部分内容，它足够全面，我不缺乏信息。

- Guy Coder

---

是的，但sub是什么？楼主说他们甚至没有pred函数。感谢链接 :) - Will Ness

Answer 2

您还需要实现自然数。这就是您将要为其编写比较运算符的原因，对吗？

我记得自然数的实现方式。一个数字n表示为一个接受函数f和值x的函数，并在x上应用f n次。

zero = λf . λx . x
succ = λn . λf . λx . n f (f x)

- md2perpe

Answer 3

“Church编码”维基百科文章中的一个章节讲述谓词，其中涵盖了EQ和LEQ。

- dansalmo