I1M2012: Ejercicios con tipos de datos algebraicos en Haskell

En las clases de ayer y hoy de Informática de 1º del Grado en Matemáticas hemos comentando soluciones de los ejercicios sobre tipos de datos algebraicos en Haskell de la relaciones 18 y 19.

En la relación 18 se consideran abreviaturas y dos tipos de datos
algebraicos: los números naturales (para los que se define su
producto) y los árboles binarios, para los que se definen funciones
para calcular:

  • los puntos más cercanos,
  • la ocurrencia de un elemento en el árbol,
  • el número de hojas,
  • el carácter balanceado de un árbol y
  • el árbol balanceado correspondiente a una lista.

En la relación 19 se plantean ejercicios sobre árboles binarios. En
concreto, se definen funciones para calcular:

  • el número de hojas de un árbol,
  • el número de nodos de un árbol,
  • la profundidad de un árbol,
  • el recorrido preorden de un árbol,
  • el recorrido postorden de un árbol,
  • el recorrido preorden de forma iterativa,
  • la imagen especular de un árbol,
  • el subárbol de profundidad dada,
  • el árbol infinito generado con un elemento y
  • el árbol de profundidad dada cuyos nodos son iguales a un elemento.

Los ejercicios, y sus soluciones, se muestran a continuación. Los de la relación 18 son
Read More “I1M2012: Ejercicios con tipos de datos algebraicos en Haskell”

RA2012: Deducción natural en lógica proposicional con Isabelle/HOL (1)

En la clase de hoy del curso de Razonamiento automático se ha presentado la deducción natural en lógica proposicional con Isabelle/HOL. La presentación se basa en los ejemplos de tema 2 del curso LI (Lógica informática), que a su vez se basa en el libro de de Huth y Ryan Logic in Computer Science. La página al lado de cada ejemplo indica la página de las transparencias de LI donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de la transparencia, las siguientes van eliminando detalles de la prueba hasta la última que es automática.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Deducción natural en lógica proposicional con Isabelle/HOL (1)”

RA2012: Introducción a la demostración asistida con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha presentado:

El ejemplo que se ha visto para introducir los elementos del lenguaje de demostración es el siguiente
Read More “RA2012: Introducción a la demostración asistida con Isabelle/HOL”

I1M2012: Ejercicios de evaluación perezosa y listas infinitas (3)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando soluciones de los sguientes ejercicios de la relación 17 (sobre evaluación perezosa y listas infinitas):

  • 8. Menor número triangular con más de n divisores.
  • 9. Números primos consecutivos con dígitos con igual media.
  • 10. Decisión de pertenencia al rango de una función creciente
  • 11. Pares ordenados por posición.
  • 12. Aplicación iterada de una función.
  • 13. La bicicleta de Turing.
  • 14. La sucesión de Golomb.

Los ejercicios, y sus soluciones, se muestran a continuación
Read More “I1M2012: Ejercicios de evaluación perezosa y listas infinitas (3)”

I1M2012: Ejercicios de evaluación perezosa y listas infinitas (2)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando soluciones de ejercicios sobre evaluación perezosa y listas infinitas de las relación 17.

En los comentarios se ha resaltado

  • en los ejercicios 2 y 3:
    • la importancia del orden de las condiciones en las definiciones de listas por comprensión,
    • la eficiencia del cálculo sobre la búsqueda.
  • en el ejecicio 6.2 el uso de iterate y
  • en la definición de los números triangulares el uso de scanl.

Los ejercicios, y sus soluciones, se muestran a continuación
Read More “I1M2012: Ejercicios de evaluación perezosa y listas infinitas (2)”