Menor elemento común en listas infinitas ordenadas en Haskell y en Clojure

PorJosé A. Alonso

El enunciado del problema 108 de 4Clojure es el siguiente

Given any number of sequences, each sorted from smallest to largest,find the smallest number which appears in each sequence. The sequences may be infinite, so be careful to search lazily.

A partir de dicho problema he elaborado las siguientes relaciones de ejercicios en Haskell y Clojure, intentando mantener la analogía entre sus soluciones.
Read More “Menor elemento común en listas infinitas ordenadas en Haskell y en Clojure”

El problema de la mayor subsucesión creciente en Haskell y en Clojure

PorJosé A. Alonso

A partir del problema 53 de 4Clojure, titulado Longest Increasing Sub-Seq, en el que se pide encontrar la subsucesión creciente más larga de elementos consecutivos de una sucesión dada, he elaborado dos relaciones de ejercicios. Una en Haskell, para la asignatura de Informática de 1º del Grado en Matemáticas, y la otra en Clojure, siguiendo el patrón de la anterior.
Read More “El problema de la mayor subsucesión creciente en Haskell y en Clojure”

Para contestar rapidito y casi sin pensar

PorJosé A. Alonso

El enunciado del problema de hoy de Números y algo más …, titulado Para contestar rapidito y casi sin pensar, es el siguiente

¿Cuál es último dígito de la suma de las cuartas potencias de los primeros 100 números enteros positivos?

A partir del problema he escrito la siguiente relación de ejercicios para la asignatura de Informática de 1º del Grado en Matemáticas.
Read More “Para contestar rapidito y casi sin pensar”

Lecturas del Grupo de Lógica Computacional (Julio de 2011)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional. La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

  1. Razonamiento formalizado para la enseñanza de las matemáticas. [#Vestigium, #Enseñanza]
  2. The Ideal Mathematician. [#Humor]
  3. El problema de las puertas en Haskell. [#Haskell]
  4. Metadata for a mathematical wiki: Initial experiments. [#Mizar]
  5. Logical Verification. [#Coq]
  6. Formal proofs for theoretical properties of Newton’s method. [#Coq]
  7. Formalisation de la logique de description ALC dans l’assistant de preuve Coq. [#Coq, #ALC]
  8. Vérification d’une méthode de preuve pour la logique de description ALC. [#Isabelle. #ALC]
  9. A critique of Abelson and Sussman or why calculating is better than scheming. [#Haskell, #Lisp]
  10. Experiments with computable matrices in the Coq system. [#Coq]
  11. Computing the homology of groups: the geometric way. [#Kenzo]
  12. Peut-on faire des mathématiques avec un ordinateur?. [#Matemática computacional]
  13. The Theory Behind TheoryMind. [#Isabelle]
  14. Provably correct conflict prevention bands algorithms. [#PVS]
  15. Peut-on avoir confiance en l’informatique?. [#Verificación]
  16. Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011). [#GLC, #Vestigium]
  17. Automated theorem provers a practical tool for the working mathematician. [#DAO, #Vestigium]
  18. Intellectual Freedom. [#Humor]
  19. Ciencia china ‘duplicada’ en Galicia. [#Sociología]
  20. Expresiones aritméticas mediante tipos abstracto de datos y polinomios. [#Haskell, #Vestigium]
  21. A verified runtime for a verified theorem prover. [#ACL2]
  22. A Framework for Automated and Certified Refinement Steps. [#Isabelle]
  23. Descomposiciones en sumas de cuadrados en Haskell. [#Haskell, #Vestigium]
  24. Interactive Proof Introduction to IsabelleHOL. [#Isabelle]
  25. Coq au vin (The Coq proof assistant and the Curry-Howard correspondence) [#Coq]
  26. Hardware languages and proof. [#Tesis, #PVS, #SAL]