【问题标题】：Lambda Calculus exfunction for Greater Than ">"大于“>”的 Lambda 微积分函数
【发布时间】：2019-01-23 23:00:41
【问题描述】：

我最近开始学习 Lambda 微积分作为作业的一部分，我的任务是为逻辑运算符 > 编写一个函数，我们使用的语法与 this video 中所示的语法相同。我们可以像这样显式地使用基本的数学运算（+、-、/、*）和等号运算符（=）：

λx.λy.(x - y)
λx.λy.(x = y) TRUE FALSE

我发现this website 解释它使用小于或等于并将其与零进行比较，问题是负数也不同于零。

有没有办法编写一个像这样的 GT 运算符一样工作的 Lambda 微积分函数？

我尝试从第二个数字中减去第一个数字，然后以某种方式将结果除以自身，这样我可以得到 1 如果> 或 -1 如果 < 但我总是以负数或< 和 > 数字对均为正数。

【问题讨论】：

【解决方案1】：

前言

我能想到的最好办法是要么只使用非负整数，要么允许平方根运算符。

没有负整数

如果您没有使用负数，则可以使用递归（使用 Y 组合器）对以下函数建模（使用 Python 语法）：

def lt(x, y):
  if y == 0:
    return False
  elif x == 0:
    return y != 0
  else:
    return lt(x - 1, y - 1)

既然这还不算太糟糕，我会让你自己弄清楚 Y 组合器的应用。如果您有问题，请随时发表评论。

如果你有负数，我能想到的最好的就是这个。我不会使用 lambda 演算符号，因此您可以自己转换这些符号：

ABS(x) = if (x == 0) then 0 else sqrt(x * x)
SIGN(x) = ABS(x) / (x + (x == 0))
LT(x, y) = (-1 == SIGN(x - y))

注意：我冒昧地让布尔表达式返回整数 1 或 0 而不是函数 TRUE 或 FALSE，如 Collected Lambdas 链接你发布了。如果这是一个问题，您可以编写一个函数，将TRUE 映射到1 和FALSE 到0。

如果您只看LT 的最后一个等式，就会很清楚它为什么起作用。你首先计算x - y。然后，你拿那个表情的符号。 x - y 的符号 if -1 iff x < y 为真。

SIGN 的解释是，当x == 0 时，我们将有表达式0/1，这是正确的。如果x != 0，那么我们将有|x|/x，这将是-1 或1，具体取决于x 的符号。

【讨论】：