PDF de programación - calculo lambda

C ´ALCULO LAMBDA

Motivaci´on: notaci´on para no necesitar nombrar funciones. Por ejemplo, x + y

puede ser:

f (x) = x + y

g(y) = x + y

h(x, y) = x + y

La notaci´on lambda permite expresar sin dar nombre:

e incluso

λx.x + y

λy.x + y

λ(x, y).x + y

λx.λy.x + y

(cid:82) x + y dx, dx enfatiza que x var´ıa e y est´a fija. En(cid:80)

En algunos contextos, los matem´aticos usan notaciones similares: En integrales,
i∈0.,10 i + j, i var´ıa y j est´a

λy.λx.x + y

fija.

El c´alculo lambda, en principio es una notaci´on para no tener que nombrar
funciones. Pero adem´as, el c´alculo lambda puro, s´olo contiene variables, aplicaciones
y la notaci´on lambda (llamada abstracci´on).
(cid:104)expr(cid:105)

::=
|
|

(cid:104)var(cid:105)
(cid:104)expr(cid:105)(cid:104)expr(cid:105)
λ(cid:104)var(cid:105).(cid:104)expr(cid:105)

t´ermino lambda, o expresi´on
variable
aplicaci´on, el primero es el operador y el segundo el operando
abstracci´on o expresi´on lambda

La aplicaci´on asocia a izquierda. En λv.e, la primer ocurrencia de v es ligadora
y su alcance es e. Por ejemplo, λx.(λy.xyx)x es lo mismo que λx.((λy.((xy)x))x).
Puesto que λ se comporta como un cuantificador, se hacen exactamente las mis-
mas definiciones de ocurrencia ligada, ocurrencia libre y variable libre. El conjunto
de variables libres se define tambi´en por inducci´on en la estructura de los t´erminos:

F V (v) ={v}

F V (e0e1) =F V (e0) ∪ F V (e1)
F V (λv.e) =F V (e) − {v}

1

2

C ´ALCULO LAMBDA

Tambi´en se define sustituci´on:

∆ =(cid:104)var(cid:105) → (cid:104)expr(cid:105)
/ ∈(cid:104)expr(cid:105) × ∆ → (cid:104)expr(cid:105)
v/δ =δv

(e0e1)/δ =(e0/δ)(e1/δ)
(λv.e)/δ =λv(cid:48).(e/[δ|v : v(cid:48)])

(cid:91)

donde v(cid:48) (cid:54)∈

F V (δw)

w∈F V (e)−{v}

Como veremos, la sustituci´on en el c´alculo lambda es fundamental: permite de-

finir la sem´antica operacional.

Propiedad 1.

1. si para todo w ∈ F V (e), δw = δ(cid:48)w entonces (e/δ) = (e/δ(cid:48))
2. sea i la sustituci´on identidad, entonces e/i = e.

3. F V (e/δ) =(cid:83)

w∈F V (e) F V (δw)

Escribimos e/v → e(cid:48) en vez de e/[i|v : e(cid:48)] y e/v1 → e1, . . . , vn → en en vez de
e/[i|v1 : e1| . . .|vn : en].

Renombre (α). La operaci´on de cambiar una ocurrencia de la expresi´on lambda λv.e
por λv(cid:48).(e/v → v(cid:48)) donde v(cid:48) (cid:54)∈ F V (e)−{v} se llama renombre o cambio de variable
ligada. Si e(cid:48) se obtiene a partir de e por cero o m´as renombres de ocurrencias de
subfrases, se dice que e(cid:48) se obtiene a partir de e por renombre. Tambi´en se dice
que “e α-convierte a e(cid:48)”. Se puede ver que ´esta es una relaci´on de equivalencia. Se
dice que e y e(cid:48) son α-equivalentes y se escribe e ≡ e(cid:48). Se supone que renombre debe
preservar la sem´antica (aunque hubo algunas excepciones en los primeros lenguajes
funcionales).
Contracci´on (β). Una expresi´on de la forma (λv.e)e(cid:48) se llama redex (plural redices,
a veces mal dicho r´edexes). Es la aplicaci´on de una funci´on (λv.e) a su argumento
e(cid:48). Debe calcularse reemplazando las ocurrencias libres de v en e por e(cid:48), es decir
(e/v → e(cid:48)).
Cuando en una expresi´on e0 se reemplaza una ocurrencia de un redex (λv.e)e(cid:48) por
(e/v → e(cid:48)) y luego de cero o m´as renombres se obtiene e1, se dice que “e0 β-contrae
a e1” y se escribe e0 → e1. A pesar que utilizamos el t´ermino contracci´on, no nece-
sariamente e1 va a ser m´as peque˜na que e0. Por ejemplo e0 = (λx.xxxx)(λy.λz.yz)
β-contrae a (λy.λz.yz)(λy.λz.yz)(λy.λz.yz)(λy.λz.yz) que es m´as grande.

Ejemplos:

→ y
(λx.y)(λz.z)
→ (λz.z)
(λx.x)(λz.z)
→ (λz.z)(λz.z) → (λz.z)
(λx.xx)(λz.z)
(λx.(λy.yx)z)(zw)→ (λx.zx)(zw) → z(zw)
(λx.(λy.yx)z)(zw)→ (λy.y(zw))z → z(zw)

Podemos comprobar que las ´ultimas expresiones de cada l´ınea no contienen re-
dices, por lo tanto no se pueden contraer m´as. Una expresi´on sin redices se llama
forma normal. Los ´ultimos dos ejemplos comienzan con la misma expresi´on, se
diferencian, pero cuando llegan a la forma normal dan el mismo resultado.

C ´ALCULO LAMBDA

3

Utilizando la notaci´on de la sem´antica de transiciones para el lenguaje imperativo

tendr´ıamos

Γ = conjunto de configuraciones
Γ =(cid:104)expr(cid:105)
Γt = expresiones sin redex, es decir en forma normal
Γn = expresiones con redex
→⊆ Γn × Γ

y como se vi´o en alguno de los ejemplos de arriba → es no determin´ıstico. Sin
embargo, si →∗ es la clausura reflexiva (y por renombre) y transitiva de →, entonces
podemos cerrar caminos que se separan.
Teorema 1. Church-Rosser. Si e →∗ e0 y e →∗ e1, entonces existe e(cid:48) tal que
e0 →∗ e(cid:48) y e1 →∗ e(cid:48).

Tambi´en se la llama confluencia o propiedad del diamante:

e

e0

e1

∗

∗

e(cid:48)

Corolario 1. Salvo renombre, toda expresi´on tiene a lo sumo una forma normal.
Demostraci´on. Supongamos que e0 y e1 son formas normales de e. Tenemos e →∗ e0
y e →∗ e1. Por teorema, existe e(cid:48) tal que e0 →∗ e(cid:48) y e1 →∗ e(cid:48). Pero como e0 y e1
eran formas normales no ten´ıan redices, por lo tanto e(cid:48) s´olo puede ser renombre de
(cid:3)
e0 y de e1, por lo tanto e0 y e1 son renombres entre s´ı.

Pero no toda expresi´on tiene forma normal; veamos dos ejemplos patol´ogicos:
1. Sea ∆ = (λx.xx), entonces

∆∆ = (λx.xx)∆ → ∆∆ → ∆∆ → . . . .

2. Sea ∆(cid:48) = (λx.xxy), entonces

∆(cid:48)∆(cid:48) = (λx.xxy)∆(cid:48) → ∆(cid:48)∆(cid:48)y → ∆(cid:48)∆(cid:48)yy → . . . .

Y hay casos en las que la forma normal s´olo se encuentra si se “ejecuta bien”:

(λx.λy.y)(∆∆)→ λy.y
(λx.λy.y)(∆∆)→ (λx.λy.y)(∆∆) → . . . .

1. Evaluacion

Hemos presentado la relaci´on → que permite realizar c´omputos, ejecuciones de un
t´ermino lambda hasta llevarlo a su forma normal en caso de que la tenga. Pero ´esa
no es exactamente la idea de ejecuci´on que implementan los lenguajes aplicativos.

4

C ´ALCULO LAMBDA

La idea de ejecuci´on (llamada evaluaci´on) que se implementa habitualmente tiene
las siguientes diferencias con la relaci´on →:

1. s´olo se eval´uan expresiones cerradas (es decir, sin variables libres)
2. es determin´ıstica
3. no busca formas normales sino formas can´onicas

Existen varias definiciones de evaluaci´on. Estudiaremos las dos m´as importantes:
la evaluaci´on (en orden) normal y la evaluaci´on eager o estricta. La primera es la
que ha dado lugar a los lenguajes de programaci´on funcionales lazy (Haskell) y la
segunda, a los estrictos (ML).

Como la evaluaci´on busca una forma can´onica de un t´ermino, las formas can´oni-
cas juegan el rol de ser ”valores”de expresiones. La noci´on de forma can´onica de-
pende de la definici´on de evaluaci´on. Se define una noci´on de forma can´onica para
la evaluaci´on normal, y otra para la evaluaci´on eager. En el caso del c´alculo lambda
coinciden: son las abstracciones (en otro lenguajes, veremos, dejan de coincidir).

Entonces tenemos: formas can´onicas = abstracciones.
Como a partir de ahora nos concentraremos en expresiones cerradas, la siguiente

propiedad ayuda para comparar las nociones de forma can´onica y forma normal:

Propiedad 2. Una aplicaci´on cerrada no puede ser forma normal.

Demostraci´on. Sea e una aplicaci´on cerrada. Sea e = e0e1 . . . en donde e0 no es una
aplicaci´on. Como e es una aplicaci´on, n (cid:62) 1. Si e0 fuera una variable, e no ser´ıa
cerrada. Por lo tanto, es una abstracci´on y e contiene el redex e0e1. Por lo tanto
(cid:3)
no es forma normal.

Entonces, podemos concluir que una expresi´on cerrada que es forma normal es
tambi´en forma can´onica. El rec´ıproco no vale, por ejemplo λx.(λy.y)x es forma
can´onica cerrada pero no es forma normal. Peor a´un, λx.∆∆ es forma can´onica
cerrada y no tiene forma normal.

¿Por qu´e conformarse con una forma can´onica en vez de continuar ejecutando

hasta obtener una forma normal? Podemos entenderlo de la siguiente manera:

1. es razonable circunscribir la atenci´on a expresiones cerradas (punto 1, apenas
empezamos a hablar de evaluaci´on) porque son las que parecen tener sentido,
2. una vez que se alcanz´o una abstracci´on λv.M , continuar evaluando implicar´ıa
evaluar M que puede no ser una expresi´on cerrada, puede contener a la
variable v.

2. Evaluaci´on en orden normal

La evaluaci´on puede definirse utilizando sem´antica natural o big-step. En este
tipo de sem´antica operacional, uno no describe un paso de ejecuci´on, sino direc-
tamente una relaci´on entre los t´erminos y sus valores (que tambi´en son t´erminos,
son formas can´onicas). Llamaremos ⇒ a esta relaci´on que est´a definida por las
siguientes reglas:

e ⇒ λv.e(cid:48)(cid:48)

(e(cid:48)(cid:48)/v → e(cid:48)) ⇒ z

ee(cid:48) ⇒ z

(abstracci´on)

λv.e ⇒ λv.e

(aplicaci´on)
Cuando afirmamos que e ⇒ z se cumple, estamos diciendo que existe un ´arbol de
derivaci´on que demuestra e ⇒ z. Estos ´arboles usualmente son dif´ıciles de graficar,
por el tama˜no de las expresiones intervinientes. Se suele usar indentaci´on para
expresar la estructura.

C ´ALCULO LAMBDA

5

Por ejemplo, la evaluaci´on normal de (λx.λy.xx)∆ se escribe:

(λx.λy.xx)∆

λx.λy.xx ⇒ λx.λy.xx
λy.∆∆ ⇒ λy.∆∆

(es una aplicaci´on, por lo tanto usamos la 2da
regla, a continuaci´on siguen los 2 hijos)
(primer hijo, es una abstracci´on,
por lo tanto usamos la 1er regla, no hay hijos)
(segundo hijo, tambi´en abstracci´on, no hay hijos)
(termin´o la prueba)

⇒ λy.∆∆
Otro ejemplo es la evaluaci´on normal de (λx.x(λy.xyy)x)(λz.λw.z):

(λx.x(λy.xyy)x)(λz.λw.z)

λx.x(λy.xyy)x ⇒ λx.x(λy.xyy)x
(λz.λw.z)(λy.(λz.λw.z)yy)(λz.λw.z)

(λz.λw.z)(λy.(λz.λw.z)yy)

λz.λw.z ⇒ λz.λw.z
λw.λy.(λz.λw.z)yy ⇒ λw.λy.(λz.λw.z)yy
⇒ λw.λy.(λz.λw.z)yy
λy.(λz.λw.z)yy ⇒ λy.(λz.λw.z)yy
⇒ λy.(λz.λw.z)yy

(aplicac. siguen 2 hijos: a,b)
(a:abstracci´on, no hay hijos)
(b:aplic. siguen 2 h: ba y bb)
(ba: aplic. Siguen 2: baa,bab)
(baa: abstracci´on,no hay h)
(bab: abstracci´on,no hay h)
(termin´o ba)
(bb: abstracci´on,no hay hijos)
(termin´o b)
(termin´o la prueba)

⇒ λy.(λz.λw.z)yy
La notaci´on con indentaci´on sola es dif´ıcil de leer, se mejora si se escriben cor-
che