Enunciado

1. Se da una estructura Dato a b = C1 | C2 a | C3 b (Dato a b) (Dato a b). Definir recursión primitiva, recursión estructural en base a la recursión primitiva, y después una función Split que tome un Dato a b y devuelva dos listas, una con los a y otra con los b, usando el fold o rec.

2. Se toma una extensión del cálculo lambda λ*. Se le agrega ∅ |- M : σ. El operador →* indica la clausura transitivo-reflexiva de la reducción. Verdadero o falso:

a. Si λ* cumple progreso, entonces M → V (falso porque puede que no se reduzca un término a valor en un sólo paso)

b. Si λ* cumple progreso, entonces M →* V (creo que falso porque necesitás terminación también para que se cumpla, aunque con terminación sería verdadero)

c. Si λ* cumple preservación y preservación, entonces M →* V (creo que sería el mismo razonamiento que el anterior, preservación no debería cambiar nada)

3. Te daba la regla de inferencia para la aplicación. Después daba dos variantes y pedía explicar por qué no funcionaban. Una quitaba la condición de que los contextos de tipado de los términos tenían que unificar para todas las variables compartidas, el otro en vez de generar una incógnita fresca le asignaba una variable de tipo directamente a la aplicación. La idea era dar una inferencia de tipo errónea con cada regla.

4. Se daba el siguiente programa en Prolog

p(a).

p(b).

q(a).

q(c).

r(X,Y) :- q(X), !, p(Y).

s(X,Y) :- p(X), not(r(X,Y).

s(Y,Y) :- q(c), r(c,Y).

Tenías que dar el árbol de búsqueda para la consulta S(X,Y).

Después te daba dos clausulas, {P(X,X)} y {not (P(X, f(Y)}. Tenías que explicar si se podía aplicar la resolvente o no, y de poder hacerlo cuál era el MGU (trivialmente se puede, y queda S= {X:=f(Y)}).

5. Tomando una representación de grafos como lista de aristas en Prolog (ejemplo: [(a,b), (b, c), (d,c)]). Se pide definir los siguientes predicados:

caminosSimples(+G, +S, +E, -P), que pide devolver todos los caminos simples entre S y E. G se puede asumir acíclico.

aciclico(+G), que devuelve si G es aciclico o no.

caminos(+G, +S, +E, -P), que devuelve todos los caminos entre S y E, para un grafo que puede tener cíclicos.

Finalmente había que analizar la reversibilidad sobre G y S para este último.

6. Probar con deducción natural

∀X(P(X)∨Q(X)) → ¬(∃Z(¬P(Z)∧¬Q(Z)))

Después daba una fórmula en cálculo lambda que era una función sobre unión disjunta (o sea, un término de tipo σ + τ) y pedía dar la fórmula lógica que correspondería a dicho término y justificar por qué correspondía (correspondencia Curry Howard).

7. Se daban las siguientes definiciones en Smalltalk:

Object subclass: #A { ... n: ^2 }

A subclass: #B { ... n: ^super n }

B subclass: #C { ... m: ^1 } C subclass: #D { ...

}

Se pedía mostrar todo el pasaje de mensajes, y el resultado, para la evaluación de (D new) n. Después se pedía el resultado de (D new) m, suponiendo que se hubiera sobreescrito el new de C para que devuelva (B new).