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/06/08 14:00] – gsototeaching:cc4101:tareas:2015-1:tarea3 [2015/07/24 14:17] (current) – gsoto
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 103: 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 127: 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 204: 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 211: 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 227: 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.