I1M2014: 5º examen de programación con Haskell
Hoy se ha realizado el 5º examen del curso de Informática (de 1º de Grado en Matemáticas). Los ejercicios, y sus soluciones, se muestran a continuación.
I1M2014: Estadística descriptiva en Haskell
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los ejercicios de la relación 33 sobre estadística descriptiva.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2014: Estadística descriptiva en Haskell”
I1M2014: El problema del calendario mediante búsqueda en espacio de estado
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los ejercicios de la relación 31 sobre el problema del calendario mediante búsqueda en espacio de estado.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2014: El problema del calendario mediante búsqueda en espacio de estado”
Reseña: A formal verification of the theory of parity complexes
Se ha publicado un artículo de razonamiento formalizado en Coq sobre topología algebraica titulado A formal verification of the theory of parity complexes.
Su autor es Mitchell Buckley (de la Macquarie University en Australia).
Su resumen es
We formalise, in Coq, the opening sections of Parity Complexes up to and including the all important excision of extremals algorithm. Parity complexes describe the essential combinatorial structure exhibited by simplexes, cubes and globes, that enable the construction of free ω-categories on such objects. The excision of extremals is a recursive algorithm that presents every cell in such a category as a composite of atomic cells, this is the sense in which the ω-category is free. Due to the complicated multi-dimensional nature of this work, the detail of definitions and proofs can be hard to follow and verify. Indeed, some corrections [Street1994] were required some years following the original publication. Our formalisation verifies that all cases of each result operate as stated. In particular, we indicate which portions of the theory can be proved directly from definitions, and which require more subtle and complex arguments. By identifying results that require the most complicated proofs, we are able to investigate where this theory might benefit from further study and which results need to be considered most carefully in future work.
El código de las correspondientes teorías en Coq se encuentra aquí.
Reseña: Higman’s lemma and its computational content
Se ha publicado un artículo de razonamiento formalizado en Minlog sobre combinatoria titulado Higman’s lemma and its computational content.
Sus autores son
- Helmut Schwichtenberg (de la Univ. de Munich en Alemania),
- Monika Seisenberger (de la Univ. de Swansea en el Reino Unido) y
- Franziskus Wiesnet.
Su resumen es
Higman’s Lemma is a fascinating result in infinite combinatorics, with manyfold applications in logic and computer science. It has been proven several times using different formulations and methods. The aim of this paper is to look at Higman’s Lemma from a computational and comparative point of view. We give a proof of Higman’s Lemma that uses the same combinatorial idea as Nash-Williams’ indirect proof using the so-called minimal bad sequence argument, but which is constructive. For the case of a two letter alphabet such a proof was given by Coquand. Using more flexible structures, we present a proof that works for an arbitrary well-quasiordered alphabet. We report on a formalization of this proof in the proof assistant Minlog, and discuss machine extracted terms (in an extension of Gödel’s system T) expressing its computational content.