Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
teaching:cc4101:tareas:2016-2:tarea2 [2016/10/26 18:55] – [P2 - Sistema de Tipos (2.0pt)] fmosso | teaching:cc4101:tareas:2016-2:tarea2 [2016/11/21 15:21] (current) – [P2 - Análisis de Terminación (3.0pt)] fmosso | ||
---|---|---|---|
Line 1: | Line 1: | ||
====== Tarea 2 ====== | ====== Tarea 2 ====== | ||
- | Esta tarea se distribuye con dos ficheros base.rkt y tests.rkt ({{ : | + | Esta tarea se distribuye con dos ficheros base.rkt y tests.rkt ({{ : |
Consulte las normas de entrega de tareas en http:// | Consulte las normas de entrega de tareas en http:// | ||
- | En esta tarea vamos a construir un lenguaje | + | En esta tarea se le pide construir un lenguaje |
- | ===== P1 - Estructuras Inductivas y Pattern Matching (2.0pt) ===== | + | ===== P1 - Estructuras Inductivas y Pattern Matching (3.0pt) ===== |
En esta primera parte defina un lenguaje con funciones de primera clase de múltiples argumentos, en donde los únicos otros valores son estructuras definibles por el usuario. | En esta primera parte defina un lenguaje con funciones de primera clase de múltiples argumentos, en donde los únicos otros valores son estructuras definibles por el usuario. | ||
Line 121: | Line 121: | ||
Funciones definidas con '' | Funciones definidas con '' | ||
+ | |||
<code scheme> | <code scheme> | ||
Line 148: | Line 149: | ||
{t : bool} | {t : bool} | ||
{f : bool}} | {f : bool}} | ||
- | {fun {x : bool} x}) | + | {fun {x : bool} x}}) |
> " | > " | ||
</ | </ | ||
Line 162: | Line 163: | ||
- | ===== P2 - Sistema de Tipos (2.0pt) ===== | ||
- | |||
- | Para el lenguaje de esta tarea, se solicita crear un sistema de tipos. 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) ===== | + | ===== P2 - Análisis de Terminación (3.0pt) ===== |
- | Tener un lenguaje donde los valores son estructuras inductivas permite detectar casos de recursión estructural, | + | Tener un lenguaje donde los valores son estructuras inductivas permite detectar casos de recursión estructural, |
<code scheme> | <code scheme> | ||
Line 244: | Line 201: | ||
Pues si bien un caso de '' | Pues si bien un caso de '' | ||
- | Implemente la función '' | + | Implemente la función |
- Si la función no es recursiva, termina | - Si la función no es recursiva, termina | ||
Line 252: | Line 209: | ||
- | Para la realización de está pregunta puede asumir que las verificaciones de tipo ya fueron realizadas. Por ejemplo ya no debe preocuparse de los casos donde no están definidos todos los patrones de un '' | + | Para está pregunta puede asumir que las verificaciones de tipo ya fueron realizadas. Por ejemplo ya no debe preocuparse de los casos donde no están definidos todos los patrones de un '' |
<code scheme> | <code scheme> | ||
Line 266: | 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}}) | ||
> " | > " | ||
</ | </ | ||
- | En el caso anterior existen dos llamadas recursivas a '' | + | En el caso anterior existen dos llamadas recursivas a '' |
<code scheme> | <code scheme> |