ベータ削減ラムダ計算

Question

。私は間違って何をしていますか？

Answer 1

ですそれに。頭正規形に到達するために

、我々は下ラムダを削減しようとすることができます...

reduction 1 
λy.(λx.λy.xx) (λx.λy.x x)  →β x [x := (λx.λy.x x)] 
λy.(λx.λy.(λx.λy.x x)(λx.λy.x x)) 

reduction 2 ... 
λy.λy.(λx.λy.x x) (λx.λy.x x) 

[OK]を、私たちはすぐにこのパターンはそれ自身を繰り返すことになりますことがわかります。ラムダの下で減らそうとするたびに、結果は別のλyにラップされます。

したがって、この特定のラムダ式はHead Normal Formを持っていません。つまり、この式の評価は（引数に適用された場合）決して終了しません。ノーマルフォームには決して達しません。

Answer 2

あなたは何も間違っていません。

発現(λx.x x) (λx. λy.x x)λy.(λx. λy.x x)(λx. λy.x x)に、次いでλy.λy.(λx. λy.x x)(λx. λy.x x)にベータ - 減少(λx. λy.x x)(λx. λy.x x)に1つのステップにおいて、ベータ - 低減します。
すべてのステップで、新しい式はすべて以前のものと同じですが、新しい抽象化に含まれます。

ラムダ計算では、縮小プロセスが終了しないことがあります。言い換えれば、プログラムは終了することはできません（チューリング完全なプログラミング言語のように）。つまり、私たちが適用する引数なしラムダλyを持っている -

本の別の例は、ここで評価

beta reduction 1 
(λx.xx) (λx.λy.x x)    →β x [x := (λx.λy.x x)] 
(λx.(λx.λy.x x)(λx.λy.x x)) 

beta reduction 2 
(λx.λy.xx) (λx.λy.x x)   →β x [x := (λx.λy.x x)] 
(λx.λy.(λx.λy.x x)(λx.λy.x x)) 

result 
λy.(λx.λy.x x) (λx.λy.x x)

今、私たちが到達している弱い頭正規形のイラストだ用語Ω = (λx.x x)(λx.x x)