「フリー変数」とは何ですか？

Question

（これは既にこのサイトで回答されているはずですが、Cの変数にfree（）を呼び出すというコンセプトで検索が氾濫しています）。

私は「η減少xが "Mで自由でない"なら、これはf x = M x ==> Mのように定義されました。つまり、関数をポイントフリーのスタイルに変換するときのように思えますが、xが自由ではないという意味についてはわかりません。ここで

Answer 1

は例です：このラムダで

\f -> f x 

、xは自由変数です。基本的に自由変数は、ラムダの引数の1つでないラムダで使用される変数です（またはlet変数）。それはラムダの文脈の外から来る。

(\x -> g x) to (g) 

をしかしxが空いていない場合にのみ（すなわち、それは使用されていないか、引数である）gに：

ETAの減少は、我々が変更できることを意味します。

(\x -> (x+) x) to (x+) ??? 

Answer 2

まあ、here's the relevant Wikipedia article、それは価値がある何のため：そうでなければ、私たちは、未知の変数を参照する式を作成することでしょう。

短いバージョンでは、 "M"のようなプレースホルダーを使ってラムダ式の本体が削除されるため、そのラムダによってバインドされている変数が、プレースホルダーが表すもので使用されていないことをさらに指定する必要があります。

だから、ここ「自由変数が」大体、いくつかのあいまいなまたは未知の外側のスコープで定義された変数を意味します - 。例えばは、\y -> x + yのような式では、xは自由変数であるが、yではありません。

Etaの削減は、余分なバインディングレイヤーを削除し、直ちに変数を適用することです。この変数は、問題の変数がその1つの場所でのみ使用されている場合にのみ有効です（あなたが想像しているように）。