Lenguajes de Programación II
Tarea 2:   ISWIM
1 Basic ISWIM (2pts)
2 Control ISWIM (2pts)
3 Equivalencia Comportamental (2pts)

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:

Tal como visto en clases, defina el significado de las primitivas con una metafunción δ.

Recuerde que la parte derecha de una cláusula en una metafunción es automáticamente "quotada", por lo que si quiere apelar a las primitivas de Racket tiene que escapar con "unquote" (,). Y use term para volver a quotear. Por ejemplo:

[(δ (add1 b)) ,(add1 (term b))]

Como metafunción de substitución, use la siguiente definició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])
Esta definición hace uso del comodín any que matchea cualquier sub-término. Esto permite una definición compacta que no se ve afectada por la introducción de nuevas formas al lenguaje (siempre y cuando no sean formas de binding!).

No olvide incluir la definición de los contextos de evaluación E, y uselos para definir la relación de reducción estándar -->. Para facilitar la definición, no trate de definir --> en base a la noción de reducción v, sino que defina directamente las reglas de reducción en contexto:
(define iswim-red
  (reduction-relation
   ISWIM
   (--> (in-hole E ((λ X M) V))
        (in-hole E ...)
        βv)
   ...))

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.

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.