Final 22/12/2014 (Paradigmas)

1) Extender el cálculo Lambda con referencias para que soporte cosas del tipo $for(i:=M_{1}|M_{2}|M_{3})$. Te dejaba usar un for'(M|M') como auxiliar.

Aximoas de tipado:

${\frac {\Gamma |>M_{1}:Nat,\Gamma \cup \{i:RefNat\}|>M_{2}:Bool,\Gamma \cup \{i:RefNat\}|>M_{3}:Unit}{\Gamma |>for(i:=M1|M2|M3):Unit}}$

Semántica operacional:

${\frac {M_{1}|\mu \rightarrow M_{1}'|\mu '}{for(i:=M_{1}|M_{2}|M_{3})|\mu \rightarrow for(i:=M_{1}'|M_{2}|M_{3})|\mu '}}$

${\frac {.}{for(i:=V|M_{2}|M_{3})|\mu \rightarrow for'(M_{2}|M_{3})|(\mu \oplus \{i\leftarrow v\})}}$

Esto es porque si reducimos $M_{2}$ entonces siempre va a evaluar a lo mismo y o no corre o no termina el for.

${\frac {.}{for'(M_{2}|M_{3})|\mu \rightarrow ifM_{2}thenM_{3};for'(M_{2}|M_{3})elseunit|\mu }}$

Algoritmo de inferencia

$W(U_{1})=\Gamma _{1}|>M_{1}:\sigma$

$W(U_{2})=\Gamma _{1}|>M_{2}:\tau$

$W(U_{3})=\Gamma _{1}|>M_{3}:\rho$

$S=mgu(\sigma =Nat,\tau =Bool,\rho =Unit)$ (falta ver que los tipos de la misma variable en distintos contexto sean el mismo tipo y que i sea de tipo ref Nat en $\Gamma _{2}$ y $\Gamma _{3}$.

$(for(i:=U_{1}|U_{2}|U_{3}))=S\Gamma _{1}\cup S\Gamma _{2}\cup S\Gamma _{3}|>for(i:=M_{1}|M_{2}|M_{3}):Unit$

2) Escribir en prolog la función esCamino(+Path,+Graph,+NodoInicial) donde Graph es lista de ejes.

esCamino([N],G,N).

esCamino([A,B|C],G,A) :- member((A,B),G), esCamino([B|C],G,B).

3) ¿Es tipable foldr map? ¿Qué representa foldr map?

foldr :: (a -> b -> b) -> b -> [a] -> b map :: (a->b) -> [a] -> [b]

Entonces podemos reemplazar por

foldr :: ((a->a) -> [a] -> [a]) -> [a] -> [a->a] -> [a] map :: (a->a) -> [a] -> [a]

y foldr map va a tener tipo [a] -> [a->a] -> [a]

El resultado de foldr map va a ser aplicarle las funciones de la lista [a->a] una atrás de la otra (como foldr) a los elementos de la lista [a] (como map).

Por ejemplo, foldr map [0,1] (+1,+2,+3) va a hacer [0,1] -> [1,2] -> [3,4] -> [6,7].