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].

---

Eso es lo que me tomó a mí, a algunos les tomó Curry y Uncurry (dar las funciones, los tipos de las mismas, dar ejemplos), también les tomó algo parecido al de for pero con árboles binarios que tenían un tipo en los nodos internos y otro en las hojas, por ejemplo: Bin A B := Hoja A | Nodo B (Bin A B) (Bin A B).

También tomó algo de resolución bastante sencillo por lo que me dijeron y algo de armar un árbol de Prolog.