Encuentro 2 - 2/6/2012 - Sistemas de tipos

Recordamos el lenguaje de la clase pasada

El lenguaje lo llamamos BN (es decir, tiene Booleanos y Naturales)

Términos:
t ::= true | false | if t then t else t | 0 | succ t | prev t | isZero t

Valores
    v ::= true | false | nv
    nv ::= 0 | succ nv

Evaluación:
if true  then t1 else t2 -> t1

if false then t1 else t2 -> t2

t1 -> t1'
_______________________________________________

if t1 then t2 else t3 -> if t1' then t2 else t3


prev (succ t) -> t

prev 0 -> 0

t-> t'
_________________

succ t -> succ t'


t -> t'
_________________

prev t -> prev t'


isZero 0 -> true


isZero (succ t) -> false


t -> t'
_____________________

isZero t -> isZero t'

Hacemos foco en:

if true  then T1 else T2 -> T1


if false then T1 else T2 -> T2


T1 -> T1'
_______________________________________________

if T1 then T2 else T3 -> if T1' then T2 else T3


Es importante notar que esto determina un orden.
Los primeros dos sistemas de reglas no van a poder aplicarse hasta que T1 se reduzca a true o false.

Se marcó que la siguiente reducción no es cierta:

T1 -> T2
X ______________

 C[T1] -> C[T2]

"Si T1 puede reducirse a T2, entonces un contexto que contiene T1 puede reducirse a ese mismo contexto conteniendo T2"

Esta afirmación es falsa. Justamente en el if T1 then T2 else T3. Yo no quiero reducir T2 si T1 no se reduce a true.

Algunas propiedades de un lenguaje o un sistema de tipos

Un programa "tipa".

Habíamos dicho que las formas normales son:

T / No existe T' . T -> T'

Dijimos también que estaría bueno que las FN sean los Valores.

"En un programa tipado, todo puede avanzar un paso o es un valor."

El objetivo de un sistema de tipos es detectar las Formas Normales que no son Valores antes de la evaluación.

defino 'v' (en realidad es => girado 90°... ¬¬):
T1 'v' T2 <=> T ->> T2 & T2 es FN

T1 'v' T2 & T1 'v' T3 => T2 = T3
"Si T2 es FN de T1 y T3 es FN de T1, entonces T2 es T3"
"Es decir, si la FN existe, es única."


Mencionamos 4 propiedades en las que nos va a interesar pensar (por lo menos):

* CONFLUENCIA (prop. de la evaluación)
t -> t1 & t -> t2 => t1 ->> t3 & t2 ->> t3
"Si tengo un t que reduce a t1 y reduce a t2 entonces se espera que en algún momento t1 y t2 reduzcan a t3"

* TERMINACION (prop. de la evaluación)
"No se puede evaluar infinitas veces. Eventualmente se termina."

* PROGRESS (prop. de los tipos)
"Todo termino que tipa o bien puede avanzar un paso más o es un Valor."

* PRESERVATION (prop. de los tipos)
t : T & t -> t' => t' : T'
"Si tengo un termino que tiene un tipo y avanzo un paso, el resultado tiene un tipo"

De hecho, para que se lleve bien con el contexto (y dado que estamos en un lenguaje sin subtipos) debe darse que :

Si t : T y t -> t' entonces t' : T

Definición formal del sistema de tipos

Tipos:
T:= Nat | Bool

Reglas de tipado:
true  : Bool

false : Bool

0 : Nat

t: Nat
____________

succ t : Nat


t: Nat
____________

prev t : Nat


t: Nat
_______________

isZero t : Bool


t1: Bool  t2 : T  t3 : T
_________________________

if t1 then t2 else t3 : T


con este sistema:

succ false    <- Este sería un error de programación
isZero (if t then true else 0) <- Este también

Implementación


Un poquito de mónadas

Ahora para seguir conviene entender un poquito de monadas... Entonces:

Las mónadas son tipos abstractos de datos que definen dos funciones:

M a 

return :: a -> M a
(>>=)  :: M a -> (a -> M b) -> M b "Se le dice bind"

El Maybe, por ejemplo, es una mónada. ¿Como están definidas estas funciones?

Nothing  >>= _ = Nothing
(Just t) >>= f = f t

return e = Just e

Las mónadas son más felices de usar ayudandonos con un do, donde podemos abrir y cerrar la mónada de forma más o menos transparente.

Breve repaso de inducción

Ok, ahora queremos demostrar cosas.

Como nuestras definiciones de tipos son recursivas, vamos a usar inducción.

Repaso de inducción:

Demostrar que 3 ^ n es impar

n = 1 : 3 ^ 1 es impar

supongo que 3 ^ n es impar

ddq 3 ^ (n + 1) es impar <- "debo demostrar que"


3 ^ (n + 1) = 3 ^ n * 3 ^ 1
= impar * impar = impar

---

¿Que tiene que tener un conjunto para poder utilizarlo en una demostración por inducción?

* Establecemos una relación de orden sobre el conjunto
Y que era orden? era una relación en la que se cumplen 3 propiedades:
* Reflexiva
a < a "Ojo, no es el > de menor"

* Antisimetrica
a > b  &&  b < a  =>  a = b

* Transitiva
a < b  &&  b < c  =>  a < c

* El orden que elijamos tiene que estar bien fundado.
"Es decir, si dado un conjunto yo puedo definir algunos *primeros* y el concepto de precedencia le va a gustar la inducción"

Justamente, los terminos que definimos para nuestro lenguaje cumplen con esto.

"t1 precede a t2 si t1 es subtermino de t2"

Como ordeno esto?

P1) 0
P2) pred 0
P3) succ 0
P4) if true then succ 0 else 0
P5) if true then pred 0 else 0
P6) if true then succ 0 else prev 0


   P6
P5  /\  P4
| /  \ | "Recordar que la relación es *es subtermino de*"
   P2  P3
 \  /
  \  /
   P1


Entonces como uso inducción?

Inducción Simple
p(1) && p(n) => p(n+1) -V-n perteneciente a los Naturales
"Si se cumple p(1) y p(n) entonces se cumple p(n+1)"

Inducción Completa
-V- i < n, p(i) => p(n) -V-n perteneciente a los Naturales
"Si se cumple para todo i menor a n, entonces se cumple para todo n"
"Notar que acá no hay un caso base..."


Ej:
Sum(1,n){i} = (n+1) n / 2

n=1 : Sum(1,1){i} = 1 = (1+1) 1 / 2
lo asumo para h

n= h+1 : Sum(1,h+1){i} = h + 1 + Sum(1,h){i}
= h + 1 + (h+1) h / 2
= (2h + 2 + (h+1) h) / 2
= (2 (h+1) + (h+1) h) / 2
= (2+h)(h+1) / 2 <- Es a lo que quería llegar

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

Ej:
g : N - {1} -> N g(n) < n -V- n
f 1 = 2
f n = f (g n) + 4

Demostrar que f n es par, -V- n

n=1 : f 1 = 2, que es par
supongo -V-i <= h, f(i) es par <- Inducción Completa

ddq f(h+1) es par
f(h+1) = f (g (h+1)) + 4
si llamo k := g (h+1)
entonces k <= h, por la condici+on dada en la def. de g
por lo tanto, puedo usar h

f(k) es par
ergo f (h+1) = f k + 4 es par

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

Una prueba de Progress para BN:

Ej:
(Todo termino que tipa o bien puede avanzar un paso más o es un Valor)

t = true es un valor
t = false es un valor
t = 0 es un valor

t = succ t1 : T donde t1 : Nat
t1 tipa => t1 es un valor o t1 puede dar otro paso
* t1 es valor
* t1 = 0 -> t = succ 0 es un valor
* t1 = succ nv -> t = succ (succ nv) es un valor

* t1 puede dar otro paso hacia t1'
existe la regla de reducción:

e -> e'
_________________

succ e -> succ e'

por lo tanto, t = succ t1' puede dar otro paso


t = prev t1 : T donde t1 : Nat
t1 tipa => t1 es un valor o t1 puede dar otro paso
* t1 es valor
* t1 = 0 -> t = 0 es un valor
* t1 = succ nv -> t = prev (succ nv)
existe la regla de reducción:

prev (succ e) -> e
por lo tanto, t = succ t1' puede dar otro paso

* t1 puede dar otro paso hacia t1'
existe la regla de reducción:

e -> e'
_________________

prev e -> prev e'

por lo tanto, t = prev t1' puede dar otro paso


t = if t1 then t2 else t3, donde t1 : Bool, t2 : T, t3 : T
t1 tipa => t1 es un valor o t1 puede dar otro paso
* t1 es valor
existen reglas para reducir puede dar otro paso

*t1 puede dar otro paso hacia t1'
existe reglas para reducir puede dar otro paso

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

Tareas

  • Para pensar:
    1. ¿Por qué el principio de inducción completa no tiene un caso base en su definición? ¿Cómo puede ser que no haga falta?
    2. Sin embargo, en la demostración de el ejercicio hicimos dos demostraciones, para f(1) y f(n), ¿por qué?
  • Demostrar por Inducción Completa Fibbonacci:
f(n) = (a^n - b^n) / a - b
a = (1 + sqrt(5)) / 2
b = (1 - sqrt(5)) / 2

  • Demostrar que el qsort devuelve una lista ordenada. Para ello hay que definir primero qué significa "ordenada". ¿Qué tipo de inducción usamos? ¿Qué orden definimos sobre las listas? ¿Se puede usar inducción estructural?
qsort [] = []
 qsort (x:xs) = qsort (menores xs) ++ [x] ++ qsort (mayores xs)
where menores xs = filter (< x) xs
where mayores xs = filter (>=x) xs

Demostrar que esto ordena cualquier lista.
  • Demostrar que esta igualdad es correcta.
map f xs == foldr (\x a -> fx : a) [] xs

Explicitar sobre qué se hace la inducción y cuál es el orden utilizado.

  • Demostrar las restantes tres propiedades del lenguaje BN (el que usamos en clase). 
    • La confluencia es obvia, ¿por qué?
    • Terminación (usar el tamaño del término).
    • Preservation
  • Agregar la suma al lenguaje
    • extender el conjunto de términos, las reglas de evaluación y las reglas de tipado.
    • demostrar las 4 propiedades buenas.
    • lo mismo para multiplicación y exponenciación
  • En sites.google.com/site/unqmatematica1 hay guias para practicar inducción
  • Demostrar que en todo programa cuyo tipo es Nat, aparece el 0.
  • Demostrar que en todo programa cuyo tipo es Bool, aparece o bien True o bien False.
  • Demostrar que el recíproco de los anteriores no es cierto, o sea, que hay programas donde aparece el 0 y tipan a Bool, y programas donde aparece True y tipan a Nat.
  • Demostrar que en todo programa que empieza con la palabra if, aparece o bien True o bien False.
  • En la definición de f_g, si se saca el +4, pensar qué se puede decir de f_g(n), y demostrarlo.
  • Demostrar que si un programa tiene un tipo, en el programa aparece succ, y no aparece iszero, entonces el tipo de programa es Nat.

ċ
Taller de Lenguajes - Clase 02.hs
(2k)
Guillermo Polito,
Jun 3, 2012, 2:54 PM
Comments