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

Question

关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。












想改善这个问题吗？更新问题，使其成为 on-topic对于堆栈溢出。

7年前关闭。




Improve this question




我正在寻找弱归一化 lambda 项的示例。
我说以下是否正确:

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

减少到:

b

或者:

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

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

Answer 1

如果您首先并连续评估正确的术语，那么它永远不会达到正常形式，因此它不是强规范化的。如果先评估左项，它将立即达到标准形式，因此它是可归一化的，并证明该项是弱归一化的。这也是无类型 lambda 演算的非融合的一个例子。

请注意，与特定术语相比，您更有可能想谈论重写系统如何规范化。因此，该术语是无类型 lambda 演算的强归一化属性的反例，但并没有提供证明 ULC 弱归一化(事实并非如此)的正面证据。