lambda

LAMBDA LIFTING DE JOHNSSON
1. Conjunto formado por todas las variables libres de todas las partes derechas.
2. Eliminar de dicho conjunto las que aparezcan en las partesizquierdas del letrec o en alguna definición del nivel superior.
3. Convertir esas variables en argumentos extras en todas las partes derechas (no β.abstracción, solo suprimer parte).
4. Añadir los argumentos extras a cada operación (izquierda) de una variable definida en letrec.
5. Elevar de nivel las definiciones de letrec, en notaciónde Súper Combinador.
Ejm:
r z = ...
f x y =
letrec
g = λp......h......x......r......
h = λq.........g.........y
in
.........g.........h.........Variables libres (derecha): {h, x, r, g, y}
Eliminando: {x, y}
r z = ...
f x y =
letrec
g = (λx. λy. λp..... (hxy).....x.....r.....)xy
h = (λx. λy. λq.....(gxy).....y.....)xy
in
.........g.........h.........

r z = ...
f x y =
letrec
g = (λx. λy. λp..... (hxy).....x.....r.....)
h = (λx. λy. λq..... (gxy).....y.....)in
.........(gxy).........(hxy).........

r z = ...
f x y = .........(gxy).........(hxy).........
g x y p = ..... (hxy).....x.....r.....
h x y q = .....(gxy).....y.....


COLISION Y CAPTURA DE NOMBRE
Se renombra la expresión entera.
Renombra antes de poner parámetros extras.
Localmente se renombra solo las variables ligadas,porque las localmente libres se corresponden con una lista de argumentos.
Requisito de implementación: generación de nombres nuevos de subíndice.
Ejm:
1. Identificadorescon el mismo nombre a diferente nivel
let
x = a + b in let a = 7 in x + a

(lambda x. ((l a. x+a)7))a+b

Fxy = letrec

G=l x . x+ (hy)
H=lz.z+x+y

In gx