0

我正在尝试在 lambda 演算中定义二进制指数运算符，例如运算符 CARAT。例如，这个运算符可能有两个参数，数字 2 的 lambda 编码和数字 4 的 lambda 编码，并计算数字 16 的 lambda 编码。我不知道我的答案是对还是错，但我花了一天时间这样做。我使用了教堂数字定义。

这是我的答案。如果我的回答有误，请纠正我。我不知道如何以正确的方式做到这一点。如果有人知道，请帮我找出简短的答案。

加一的后继函数可以用和next定义自然数：zeronext

1 = (next 0)    
2 = (next 1)
  = (next (next 0))    
3 = (next 2)
  = (next (next (next 0)))

根据以上结论，我们可以定义next如下函数：

next = λ n. λ f. λ x.(f ((n f) x))
one  = (next zero)
     => (λ n. λ f. λ x.(f ((n f) x)) zero)
     => λ f. λ x.(f ((zero f) x))
     => λ f. λ x.(f ((λ g. λ y.y f) x)) -----> (* alpha conversion avoids clash *)
     => λ f. λ x.(f (λ y.y x))
     => λ f. λ x.(f x)

因此，我们可以有把握地证明……

zero = λ f. λ x.x
one = λ f. λ x.(f x)
two = λ f. λ x.(f (f x))
three = λ f. λ x.(f (f (f x)))
four = λ f. λ x.(f (f (f (f x))))
:
:
:
Sixteen = λ f. λ x.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))

加法只是继任者的迭代。我们现在可以根据以下条件定义加法next：

m next n => λx.(nextm x) n => nextm n => m+n
add = λ m. λ n. λ f. λ x.((((m next) n) f) x)
four = ((add two) two)
     => ((λ m. λ n. λ f. λ x.((((m next) n) f) x) two) two)
     => (λ n. λ f. λ x.((((two next) n) f) x)two)
     => λ f. λ x.((((two next) two) f x)
     => λ f. λ x.(((( λ g. λ y.(g (g y)) next) two) f x)
     => λ f. λ x.((( λ y.(next (next y)) two) f) x)
     => λ f. λ x.(((next (next two)) f) x)
     => λ f. λ x.(((next (λ n. λ f. λ x.(f ((n f) x)) two)) f) x)

在将值替换为 'next' 和随后的 'two' 之后，我们可以进一步将上述形式简化为

     => λ f. λ x.(f (f (f (f x))))

即四个。

同样，乘法是加法的迭代。因此，乘法定义如下：

mul = λ m. λ n. λ x.(m (add n) x)
six = ((mul two) three)
 => ((λ m. λ n. λ x.(m (add n) x) two) three)
 => (λ n. λ x.(two (add n) x) three)
 => λ x.(two (add three) x
 => ( λf. λx.(f(fx)) add three) 
 =>( λx.(add(add x)) three)
 => (add(add 3))
 => ( λ m. λ n. λ f. λ x.((((m next) n) f) x)add three)
 => ( λ n. λ f. λ x.((( three next)n)f)x)add)
 => ( λ f. λ x.((three next)add)f)x)

在将值替换为“three”、“next”和随后的“add”，然后再次替换“next”后，上述形式将简化为

 => λ f. λ x.(f (f (f (f (f (f x))))))

即六个。

最后，幂可以通过迭代乘法来定义

假设取幂函数被称为 CARAT

CARAT = λm.λn.(m (mul n) )
sixteen => ((CARAT four) two)
 => (λ m. λ n.(m (mul n) four) two)
 => (λ n.(two (mul n)four
 => (two (mul four))
 => ((λ f. λ x.(f (f x))))mul)four)
 => (λ x. (mul(mul x))four)
 => (mul(mul four))))
 => (((((λ m. λ n. λ x.(m (add n) x)mul)four)
 => ((((λ n. λ x.(mul(add n) x)four)
 => (λ x.(mul(add four) x))
 => (λ x (λ m. λ n. λ x.(m (add n) x add)four) x
 => (λ x (λ n. λ x. (add(add n) x)four)x
 => (λ x (λ x (add (add four) x) x)
 => (λ x (λ x (λ m. λ n. λ f. λ x((((m next) n) f) x)add )four) x) x)
 => (λ x (λ x (λ n. λ f. λ x(((add next)n)f)x)four)x)x)
 => (λ x (λ x (λ f. λ x((add next)four)f)x)x)x) 
 => (λ x (λ x (λ f. λ x((λ m. λ n. λ f. λ x((((m next) n) f) x)next)four)f)x)x)x)
 => (λ x (λ x (λ f. λ x((λ n. λ f. λ x.(((next next)n)f)x)four)f)x)x)x)
 => (λ x (λ x (λ f. λ x((λ f. λ x ((next next)four)f)x)f)x)x)x)
 => (λ x (λ x (λ f. λ x((λ f. λ x(((λ n. λ f. λ x.(f ((n f) x))next)four)f)x)f)x)x)x)

现在，将上述表达式归约并代入“next”和“four”并进一步归约，我们得到以下形式

λ f. λ x.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))

即十六。

4

1 回答 1

1

首先，重写next = λ n. λ f. λ x.(f ((n f) x))为

next = λ num. λ succ. λ zero. succ (num succ zero)

在 lambda 演算中，括号仅用于分组；应用程序通过术语并列来表示，即只需将一个术语写在另一个术语旁边，并在左侧关联。

我们如何阅读以上内容？这是一个 lambda 项。当它应用于其他一些 lambda 项时，例如NUM，它将简化为 lambda 项λ succ. λ zero. succ (NUM succ zero)。这将是直接结果，表示由 表示的给定数字的下一个数字NUM。我们可以把它读成对我们说：“我不知道如何计算后继者，也不知道零意味着什么，但如果两者都提供给我，我会根据它们产生一些结果，并根据用于创建我的lambda 项NUM，通过将这些计算方式提供给NUM然后将其结果再次应用于给我的后继函数”。

这当然是假设NUM尊重相同的假设并以一致的方式运作。特别是ZERO，当应用于 ans和 a时z，必须返回z：

ZERO = λ s. λ z. z  ; == λ a. λ b. b == ...

其他一切都由此而来。

于 2013-12-09T07:56:55.043 回答