Encuentro 4 - 14/7/2012 - Cálculo Lambda

TALLER DE LENGUAJES: 04 (14/07/12)

Cálculo Lambda

La idea es programar TODO con funciones.

Ok, entonces que tengo? Una construcción que me genera una función.

(\x-> x + x)

Cuando pongo un número en un lenguaje, en realidad pongo un algo que "codifica" al número. No puedo poner a EL 5. Pongo algo que luego interpretaré como el 5.

La otra vez definimos que:
_ _    _____      _          _
suma n m -> n + m <- /* La suma del término n y el termino m da el termino al cual yo asocio a la suma de los naturales n y m */

Hay que notar que la suma trabaja sobre una codificación que me representa los números.

La codificación propuesta para los números por Church es:

zero = \ s z -> z
n = \ s z -> s^n (z)

ej:

3 = \s z -> s s s z

<<<ver Lambda.hs>>>

EL NÚMERAL DE CHURCH ES SU PROPIO FOLD, BOLUDOOOOOOO!!!!

Hay que hacer el encode, decode, succ, sum, pow, mul y, los guapos, pre y sub.


Más detalle sobre el Calculo Lambda


SINTAXIS:

t ::= x | (\x->t) | t t <- variable | abstracción | aplicación

v ::= (x.t) | x <- las variables son valores "intermedios"

\x.(x x) y hay 2 "ocurrencias" de x

Las ocurrencias de variables pueden estar libres o ligadas.

\x.t liga las ocurrencias de x dentro de t. 

Los términos son cerrados, si no tienen ocurrencias libres o abiertos si tienen.


EVALUACION

[BETA] (\x.t) u -> t{x:=u} <- la "sustitución", está por afuera del C.L.

{x:=u}x := u
{x:=u}y := y y!=x
{x:=u}(t1 t2) := ({x:=u}t1) ({x:=u}t2)
{x:=u}(\y.t) := \y.t{x:=u}
{x:=yz}(\y.wxy) := (\y.w(yz)y)
CONVENCION DE VARIABLES: En todos los contextos los nombres de las variables ligadas son distintos entre si y con cada una de las variables de ocurrencia libres

Ahora, la evaluación tiene dos variantes, una utilizando la regla ALPHA y otra definiendo las estrategias de evaluación dentro del Lambda.

[ALPHA] (\x.t) -> \y.t{x:=y} si y no pertenece a las variables libres


[SUSTITUCIONES EXPLICITAS]

t -> t'   t -> t'          t -> t'
_________________ ___________ ___________

(\x.t) -> (\x.t')           t u -> t' u         u t -> u t'


((\w.(\z.w)) v) ((\x.xx) (\y.y y)) <- dada esta expresión, hay 2 pasos posibles
 \__________/   \_____________/
| |
 paso 2 paso 1

El paso 1 se llama Omegón  _()_  que reduce cada vez a algo más grande.

Es importante notar que las reglas no dicen por que paso avanzar.

    @
  /   \
 @    @
/ \   /   \
\w v \x   \y
|      |    |
\z     @    @
|     / \  / \
w    x   x y  y

Fijate que en cualquier subarbol que machee con:

 @
/ \
\x  y
Hay un redex (lo llaman Beta-redex)


((\w.(\z.w)) v) ((\x.xx) (\y.y y))
 \__________/   \_____________/
| |
 paso 2  paso 1

  | |
  v v     <-
  (\z.v) _()_ _| _()_ reduce a sí mismo infinitamente
    \___/ \__/
      |       |
paso 2  paso 1

|
v

v

Hay infinitos caminos que terminan e infinitos caminos que no.


Incorporamos a la Sintaxis:

C ::= [] | \x.C | C t | C t


PROPIEDADESTALLER DE LENGUAJES: 04 (14/07/12)

Cálculo Lambda

La idea es programar TODO con funciones.

Ok, entonces que tengo? Una construcción que me genera una función.

(\x-> x + x)

Cuando pongo un número en un lenguaje, en realidad pongo un algo que "codifica" al número. No puedo poner a EL 5. Pongo algo que luego interpretaré como el 5.

La otra vez definimos que:
_ _    _____  _ _
suma n m -> n + m <- /* La suma del término n y el termino m da el termino al cual yo asocio a la suma de los naturales n y m */

Hay que notar que la suma trabaja sobre una codificación que me representa los números.

La codificación propuesta para los números por Church es:

zero = \ s z -> z
n = \ s z -> s^n (z)

ej:

3 = \s z -> s s s z

<<<ver Lambda.hs>>>

EL NÚMERAL DE CHURCH ES SU PROPIO FOLD, BOLUDOOOOOOO!!!!

Hay que hacer el encode, decode, succ, sum, pow, mul y, los guapos, pre y sub.


Más detalle sobre el Calculo Lambda


SINTAXIS:

t ::= x | (\x->t) | t t <- variable | abstracción | aplicación

v ::= (x.t) | x <- las variables son valores "intermedios"

\x.(x x) y hay 2 "ocurrencias" de x

Las ocurrencias de variables pueden estar libres o ligadas.

\x.t liga las ocurrencias de x dentro de t. 

Los términos son cerrados, si no tienen ocurrencias libres o abiertos si tienen.


EVALUACION

[BETA] (\x.t) u -> t{x:=u} <- la "sustitución", está por afuera del C.L.

{x:=u}x := u
{x:=u}y := y y!=x
{x:=u}(t1 t2) := ({x:=u}t1) ({x:=u}t2)
{x:=u}(\y.t) := \y.t{x:=u}
{x:=yz}(\y.wxy) := (\y.w(yz)y)
CONVENCION DE VARIABLES: En todos los contextos los nombres de las variables ligadas son distintos entre si y con cada una de las variables de ocurrencia libres

Ahora, la evaluación tiene dos variantes, una utilizando la regla ALPHA y otra definiendo las estrategias de evaluación dentro del Lambda.

[ALPHA] (\x.t) -> \y.t{x:=y} si y no pertenece a las variables libres


[SUSTITUCIONES EXPLICITAS]

t -> t'  t -> t'  t -> t'
_________________ ___________ ___________

(\x.t) -> (\x.t') t u -> t' u u t -> u t'


((\w.(\z.w)) v) ((\x.xx) (\y.y y)) <- dada esta expresión, hay 2 pasos posibles
 \__________/   \_____________/
| |
 paso 2  paso 1

El paso 1 se llama Omegón  _()_  que reduce cada vez a algo más grande.

Es importante notar que las reglas no dicen por que paso avanzar.

@
  /   \
 @      @
/ \   /   \
\w  v \x   \y
|      |    |
\z     @    @
|     / \  / \
w    x   x y  y

Fijate que en cualquier subarbol que machee con:

 @
/ \
\x  y
Hay un redex (lo llaman Beta-redex)


((\w.(\z.w)) v) ((\x.xx) (\y.y y))
 \__________/   \_____________/
| |
 paso 2  paso 1

  | |
  v v <-
  (\z.v) _()_ _| _()_ reduce a si mismo infinitamente
\___/ \__/
 |    |
paso 2  paso 1

|
v

v

Hay infinitos caminos que terminan e infinitos caminos que no.


Incorporamos a la Sintaxis:

C ::= [] | \x.C | C t | C t


PROPIEDADES

* Confluencia = CR (Se cumple)
-V- t,t1,t2 . t ->> t1 & t->> t2 -]u . t1 ->> u & t2 ->> u

* Terminación (No se cumple)

------------------------------------------------------------------------------------------

Tarea:
* Modelar con Calculo Lambda:
- encode, decode, succ, sum, pow, mul y, los guapos, pre y sub
- Los booleanos
- Los pares
- Las listas

* Confluencia = CR (Se cumple)
-V- t,t1,t2 . t ->> t1 & t->> t2 -]u . t1 ->> u & t2 ->> u

* Terminación (No se cumple)

------------------------------------------------------------------------------------------

Tarea:
* Modelar con Calculo Lambda:
- encode, decode, succ, sum, pow, mul y, los guapos, pre y sub
- Los booleanos
- Los pares
- Las listas
ċ
Lambda.hs
(0k)
Guillermo Polito,
Jul 17, 2012, 3:55 PM
Comments