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:2016-2:tarea2 [2016/11/02 11:51] – [P3 - Análisis de Terminación (3.0pt)] fmossoteaching:cc4101:tareas:2016-2:tarea2 [2016/11/21 11:21] (current) – [P2 - Análisis de Terminación (3.0pt)] fmosso
Line 122: Line 122:
 Funciones definidas con ''def'' pueden ser recursivas y tener más de un argumento. Funciones definidas con ''def'' pueden ser recursivas y tener más de un argumento.
  
-<code scheme> 
-(run '{{deftype nat 
-          {O : nat} 
-          {S : {nat -> nat}}} 
-       {def byZero {n : nat} : nat 
-               {match n 
-                 {{case {O} => {O}} 
-                  {case {S {O}} => {byZero {O}}} 
-                  {case {S {S {O}}} => {byZero {S {O}}}}}}} 
-       {byZero {S {S {O}}}}}) 
->"(O) : nat" 
-</code> 
  
 <code scheme> <code scheme>
Line 235: Line 223:
                   {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 n3}}}}}}}}
              {O}})              {O}})
 > "terminate"              > "terminate"             
 </code> </code>
  
-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 n2}'' disminuye en ambos argumentos. Por lo tanto la función reduce en el primer argumento.+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.
  
 <code scheme> <code scheme>