ラムダ計算の発現

Question

ラムダの表現の場合 (x (λx y. x y) z h), 、私は自由変数を理解していませんでした x (outer x), z と h Cコードで変換できますか？

よろしく、ダーク

Answer 1

自由変数は、ラムダ計算の特別なケースです。それらは何にも「変換」することはできないため、通常は単なるシンボルと見なされます。あなたの例では、Lambda式の架空のコンストラクターを与えられると、次の（暗黙のカレーへの対処を含む）Cのような表現に翻訳します。

mk_app(mk_app(mk_app(mk_sym("x"),
                     mk_lam("x",
                            mk_lam("y",
                                   mk_app(mk_var("x"),
                                          mk_var("y"))))),
              mk_sym("z")),
       mk_sym("h"));

明らかに、使用できます mk_var() これらのシンボルにとっても、それは実際には変数ではないため、誤解を招くでしょう。言い換えれば、式でアルファ変換を行う場合、それらは同じままでなければなりません。

（ところで、ここで関連する部分は、Barendregtの無料変数仮定です。）

Answer 2

Lambda計算をCコードに変換することは自明ではありません。通常、段階的な評価を評価する通訳を書きます。つまり、式を木に変え、左側がラムダであるアプリケーションであるルートに最も近いノードを見つけます。右側に置き換えます。これ以上適用できなくなるまで繰り返し、結果が得られます。

ここには、自由変数に直接相当するものはないことに注意してください。私たちはそれらを使用して、どこに置き換えるかを知るだけです。

チューリングの等価性は必要ないことに注意してください ちょうど 2つのチューリング複雑な言語の任意の概念間の同等性。単に、一方を他方とエミュレートできる必要があります。その逆も同様です。