functional-programming - 寻找 Church 编码(lambda 演算)来定义 < , > , !=

Question

我必须为 > 、 < 和 != 创建一些 Lambda 函数

我不知道该怎么做，有人可以帮我吗？PS:我们刚刚开始学习 Lambda 微积分，所以请不要假设任何先前的知识。

谢谢期待!

编辑 - 我的意思是Arithmetic in Lambda Calculus

编辑 2 - 更准确:寻找 Church 编码(lambda 演算)来定义 < , > , !=

---

编者注:我认为这就是 OP 试图提出的问题:

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

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

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

1. bool 值真(TRUE 或 λx.λy.x)。
2. bool 值 false(FALSE 或 λx.λy.y)。
3. 逻辑与(AND 或 λp.λq.p q p)。
4. 逻辑或(OR 或 λp.λq.p p q)。
5. 逻辑非(NOT 或 λp.λa.λb.p b a)。

你会怎么写 GT , LT和 NE无类型 lambda 演算中的函数？

Answer 1

使用 "An Introduction To Functional Programming Through Lambda Calculus"通过格雷格迈克尔森

开始于

Section 4.8.3. Comparison

There are a number of ways of defining equality between numbers. One approach is to notice that the difference between two equal numbers is zero. However, if we subtract a number from a smaller number we also get zero so we need to find the absolute difference between them; the difference regardless of the order of comparison. To find the absolute difference between two numbers, add the difference between the first and the second to the difference between the second and the first:

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

If they are both the same then the absolute differences will be zero because the result of taking each from the other will be zero. If the first is greater than the second then the absolute difference will be the first minus the second because the second minus the first will be zero. Similarly, if the second is greater than the first then the difference will be the second minus the first because the first minus the second will be zero.

Thus, we can define:

def equal x y = iszero (abs_diff x y)

We can also use subtraction to define arithmetic inequalities. For example, a number is greater than another if subtracting the second from the first gives a non-zero result:

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

Less 定义在后面的习题解答部分。

def less x y = greater y x

现在使用链接中的书，只需找到所有从属函数，你就会有 =、>、<。虽然这本书没有定义 != 它应该是显而易见的。

编辑

根据 WillNess 的评论

4.8.2. Subtraction

To find the difference between two numbers, find the difference between the numbers after decrementing both. The difference between a number and zero is the number:

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

请注意“现在使用链接中的书，只需找到所有从属函数”。

我不打算搜索所有从属函数并在此处列出它们，因为它们会爆炸并在此处重新创建许多函数。我已经阅读并通读了本书的部分内容，它非常全面，我并不缺乏信息。