Lenguajes de Programación II
Tarea 2: ISWIM
Esta tarea tiene 3 partes. Las partes 2 y 3 dependen de la parte 1, pero son independientes entre sí.
1 Basic ISWIM (2pts)
Defina en PLT Redex el language ISWIM, con las siguientes simplificaciones/instanciaciones:
tipos primitivos booleanos y números
soporte para primitivas unarias (add1 sub1 zero? not) y binarias (+ - * / < and or)
condicional if
Tal como visto en clases, defina el significado de las primitivas con una metafunción δ.
(define-metafunction ISWIM [(subst (λ X_1 any_1) X_1 any_2) (λ X_1 any_1)] [(subst (λ X_1 any_1) X_2 any_2) (λ X_3 (subst (subst-var any_1 X_1 X_3) X_2 any_2)) (where X_3 ,(variable-not-in (term (X_2 any_1 any_2)) (term X_1)))] [(subst X_1 X_1 any_1) any_1] [(subst (any_2 ...) X_1 any_1) ((subst any_2 X_1 any_1) ...)] [(subst any_2 X_1 any_1) any_2]) (define-metafunction ISWIM [(subst-var (any_1 ...) variable_1 variable_2) ((subst-var any_1 variable_1 variable_2) ...)] [(subst-var variable_1 variable_1 variable_2) variable_2] [(subst-var any_1 variable_1 variable_2) any_1])
Entregue una batería de tests que validen la definición de su lenguaje
Formule y random-testee (usando redex-check) la propiedad esperada de -->: es una reducción determinista a cada paso.
2 Control ISWIM (2pts)
Estudie las secciones 19.1 hasta 19.3 del PLAI para asegurarse que entiende bien como funcionan las continuaciones. Es altamente recomendado que experimenten con call/cc y let/cc en Racket. De la explicación del PLAI, asegurese de asimilar bien la necesidad de las escaper procedures, λ↑, que se usan para las continuaciones.
Antes de programar, trate de escribir en papel las reglas de evaluación (en contexto) para call/cc (o let/cc) y aplicación de continuaciones (λ↑).
Testee al menos los ejemplos que están en el PLAI 19.1-19.3
3 Equivalencia Comportamental (2pts)
La equivalencia comportamental entre dos términos implica una cuantificación universal sobre los contextos en los cuales los términos pueden ser insertos (Section 4.7 del SEwPR). Si bien Redex no nos puede ayudar en demostrar que dos terminos son equivalentes, podemos usar el soporte para testing aleatorio de predicados para ver si Redex es capaz de encontrar un contexto que permite discriminar dos términos o no.
En esta pregunta, no se preocupe de términos cuya evaluación núnca termina.
Defina la función (eval t) que dado un termino t, lo reduce usando la relación de reducción estándar, y luego retorna su valor si es un número o un booleano, retorna 'function si es una función, o 'stuck si es un término pegado.
Defina la función (eval-same? t1 t2 c) que determina si los terminos t1 y t2 evaluan al mismo resultado cuando pluggeado en el contexto c.
Defina la función (check-equiv t1 t2) que hace randomized testing de la equivalencia de t1 y t2, usando redex-check para generar contextos aleatorios.
Provea ejemplos documentados que ilustren el uso de check-equiv.