仅使用递增、循环、赋值、零的关系操作

Question

这是以下问题的后续问题：

我们只允许使用以下操作：

incr(x) - 一旦调用此函数，它将 x + 1 分配给 x
assign(x, y) - 此函数将把 y 的值赋给 x (x = y)
zero(x) - 此函数会将 0 分配给 x (x = 0)
loop X { } - 括号内的操作将执行 X 次

例如加法可以这样实现：

add(x, y) {
    loop x
        { y = incr(y) }
    return y
}

如何使用这四种操作实现 relational operators？关系操作是：

eq(x, y) - x 等于 y 吗？
lt(x, y) - x 是否小于 y？
gt(x, y) - x 是否大于 y？

我们也有他们的对立面：

ne(x, y) - x 不等于 y 吗？
gte(x, y) - x 是否大于或等于 y？
lte(x, y) - x 是否小于或等于 y？

任何帮助将不胜感激。

Answer 1

自然数集N在加减法下是封闭的：

N + N = N
N - N = N

这意味着两个自然数的加法或减法也是自然数（考虑到0 - 1是0而不是-1，我们不能有负自然数).

然而，自然数集N在关系运算下不闭合：

N < N = {0, 1}
N > N = {0, 1}

这意味着比较两个自然数的结果要么为真（即1），要么为假（即0）。

因此，我们将布尔集（即{0, 1}）视为自然数的受限集（即N）。

false = 0
true  = incr(false)

我们必须回答的第一个问题是“我们如何对 if 语句进行编码，以便我们可以根据真假进行分支？”答案很简单，我们使用loop操作：

isZero(x) {
    y = true
    loop x { y = false }
    return y
}

如果循环条件是true（即1）那么循环只执行一次。如果循环条件是 false（即 0），则循环不执行。我们可以用它来编写分支代码。

那么，我们如何定义关系操作呢？事实证明，一切都可以用 lte:

来定义

lte(x, y) {
    z = sub(x, y)
    z = isZero(z)
    return z
}

我们知道x ≥ y和y ≤ x是一样的。因此：

gte(x, y) {
    z = lte(y, x)
    return z
}

我们知道，如果 x > y 为真，那么 x ≤ y 为假。因此：

gt(x, y) {
    z = lte(x, y)
    z = not(z)
    return z
}

我们知道x < y和y > x是一样的。因此：

lt(x, y) {
    z = gt(y, x)
    return z
}

我们知道如果 x ≤ y 和 y ≤ x 那么 x = y。因此：

eq(x, y) {
    l = lte(x, y)
    r = lte(y, x)
    z = and(l, r)
    return z
}

最后，我们知道如果 x = y 为真那么 x ≠ y 为假。因此：

ne(x, y) {
    z = eq(x, y)
    z = not(z)
    return z
}

现在，我们需要做的就是定义以下函数：

sub函数定义如下：

sub(x, y) {
    loop y
        { x = decr(x) }
    return x
}

decr(x) {
    y = 0
    z = 0

    loop x {
        y = z
        z = incr(z)
    }

    return y
}

not函数与isZero函数相同：

not(x) {
    y = isZero(x)
    return y
}

and函数与mul函数相同：

and(x, y) {
    z = mul(x, y)
    return z
}

mul(x, y) {
    z = 0
    loop x { z = add(y, z) }
    return z
}

add(x, y) {
    loop x
        { y = incr(y) }
    return y
}

这就是您所需要的。希望对您有所帮助。

仅使用递增、循环、赋值、零的关系操作

Relational operations using only increment, loop, assign, zero

algorithm

math

logic

equality

lambda-calculus