大于 ">" 的 Lambda 演算函数

Question

我最近开始学习 Lambda 微积分作为作业的一部分，我的任务是为逻辑运算符

>

编写一个函数，我们使用的语法与这个视频中所示的相同。 我们可以明确地使用基本数学运算（+、-、/、*）和等于运算符（=），如下所示：

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

我发现这个网站解释了它使用小于或等于并将其与零进行比较，问题在于负数也不同于零。

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

我尝试用第二个数字减去第一个数字，然后以某种方式将结果除以自身，这样我就可以得到

1

if

>

或

-1

if

<

但我总是以负数或正数结束

<

和

>

都是数字对。

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 组合器的应用。如果遇到问题请随时评论。

负整数和平方根运算符

定义

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

的符号。

Answer 2

如果心中的数字是教堂数字，他们会尝试：

lambda n: lambda m: isZero (m - n)

其中：

为零 =

lambda n: n (lambda _: False) True

(-) =

lambda m: lambda n: m pred n

预测 =

λn.λf.λx. n (λg.λh. h (g f)) (λu.x) (λu.u)

（pred 来自维基百科）