I1M2010: Patrones de definiciones por recursión en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos visto patrones recursión:

  • recursión sobre varios argumentos,
  • recursión múltiple y
  • recursión mutua.

Además, hemos visto una heurística para definir funciones por recursión.

Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 8ª relación.

Las transparencias usadas en la clase son las comprendidas entre las páginas 13 y 30 del tema 6
Read More “I1M2010: Patrones de definiciones por recursión en Haskell”

RA2010: Isabelle como un lenguaje funcional

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede en Isabelle/HOL

  • calcular con los números naturales, los números enteros y los booleanos,
  • definir funciones mediante composición, condicionales, casos e inducción,
  • demostrar propiedades mediante simplificación,
  • definir tipos de datos recursivos,
  • definir y modificar registros y
  • refutar propiedades con QuickCheck.

Read More “RA2010: Isabelle como un lenguaje funcional”

Trabajo de Lógica Computacional en Saarbrücken (Alemania)

PorJosé A. Alonso

El Grupo de automatización de la Lógica (del Instituto Max Planck en Saarbrücken, Alemania) ha publicado una oferta de plaza: PhD/Project Position.

La investigación se centrará en la integración de un sistema de razonamiento automático (SPASS) con otro interactivo (Isabelle).

El trabajo será dirigido por Christoph Weidenbach y se desarrollará en cooperación con el Grupo de demostración automática de la Universidad de Munich que dirige Tobias Nipkow.

I1M2010: Resolución de problemas mediante listas de comprensión en Haskell

PorJosé A. Alonso

El objetivo de la clase de hoy es aprender, resolviendo ejercicios, a definir funciones en Haskell usando las listas de comprensión introducidas en el tema 5.

En concreto, se han comentado la solución de los ejercicios 5, 6, 7 y 8 de la 5ª relación y los ejercicios 4.2, 4.3, 5.1 y 5.2 de la 6ª relación

Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 7ª relación y de la de la 8ª relación.