Encuentro 3 - 16/6/2012 - Práctica

TALLER DE LENGUAJES: 03 (16/06/12)

Revisamos la taréa, primero la implementación de la suma.

Defino una semántica para la suma: (una interpretación que yo le doy a los terminos)
_
0 = 0 <- "La transformada de cero es el termino cero" (le ponemos _ arriba a los terminos)
___   _
n+1 = succ n
_ _ _____
suma n m ->> n + m

Estas relaciones son en realidad una FUNCION BIYECTIVA que me relaciona los |N con mis términos.
Ahora pensemos en las reglas de reducción:

[S0D] sum n 0 -> n
[S0I] sum 0 m -> m
[SPREV] sum n m -> sum (succ n) (prev m) <- esta no está tan buena, porque mete un prev, que no es un valor.
[SSUCC] sum n (succ m) -> succ (sum n m) <- esta es la que es más de libro
[SCHOT] sum n (succ m) -> sum (succ n) m <- esta variante es buena si busco que evalúe lazy.

Faltan y sobran reglas :) Quitamos algunas redundantes antes de seguir, y nos quedan:

[S0] sum n 0 -> n
[SSUCC] sum n (succ m) -> succ (sum n m) <- esta es la que es más de libro

Y agregamos:

[SL] n -> n'
___________________

sum n m -> sum n' m


[SR] m -> m'
_____________________

sum nv m -> sum nv m' <- el nv es para que sea un valor numérico, eso evita ambigüedad al elegir que regla evaluar entre SL y SR.


Fijate que si tengo:
n -> Valor, m -> Valor ==(APLICA)==> S0 si m = 0 y SSUCC si m = succ nv
n -> Termino, m -> Termino ==(APLICA)==> SL
n -> Termino, m -> Valor ==(APLICA)==> S0 si m = 0 y SSUCC si m = succ nv
n -> Valor, m -> Termino ==(APLICA)==> SR

Como solo hay un camino para reducir, demostramos "Grátis" la CONFLUENCIA.

Demostremos ahora que la suma termina:

Demostración inducción en |N sobre m
_ _ _   _   ___
* m = 0 suma n 0 = suma n 0 -> n = n+0
_ _     ___
* supongo suma n m ->> n+m
_ ___   _______
* ddq suma n m+1 ->> n+(m+1)

_ ___         _     _
suma n m+1   =  suma n (succ m)
 _ _
[SSUCC]    -> succ (suma n m)
___
[HI]   ->> suc (n+m)
  _______
[DEF. DE SEMANTICA]     = (n+m)+1
  _______
[ASOCIATIVIDAD DE |N]    = n+(m+1)



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

A otro tema.

Definimos contexto, como una definición de termino que tiene una "caja abierta".

E ::= [] | succ E | prev E | isZero E | if E then t else t | suma E t | suma nv E

E(t) { [](t) = t
{(succ E)(t) = succ(E(t))
...


t->t'
_____________

E(t) -> E(t')


Establecemos un orden, que cumpla con ser un buen orden. Dos ordenes posibles son:

1) t < t' sii t es subtérmino de t'
2) f: T -> |N
|0| = 0
|true| = 0
|false| = 0
|succ t| = 1 + |t|
|if t1 then t2 else t3| = 1 + |t1| + |t2| + |t3|
...

voy a buscar que se cumpla:

t -> t' => |t'| < |t|

por inducción en t con orden 1
-V- t . t1 -> t1' => |t1'| < |t1|
entonces t -> t'  => |t' | < |t |


case t = true
como no existe t' / t -> t' => se cumple
case t = false
como no existe t' / t -> t' => se cumple
case t = 0
como no existe t' / t -> t' => se cumple

case t = succ t1
t1 < t, entonces puedo suponer que si t1 -> t1' entonces |t1'| < |t1|
solo tengo una regla de reducción para succ, entonces t -> t' =>  t' = succ t1' con t1 -> t1' (regla R7)
|t| = |succ t1| [pq t = succ t1]
= 1 + |t1| [por f]
> 1 + |t1'| [pq |t1| > |t1'| por HI]
= |succ t1'| [por f]
= |t'| [pq t = succ t1]

case t = if t1 then t2 else t3
t->t'
ddq |t'| < |t|

[IF-TRUE] : t' = t2
|t| = |if t1 then t2 else t3| = 1 + |t1| + |t2| + |t3| > |t2| = |t'|
[E-IF] : t' = if t1' then t2 else t3 t1 < t & t1 -> t1' por HI  |t1'| < |t1|

case suma t1 t2

tengo que definir f para la suma. Una aproximación intuitiva sería:

|suma t1 t2| = 1 + |t1| + |t2|

pero vemos que no funca bien:

|suma nv1 (succ nv2)| = 1 + |nv1| + (1 + |nv2|) = 2 + |nv1|+|nv2|
|succ (sum n1 n2)|    = 1 + (1 + |nv1| + |nv2|) = 2 + |nv1|+|nv2|

Entonces empiezo a tirar posibilidades...

Notamos que lo que tiene que tener más peso es lo que "se va achicando". Eso en nv2. Entonces lo "cargo" con más valor:

|suma t1 t2| = 1 + |t1| + 2 * |t2|

|suma nv1 (succ nv2)| = 1 + |nv1| + 2 * (1 + |nv2|) = 3 + |nv1|+ 2 * |nv2|
|succ (sum n1 n2)|    = 1 + (1 + |nv1| + 2 * |nv2|) = 2 + |nv1|+ 2 * |nv2|

Ok, ahora sí. :)

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

TAREA:

* Tratar de demostrar que no termina (o encontrar un orden para que termine) la suma con la siguiente regla:

S0, SL, SR y...

[SPREV] suma nv1 nv2 -> suma (succ nv1) (prev nv2)
Comments