El tipo abstracto de datos de las colas en Haskell

PorJosé A. Alonso

En este artículo continúo la serie dedicada a los tipos de datos abstractos (TAD) en Haskell presentando el TAD de las colas.

Al igual que hice en los anteriores TAD, usaré módulos, funciones de escritura y QuickCheck para conseguir la abstracción, independencia y certificación de los resultados de las implementaciones.

Una cola es una estructura de datos, caracterizada por ser una secuencia de elementos en la que la operación de inserción se realiza por un extremo (el posterior o final) y la operación de extracción por el otro (el anterior o frente). Las colas también se llaman estructuras FIFO (del inglés First In First Out), debido a que el primer elemento en entrar será también el primero en salir. Este comportamiento es análogo a las colas del cine.

El contenido del resto del artículo es el siguiente:

  • la signatura del TAD de las colas;
  • las propiedades del TAD de las colas;
  • la implementación, en Haskell, de las colas mediante listas;
  • la implementación, en Haskell, de las colas mediante pares de listas y
  • la comprobación con QuickCheck de sus propiedades.

Read More “El tipo abstracto de datos de las colas en Haskell”

RA2010: Funciones recursivas generales en Isabelle

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir funciones recursivas generales en Isabelle y cómo demostrar por inducción propiedades sobre las mismas. En concreto, se ha estudiado:

  • cómo definir funciones recursivas que no son primitivas recursivas (por ejemplo, la función de Ackermann) usando fun,
  • cómo obtener el esquema de inducción correpondiente a las definiciones anteriores,
  • cómo demostrar propiedades de las funciones antereiores con el esquema de inducción correspondiente,
  • cómo definir tipos de datos recursivos cruzados,
  • cómo obtener el esquema de inducción correpondiente a las definiciones anteriores,
  • cómo definr funciones con recursión cruzada,
  • cómo demostrar propiedades por inducción cruzada.

En la clase se ha presentado el tema 5 (desde la página 43 a la 47).

El código correspondiente se encuentra en Cap_5.thy .

I1M2010: Un calculador de tautologías en Haskell como caso de estudio de tipos de datos definidos

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado una aplicación de la definición de tipos. Concretamente, se ha estudiado cómo definir el tipo de las fórmulas proposicionales y, trabajando con dicho tipo, construir un programa para determinar si una fórmula es una tautología.

Las transparencias usadas en la clase son las del tema 9 (páginas 25-33):
Read More “I1M2010: Un calculador de tautologías en Haskell como caso de estudio de tipos de datos definidos”

I1M2010: Definiciones de tipos de datos en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la definición de nuevos tipos de datos y de funciones sobre dichos tipos. Concretamente, se ha estudiado

  • cómo definir tipos usando type,
  • cómo definir funciones con dominio o rango en tipos definidos usando type,
  • cómo definir tipos usando data,
  • cómo definir funciones con dominio o rango en tipos definidos usando data y
  • cómo definir tipos de datos recursivos (p.e. naturales, listas y árboles).

Las transparencias usadas en la clase son las del tema 9 (páginas 1-24):
Read More “I1M2010: Definiciones de tipos de datos en Haskell”