Co to jest "zmienna wolna"?

Question

(Jestem pewien, że na tę stronę już trzeba było odpowiedzieć, ale wyszukiwanie zostaje zalane koncepcją wywoływania free() na zmiennej w C.)

Natknąłem się na termin "redukcja eta", który został zdefiniowany tak, jak f x = M x ==> M, jeśli x jest "nie wolny w M". Chodzi mi o to, myślę, że rozumiem sedno tego, co próbuje powiedzieć, wydaje się, że robisz to, gdy konwertujesz funkcję na styl bezcłowy, ale nie wiem, co oznacza, że ​​kwalifikator na x nie jest wolny.

Answer 1

Oto przykład:

\f -> f x 

W tym lambda, x jest zmienną wolną. Zasadniczo zmienna wolna jest zmienną używaną w lambda, która nie jest jednym z argumentów lambda (lub zmienną let). Pochodzi spoza kontekstu lambdy.

redukcja Eta oznacza, że ​​możemy zmienić:

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

ale tylko jeśli x nie jest za darmo (to znaczy nie jest używany lub jest argumentem) w g. W przeciwnym razie bylibyśmy tworząc wyrażenie, które odnosi się do nieznanej zmiennej:

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

Answer 2

dobrze, here's the relevant Wikipedia article za to, co to jest warte.

Krótka wersja jest taka, że ​​takie definicje przesuwają treść wyrażenia lambda za pomocą symbolu zastępczego takiego jak "M", a więc muszą dodatkowo określać, że zmienna związana przez tę lambdę nie jest używana w tym, co reprezentuje symbol zastępczy.

Tak, „wolna zmienna” tutaj z grubsza oznacza zmienną zdefiniowaną w jakiś dwuznaczny lub nieznanym zewnętrznej zakresu. - na przykład, w wyrażeniu jak \y -> x + y, x jest zmienną wolną ale y nie jest.

Redukcja ETA polega na usunięciu zbędnej warstwy wiązania i natychmiastowym zastosowaniu zmiennej, która (jak można sobie wyobrazić) jest ważna tylko wtedy, gdy dana zmienna jest używana tylko w tym jednym miejscu.