Tarea 2

Esto es un draft, todavía no es la tarea oficial!! Consulte las normas de entrega de tareas en http://pleiad.cl/teaching/cc4101.

En esta tarea se explorá el mundo de la lógica, a través de la implementación de un “evaluador de predicados”. Esto con el fin de evaluar expresiónes en notación prefija como:

; Todo elemento en S tiene una factorización en S
(with (S (set (2 3 4 5 6)))
         (all x in S
              (exists y in S
                      (exists z in S
                              (= x (* y z))))))

O bien consultar si la siguiente afirmación es satisfacible:

(<=> (=> p q) (or (¬ p) q))

Recordemos que la nocion de satisfacibilidad es distinta a la de equivalencia. En el predicado anterior se cumple que ambos costados de la ⇔ tienen los mismos valores de verdad para cualquier valor de p y q. Un ejemplo de un predicado que no es siempre cierto pero si es satisfacible es el siguiente:

(<=> (=> p q) (or p (¬ q)))

El cuál por reglas de reducción no es cierta para todos los casos, pero si es satisfacible pues cuando p y q son ambos falsos el predicado es verdadero.

Con la intención de mejorar la expresividad en los predicados, se agregará al lenguaje la opción de definir funciones globales. Tendremos programas con varias definiciones de función, seguidas por una expresión “main”.

{{define {esPar? x} { (= (mod x 2) 0)}}
 {define {unfuncion x} {una implementación}}
    in
    '{with (S (set (10 20 30 40)))         
         (all n in S
                 (esPar? n))}}

El siguiente listado muestra la grámatica BNF de nuestro lenguaje.

<prog> ::= <fun-def>* in <expr>

<fun-def> ::= (define {<id> <id>} : <expr>)

<expr> ::= <AE>
         | <prop>         
         | (set [<expr>*])

<prop> ::= #t 
         | #f
         | <id>
         | (with (<id> <Expr>) <Expr>)
         | (or <prop> <prop>)
         | (and <prop> <prop>)
         | (not <prop>)
         | (xor <prop> <prop>)
         | (=> <prop> <prop>)
         | (<=> <prop> <prop>)
         | (all <id> <Set> <prop>) 
         | (exist <id> <Set> <prop>)
         | (< <AE> <AE>)
         | (= <AE> <AE>)         

<AE>   ::= <num>
         | <id>
         | (with (<id> <Expr>) <Expr>)
         | (+ <AE> <AE>)
         | (- <AE> <AE>)
         | (* <AE> <AE>)
         | (/ <AE> <AE>)  

El AST que deberá usar para representar dicha gramática se encuentra adjunto en el fichero <link a fichero start.rkt con gramática>. Note que la gramática permite ⇒, ⇔ y xor como azucares sintácticos, su parser debe encargarse de reemplazarlas por expresiones equivalentes en el AST adjunto (sin necesidad de crear nuevos nodos, lo cual será verificado). Implemente la función parse para su lenguaje:

(define (parse s-expr) ...)

1. (0.5) Escriba los siguientes predicados usando la gramática definida. Estos predicados los podrá usar como tests.
   • a) Sea un conjunto S = { … } de números enteros. Este conjunto tiene un mínimo
   • b) Sea un conjunto P = { … } de números enteros. Existe un elemento en el conjunto que es primo
   • c) Todos los elementos de un conjunto P = { … } de números enteros son primos
   • d) Todos los elementos de un conjunto P = { … } son pares
   • e) Para todo par a, b en un conjunto N de naturales se cumple a^2 + b^2 < (a+b)^2

Nota: Como los conjuntos (S, P, N) son finitos y definidos por usted, se pueden usar conjuntos auxiliares para expresar sus predicados. En caso de que los conjuntos fueran finitos, pero arbitrarios, ¿que necesitaría para poder expresar los predicados b), c) y d) de manera genérica?

1. Defina la función (eval expr) que evalua una expresión con cuantificadores sobre conjuntos acotados. Recuerde que basta con que para al menos un valor del cuerpo del cuantificador existencial (exists) evalue a #t para que toda la expresión evalue a #t, mientras que para el cuantificador universal (all) se requiere que todos los valores del cuerpo sean #t para evaluar a #t

   ; Todos los elementos del conjunto son menores a 4
   > (eval (parse '(all x in (set (1 2 3)) (< x 4))))
   #t
   ; Sea el conjunto N los numeros del 1 al 9
   ; Para todo x < 4 en N, x^2 pertenece a N
   > (eval (parse '(with (N (set (1 2 3 4 5 6 7 8 9)))
                         (all x in N
                              (exists y in N
                                      (or (not (< x 4))
                                          (= y (* x x))))))))
   #t
   ; Sea Z el conjunto de enteros entre -3 y 3
   ; Elevar al cuadrado cualquier valor en Z resulta en un número no negativo
   > (eval (parse '(with (Z (set (-3 -2 -1 0 1 2 3)))
                         (all z in Z
                              (not (< (* z z) 0))))))
   #t
   > (eval (parse '(/ 5 2)))
   2

2. Defina la función (free-vars expr) que entregue una lista con las variables libres de un predicado sin repetir. TODO: Definir este caso

   > (free-vars (parse 
                 '(with (x y)
                        x)))

3. Defina la función (satisfiable? s-expr) que utilice (free-vars expr) para determinar si un predicado booleano es satisfacible para algun valor de verdad de sus variables libres. Hint: use el cuantificador de existencialidad sobre las variables libres y el conjunto predefinido {#t ,#f}.

   > (satisfiable? '(or p q))
   #t
   > (satisfiable? '(and p (: p)))
   #f
   > (satisfiable? '(<=> (=> p q) (or p q)))
   #t
   > (satisfiable? '(<=> (=> p q) (and p (: q))))
   #f

Si bien el interprete anterior logra calcular los resultados esperados, es ineficiente dado que debe intentar hacer todas las sustituciones posibles de todos los valores de verdad. Por ejemplo en el caso (and #f (or p q)) podemos saber inmediatamente que para cualquier valor de p o q siempre el valor resultante será #f, por lo que vamos a agregar un paso antes de la evaluación que elimine tautologías y simplifique el calculo posterior.

1. Defina la función (deMorgan expr) que toma una expresión y le aplica las leyes de DeMorgan 2. Con esto se puede asegurar que las negaciones ¬ solo aparecen inmediatamente después de un identificador o un valor booleano
2. Defina la función (simplify expr) que se encarge de eliminar las siguientes expresiones: (and #f p), (or #t p), (¬ #t), (¬ #f), (or p p) y (and p p) del predicado representado por expr. Asegurese de utilizar la función deMorgan definida anteriormente para uniformar las expresiones pues el predicado p puede ser arbitrariamente complejo. Hint: use la función equal? para verificar igualdad de predicados arbitrariamente complejos. No es necesario verificar permutaciones.
3. Constant folding es una optimización utilizada en compiladores que elimina el cálculo innecesario de expresiones constantes, y las reemplaza directamente con su valor. Los siguientes test deben pasar:

   (test (constant-folding
            (parse ’{with {x 1} {+ x {- 1 {+ 2 3}}}}))
           (parse ’{with {x 1} {+ x -4}}))

   Implemente la función (constant-folding expr) que aplique esta optimización

4. Defina la función (o-satisfiable? s-expr) que elimina tautologías (y posiblemente identificadores libres) antes de evaluar. De un ejemplo de un predicado que toma mucho más tiempo de evaluar con la función satisfiable? que con o-satisfiable?