haskell - ¿Qué es una “variable libre”?

functional-programming lambda-calculus

Question

(Estoy seguro de que esto ya debe haber sido respondido en este sitio, pero la búsqueda se ve inundada por el concepto de llamar gratis () a una variable en C.)

Encontré el término "reducción eta", que se definió algo así como fx = M x ==> M si x no está "libre en M". Quiero decir, creo que entiendo lo esencial de lo que está tratando de decir, parece ser lo que haces cuando conviertes una función a un estilo sin puntos, pero no sé qué significa el calificador de x no ser libre.

Answer 1

Aquí hay un ejemplo:

/f -> f x

En esta 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 la lambda (o una variable let ). Viene de fuera del contexto de la lambda.

Reducción de etapa significa que podemos cambiar:

(/x -> g x) to (g)

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

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

Answer 2

Bueno, aquí está el artículo relevante de Wikipedia , por lo que vale la pena.

La versión corta es que tales definiciones ocultan el cuerpo de una expresión lambda que usa un marcador de posición como "M", y por lo tanto tienen que especificar adicionalmente que la variable que está vinculada por ese lambda no se usa en lo que represente el marcador de posición.

Por lo tanto, una "variable libre" aquí significa aproximadamente una variable definida en un ámbito externo ambiguo o desconocido, por ejemplo, en una expresión como /y -> x + y , x es una variable libre pero y no lo es.

La reducción de etapa consiste en eliminar una capa superflua de unión y aplicar inmediatamente una variable, lo que es (como probablemente imaginaría) solo es válido si la variable en cuestión solo se usa en ese lugar.