I1M2010: Definiciones por recursión sobre números naturales y listas

PorJosé A. Alonso

Los objetivos de la clase de hoy son:

  • Aprender a desarrollar aplicaciones usando listas de comprensión. Para ello, se ha desarrollado un programa para descifrar mensajes que usen el cifrado de César.
  • Aprender a definir funciones por recursión sobre los números naturales.
  • Aprender a definir funciones por recursión sobre listas.
  • Aprender a definir funciones por recursión sobre listas que necesiten guardas en el caso recursivo.

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

Las transparencias usadas en la clase son las comprendidas entre las páginas 27 y 34 del tema 5 y las 12 primeras del tema 6

Descargar (PDF, 231KB)

I1M2010: Definiciones por comprensión

PorJosé A. Alonso

El objetivo de la clase de hoy es continuar aprendiendo a definir funciones en Haskell usando listas de comprensión. En concreto, se ha visto cómo usar las definiciones por comprensión con las funciones de emparejamiento (zip) y con las cadenas y se ha comenzado como caso de estudio la codificación de César.

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

Las transparencias usadas en la clase son las comprendidas entre las páginas 12 y 27 del tema 5

Descargar (PDF, 287KB)

Lectura e introspección

PorJosé A. Alonso

Leyendo el libro de Marvin Minsky ‘La máquina de las emociones (Sentido común, inteligencia artificial y el futuro de la mente humana)” me he encontrado en la página 19 con la siguiente cita de Marcel Proust

Todo lector lee únicamente lo que ya tiene dentro de sí mismo. Un libro no es más que una especie de instrumento óptico que el autor ofrece para dejar que el lector pueda descubrir en sí mismo lo que nunca habría encontrado sin ayuda del libro.

Con esta cita comienzo una nueva sección de Vestigium en la que iré recopilando citas de mis lecturas.

RA2010: Visión panorámica del razonamiento automático

PorJosé A. Alonso

Hoy ha comenzado el curso de Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla.

En la clase de hoy se ha presentado la asignatura y se ha comentado una visión panorámica del razonamiento automático a través de ejemplos con los sistemas de razonamiento Otter/Mace, ACL2, PVS e Isabelle/HOL.
Read More “RA2010: Visión panorámica del razonamiento automático”

Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude

PorJosé A. Alonso

EL 29 de Octubre se publicó un nuevo artículo de vrificación: Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude, Science of Computer Programming en la revista Science of Computer Programming.

Los autores del artículo son Kyungmin Bae (de la University de Illinois en Urbana-Champaign), Peter Csaba Olveczky (de la Universidad de Oslo), Thomas Huining Feng, Edward A. Lee y Stavros Tripakis (los tres últimos, de la Universidad de California en Berkeley).

El resumen del artículo es

This paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies.

Una versión previa del artículo, de libre acceso, es Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude.