Che cos'è una "variabile libera"?

Question

(Sono sicuro che a questo sito è già stata data risposta, ma la ricerca viene sommersa dal concetto di chiamare free() su una variabile in C.)

Mi sono imbattuto nel termine "riduzione di eta" che è stato definito qualcosa come f x = M x ==> M se x è "non libero in M". Voglio dire, penso di capire il senso di ciò che sta cercando di dire, sembra quello che fai quando converti una funzione in stile point-free, ma non so quale sia il significato di x non essere libero.

Answer 1

Ecco un esempio:

\f -> f x 

In questo lambda, x è una variabile libera. Fondamentalmente una variabile libera è una variabile usata in un lambda che non è uno degli argomenti di lambda (o una variabile let). Viene fuori dal contesto del lambda.

riduzione Eta significa che possiamo cambiare:

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

Ma solo se x non è libero (ossia non viene usato o è un argomento) in g. Altrimenti saremmo creando un'espressione che si riferisce ad una variabile sconosciuta:

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

Answer 2

Beh, here's the relevant Wikipedia article, per quello che vale la pena.

La versione breve è che tali definizioni elidano il corpo di un'espressione lambda usando un segnaposto come "M", e quindi devono specificare inoltre che la variabile vincolata da quel lambda non viene utilizzata in ciò che rappresenta il segnaposto.

Così, un "variabile libera" qui significa approssimativamente una variabile definita in qualche ambito esterno ambiguo o sconosciuti -. Per esempio, in un'espressione come \y -> x + y, x è una variabile libera ma y non è.

Eta riduzione riguarda la rimozione di uno strato superfluo di rilegatura e l'applicazione immediata di una variabile, che è (come probabilmente si immagina) valida solo se la variabile in questione viene utilizzata solo in quella posizione.