Final 03/08/2022 (Paradigmas)

Funcional

• Si tenés una función de fold con el siguiente tipo, cómo sería la estructura de datos para D?

    foldA :: (b -> b) -> (b -> a -> b) -> D a -> b

Rta:

    data D a =  C (D a) | N (D a) a

• Ahora imaginate que querés usar foldA para calcular una función “ok” que te devuelve false si la estructura contiene en algún lugar un doble llamado consecutivo al constructor “C” (y true en caso contario), es decir:

    ok :: D a -> Bool
    ok  N (C (C unC)) -> false

Rta: Era una pregunta trampa, porque con foldA no es fácil de definir: tenés que hacer el truquito de devolver una tupla con el resultado recursivo y el resto de tu estructura (no me pidió que lo haga, sólo lo charlamos un poco). Usando una función de recursión primitiva recA sí podrías fácilmente:

    recA :: ((D a) -> b -> b) -> ((D a) -> b -> a -> b) -> D a -> b

    ok = recA (\est rec -> if isC(est) then False else rec) (\est rec x -> rec)

donde

    isC :: D a -> Bool
    isC (C x) = True
    isC _ = False

Lambda Cálculo

• Imaginate que modifico la regla de proyección sobre registros de la siguiente forma:

    1 =< j =< n
 ------------------------------
   {l1 = M1, …, ln =Mn}.lj -> Mj

Es decir, no pedimos que todos los campos sean valores. Qué problema hay con esto?

Rta: rompés determinismo, porque si te encontrás con un término {l1 = M1, …, ln =Mn}.lj no sabés si seguir reduciendo el registro o proyectar.

• Borrar la siguiente regla lo arregla?

    M -> M’
 ---------------
   M.li -> M’.li

Rta: no, porque podés tener términos M que no son registros pero que sí reducirían a uno, e.g.

( (\x : nat. {l1 = M1, …, ln =Mn}) 2 ).lj

Subtipado

• Qué problema introduce la regla de subtipado T-Subs? Cómo se arregla?

Rta: las reglas de tipado dejan de ser dirigidas por sintaxis. Se arregla “cableando” la regla dentro de la regla de aplicación.

• Y si ahora queremos poder subtipar en las funciones de naturales?

Rta: Después de charlar un poco me di cuenta de que lo que me estaba pidiendo era permitir hacer cosas como succ(False) (ya que Bool <: Nat). Hay que cablear esa regla en isZero, succ, pred, de forma de permitir que puedan ser aplicadas a subtipos de nat. Por ejemplo:

    Gamma |- M : sigma,  sigma <: nat
  --------------------------------------
    Gamma |- succ(M) : nat

Cálculo Sigma

• Cómo codificás booleanos en cálculo sigma?

Rta: Acá hice agua porque no lo tenía nada presente, pero me ayudó e hice lo siguiente y con eso alcanzó:

    True = [
        not = c(x). [
            not = c(y).x
            if = c(y)(\ m n -> n)
        ]
        if = c(x) (\ m n -> m)
    ]

Lógico

• Cómo funciona not en programación lógica?

Rta: Le escribí la definición, charlamos un poco sobre por qué no es negación lógica y por qué no instancia variables.

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

• Si las siguientes cláusulas están skolemizadas, de qué fórmula de primer orden pueden haber venido?

{P(X,f(e))} , {Q(Y, f(Y))}

Rta:

La cláusula se puede reescribir como:

 $[(\forall X)P(X,f(e))]and[(\forall Y)Q(Y,f(Y))]$

Lo cual antes de skolemizar puede haber sido:

 $[(\exists Z)(\forall X)P(X,f(Z))]and[(\forall Y)Q(Y,f(Y))]$

Javascript

• Cómo funciona la herencia en javascript?

Rta: Mediante prototipado, le expliqué que podés clonar a un objeto y te va a poner al objeto como protipo, y que también podés sobrescribir el prototipo.

• Cómo funciona el protipado con funciones constructoras?

Rta: Esto no lo supe responder