有关本科计算机科学的主题。在回顾该理论时，我遇到了一个关于(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
谢谢。
有关本科计算机科学的主题。在回顾该理论时，我遇到了一个麻烦的问题，关于（0 m）的问题，在lambda演算中，教堂的数字取幂。据我...
一个简单的误解：您说“ λx. x，不是1”，但是λx. x的确是教会数字1。您可能知道教堂数字1为λfx. f x，但是简单的eta归约和alpha转换表明它等同于λx. x。