lambda - Church 数字中 m 的 0 次方

Question

本科水平计算机科学主题。
我遇到了一个关于(0 m)的令人烦恼的问题在回顾理论时，用 lambda 演算中教会数字的幂表示。
据我所知，(0 m)当减少结果为λx. x时，这不是 1 (= m^0)正如预期的那样，甚至不在教会的数字之内。

我采用 lambda 演算中的自然数 n，通常由 Church 的编码编码，如下

n := λfx. (f^n x) = (f ... (f x))

很多文献都这么说

EXP(m, n) := λmn. (n m)

返回m^n对于给定的m和n教堂的数字，我知道该函数在大多数情况下都能正确响应。 但当n = 0时情况并非如此。自从

(0 m) = ((λfx. x) m) → λx. x

在数学中，1是被视为乘法群的自然数的单位元，即 x * 1 = 1 * x对于任何 x在N 。所以如果我设置 EXP函数形式为

EXP’(m, n) := λmn. (n (MUL m) 1)

对于MUL(m, n) = m * n ，这似乎工作正常，与事实相符 m^0通常定义为1在数学中。而且，从 super 操作的意义上来说，这似乎很简单。

过度操作:https://en.m.wikipedia.org/wiki/Hyperoperation

我预计会有一些批评，例如 m^0不一定1在数学中，严格的数学专家会说这一切都取决于定义。但是采用前一种风格有任何逻辑支持吗EXP(m, n) ？当 n = 0 时，它不会返回教堂的数字。 ，所以对我来说仍然定义不明确。

问题是

1. “为什么定义EXP(m, n) := λmn. (n m)通常接受 m^n虽然 它的输出可以是非教会的数字作为教会的数字输入？”

2. “你知道EXP有什么细微的修正吗？所以这个函数适用于所有教堂的数字输入？”

3. “任何问题或误解我的批评(0 m) .”

此外，(0 m)的结果有没有逻辑背景？成为λx. x ，它是函数组合的单位元，而不是 1？这只是巧合还是我想得太认真了？

欢迎任何想法。

如有必要，我想遵循与教堂数字相关的代数的维基百科定义。

教堂的编码:https://en.m.wikipedia.org/wiki/Church_encoding

谢谢。

Answer 1

一个简单的误解:你说“λx. x ，它不是 1 ”，而是 λx. x确实是教堂数字 1 。您可能知道教堂数字1如λfx. f x ，但简单的 eta 缩减和 alpha 转换表明这相当于 λx. x .