lambda-calculus - ラムダ計算式

Question

ラムダ式の場合、自由変数がどのように C コードに変換できる(x (λx y. x y) z h)かがわかりませんでした。x (outer x)zh

よろしく、ダーキー

Answer 1

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

ここでは、自由変数に直接相当するものはないことに注意してください。代用する場所を知るためにそれらを使用しているだけです。

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

Answer 2

Free variables are a special case in the Lambda Calculus -- they cannot be "converted" to anything, so usually they're taken as just symbols. In your example, and given some fictitious constructors for lambda expressions, you'd translate it to the following (which includes dealing with the implicit currying) C-like expression:

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"));

Obviously, you can use mk_var() for those symbols too, but that would be misleading since they're not really variables, since they're not bound. In other words, if you do any alpha conversion on the expression, they will have to stay the same.

(BTW, the relevant part here is Barendregt's free variable assumption.)