I1M2013: Ejercicios de cálculo numérico en Haskell

En la primer parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la 20ª relación, en la que se definen funciones para resolver los siguientes problemas de cálculo numérico:

  • diferenciación numérica,
  • cálculo de la raíz cuadrada mediante el método de Herón,
  • cálculo de los ceros de una función por el método de Newton y
  • cálculo de funciones inversas.

Un aspecto a destacar desde el punto de vista de la programación es el uso de la abstracción de procedimientos.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2013: Ejercicios de cálculo numérico en Haskell”

I1M2013: Ejercicios con tipos de datos algebraicos en Haskell

En las clases de ayer y hoy de Informática de 1º del Grado en Matemáticas hemos comentando soluciones de los ejercicios sobre tipos de datos algebraicos en Haskell de la relaciones 18 y 19.

En la relación 18 se consideran abreviaturas y dos tipos de datos algebraicos: los números naturales (para los que se define su producto) y los árboles binarios, para los que se definen funciones para calcular:

  • los puntos más cercanos,
  • la ocurrencia de un elemento en el árbol,
  • el número de hojas,
  • el carácter balanceado de un árbol y
  • el árbol balanceado correspondiente a una lista.

En la relación 19 se plantean ejercicios sobre árboles binarios. En concreto, se definen funciones para calcular:

  • el número de hojas de un árbol,
  • el número de nodos de un árbol,
  • la profundidad de un árbol,
  • el recorrido preorden de un árbol,
  • el recorrido postorden de un árbol,
  • el recorrido preorden de forma iterativa,

Los ejercicios, y sus soluciones, se muestran a continuación. Los de la relación 18 son
Read More “I1M2013: Ejercicios con tipos de datos algebraicos en Haskell”

Coinitial semantics for redecoration of triangular matrices

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Coinitial semantics for redecoration of triangular matrices.

Sus autores son Benedikt Ahrens y Régis Spadotti (del IRIT, Université Paul Sabatier).

Su resumen es

Infinite triangular matrices and, in particular, the redecoration operation on them, were studied by Matthes and Picard. In their work, redecoration is characterized as the cobind operation of what the authors call a “weak constructive comonad”.

In this work, we identify weak constructive comonads as an instance of the more general notion of relative comonad. Afterwards, building upon the work by Matthes and Picard, we give a category-theoretic characterisation of infinite triangular matrices—equiped with the canonical bisimulation relation and a compatible comonadic cobind operation—as the terminal object in some category.

El código de las correspondientes teorías en Coq se encuentra aquí.