Tarea 2

Esta tarea se distribuye con dos ficheros base.rkt y tests.rkt (base tarea 2). Considere las definiciones del archivo base.rkt y escriba sus funciones en él. Escriba sus tests en el archivo tests.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 le pide construir un lenguaje capaz de definir sus propios tipos. Use el archivo base.rkt como punto de partida.

En esta primera parte defina un lenguaje con funciones de primera clase de múltiples argumentos, en donde los únicos otros valores son estructuras definibles por el usuario.

A continuación se presenta la gramática BNF del lenguaje y las especificaciones para los aspectos mas importantes del mismo.

<prog> ::= {<def>* <expr>}
 
<def> ::= {deftype <id> {<id> : <type>}+}
        | {def <id> {<id> : <type>}* : <type> <expr>}
 
<type> ::= <id>
         | {<type>+ -> <type>}
 
<expr> ::= <id>
         | {fun {<id> : <type>}+ <expr>}
         | {match <expr> {<case>+}}
         | {<expr> <expr>*}
 
<case> ::= {case <pattern> => <expr>}
 
<pattern> ::= <id>
            | {<id> <id>*}

Una definición de estructuras inductivas cuenta con una definición de tipo, y sus constructores asociados usando deftype. Para esta pregunta solo considere los tipos como anotaciones y asuma que no hay dos definiciones para tipos ni constructores con el mismo nombre (incluso para tipos distintos). En el siguiente ejemplo el programador define los números naturales a través de un tipo inductivo nat y dos constructores O y S, que simbolizan el 0 y el sucesor de un natural, respectivamente.

(run '{{deftype nat 
          {O : nat}
          {S : {nat -> nat}}}
       {O}})
> "(O) : nat"            

Cada constructor genera estructuras del tipo nat al ser aplicado. Puede representar sus estructuras como le parezca conveniente pero la función run siempre debe retornar un String con el tipo correspondiente como en los ejemplos. Existen dos tipos de constructores posibles, aquellos con y aquellos sin argumentos.

En el ejemplo O corresponde a un constructor que no requiere parámetros y construye un elemento de tipo nat, en donde {O : nat} es azúcar sintáctico para una función con tipo () → nat.

El constructor S en cambio, usa un elemento de tipo nat para construir otro elemento de tipo nat.

El tipo expr posee dos constructores num y add que usa dos expr para construir un elemento.

(run '{{deftype nat 
               {O : nat}
               {S : {nat -> nat}}}
             {deftype expr 
               {num : {nat -> expr}}
               {add : {expr expr -> expr}}}   
             {add {num {S {O}}} {num {O}}}})
> "(add (num (S (O))) (num (O))) : expr"

Asociar una función a un nombre se realiza usando def, donde las funciones tienen anotación de tipo para sus argumentos y retorno. Como ejemplo, en el caso de pred la función utiliza pattern matching para retornar su resultado, en ese caso se espera que primero se interprete el elemento sobre el cual matchear, n, para luego ir comprobando uno a uno con que patrón coincide. Si en un case el patrón incluye un identificador libre, este funciona como un binding para el cuerpo del caso (ejemplo case {S n1} ⇒ n1})

(run '{{deftype nat
          {O : nat}
          {S : {nat -> nat}}}
       {def pred {n : nat} : nat
               {match n
                 {{case {O} => {O}}
                  {case {S n1} => n1}}}}
       {pred {S {O}}}})
> "(O) : nat"            

En caso de no encontrar un case que corresponda:

(test/exn 
 (run '{{deftype bool 
          {t : bool}
          {f : bool}}
       {def not {b : bool} : bool
                {match b
                 {{case {t} => {f}}}}}
       {not {f}})
   "match error")

De todas formas un identificador puede servir para hacer match de los casos restantes:

(run '{{deftype day 
         {monday : day}
         {tuesday : day}
         {wednesday : day}
         {thursday : day}
         {friday : day}
         {saturday : day}
         {sunday : day}}
       {deftype bool
         {t : bool}
         {f : bool}}
       {def weekday {d : day} : bool
         {match d
           {{case {saturday} => {f}}
            {case {sunday} => {f}}
            {case otherday => {t}}}}}
       {weekday {monday}}})
> "(t) : bool"         

Funciones definidas con def pueden ser recursivas y tener más de un argumento.

(run '{{deftype bool 
          {t : bool}
          {f : bool}}
       {deftype nat 
          {O : nat}
          {S : {nat -> nat}}}
       {def not {b : bool} : bool
                {match b
                 {{case {t} => {f}}
                  {case {f} => {t}}}}}
       {def even {n : nat} {b : bool} : bool 
               {match n
                 {{case {O} => b}
                  {case {S n1} => {even n1 {not b}}}}}}
       {even {S {S {S {O}}}} {t}}})
> "(f) : bool"

Las funciones se representan por el simbolo lambda:

(run '{{deftype bool 
          {t : bool}
          {f : bool}}
       {fun {x : bool} x}})
> "λ"

Con esto en mente, defina lo siguiente:

1. Defina el AST para soportar programas del lenguaje. Note que un programa es una lista de definiciones seguida de una expresión. Dos tipos de definiciones son posibles deftype y def.
2. Defina la función parser :: s-expr -> Expr que parsea el lenguaje
3. Defina la función interp :: Expr x Env -> Val que evalua un programa con semántica eager.
4. Defina la función run :: s-expr -> String que toma un programa fuente y retorna la representación en String del valor resultante de la interpretación con su tipo anotado. Es recomendable definir una función auxiliar que le permita pasar de su representación de estructuras a la notación de los ejemplos con Strings.

Nota: Observe que la definición de funciones con def permite múltiples argumentos y por tanto el constructor de tipos → recibe una lista de tipos en la entrada. Puede asumir que para toda la tarea nunca se van a entregar dos argumentos con el mismo nombre.

Tener un lenguaje donde los valores son estructuras inductivas permite detectar casos de recursión estructural, lo que permite concluir sintácticamente cuando una función termina. Por ejemplo, en el siguiente caso es posible saber que la función even termina sin ejecutarla, pues sus posibles retornos son valores directos o llamados recursivos con argumentos que corresponden a sub-estructuras:

(terminate '{{deftype bool 
                {t : bool}
                {f : bool}}
             {deftype nat 
                {O : nat}
                {S : {nat -> nat}}}
             {def even {n : nat} : bool 
                    {match n
                      {{case {O} => {t}}
                       {case {S n1} => {match n1
                                         {{case {O} => {f}}
                                          {case {S n2} => {even n2}}}}}}}}
             {even {S {S {O}}}}})
> "terminate"             

No así como en el siguiente caso:

(terminate '{{deftype nat 
                {O : nat}
                {S : {nat -> nat}}}
             {def inf {n : nat} : nat 
                        {match n
                         {{case {O} => {O}}
                          {case {S n1} => {inf n}}}}}
             {inf {S {O}}}})
> "cannot detect structural recursion"

Pues si bien un caso de match corresponde a un constructor aplicado sin argumentos, el otro caso corresponde a una llamada donde el argumento no se reduce.

Implemente la función terminate :: s-expr → String que intenta decidir si un programa termina o no. La función terminate debe verificar cada def según la siguiente lógica:

1. Si la función no es recursiva, termina
2. Si la función es recursiva entonces todas las llamadas recursivas deben reducir en al menos un argumento y este debe ser el mismo en todos los casos.
3. Se considera como argumento disminuido estructuralmente a un identificador extraído de un match, siempre y cuando el argumento de match sea directamente un identificador.
4. Considere que para cualquier argumento de una llamada recursiva, si no es un identificador proveniente de un match, no puede saber si disminuye estructuralmente.

Para está pregunta puede asumir que las verificaciones de tipo ya fueron realizadas. Por ejemplo ya no debe preocuparse de los casos donde no están definidos todos los patrones de un match.

(terminate '{{deftype bool 
               {t : bool}
               {f : bool}}
             {deftype nat 
               {O : nat}
               {S : {nat -> nat}}}
             {def weird {n1 : nat} {n2 : nat} : bool 
               {match n2
                 {{case {O} => {t}}
                  {case {S n3} => {match n1
                                    {{case {O} =>    {weird n3 {S n1}}}
                                     {case {S n4} => {weird n4 n3}}}}}}}}
             {O}})
> "terminate"             

En el caso anterior existen dos llamadas recursivas a weird. La primera llamada recursiva {weird n3 {S n1}} disminuye en el primer argumento, pero no necesariamente en el segundo y la segunda llamada recursiva {weird n4 n3} disminuye en ambos argumentos. Por lo tanto la función reduce en el primer argumento.

(terminate '{{deftype bool 
               {t : bool}
               {f : bool}}
             {deftype nat 
               {O : nat}
               {S : {nat -> nat}}}
             {def weird {n1 : nat} {n2 : nat} : bool 
               {match n2
                 {{case {O} => {t}}
                  {case {S n3} => {match n1
                                    {{case {O} =>    {weird n3 {S n1}}}
                                     {case {S n4} => {weird {S n4} n2}}}}}}}}
             {O}})
> "cannot detect structural recursion"             

En el último caso, se debe detectar que la primera llamada recursiva {weird n3 {S n1}} disminuye en el primer argumento y que la segunda llamada recursiva {weird {S n4} n2}} no disminuye en ninguno. Por lo tanto no se puede deducir si la función es estructuralmente recursiva.