Final 13/12/2016 (Paradigmas)

Era escrito (5 personas dando el final). Era a libro abierto y constaba de 7 puntos. Pedida que las respuestas sean lo más cortas y concretas posibles (ej, media carialla). Llegabas medio justo con el tiempo.

1. Dadas:

l = 1:l

f = foldr (\x y -> 1) 0

g = foldl (\x y -> 1) 0

explicar cual es el resultado de evaluar f l y g l

2. Es correcto cambiar la regla de semántica del fix por: fix V -> V (fix V) ?

3. Extendemos el calculo lambda con el operador suma (+), que vendría a ser como un Either en Haskell. Nos dan las reglas de tipado:

\-----------------------------------\

Gamma |- in1 : sigma -> sigma + tau

\-----------------------------------\

Gamma |- in2 : tau -> sigma + tau

Gamma |- M : sigma + tau -> rho, Gamma |- N : sigma + tau -> rho

\----------------------------------------------------------------\

Gamma |- case in1 => M or case in2 => N : sigma + tau -> rho

Mostrar que problemas trae a las propiedades del sistema de tipado.

4. Mostrar con un ejemplo concreto que pasa si le quitamos a la regla de inferencia del Abs la parte de: Gamma' = Gamma - {x}

5. Dado el programa en prolog:

a(1).

a(2).

p(X,Y) :- a(Z), not(member(Z,X)), P([Z|X], Y).

p(X,X).

a. Dar la cantidad de soluciones de la consulta P([], X). (usando el arbol SLD)

b. Que pasa con la cantidad de soluciones si cambiamos la 3er regla por:

  i. p(X,Y) :- a(Z), not(member(Z,X)), !, P([Z|X], Y).
  ii. p(X,Y) :- not(member(Z,X)), a(Z), P([Z|X], Y).

6. Verdadero o Falso justificando:

a. Es cierto que las clausulas {P(x,f(y)}, {P(y,y} no se pueden refutar ya que no unifican ?

b. Te daban dos formulas y decian que una era la Skolem de la otra. c. Dada G la Skolem de F.

 1. Si no existe refutación para G, entonces F es válida
 2. Si existe refutación para \lnot G, entonces F es válida

7. Eran unas clases en Smalltalk, había que hacer 2 seguimientos.