Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
teaching:cc4101:tareas:2016-2:tarea2 [2016/11/02 00:46] – [Tarea 2] fmosso | teaching:cc4101:tareas:2016-2:tarea2 [2016/11/02 00:48] – [Recursión] fmosso | ||
---|---|---|---|
Line 121: | Line 121: | ||
Funciones definidas con '' | Funciones definidas con '' | ||
+ | |||
+ | |||
<code scheme> | <code scheme> | ||
Line 162: | Line 164: | ||
- | ===== P2 - Sistema de Tipos (2.0pt) ===== | ||
- | |||
- | Para esta parte, se le solicita crear un sistema de tipos para el lenguaje definido en la primera parte. Los tipos del lenguaje corresponden a los tipos definidos con '' | ||
- | |||
- | Las definiciones de funciones llevan anotado el tipo de retorno, pues es necesario para verificar la correctitud de funciones recursivas. | ||
- | |||
- | Defina un sistema de tipos con la función **'' | ||
- | |||
- | - '' | ||
- | - '' | ||
- | - '' | ||
- | - '' | ||
- | - '' | ||
- | - '' | ||
- | - '' | ||
- | - '' | ||
- | |||
- | Nuevamente, el output de la función es un '' | ||
- | |||
- | <code scheme> | ||
- | (typeof ' | ||
- | {O : nat} | ||
- | {S : {nat -> nat}}} | ||
- | {O}}) | ||
- | > " | ||
- | </ | ||
- | Los constructores tienen tipos de función con '' | ||
- | <code scheme> | ||
- | (typeof ' | ||
- | {O : nat} | ||
- | {S : {nat -> nat}}} | ||
- | O}) | ||
- | "() -> nat" | ||
- | </ | ||
- | <code scheme> | ||
- | (test/exn (typeof ' | ||
- | {t : bool} | ||
- | {f : bool}} | ||
- | {deftype nat | ||
- | {O : nat} | ||
- | {S : {nat -> nat}}} | ||
- | {S {t}}}) | ||
- | "TYPE ERROR: wrong argument type") | ||
- | </ | ||
===== P3 - Análisis de Terminación (2.0pt) ===== | ===== P3 - Análisis de Terminación (2.0pt) ===== |