haskell - Lambda微积分(λa.b)((λx.xx)(λx.xx))

Closed. This question does not meet Stack Overflow guidelines。它当前不接受答案。












想要改善这个问题吗？更新问题，以便将其作为on-topic用于堆栈溢出。

7年前关闭。



Improve this question




我正在寻找一个弱标准化的lambda项的示例。
我说的对吗？

(λa.b)((λx.xx)(λx.xx))

减少到:

b

或者:

不会终止(如果您尝试减少(λx.xx)(λx.xx))

我不确定第一次减少是否正确，所以只需要澄清一下，
谢谢。

最佳答案

如果您先对正确的术语进行评估，然后再对其进行评估，那么它将永远无法达到正常形式，因此无法高度归一化。如果您首先评估左项，它将立即达到范式，因此可以归一化并证明该项是弱归一化的。这也是未类型化lambda演算不融合的一个示例。

请注意，与特定术语相比，您更有可能想谈谈重写系统如何规范化。因此，该术语是对未类型化的lambda演算的强归一化特性的反例，但并未提供有关ULC弱归一化的积极证据(并非如此)。

关于haskell - Lambda微积分(λa.b)((λx.xx)(λx.xx))，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/21020497/