logical-operators - 大于 ">"的 Lambda 微积分函数

Question

我最近开始学习 Lambda 微积分作为作业的一部分，我的任务是为逻辑运算符编写函数 > ，我们使用的语法与 this video 中所示的相同.
我们可以明确地使用基本的数学运算(+、-、/、*)和等号运算符(=)，如下所示:

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

我找到了 this website这解释了它使用小于或等于并将其与零进行比较，问题在于负数也不同于零。

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

我尝试从第二个数字中减去第一个数字，然后以某种方式将结果除以本身，这样我就可以得到 1如果 >或 -1如果 <但我总是以消极或积极的方式结束 <和 >数对。

Answer 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-combinator的应用。如果您遇到问题，请随时发表评论。

负整数和平方根运算符

定义

如果你有负数，我能想到的最好的就是这个。我不会使用 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))

注:我冒昧让 bool 表达式返回整数 1或 0而不是函数 TRUE或 FALSE ，如 Collected Lambdas你贴的链接。如果这是一个问题，您可以编写一个映射 TRUE 的函数。至 1和 FALSE至 0 .

解释

如果你只看 LT 的最后一个等式，很明显它为什么起作用。您首先计算 x - y .然后，你取那个表达式的符号。 x - y的标志如果 -1伊夫 x < y是真的。
SIGN的解释就是，当 x == 0 ，我们将得到表达式 0/1 ， 哪个是正确的。如 x != 0 ，那么我们将有 |x|/x ，这将是 -1或 1取决于 x的标志.