Paradigmas de Lenguajes de Programación 1C2024

Resumen para el primer parcial

Todo el contenido de este archivo es una recopilación/resumen del contenido de las teóricas/prácticas del campus de la materia, que fue transcrito en Latex por mi. Puede contener errores.

versión en pdf

Haskell

Tipos de datos algebraicos

En general, los tipos de datos algebraicos tienen la siguiente estructura:

Los constructores base NO reciben parámetros de tipo T.

Los constructores recursivos reciben al menos UN parámetro de tipo T.

Definición inductiva de T: Los valores de tipo T solamente se pueden construir aplicando una cantidad finita de constructores base y/o recursivos del mismo tipo T.

data T =  casoBase1 <parametros>
	| casoBase2 <parametros>
	...
	| casoBaseN <parametros>
						
	| casoRecursivo1 <parametros>
	| casoRecursivo2 <parametros>
	...
	| casoRecursivoN <parametros>
				

Recursión estructural

Dada una función g : T → Y definida por ecuaciones:

g(Cbase1 <parametros>)       = <caso base1>
g(Cbase2 <parametros>)       = <caso base2>
...
g(CbaseN <parametros>)       = <caso baseN>

g(Crecursivo1 <parametros>)  = <caso recursivo1>
g(Crecursivo2 <parametros>)  = <caso recursivo2>
...
g(CrecursivoN <parametros>)  = <caso recursivoN>

g está dada por recursión estructural si cumple:

1. Cada caso base devuelve un valor fijo
2. Cada caso recursivo se escribe combinando:
   1. Los parámetros del constructor que NO son de tipo T (sin usar los parámetros del constructor que son del tipo T).
   2. El llamado recursivo sobre cada parámetro de tipo T (sin hacer otros llamados recursivos).

Ejemplo de recursión estructural:

data AB a = Nil | Bin (AB a) a (AB a)
							  
-- Funcion que abstrae el esquema de recursion estructural en arboles binarios:
foldAB :: b -> (b -> a -> b -> b) -> (AB a) -> b
foldAB cNil cBin Nil = cNil
foldAB cNil cBin (Bin izq r der) = 
	cBin (foldAB cNil cBin izq) r (foldAB cNil cBin der)
	
-- Ejemplo de uso: sumar todos los elementos del arbol 
sumAB :: (Num a) => AB a -> a
sumAB = foldAB 0 (\recI r recD -> recI + r + recD)

mapAB :: (a->b) -> AB a -> AB b
mapAB fMap = foldAB Nil (\recI r recD -> Bin recI (fMap r) recD)

Recursión primitiva

Dada una función g : T → Y

g está dada por recursión primitiva si cumple:

1. Cada caso base devuelve un valor fijo
2. Cada caso recursivo se escribe combinando:
   1. Todos los parámetros del constructor del tipo T (incluyendo a los que son de tipo T)
   2. El llamado recursivo sobre todos los constructores recursivos (sin hacer otros llamados recursivos)

Recursión iterativa

— TO-DO (en el parcial entra recursión estructural sobre tipos algebraicos)

Inducción estructural

Queremos demostrar que ciertas expresiones son equivalentes

Para eso debemos asumir lo siguiente:

1. Trabajamos con estructuras de datos finitas: tipos de datos inductivos
2. Trabajamos con funciones totales:
   1. Las ecuaciones deben cubrir todos los casos.
   2. La recursión siempre debe terminar.
3. El programa no depende del orden de las ecuaciones.

Principio de reemplazo

Sea e1 = e2 una ecuación dentro del programa. Las siguientes operaciones preservan la igualdad de expresiones:

1. Reemplazar cualquier instancia de e1 por e2
2. Reemplazar cualquier instancia de e2 por e1

Si una igualdad se puede demostrar solo por principio de reemplazo, decimos que la igualdad vale por definición.

A veces conviene dar nombre a todas las ecuaciones del programa para saber cuál ecuación se utilizó para reemplazar una instancia por otra.

Ejemplo:

sucesor :: Int -> Int
-- tenemos una igualdad de la forma e1 = e2
sucesor n = n+1      -- {SUC}

-- sucesor (factorial 10) + 1
-- ((factorial 10) + 1) + 1        (por SUC. reemplazo e1 por e2)
-- sucesor (factorial 10 + 1)      (por SUC. reemplazo e2 por e1)

Inducción sobre booleanos

Si $P(True)\ \text y\ P(False)$ entonces: $∀x :: Bool.\enspace P(x)$

Ejemplo:

Ahora podemos usar principio de reemplazo usando las siguientes ecuaciones para probar 1 y 2:

not True  = False   -- {NT}
not False = True    -- {NF}

Inducción sobre pares

Ejemplo:

Y para probar esto podemos usar ppo. de reemplazo usando, por ejemplo, las siguientes ecuaciones dadas:

fst (x,_)   =  x      -- {FST}
snd (_,y)   =  y      -- {SND}
swap (x, y) = (y, x)  -- {SWAP}

Inducción sobre naturales

-- Usamos la siguiente representacion de numeros naturales
data Nat = Zero | Suc Nat

Inducción estructural

Para probar una propiedad $P$ sobre todas las instancias de tipo $T$, basta probar $P$ para cada uno de los constructores (asumiendo como H.I que se cumple para los constructores recursivos)

Tenemos un tipo de datos inductivo de la forma:

data T =  casoBase1 <parametros>
	| casoBase2 <parametros>
	...
	casoBaseN <parametros>
						
	| casoRecursivo1 <parametros>
	| casoRecursivo2 <parametros>
	...
	| casoRecursivoM <parametros>

Ejemplo: Inducción sobre árboles binarios

data AB a = Nil | Bin (AB a) a (AB a)

Ejemplo: Inducción sobre listas

data [a] = [] | a : [a]

Extensionalidad

Extensionalidad para pares

(se prueba mediante ppo. de inducción estructural)

Extensionalidad para sumas

data Either a b = Left a | Right b

Principio de extensionalidad funcional

Sea $\text{f, g :: \ a} \to \text{b}$

Para probar una igualdad de tipo $\text{f = g}$ basta con probar que vale $\text{f x = g x}$ para todo $\text{x}$ del dominio de las funciones $\text{f}$ y $\text{g}$. (Son iguales punto a punto)

Calculo lambda

Calculo lambda puro (sin tipos) extendido con booleanos

-- Sintaxis (términos)
M := x                     -- Variables 
	| λx.M                 -- Abstraccion
	| M M                  -- Aplicacion
		
	| true
	| false
	| if M then M else M
		
-- Semantica (reglas de reduccion)
Si M -> M' entonces:
	M N  ->  M' N
	N M  ->  N M'
	λx.M ->  λx.M'
	
	if M then N else O -> if M' then N else O
	

Calculo lambda tipado. $\lambda ^{BN}$

Se agregan los siguientes tipos:

• Funciones
• Booleanos
• Naturales

Es determinista: estrategia Call-by-value (evaluar primero los argumentos antes de pasarlos a la función).

$\lambda (x.M)\, V $ reduce solo cuando V está en forma normal (no existe V’ tal que V → V’)

Sintaxis del cálculo lambda tipado $\lambda ^{BN}$

-- Términos
M ::=  x 
	| λx:σ. M
	| M M 
	| true
	| false
	| if M then M else M
	| zero 
	| suc(M)
	| pred(M)
	| isZero(M)
		
-- Tipos
σ ::= Bool      -- Booleanos
	| Nat       -- Naturales
	| σ -> σ    -- Funciones

Reglas de tipado de $\lambda ^{BN}$

Cada término tiene su propia regla de tipado.

Semántica del cálculo lambda tipado $\lambda ^{BN}$

Valores: Son los términos M los cuales están en forma normal y además FV(M) = ∅

Semántica operacional (small-step):

Las reglas de cómputo nos dan el significado de los términos al definir como operan.

Las reglas de congruencia permiten reducir subtérminos. (Términos que están dentro de otros términos)

-- Valores
V  ::=  true
	| false
	| λx:σ.M
	| zero
	| succ(V)
		
-- Semantica operacional:
	-- Reglas de cómputo
{β}       - (λx:σ.M) V             -> M{x := V}
{if_t}    - if true then M else N  -> M
{if_f}    - if false then M else N -> N
{pred_}   - pred(succ(V))          -> V
{isZero0} - isZero(zero)           -> true
{isZeroN} - isZero(succ(V))        -> false 

	-- Reglas de congruencia
	-- Si M -> M' entonces:
{u}       - M N                 -> M' N
{v}       - V M                 -> V M'
{ifC}     - if M then N else O  -> if M' then N else O
{succC}   - succ(M)             -> succ(M')
{predC}   - pred(M)             -> pred(M')
{isZero}  - isZero(M)           -> isZero(M')

Captura de variables (sustituciones)

$M{x:=N}$ significa sustitución sin captura de variables de las ocurrencias libres de x en M por N. Se define por inducción en M:

x{x := N}        = N
y{x := N}        = y
(λx:σ.M){x := N} = M{x := N}                -- No puedo sustituir x porque no está libre
(λy:σ.M){x := N} = λy:σ.(M{x := N})          -- Si y ∉ FV(N)
(λy:σ.M){x := N} = λz:σ.(M{y := z}{x := N})  -- Si y ∈ FV(N), z ∉ FV(N)
(M O){x := N}    = (M{x := N})(O{x := N}) 

true{x := N}                  = true
false{x := N}                 = false
zero{x := N}                  = zero
(if M then O else P){x := N}  = (if M{x := N} then O{x := N} else P{x := N}) 
succ(M){x := N}               = succ(M{x := N})
pred(M){x := N}               = pred(M{x := N})
isZero(M){x := N}             = isZero(M{x := N})

Inferencia de tipos

Un término $U$ sin anotaciones de tipo es Tipable si y solo si existen:

• Un contexto de tipado $\Gamma$
• Un término con anotaciones de tipos $M$
• Un tipo $\tau$

Tales que erase(M) = U y $\ \Gamma \vdash M : \tau$

Donde erase(M) es el término sin anotaciones de tipos que resulta de borrar las anotaciones de tipos de M.

Problema de inferencia de tipos

• Dado un término $U$, determinar si este es tipable.
• En caso de que $U$ sea tipable:
  • hallar un contexto $\Gamma$, un término $M$ y un tipo $\tau$ tales que erase(M) = U y $\ \Gamma \vdash M : \tau$

Se resuelve con algoritmo $W$ de inferencia de tipos.

Algoritmo de unificación de Martelli-Montanari

Unificación: Problema de resolver sistemas de ecuaciones entre tipos con incógnitas.

Definición:

Dado un problema de unificación $E$:

• Mientras $E \neq \varnothing$, se aplica sucesivamente alguna de las seis reglas de unificación
• La regla puede resultar en una falla
• De lo contrario, la regla es de la forma $E \to_S E’$ La resolución del problema E se reduce a resolver otro problema $E’$ aplicando la sustitución $S$.

Si $E = E_0 \to_{S_1} E_1 \to_{S_2} E_2 \to … \to_{Sn} E_n \to_{Sn+1} \text{falla}$ En tal caso, el problema de unificación $E$ no tiene solución.

Si $E = E_0 \to_{S_1} E_1 \to_{S_2} E_2 \to … \to_{Sn} E_n \to_{Sn+1} E_n = \varnothing$ En tal caso, el problema de unificación $E$ tiene solución.

Reglas:

1. Delete
   $ {x\stackrel{?}{=}x } \ \cup E \to \quad E$
2. Decompose
   ${C(\tau_1, …,\tau_n)\stackrel{?}{=}C(\sigma_1,…,\sigma_n)} \ \cup \ E \quad \to \quad { \tau_1 \stackrel{?}{=} \sigma_1,…, \tau_n \stackrel{?}{=}\sigma_n} \ \cup \ E$
3. Swap
   ${\tau\stackrel{?}{=}\ {?n}} \ \cup E \to \quad {?n \stackrel{?}{=} \tau} \cup E$
   (Si $\tau$ no es una incógnita)
4. Elim
   ${?n\stackrel{?}{=}\tau} \ \cup E \to_{{?n\ := \ \tau}} \quad E’ = {{?n} := \tau }(E)$ (Si ?n no ocurre en $\tau$)
5. Clash
   ${C(\tau_1, …,\tau_n)\stackrel{?}{=}C(\sigma_1,…,\sigma_n)} \ \cup \ E \phantom{lll}\to \quad \text{falla}$ (Si $C \neq C’)$
6. Occurs-Check
   ${?n\stackrel{?}{=}\tau} \ \cup E \to \quad \text{falla}$ (Si $?n \neq \tau \; \text{y} \; ?n$ ocurre en $\tau$)

Corrección del algoritmo de Martelli-Montanari

1. El algoritmo termina para cualquier $E$
2. Si $E$ no tiene solución, el algoritmo $\text{falla}$
3. Si $E$ tiene solución, el algoritmo llega a: $\boxed{E = E_0 \to_{S_1} E_1 \to_{S_2} E_2 \to … \to_{Sn} E_n \to_{Sn+1} E_n = \varnothing }$ Y además: $\boxed{S = S_n\ \circ \ … \ \circ S_2 \ \circ S_1}$ Es el unificador más general posible (mgu)

Algoritmo W de inferencia de tipos

Recibe un término $U$ sin anotaciones de tipos. Procede recursivamente sobre la estructura de $U$:

• Si falla, entonces $U$no es tipable.
• Si tiene éxito: Devuelve una tripla ($\Gamma$, $M$, $\tau$) tal que: erase($M$) = $U$ y $\Gamma \vdash M : \tau$ es válido.

Escribimos $W(U) \rightsquigarrow \Gamma \vdash M : \tau$ para indicar que el algoritmo de inferencia tiene éxito cuando se le pasa U como entrada y devuelve una tripla $(\Gamma, M, \tau)$.

Reglas:

Algoritmo $W$ extendido para $\large\lambda^{BN}$