Tarea 2

Esto es un draft, todavía no es la tarea oficial!! Considere las definiciones del archivo start.rkt y escriba sus funciones en él. Escriba sus tests en el archivo test.rkt adjunto. Ambos fichero deben ser entregados vía U-Cursos. 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 expresiones 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 noción 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} (= (% x 2) 0)} 
    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-defs>* in <expr>

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

<expr> ::= #t 
         | #f                  
         | (or <expr> <expr>)
         | (and <expr> <expr>)
         | (not <expr>)
         | (xor <expr> <expr>)
         | (=> <expr> <expr>)
         | (<=> <expr> <expr>)
         | (all <id> <Set> <expr>) 
         | (exist <id> <Set> <expr>)
         | (< <expr> <expr>)
         | (= <expr> <expr>))

         | <num>         
         | (+ <expr> <expr>)
         | (- <expr> <expr>)
         | (* <expr> <expr>)
         | (/ <expr> <expr>)
         | (% <expr> <expr>)
         
         | <id>
         | (with (<id> <expr>) <expr>)
         | (if <expr> <expr> <expr>)
         | (<id> <expr>)
         | (set [<expr>*])

El AST que deberá usar para representar dicha gramática se encuentra adjunto (en el fichero start.rkt). 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 las funciones parse-expr y parse-prog para parsear expresiones y programas (de su lenguaje) respectivamente:

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

(define (parse-prog s-prog) ...)
</scheme>
 
 
 
===== (2.0) Interpretación sobre conjuntos finitos =====
 
  - (0.4) 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 
    * 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 (estáticamente conocidos) para expresar sus predicados. En caso de que los conjuntos fueran finitos, pero arbitrarios, ¿que necesitaría para poder expresar los predicados b) y c) de manera genérica?//
  - (1.0) Defina la función ''%%(eval-expr expr)%%'' que evalúa una expresión con cuantificadores sobre conjuntos acotados. Recuerde que basta con que para al menos un valor del cuerpo del cuantificador existencial (exists) evalúe a ''%%#t%%'' para que toda la expresión evalúe a ''%%#t%%'', mientras que para el cuantificador universal (all) se requiere que todos los valores del cuerpo sean ''%%#t%%'' para evaluar a ''%%#t%%'' <code scheme>
; Todos los elementos del conjunto son menores a 4
> (eval-expr (parse-expr '(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-expr (parse-expr '(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-expr (parse-expr '(with (Z (set (-3 -2 -1 0 1 2 3)))
                      (all z in Z
                           (not (< (* z z) 0))))))
#t
;Evaluación de / arroja resultado de división entera
> (eval-expr (parse-expr '(/ 5 2)))
2

1. (0.6) Define la función (eval-prog prog) para evaluar programas.

   > (eval-prog (parse-prog '{{define {cuadrado x} {* x x}} 
                       {define {g s} {all n in s
                                          {with {s1 {set {1 4 25}}}
                                                {exists y in s1
                                                        {= y (cuadrado n)}}}}} 
                       in {g {set {1 2 5}}}}))
   #t

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

   > (satisfiable? (parse-expr '(or p q)))
   #t
   > (satisfiable? (parse-expr '(and p (: p))))
   #f
   > (satisfiable? (parse-expr '(<=> (=> p q) (or p q))))
   #t
   > (satisfiable? (parse-expr '(<=> (=> 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. (0.5) Defina la función (simplify-negations expr) que toma una expresión y aplica las siguientes optimizaciones:
   • Leyes de Morgan:
     • ¬(p v q) ⇔ ¬p ^ ¬q
     • ¬(p ^ q) ⇔ ¬p v ¬q
   • ¬(∀x p(x)) ⇔ ∃x ¬p(x)
   • ¬(∃x p(x)) ⇔ ∀(x) ¬p(x)
   • ¬¬p ⇔ p

Con esto se puede asegurar que en un programa válido, después de las negaciones ¬ no aparecen las expresiones: v, ^, ∀, ∃, ¬. Entiéndase programa válido (a este nivel), aquellos programas que no contienen operaciones invalidas como (+ #f 1). Ejemplos:

> (simplify-negations (parse-expr '(¬ (or (¬ p) (¬ q)))))
(my-and (id 'p) (id 'q))
> (simplify-negations (parse-expr '(¬ (¬ (¬ (or p q))))))
(my-and (id 'p) (id 'q))
 

1. (0.5) Defina la función (simplify expr) que se encargue 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. Asegúrese de utilizar la función simplify-negations 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.

   > simplify (parse-expr '(or (and p (and q (and r w)))
                               (and p (and q (and r w))))))
   (my-and (id 'p) (my-and (id 'q) (my-and (id 'r) (id 'w))))                    

2. 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

3. (0.5) Defina la función (o-satisfiable? s-expr) que realiza optmización (usando simplify) 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?