¿Qué es una "variable libre"?

Question

(Estoy seguro de que ya debe haber sido respondido en este sitio, pero la búsqueda se inunda con el concepto de llamar a free() en una variable en C.)

Me encontré con el término "reducción eta" que se definió como f x = M x ==> M si x no es "libre en M". Quiero decir, creo que entiendo la esencia de lo que está tratando de decir, parece lo que haces cuando conviertes una función en un estilo sin puntos, pero no sé qué significa el calificador sobre x no ser libre.

Answer 1

He aquí un ejemplo:

\f -> f x 

En este lambda, x es una variable libre. Básicamente, una variable libre es una variable utilizada en una lambda que no es uno de los argumentos de lambda (o una variable let). Viene de fuera del contexto de la lambda.

reducción de Eta significa que podemos cambiar:

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

Pero sólo si x no es libre (es decir, no se utiliza o es un argumento) en g. De lo contrario estaríamos creando una expresión que hace referencia a una variable desconocida:

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

Answer 2

Bueno, here's the relevant Wikipedia article, por lo que vale la pena. La versión corta es que tales definiciones eluden el cuerpo de una expresión lambda usando un marcador de posición como "M", y por lo tanto tienen que especificar adicionalmente que la variable atada por esa lambda no se usa en lo que representa el marcador de posición.

lo tanto, una "variable libre" aquí significa más o menos una variable definida en un cierto margen exterior ambigua o desconocido -. Por ejemplo, en una expresión como \y -> x + y, x es una variable libre, pero no es y.

La reducción de Eta consiste en eliminar una capa superflua de vinculación y aplicar inmediatamente una variable, que es (como probablemente se imaginaría) solo válida si la variable en cuestión solo se utiliza en ese lugar.