关于本科水平计算机科学的主题。
在复习该理论时，我遇到了一个令人烦恼的问题，即关于(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的任何一个。因此，如果我以以下形式设置功能xNEXP
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即使它的输出可以是非教堂的数字，用于教堂的数字输入？”</p>“你知道任何轻微的修正，
EXP因此该功能适用于所有教堂的数字输入吗？”</p>“对我的批评有任何问题或误解
(0 m)。”</p>
另外，作为函数组合的单位元的(0 m)to be的结果是否有逻辑背景λx. x，而不是 1？这只是巧合还是我想得太认真了？
欢迎任何想法。
如有必要，我想遵循与教堂数字相关的代数的维基百科定义。
教会的编码：https ://en.m.wikipedia.org/wiki/Church_encoding
谢谢。