Final 09/03/2017 (Paradigmas)

1. Para cada afirmación decidir si es verdadera o falsa y justificar:
   1. $\forall$ término M $\in \lambda ^{bn}$, si $\emptyset \vdash M:\sigma$ es derivable, entonces existe un valor $V$ tal que $fix\ M\twoheadrightarrow V$
   2. $\exists M\in \lambda ^{bn},\ \emptyset \vdash M:\sigma$ es derivable, y hay un valor $V$ tal que $fix\ fix\ M\twoheadrightarrow V$ y $fix\ M\twoheadrightarrow V$
2. Sea M un término tal que $\emptyset \vdash M:\sigma$, sea $W(ERASE(M))=\Gamma \vdash M':\rho$, decidir si es posible que:
   1. $\sigma \neq \rho$
   2. $\sigma =\rho ,\ M\neq M'$
3. Sea un lenguaje orientado a objetos donde no se permite sobrecarga, decidir si las siguientes situaciones son admitidas por el sistema de tipos o no. Justificar.
   1. Se sobrescribe el método de una clase y se reemplaza el tipo del argumento por un subtipo del tipo que tenía en la superclase.
   2. Se tiene un atributo de tipo ref t (es un atributo mutable), se lo sobrescribe en una subclase por un tipo ref s, donde s es subtipo de t.
4. Decidir si es verdadero o falso:
   1. {P(x, y)} y {P(y, f(y)} no unifican.
   2. $\forall x.\forall y.P(x,f(x))\ \wedge \ \lnot P(y,f(y))$ es una forma normal de Skolem de $\forall x.\forall y.\exists z.P(x,z)\ \wedge \ \lnot P(y,z)$.
   3. Sea un programa de Prolog con unicas clausulas: "P(X,Y) :- q(X). P(X,Y) :- q(Y)", la expresion "q(X), ~q(Y)" aparece en el arbol de busqueda de Prolog de "P(X,X), ~P(Y,Y)".

5. Sea un programa en Prolog que redefine el "not" como:

not(G) :- call(G), fail, !.
not(G).

Comparar el resultado de evaluar not(P) si el arbol de resolucion SLD de P es:

a) finito y sin solución

b) finito y con solución

c) infinito y con solución

6. Seguimiento en Smalltalk