Sintaxis lambda
Avanzado Lógica Notación
El cálculo λ tiene una gramática lo bastante pequeña para caber en un sello — pero al principio no se lee para nada como el álgebra escolar. Esta página es el manual de frases.
La gramática, entera
Todo término λ legal es una de esas tres cosas, construido a partir de términos λ más pequeños. No existe nada más.
Leer una abstracción
La λ termina en un punto: λx.M significa que el cuerpo
es todo lo que sigue al punto. Así que λx.x y
es una función cuyo cuerpo es x y — no es
(λx.x) y.
λx.x y ≠ (λx.x) y. La primera es una
función (cuerpo x y). La segunda es la función
identidad aplicada a y — que se reduce simplemente a
y. Los paréntesis mueven todo el significado.
La aplicación se agrupa a la izquierda
Cuando las aplicaciones se encadenan, se agrupan a la izquierda:
Así que λf.λx.f (f x) significa: una función de f que
devuelve una función de x que aplica f dos veces — escrito sin tinta
extra.
Currificación: funciones que toman una cosa
El cálculo λ no tiene funciones de varios argumentos. No los necesita — una función puede devolver una función:
Este truco — un argumento por función, λ anidadas para más — se llama currificación, por Haskell Curry. Dos marcadores de posición, uno cada vez.
Ve la estructura
Todo término λ es un árbol: los nodos λ ligan una variable,
los nodos @ aplican y las hojas son variables. Aquí está
(λx.λy.x) a b:
Libre contra ligada
Dentro de λx.M, cada x en M está
ligada — pertenece a esa λ. Una variable sin λ que
la posea es libre. En λx.x y: x está
ligada, y es libre — flota desde quien escribió el término. Las
variables libres son las entradas; las ligadas son las piezas móviles
de la máquina. Esto importa enormemente en la página siguiente,
cuando llega la sustitución.
λx.x y significa…
f g h se analiza como…
En λx.x y, la variable y es…
Reduce por currificación: (λx.λy.x) a b → ___
Siguiente: beta reducción · Anterior: cálculo lambda