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 00:54] – [P3 - Análisis de Terminación (2.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 176: Line 164:
  
  
-===== P3 - Análisis de Terminación (3.0pt) =====+===== P2 - Análisis de Terminación (3.0pt) =====
  
 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: 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:
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>