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/23 16:39] – 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> </code>
Line 226: 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 234: Line 234:
 <code scheme> <code scheme>
 (terminate '{{deftype bool  (terminate '{{deftype bool 
-                {t : bool} +               {t : bool} 
-                {f : bool}}+               {f : bool}}
              {deftype nat               {deftype nat 
-                         {O : nat} +               {O : nat} 
-                         {S : {nat -> 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 253: Line 253:
 <code scheme> <code scheme>
 (terminate '{{deftype bool  (terminate '{{deftype bool 
-                {t : bool} +               {t : bool} 
-                {f : bool}}+               {f : bool}}
              {deftype nat               {deftype nat 
-                         {O : nat} +               {O : nat} 
-                         {S : {nat -> 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.