Menu Close

Autor: José A. Alonso

I1M2018: Las librerías de vectores y matrices en Haskell

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado cómo se puede trabajar eh Haskell con vectores y matrices usando las librerías Data.Vector y Data.Matrix.

Para instalarla con Cabal hay que ejecutar las siguientes órdenes

cabal update
cabal install vector matrix

Los correspondientes manuales, con ejemplos de las funciones, se encuentran en

LMF2018: Sintaxis y semántica de la lógica proposicional

En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado la sintaxis de la lógica proposicional insistiendo en el carácter inductivo del tipo de datos de las fórmulas proposicionales, del procedimiento de definiciones por recursión sobre las fórmulas y de demostración de propiedades por inducción sobre las fórmulas.

Finalmente, se ha iniciado el estudio de la semántica de la lógica proposicional definiendo los booleanos, las interpretaciones, las funciones de verdad de las conectivas y mostrando cómo a partir de dichos conceptos se puede calcular el valor de verdad de una fórmula respecto de una interpretación.

A partir de lo anterior se han estudiado los modelos de fórmulas, la clasificación semántica de fórmulas (satisfacibles, insatisfacibles, tautologías, contradictorias y contingentes), los problemas SAT y TAUT. Finalmente, se han visto dos algoritmos para la solución de los problemas SAT y TAUT: tablas de verdad y método de Quine.

A continuación se ha estudiado la equivalencia de fórmulas.

Las transparencias de esta clase son las páginas 1-26 del tema 1.

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

RA2018: Razonamiento automático con Coq

En la clase de hoy del curso de Razonamiento automático se ha explicado cómo se puede usar Coq como alternativa a Isabelle/HOL que hemos utilizado anteriormente en el curso.

Los temas, con las correspondientes teorías de Coq, que se han explicado
son:

I1M2018: Matrices en Haskell

En la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha estudiado cómo trabajar con tablas en Haskell usando el módulo Data.Array.

En la primera parte se ha explicado El tipo predefinido de las tablas (“arrays”) se han estudiado las funciones sobre índices (range, index, inRange, rangeSize) y sobre tablas (array, (!), bounds, indices, elems, assocs, (//), listArray y accumArray). También se han estudiado ejemplos de definiciones con dichas funciones.

Los apuntes correspondientes son

En la segunda parte se han comentado las soluciones de los siguientes ejercicios de la Relación 15:

LMF2018: Presentación del curso de “Lógica matemática y fundamentos”

En la clase de hoy, se ha presentado el curso Lógica matemática y fundamentos siguiendo el plan de la asignatura. Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red:

También se ha comentado el sistema de demostración que se usará a lo largo del curso: Isabelle/HOL y su bibliografía fundamental.

Finalmente, se han comentado en las listas de teoremas enormes y de teoremas incompletos.

RA2018: Definiciones inductivas en IsabelleHOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.

La clase se ha basado en la siguiente teoría Isabelle

chapter {* Tema 11: Definiciones inductivas *}
 
theory T11_Definiciones_inductivas
imports Main
begin
 
section {* El conjunto de los números pares *}
 
text {* 
  · El conjunto de los números pares se define inductivamente como el
    menor conjunto que contiene al 0 y es cerrado por la operación (+2).
 
  · El conjunto de los números pares también puede definirse como los 
    naturales divisible por 2.
 
  · Veremos cómo se escriben las dos definiciones en Isabelle/HOL y cómo
    se demuestra su equivalencia.
*}
 
subsection {* Definición inductiva del conjunto de los pares *}
 
inductive_set par :: "nat set" where
  cero [intro!]: "0 ∈ par" 
| paso [intro!]: "n ∈ par ⟹ (Suc (Suc n)) ∈ par"
 
text {*
  · Una definición inductiva está formada con reglas de introducción.
 
  · La definición inductiva genera varios teoremas:
    · par.cero:   0 ∈ par
    · par.paso:   n ∈ par ⟹ Suc (Suc n) ∈ par
    · par.simps:  (a ∈ par) = (a = 0 ∨ (∃n. a = Suc (Suc n) ∧ n ∈ par))
*}
 
subsection {* Uso de las reglas de introducción *}
 
text {*
  Lema: Los números de la forma 2*k son pares.
*}
 
― ‹La demostración automática es›
lemma dobles_son_pares [intro!]: 
  "2*k ∈ par"
by (induct k) auto
 
― ‹La demostración estructurada es›
lemma dobles_son_pares_2:
  "2*k ∈ par"
proof (induct k)
  show "2 * 0 ∈ par" by auto
next
  show "⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par" by auto
qed
 
text {*
  · Nota: Nuestro objetivo es demostrar la equivalencia de la definición
    anterior y la definición mediante divisibilidad (even).
 
  · Lema: Si n es divisible por 2, entonces es par.
*}
 
lemma even_imp_par: "even n ⟹ n ∈ par"
by auto
 
subsection {* Regla de inducción *} 
 
text {*
  Entre las reglas generadas por la definión de par está la de
  inducción:
  · par.induct: ⟦ x ∈ par; 
                 P 0; 
                 ⋀n. ⟦n ∈ par; P n⟧ ⟹ P (Suc (Suc n))⟧ 
                ⟹ P x
*}
 
text {*
  Lema: Los números pares son divisibles por 2.
*} 
 
― ‹1ª demostración (detallada)lemma par_imp_even: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "2 dvd (0::nat)" by (simp_all add: dvd_def)
next
  fix n::nat
  assume H1: "n ∈ par" and
         H2: "even n"
  have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
  then obtain k where "n = 2*k" ..
  then have "Suc (Suc n) = 2*(k+1)" by auto
  then have "∃k. Suc (Suc n) = 2*k" ..
  then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
 
― ‹2ª demostración (con arith)lemma par_imp_even_2: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "even (0::nat)" by (simp_all add: dvd_def)
next
  fix n::nat
  assume H1: "n ∈ par" and
         H2: "even n"
  then show "even (Suc (Suc n))" by (auto simp add: dvd_def, arith)
qed
 
― ‹3ª demostración (automática)lemma par_imp_even_3: 
  "n ∈ par ⟹ even n"
by (induction rule:par.induct) (auto simp add: dvd_def, arith)
 
text {*
  Lema: Un número n es par syss es divisible por 2. 
*}
 
theorem par_iff_even: "(n ∈ par) = (even n)"
by (blast intro: even_imp_par par_imp_even)
 
subsection{* Generalización y regla de inducción *}
 
text {*
  · Antes de aplicar inducción se debe de generalizar la fórmula a
    probar.
 
  · Vamos a ilustrar el principio anterior en el caso de los conjuntos
    inductivamente definidos, con el siguiente ejemplo: si n+2 es par,
    entonces n también lo es.
 
  · El siguiente intento falla:
*}
 
lemma "Suc (Suc n) ∈ par ⟹ n ∈ par"
  apply (erule par.induct) 
oops
 
text {*
  En el intento anterior, los subobjetivos generados son
     1. n ∈ par
     2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par
  que no se pueden demostrar.
 
  Se ha perdido la información sobre Suc (Suc n).
*}
 
text {*
  Reformulación del lema: Si n es par, entonces n-2 también lo es.
*}
 
― ‹La demostración automática es›
lemma par_imp_par_menos_2: 
  "n ∈ par ⟹ n - 2 ∈ par"
by (induction rule:par.induct) auto
 
― ‹La demostración estructurada es›
lemma "n ∈  par ⟹ n - 2 ∈ par"
proof (induction rule:par.induct)
  show "0 - 2 ∈ par" by auto
next
  show "⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par" by auto
qed
 
text {* 
  Con el lema anterior se puede demostrar el original.
*}
 
― ‹La demostración estructurada es›
lemma
  assumes "Suc (Suc n) ∈ par" 
  shows   "n ∈ par"
proof -
  have "Suc (Suc n) - 2 ∈ par" using assms by (rule par_imp_par_menos_2)
  then show "n ∈ par" by simp 
qed
 
― ‹La demostración aplicativa es›
lemma 
  "Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (drule par_imp_par_menos_2) 
apply simp
done
 
(* Comentar el uso de drule *)
 
― ‹La demostración automática es›
lemma Suc_Suc_par_imp_par: 
  "Suc (Suc n) ∈ par ⟹ n ∈ par"
by (drule par_imp_par_menos_2, simp)
 
text {*
  Lemma. Un número natural n es par syss n+2 es par.
*}
 
lemma [iff]: "((Suc (Suc n)) ∈ par) = (n ∈ par)"
by (blast dest: Suc_Suc_par_imp_par)
 
text {*
  Se usa el atributo "iff" porque sirve como regla de simplificación.
*}
 
subsection {* Definiciones mutuamente inductivas *}
 
text {*
  Definición cruzada de los conjuntos inductivos de los pares y de los 
  impares:
*}
 
inductive_set
  Pares    :: "nat set" and
  Impares  :: "nat set"
where
  ceroP:    "0 ∈ Pares"
| ParesI:   "n ∈ Impares ⟹ Suc n ∈ Pares"
| ImparesI: "n ∈ Pares   ⟹ Suc n ∈ Impares"
 
text {*
  El esquema de inducción generado por la definición anterior es
  · Pares_Impares.induct:
    ⟦P1 0; 
     ⋀n. ⟦n ∈ Impares; P2 n⟧ ⟹ P1 (Suc n);
     ⋀n. ⟦n ∈ Pares;   P1 n⟧ ⟹ P2 (Suc n)⟧
    ⟹ (x1 ∈ Pares ⟶ P1 x1) ∧ (x2 ∈ Impares ⟶ P2 x2)
*}
 
text {*
  Ejemplo de demostración usando el esquema anterior.
*}
 
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
proof (induction rule:Pares_Impares.induct)
  show "even (0::nat)" by simp
next
  fix n :: "nat"
  assume H1: "n ∈ Impares" and
         H2: "even (Suc n)"
  show "even (Suc n)" using H2 by simp
next
  fix n :: "nat"
  assume H1: "n ∈ Pares" and
         H2: "even n"
  have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
  then obtain k where "n = 2*k" ..
  then have "Suc (Suc n) = 2*(k+1)" by auto
  then have "∃k. Suc (Suc n) = 2*k" ..
  then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
 
subsection {* Definición inductiva de predicados *}
 
text {*
  Definición inductiva del predicado es_par tal que (es_par n) se
  verifica si n es par.
*}
 
inductive es_par :: "nat ⇒ bool" where
  "es_par 0" 
| "es_par n ⟹ es_par (Suc(Suc n))"
 
text {*
  Heurística para elegir entre definir conjuntos o predicados:
  · si se va a combinar con operaciones conjuntistas, definir conjunto;
  · en caso contrario, definir predicado.
*}
 
end

Como ejercicio se propuso la relación 8 sobre gramáticas libres de contexto.