。私は間違って何をしていますか?ベータ削減ラムダ計算
0
A
答えて
2
ですそれに。頭正規形に到達するために
、我々は下ラムダを削減しようとすることができます...
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を持っていません。つまり、この式の評価は(引数に適用された場合)決して終了しません。ノーマルフォームには決して達しません。
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)
関連する問題
- 1. ラムダ計算を減らす方法
- 2. ラムダ計算:次のベータの減少は型なしラムダ計算に許可されている理由を私は理解できない
- 3. Haskellを使ったラムダ計算のベータ縮小
- 4. ラムダ計算ヘルプ
- 5. ラムダ計算
- 6. 再帰ラムダ計算関数
- 7. ラムダ計算の質問 - コンクリート
- 8. ラムダ計算:Scalaで適用
- 9. 日付計算減算日付
- 10. 出力問題のラムダ計算インタープリタ
- 11. ラムダ計算 - 複数のパラメータが
- 12. 増減の割合を計算する
- 13. Androidの基本的な計算は、乗算、減算、追加
- 14. いくつかのラムダのベータ還元
- 15. 最初の計算機での減算のコード
- 16. 減算
- 17. NSDateFormatterの減算
- 18. sqlクエリ減算
- 19. SQLite3テーブル減算
- 20. 日付減算
- 21. 減算VBA
- 22. 減算int型:
- 23. SQL - 減算行
- 24. アレイアドレス減算
- 25. 減算のキャリーフラグ
- 26. タイムスパン減算ストップウォッチカウントダウン
- 27. Delphi:加算と減算
- 28. 加算または減算
- 29. 8086アセンブリシフト減算と除算
- 30. パンダのデータフレーム - ラムダ計算とシリーズあたりの最小値
大変ありがとうございます –