I1M2012: El TAD de los polinomios en Haskell (1)

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de los polinomios y su implementación en Haskell.

Comenzamos la clase analizando las posibles representaciones de los polinomios y, como consecuencia, establecer la signatura y las propiedades del TAD de los polinomios.

A continuación, estudiamos tres prosibles representaciones del TAD de los polinomios: mediante tipos algebraicos, mediantes listas dispersas y mediante listas densas.

Finalmente, estudiamos la implementación de los polinomios como tipo algebraico y mediantes listas dispersas.

Las transparencias usadas en la clase son las páginas 1-29 del tema 21
Read More “I1M2012: El TAD de los polinomios en Haskell (1)”

I1M2012: Comentario del 4º examen de la evaluacion continua

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha comentado el 4º examen de la evaluación continua.

Se ha resaltado los puntos de mayor dificultad:

  • Cómo buscar el plan a través de ejemplos (p.e. en el ejercicio 1 la clave estaba en la suma de los elementos del par),
  • Cómo trabajar con generadores ifinitos: si el primer generador es infinito, buscar cómo acotar el segundo,
  • Cómo definir funciones sobre tipos de datos recursivos: una ecuación por cada generador.
  • Cómo trabajar con listas de listas (p.e. en el ejercicio 4).

A continuación se muestra el examen junto con su solución:
Read More “I1M2012: Comentario del 4º examen de la evaluacion continua”

Reseña: Formalization of the complex number theory in HOL4

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre números complejos titulado Formalization of the complex number theory in HOL4.

Sus autores son Zhiping Shi, Liming Li, Yong Guan, Xiaoyu Song, Minhua Wu y Jie Zhang.

Su resumen es

In this paper, the theory of complex numbers is formalized and the theorem library of complex numbers is embedded in HOL4, the theorem prover of High Order Logics. The theorem library introduces a data type ℂ by an ℝ × ℝ type abbreviation, and defines arithmetic operations of complex numbers in terms of group and field theories. Moreover, the polar and exponential forms are provided for simplifying the applications in control theory and signal analysis. We define the scalar multiplication of complex numbers and prove some properties about ℝ-module of complex numbers. The theorem library extends the scope of application of HOL4. The developed complex number theory has been released in HOL4 Kananaskis-7.

Reseña: Programming and reasonning with PowerLists in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre programas paralelos titulado Programming and reasonning with PowerLists in Coq.

Sus autores son

Su resumen es

For parallel programs correctness by construction is an essential feature since debugging is almost impossible. To build correct programs by constructions is not a simple task, and usually the methodologies used for this purpose are rather theoretical based on a pen-and-paper style. A better approach could be based on tools and theories that allow a user to develop an efficient parallel application by implementing easily simple programs satisfying conditions, ideally automatically, proved. PowerLists theory and the variants represent a good theoretical base for an approach like this, and Coq proof assistant is a tool that could be used for automatic proofs. The goal of this paper is to model the PowerList theory in Coq, and to use this modelling to program and reason on parallel programs in Coq. This represents the first step in building a framework that ease the development of correct and verifiable parallel programs.

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

LMF2013: Ejercicios de deducción natural en lógica proposicional con Isabelle/HOL (2)

PorJosé A. Alonso

En las clases del miércoles y de hoy del curso Lógica matemática y fundamentos se ha continuado comentando soluciones de los ejercicios de deducción natural en lógica proposicional con Isabelle/HOL de la relación 3.

También se han comentado ejercicios de la relación 4 (de argumentación proposicional con Isabelle/HOL) y de la relación 5 (de eliminación de conectivas).

Se ha propuesto la solución de los ejercicios de la relación 6 (sobre formalización de argumentos en lógica de primer orden).

Finalmente, se ha propuesto como tarea el enviar por correo la solución mediante deducción natural de 3 ejercicios elegidos entre los propuestos en los exámenes de los temas 2, 3 y 5 del libro de ejercicios.