Final 13/07/2020 (Paradigmas)

De cálculo lambda: Definir con fix la función 'esPar'

  let esPar = 
  \f: Nat -> Bool. 
  \x:Nat.
     if isZero(x) then true else
     if isZero(pred(x)) then false else 
     f pred(pred(x))
  in fix esPar 

M':=\x:Nat. if isZero(x) then true else if isZero(pred(x)) then false else f pred(pred(x)) M:= (\f: Nat -> Bool.M')

let esPar = (\f: Nat -> Bool) M' in fix esPar

De cálculo lambda: Que problema hay con definir la regla de semántica de "fix f -> f fix f" (lease f como un lambda)

En Haskell anda porque hay evaluación Lazy, en Cálculo Lambda no (loop infinito). La regla de aplicación de Cálculo Lambda espera a que del lado derecho haya un valor para aplicar la función. Pero fix f con esta definición nunca llega a un valor.

Qué relación hay entre el juicio de tipado de un término M, y el juicio de tipado producto de hacer W(Erase(M)))

El juicio de tipado producto de hacer W(Erase(M))) es un tipo principal, incluye al juicio de tipado del término M. En otras palabras, el juicio de tipado de W(Erase(M))) puede tener variables de tipo, mientras que el de M no.

De regla de inferencia: Encontrar un término M que al hacer W(Erase(M)), te queda un término distinto sintácticamente a M, pero del mismo tipo

M = (\f:Nat -> Nat. true) (\x:Nat. x) M' te queda (\f:t->t.true) (\x:t. x) M' =! M, pero ambos son de tipo Bool (evaluan a true)

De lógica: not(P(X)), cuando falla, cuando no. Si el árbol de resolución es infinito, ¿qué pasa?

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

Importante entender como funciona: Si encuentra una solución para g falla, pero por el corte NO BUSCA OTRAS SOLUCIONES. Entonces devuelve false. Si no encuentra una solución para g también falla, pero entra en la segunda regla. Por eso devuelve true (importante, no instancia variables)

Por eso no es igual al not lógico, que sea falso significa que no pudo probar que es verdadero.

not es verdadero, cuando el árbol de P falla finitamente, es decir pudo recorrer todas las ramas de árbol y no encontró ninguna solución. Si encuentra una sol (aunque sea infinito) da false, y si no encuentra sol, pero es infinito se cuelga el programa y por ende el not. (Se puede separar en infinito por izq y por derecha, si es por izq se cuelga, si es por derecha capaz encuentra algo antes de perderse)