Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
teaching:cc4101:tareas:2015-1:tarea3 [2015/05/20 15:37] – gsototeaching:cc4101:tareas:2015-1:tarea3 [2015/07/24 14:17] (current) – gsoto
Line 18: Line 18:
 </code> </code>
  
-Cada constructor genera estructuras del tipo ''nat'' al ser aplicadas. 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. Dos tipos de constructores son posibles, con o sin argumentos. En el ejemplo ''O'' corresponde a un constructor que no requiere parámetros y construye un elemento de tipo ''nat''. El constructor ''S'' usa un elemento de tipo ''nat'' para construir otro elemento de tipo ''nat''. El tipo ''expr'' posee un único constructor ''add'' que usa dos ''nat'' para construir un elemento.+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. Dos tipos de constructores son posibles, con o sin argumentos. En el ejemplo ''O'' corresponde a un constructor que no requiere parámetros y construye un elemento de tipo ''nat'' (''{O : nat}'' es un azucar sintáctico para una función con tipo ''() -> nat''). El constructor ''S'' 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.
  
 <code scheme> <code scheme>
Line 55: Line 55:
                 {match b                 {match b
                  {{case {t} => {f}}}}}                  {{case {t} => {f}}}}}
-       {even {f}})+       {not {f}})
    "match error")    "match error")
 +</code>
 +
 +De todas formas un identificador puede servir para hacer match de los casos restantes:
 +
 +<code scheme>
 +(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"         
 </code> </code>
  
Line 76: Line 99:
                  {{case {O} => b}                  {{case {O} => b}
                   {case {S n1} => {even n1 {not b}}}}}}                   {case {S n1} => {even n1 {not b}}}}}}
-       {even {S {S {S {O}}}}} {t}})+       {even {S {S {S {O}}}} {t}}})
 > "(f) : bool" > "(f) : bool"
 +</code>
 +
 +Las funciones se representan por el simbolo lambda:
 +<code scheme>
 +(run '{{deftype bool 
 +          {t : bool}
 +          {f : bool}}
 +       {fun {x : bool} x})
 +> "λ"
 </code> </code>
  
Line 83: Line 115:
  
 <code scheme> <code scheme>
-<prog> ::= {{<def>}* <expr>}+<prog> ::= {<def>* <expr>}
  
 <def> ::= {deftype <id> {<id> : <type>}+} <def> ::= {deftype <id> {<id> : <type>}+}
Line 94: Line 126:
          | {fun {<id> : <type>}+ <expr>}          | {fun {<id> : <type>}+ <expr>}
          | {match <expr> {<case>+}}          | {match <expr> {<case>+}}
-         | {<expr> <expr>+}+         | {<expr> <expr>*}
  
 <case> ::= {case <pattern> => <expr>} <case> ::= {case <pattern> => <expr>}
Line 118: Line 150:
   - ''(error "TYPE ERROR: wrong argument type")'' : En caso de que algún argumento no tenga el tipo esperado para el tipo de entrada de la función en una aplicación.   - ''(error "TYPE ERROR: wrong argument type")'' : En caso de que algún argumento no tenga el tipo esperado para el tipo de entrada de la función en una aplicación.
   - ''(error "TYPE ERROR: application of a non-function")'' : Cuando se intente aplicar un valor que no es función.   - ''(error "TYPE ERROR: application of a non-function")'' : Cuando se intente aplicar un valor que no es función.
-  - ''(error "TYPE ERROR: incorrect pattern")'': En caso de que los patrones de un match no estén bien compuestos.  
   - ''(error "TYPE ERROR: non-uniform pattern")'': En caso de que los patrones de un match no sean del mismo tipo.   - ''(error "TYPE ERROR: non-uniform pattern")'': En caso de que los patrones de un match no sean del mismo tipo.
   - ''(error "TYPE ERROR: non-uniform match return type")'': Si los tipos de retorno de match no son del mismo tipo.   - ''(error "TYPE ERROR: non-uniform match return type")'': Si los tipos de retorno de match no son del mismo tipo.
Line 124: Line 155:
   - ''(error "TYPE ERROR: wrong return type")'': Si en una definición 'def' el tipo de retorno es distinto al tipo declarado.   - ''(error "TYPE ERROR: wrong return type")'': Si en una definición 'def' el tipo de retorno es distinto al tipo declarado.
   - ''(error "TYPE ERROR: redefinition")'': Si existen dos ''deftype'', constructores o ''def'' con el mismo nombre.   - ''(error "TYPE ERROR: redefinition")'': Si existen dos ''deftype'', constructores o ''def'' con el mismo nombre.
 +  - ''(error "TYPE ERROR: incorrect constructor type")'': Si el tipo de salida de un constructor no corresponde al tipo que define su ''deftype''.
  
 Nuevamente, el output de la función es un ''String''. Ejemplos: Nuevamente, el output de la función es un ''String''. Ejemplos:
Line 134: Line 166:
 > "nat" > "nat"
 </code> </code>
-Los constructores tienen tipos. La ausencia de argumentos se representa por ''()'' como sigue:+Los constructores tienen tipos de función con ''->''. La ausencia de argumentos se representa por ''()'' como sigue:
 <code scheme> <code scheme>
 (typeof '{{deftype nat  (typeof '{{deftype nat 
Line 141: Line 173:
                   O})                   O})
 "() -> nat" "() -> nat"
-</code> 
-El tipo de función va con ''->'' 
-<code scheme> 
-(typeof '{{deftype nat 
-                    {O : nat} 
-                    {S : {nat -> nat}}} 
-                  S}) 
-> "nat -> nat" 
 </code> </code>
 <code scheme> <code scheme>
Line 158: Line 182:
                          {S : {nat -> nat}}}                          {S : {nat -> nat}}}
                       {S {t}}})                       {S {t}}})
-          "TYPE ERROR: incorrect pattern")+          "TYPE ERROR: wrong argument type")
 </code> </code>
  
Line 202: Line 226:
   - Si la función no es recursiva, termina   - Si la función no es recursiva, termina
   - 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.    - 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. 
-  - Se considera como argumento disminuido estructuralmente a un identificador extraído de un match.+  - 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.
   - Considere que para cualquier argumento de una llamada recursiva, si no es un identificador proveniente de un match, no puede saber si disminuye estructuralmente.   - Considere que para cualquier argumento de una llamada recursiva, si no es un identificador proveniente de un match, no puede saber si disminuye estructuralmente.
  
Line 209: Line 233:
  
 <code scheme> <code scheme>
-(terminate '{{deftype nat  +(terminate '{{deftype bool  
-                         {O : nat} +               {t : bool} 
-                         {S : {nat -> nat}}}+               {f : bool}} 
 +             {deftype nat  
 +               {O : nat} 
 +               {S : {nat -> nat}}}
              {def weird {n1 : nat} {n2 : nat} : bool               {def weird {n1 : nat} {n2 : nat} : bool 
-                         {match n +               {match n2 
-                           {{case {O} => {t}} +                 {{case {O} => {t}} 
-                            {case {S n3} => {match n1 +                  {case {S n3} => {match n1 
-                                              {{case {O} =>    {weird n3 {S n1}}} +                                    {{case {O} =>    {weird n3 {S n1}}} 
-                                               {case {S n4} => {weird n4 n2}}}}}}}} +                                     {case {S n4} => {weird n4 n2}}}}}}}} 
-             {O})+             {O}})
 > "terminate"              > "terminate"             
 </code> </code>
Line 225: Line 252:
  
 <code scheme> <code scheme>
-(terminate '{{deftype nat  +(terminate '{{deftype bool  
-                         {O : nat} +               {t : bool} 
-                         {S : {nat -> nat}}}+               {f : bool}} 
 +             {deftype nat  
 +               {O : nat} 
 +               {S : {nat -> nat}}}
              {def weird {n1 : nat} {n2 : nat} : bool               {def weird {n1 : nat} {n2 : nat} : bool 
-                         {match n +               {match n2 
-                           {{case {O} => {t}} +                 {{case {O} => {t}} 
-                            {case {S n3} => {match n1 +                  {case {S n3} => {match n1 
-                                              {{case {O} =>    {weird n3 {S n1}}} +                                    {{case {O} =>    {weird n3 {S n1}}} 
-                                               {case {S n4} => {weird {S n4} n2}}}}}}}} +                                     {case {S n4} => {weird {S n4} n2}}}}}}}} 
-             {O})+             {O}})
 > "cannot detect structural recursion"              > "cannot detect structural recursion"             
 </code> </code>
  
-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}}'' disminuye en el segundo. Por lo tanto no se puede deducir si la función es estructuralmente recursiva.+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.