Tarea 2

Esta tarea se distribuye con dos ficheros start.rkt y tests.rkt (mediante U-Cursos). Considere las definiciones del archivo start.rkt y escriba sus funciones en él. Escriba sus tests en el archivo test.rkt adjunto. Ambos ficheros deben ser entregados vía U-Cursos. Los tests forman parte de su evaluación! 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 (not 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 (not 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, tendremos la opción de definir funciones globales para ser usadas en los predicados. Concretamente 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-def>* 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> in <expr> <expr>) 
         | (exists <id> in <expr> <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 (no tienen equivalente directo en el AST). Su parser debe encargarse de reemplazarlas por expresiones equivalentes en el AST adjunto (sin necesidad de crear nuevos nodos, lo cual será verificado).

1. (0.7) Implemente la función (parse-expr s-expr) para parsear expresiones
2. (0.3) Implemente la función (parse-prog s-expr) para parsear programas

   > (parse-prog '((define (add1 x) (+ x 1))
                   in
                   (add1 2)))
   (program (list (fundef 'add1 'x (plus (id 'x) (num 1)))) (app 'add1 (num 2)))

Considere usar las siguientes expresiones equivalentes para reemplazar ⇒, ⇔ y xor:

• p => q es equivalente a ¬p v q
• p <=> q es equivalente a (¬p v q) ^ (¬q v p)
• p xor q es equivalente a (p v q) ^ ¬ (p ^ q)

Recuerde que durante el proceso de parsing no se valida que el programa sea (semánticamente) correcto sino sintácticamente correcto, el siguiente programa debería parsear:

> (parse-expr '(fact (+ #f 1)))
(app 'fact (plus (bool #f) (num 1)))

Note que tanto la expresión (+ #f 1) como la aplicación de la función fact son semánticamente incorrectas, pero no es responsabilidad del parser detectarlo

1. (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² + b² < (a+b)²

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.5) Defina la función (subst expr x val) que substituye en la expresión expr el valor val por la variable x (preservando el scope léxico). Ejemplos:

   > (subst (parse-expr '(if (< x 1) (% x y) (+ x y))) 'x (num 1))
   (my-if (lesser (num 1) (num 1))  (mod (num 1) (id 'y))  (plus (num 1) (id 'y)))
   > (subst (parse-expr '(with (x 5) (+ x y))) 'x (sub (num 1) (num 2)))
   (with 'x (num 5) (plus (id 'x) (id 'y)))

2. (1.0) Defina la función (eval-expr expr) que evalúa una expresión con cuantificadores sobre conjuntos acotados. Utilice la función subst en su implementación (para sustituir identificadores por su valor). 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.

   ; 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

3. (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
   > (eval-prog (parse-prog '(in (if (< 3 2) 
                                     (set (1 3 5))
                                     (set (2 4))))))
   ;Edit: (list (num 2) (num 4)) por:
   (list 2 4)

   En caso de evaluar un programa que aplique una función no definida deberá lanzar un error “function not defined”. Note que (eval-expr expr) se debe comportar como (eval-prog (program '() expr)). En caso de evaluar un programa que use una variable no definida deberá lanzar un error “unbound identifier”.

4. (0.5) Defina la función (satisfiable? 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 (not p))))
   #f
   > (satisfiable? (parse-expr '(<=> (=> p q) (or p q))))
   #t
   > (satisfiable? (parse-expr '(<=> (=> p q) (and p (not 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 '(not (or (not p) (not q)))))
(my-and (id 'p) (id 'q))
> (simplify-negations (parse-expr '(not (not (not (or p q))))))
(my-and (my-not (id 'p)) (my-not (id 'q)))
 

1. (0.5) Defina la función (simplify expr) que se encargue de remplazar las siguientes expresiones: (and #f p), (or #t p), (¬ #t), (¬ #f), (or p p) y (and p p) por versiones más simples en el 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))))
   > (simplify (parse-expr '(or (and p (and q (and #f w)))
                               (and p (and q (and #f w))))))
   (bool #f)
   ;la optimización no aplica a permutaciones
   > (simplify (parse-expr '(or (and p q)
                               (and q p))))
   (my-or (my-and (id 'p) (id 'q)) (my-and (id 'q) (id 'p)))                    

2. (0.3) Defina la función (o-satisfiable? 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?

1. (0.7) En el fichero start.rkt se brinda una implementación de type-expr que dado un Expr retorna su tipo o un error en caso de no cumplirse la validación de tipos. La función type-expr es implementada internamente con typeof donde se usa un ambiente de tipos para conocer el tipo de las variables. Su tarea consiste en extender typeof para implementar el chequeo de tipos para las expresiones set, all y exists. En caso de la expresión app no tiene que implementar su chequeo de tipo. Su extensión debería contemplar que:
   • El tipo de set es (Tset ...)

     > (type-expr (parse-expr '(set ((% 7 3) 2))))
     (TSet (TInt))
     > (type-expr (parse-expr '(set (#t (and #f #t)))))
     (TSet (TBool))
     > (type-expr (parse-expr '(set (#f 2)))); debe lanzar el error "TYPE_ERROR: same type expected"

   • Un conjunto vació no se le puede dar tipo, por tanto debe lanzar el error “TYPE_ERROR: empty set”.
   • Tanto para (all x in S body) como (exists x in S body) se debe verificar que S sea de tipo (TSet ...). En caso contrario lanzar error “TYPE_ERROR: a set was expected”. Además se debe verificar body es de tipo TBool. En caso de no cumplirse esto último se debe lanzar el error “TYPE_ERROR: TBool expression expected”. El tipo de ambas expresiones es TBool