I1M2010: Expresiones lambdas y secciones en Haskell

Los objetivos de la clase de hoy de Informática de 1º del Grado en Matemáticas han sido los siguientes:

  • aprender la notación lambda para representar funciones,
  • aprender a definir funciones en Haskell mediante expresiones lambda,
  • aprender a definir funciones parcializadas,
  • aprender la utilidad de las expresiones lambdas,
  • aprender a evaluar secciones,
  • aprender a definir las secciones mediante expresiones lambda,
  • aprender a evaluar expresiones con secciones y
  • aprender la utilidad de las secciones.

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

Las transparencias usadas en la clase son las comprendidas entre las páginas 21 y 30 del tema 4
Read More “I1M2010: Expresiones lambdas y secciones en Haskell”

RA2010: Ejercicios de razonamiento proposicional con Isabelle

La clase de hoy del curso de Razonamiento automático ha consistido en la formalización en Isabelle/Isar de demostraciones por deducción natural en lógica proposicional. Para ello se han formalizado todas las demostraciones del tema de deducción natural proposicional del curso de Lógica informática

Las formalizaciones realizadas en clase se encuentran en el siguiente documento
Read More “RA2010: Ejercicios de razonamiento proposicional con Isabelle”

Open project position at TUM: Computer-supported verification of automata constructions

El grupo Foundations of Software Reliability and Theoretical Computer Science de la Universidad Politécnica de Munich ha anunciado la oferta de una plaza de trabajo en Lógica Computacional: Open project position at TUM: Computer-supported verification of automata constructions

El objetivo del trabajo es la realización de una biblioteca formalmente verificada con Isabelle de algoritmos de verificación de modelos (en inglés, model checking). El proyecto se enfoca en la aproximación a la verificación de modelos basada en automata. Por tanto, para su realización se será necesario formalizar en Isabelle los conceptos habituales de la teoría de automata.

Los directores del proyecto son Javier Esparza, Tobias Nipkow y Jan-Georg Smaus.

I1M2010: Segundo examen de la evaluación continua

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

Las notas se han publicado en la WebCT.

En la página de la asignatura se han publicado las soluciones del examen.

El resumen estadístico del resultado del examen es el siguiente

No presentados 12
Suspensos 5 25%
Aprobados 3 15%
Notables 6 30%
Sobresalientes 6 30%
Total 32

El porcentaje de aprobados (sobre presentados) es 75.0 y la nota media es 7.1.

Desarrollo del comando wc de Unix en Haskell

wc (en referencia a los términos ingleses “word count”) es un comando utilizado en el sistema operativo Unix que se utiliza para saber el número de palabras, líneas y caracteres de un fichero. Por ejemplo, si tenemos un fichero ciudades.txt cuyo contenido es

podemos contar con wc sus líneas, palabras y caracteres como sigue

En Haskell se pueden desarrollar programas simples con análogo comportamiento. Por ejemplo se puede contar las líneas del fichero como sigue

El contenido del programa CuentaLineas.hs es simplemente

Read More “Desarrollo del comando wc de Unix en Haskell”