RA2010: Patrones de demostración y heurística de generalización en Isabelle

En la clase de hoy del curso de Razonamiento automático se han presentado los patrones fundamentales de demostración en Isabelle. En concreto, se han estudiado las demostraciones por casos, con negaciones, por contradicción, con equivalencias. También se ha estudiado la heurística de generalización en las demostraciones por inducción.

Las transparencias usadas en clase son las páginas 35-39 del tema 4 y las páginas 40-43 del tema 5.

El código correspondiente se encuentra en Cap_4.thy y Cap_5.thy.

Determinación, esperanza y éxitos en la resolución de problemas

Uno de mis libros favoritos es Cómo plantear y resolver problemas de G. Pólya. Suelo releerlo periódicamente y en la lectura de hoy me ha llamado la atención el siguiente párrafo sobre la importancia de las emociones en la resolución de problemas

Sería un error el creer que la solución de un problema es un “asunto puramente intelectual”: la determinación, las emociones, juegan un papel importante. Una determinación un tanto tibia, un vago deseo de hacer lo menos posible pueden bastar a un problema de rutina que se plantea en la clase; pero, para resolver un problema científico serio, hace falta una fuerza de voluntad capaz de resistir durante años de trabajo amargos fracasos.

y sus consecuencias en la enseñanza

Cuando un alumno comete errores verdaderamente garrafales, cuando es de una lentitud exasperante, casi siempre es por las mismas razones; no tiene absolutamente ningún deseo de resolver el problema, no desea incluso comprenderlo como es debido, y por tanto, no lo comprende. Así, el profesor que desee realmente ayudar a un alumno, debe ante todo despertar su curiosidad, comunicarle el deseo de lograrlo. Debe también conceder al alumno un cierto tiempo para reflexionar, al cabo del cual quizá se decida a trabajar.

I1M2010: Tipos y clases en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado los tipos y las clases en Haskell. Los objetivos de tema son aprender

  • qué es un tipo,
  • cómo expresar que una expresión tiene un tipo determinado,
  • cómo preguntar a Haskell por el tipo de una expresión,
  • cómo determinar el tipo de una expresión,
  • cuáles son las ventajas de los tipos en programación,
  • cuáles son los tipos básicos (Bool, Char, String, Int, Integer, Float y Double),
  • cuáles son los tipos compuestos (listas, tuplas y funciones),
  • cómo usar funciones parcializadas,
  • qué es el polimorfismo y la sobrecarga de funciones y
  • cuáles son las clases básicas (Eq, Ord, Show, Read, Num, Integral y Fractional), sus métodos e instancias.

Las transparencias usadas en la clase son las del tema 3:
Read More “I1M2010: Tipos y clases en Haskell”

I1M2010: Evaluación perezosa en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la evaluación perezosa en Haskell. Se han visto la estrategias de evaluación perezosa e impaciente, se han comparado respecto de la terminación y el número de pasos necesarios en las computaciones, se ha aplicado a la computación con estructuras infinitas y se han visto casos en los que se aumenta la eficiencia con evaluación estricta.

Las transparencias usadas en la clase son las del tema 10:
Read More “I1M2010: Evaluación perezosa en Haskell”