I1M2016: Introducción a la programación funcional con Haskell

PorJosé A. Alonso

La segunda parte de la clase de hoy del curso de Informática (de 1º de Grado en Matemáticas) ha consistido en una introducción a la programación funcional basada en el tema 1. Se ha explicado

  • cómo definir y evaluar funciones en Haskell,
  • cómo comprobar propiedades de funciones en Haskell con QuickCheck,
  • cómo se resuelve un problema mediante programación imperativa y funcional,
  • los rasgos característicos de la progración funcional con Haskell y
  • cómo definir funciones mediante recursión y comprensión.

En la tercera parte de la clase se ha explicado el tema 2 en el que se hace una introducción a la programación con Haskell usando emacs como entorno de programación. Concretamente, se ha explicado cómo

  • usar Haskell como calculadora aritmética (con las funciones +, -, *, /, div y ^).
  • escribir guiones de Haskell en emacs.
  • cargar los guiones y evaluar expresiones con las funciones definidas.

También se han comentado las funciones sobre números, listas y booleanos en el resumen de funciones.

Finalmente, se ha mostrado el uso de Haskell y emacs (la sesión está grabada en este vídeo) y el proceso para la solución colaborativa de ejercicios (la sesión está grabada en este vídeo).

Se han propuesto como ejercicios los de la 1ª relación.

I1M2016: Introducción a la programación funcional

PorJosé A. Alonso

En primera parte de la clase de hoy del curso de Informática (de 1º de Grado en Matemáticas) se ha presentado la asignatura siguiendo el resumen del proyecto docente y los materiales en la página de la asignatura:

Se ha explicado cómo instalar los sistemas.

Se ha comentado el sistema de evaluación y se ha anunciado las fechas de los exámenes de todo el curso.

La segunda parte de la clase ha consistido en una introducción a la
programación funcional basada en el tema 0 en el que se usa CodeWorld/Haskell para mostrar cómo escribir las funciones de los programas para hacer dibujos. En concreto se han
estudiado

  • cómo programar dibujos elementales
  • cómo programar dibujos compuestos
  • cómo transformar dibujos con traslaciones, rotaciones, escalamiento y coloreado.
  • cómo programar animaciones

Reseña: Proving divide and conquer complexities in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Proving divide and conquer complexities in Isabelle/HOL

Su autor es Manuel Eberl (de la Technische Universität München, Alemania).

Su resumen es

The Akra–Bazzi method, a generalisation of the well-known Master Theorem, is a useful tool for analysing the complexity of Divide & Conquer algorithms. This work describes a formalisation of the Akra–Bazzi method (as generalised by Leighton) in the interactive theorem prover Isabelle/HOL and the derivation of a generalised version of the Master Theorem from it. We also provide some automated proof methods that facilitate the application of this Master Theorem and allow mostly automatic verification of Θ-bounds for these Divide & Conquer recurrences. To our knowledge, this is the first formalisation of theorems for the analysis of such recurrences.

La versión final del trabajo se ha publicado en el Journal of Automated Reasoning.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.