lambda - m 在教会数字中的 0 次方

Question

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

我在 lambda 演算中采用自然数的 n 由教堂编码通常如下
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在数学中。这在超操作的意义上也很简单。

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

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

问题是

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

“你知道EXP的任何轻微修正吗？所以这个函数对所有教会的数字输入都很有用？”

“我对 (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 .