Menu Close

Etiqueta: Isabelle/HOL

RA2017: Demostración en Isabelle de la corrección de un compilador

En la segunda 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 9: Caso de estudio: Compilación de expresiones *}
 
theory T9
imports Main
begin
 
text {*
  El objetivo de este tema es contruir un compilador de expresiones
  genéricas (construidas con variables, constantes y operaciones
  binarias) a una máquina de pila y demostrar su corrección.
*}
 
section {* Las expresiones y el intérprete *}
 
text {*
  Definición. Las expresiones son las constantes, las variables
  (representadas por números naturales) y las aplicaciones de operadores
  binarios a dos expresiones. 
*}
 
type_synonym 'v binop = "'v ⇒ 'v ⇒ 'v"
 
datatype 'v expr = 
  Const 'v 
| Var nat 
| App "'v binop" "'v expr" "'v expr" 
 
text {*
  Definición. [Intérprete] 
  La función "valor" toma como argumentos una expresión y un entorno
  (i.e. una aplicación de las variables en elementos del lenguaje) y
  devuelve el valor de la expresión en el entorno.
*}
 
fun valor :: "'v expr ⇒ (nat ⇒ 'v) ⇒ 'v" where
  "valor (Const b) ent = b"
| "valor (Var x) ent = ent x"
| "valor (App f e1 e2) ent = (f (valor e1 ent) (valor e2 ent))"
 
text {*
  Ejemplo. A continuación mostramos algunos ejemplos de evaluación con
  el intérprete. 
*}
 
lemma 
  "valor (Const 3) id = 3 ∧
   valor (Var 2) id = 2 ∧
   valor (Var 2) (λx. x+1) = 3 ∧ 
   valor (App (op +) (Const 3) (Var 2)) (λx. x+1) = 6 ∧
   valor (App (op +) (Const 3) (Var 2)) (λx. x+4) = 9" 
by simp
 
section {* La máquina de pila *}
 
text {*
  Nota. La máquina de pila tiene tres clases de intrucciones:
  · cargar en la pila una constante,
  · cargar en la pila el contenido de una dirección y
  · aplicar un operador binario a los dos elementos superiores de la pila.
*}
 
datatype 'v instr = 
  IConst 'v 
| ILoad nat 
| IApp "'v binop"
 
text {*
  Definición. [Ejecución]
  La ejecución de la máquina de pila se modeliza mediante la función 
  "ejec" que toma una lista de intrucciones, una memoria (representada 
  como una función de las direcciones a los valores, análogamente a los 
  entornos) y una pila (representada como una lista) y devuelve la pila
  al final de la ejecución.
*}
 
fun ejec :: "'v instr list ⇒ (nat⇒'v) ⇒ 'v list ⇒ 'v list" where
  "ejec [] ent vs = vs"
| "ejec (i#is) ent vs = 
     (case i of
        IConst v ⇒ ejec is ent (v#vs)
      | ILoad x ⇒ ejec is ent ((ent x)#vs)
      | IApp f ⇒ ejec is ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))"
 
text {* 
  A continuación se muestran ejemplos de ejecución.
*}
 
lemma
  "ejec [IConst 3] id [7] = [3,7] ∧
   ejec [ILoad 2, IConst 3] id [7] = [3,2,7] ∧
   ejec [ILoad 2, IConst 3] (λx. x+4) [7] = [3,6,7] ∧
   ejec [ILoad 2, IConst 3, IApp (op +)] (λx. x+4) [7] = [9,7]"
by simp
 
section {* El compilador *}
 
text {*
  Definición. El compilador "comp" traduce una expresión en una lista de
  instrucciones. 
*}
 
fun comp :: "'v expr ⇒ 'v instr list" where
  "comp (Const v) = [IConst v]"
| "comp (Var x) = [ILoad x]"
| "comp (App f e1 e2) = (comp e2) @ (comp e1) @ [IApp f]"
 
text {*
  A continuación se muestran ejemplos de compilación.
*}
 
lemma
  "comp (Const 3) = [IConst 3] ∧
   comp (Var 2) = [ILoad 2] ∧
   comp (App (op +) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (op +)]"
by simp
 
section {* Corrección del compilador *}
 
text {*
  Para demostrar que el compilador es correcto, probamos que el
  resultado de compilar una expresión y a continuación ejecutarla es lo
  mismo que interpretarla; es decir, 
*}
 
theorem "ejec (comp e) ent [] = [valor e ent]" 
oops
 
text {*
  El teorema anterior no puede demostrarse por inducción en e. Para
  demostrarlo, lo generalizamos a
*}
 
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
oops
 
text {*
  En la demostración del teorema anterior usaremos el siguiente lema.
*}
 
lemma ejec_append:
  "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume "?P xs"
  thus "?P (a#xs)" by (cases "a", auto)
qed
 
-- "La demostración detallada es" 
lemma ejec_append_1:
  "∀ vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  thus "?P (a#xs)"
  proof (cases "a")
    case IConst thus ?thesis using HI by simp
  next
    case ILoad thus ?thesis using HI by simp
  next
    case IApp thus ?thesis using HI by simp
  qed
qed
 
text {*
  Una demostración más detallada del lema es la siguiente:
*}
 
lemma ejec_append_2:
  "∀vs. ejec (xs@ys) ent vs = ejec ys ent (ejec xs ent vs)" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next
  fix a xs
  assume HI: "?P xs"
  thus "?P (a#xs)"
  proof (cases "a")
    fix v assume C1: "a=IConst v"
    show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((IConst v)#xs)@ys) ent vs"
        using C1 by simp
      also have "… = ejec (xs@ys) ent (v#vs)" by simp
      also have "… = ejec ys ent (ejec xs ent (v#vs))" using HI by simp
      also have "… = ejec ys ent (ejec ((IConst v)#xs) ent vs)" by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C1 by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  next
    fix n assume C2: "a=ILoad n"
    show " ∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((ILoad n)#xs)@ys) ent vs"
        using C2 by simp
      also have "… = ejec (xs@ys) ent ((ent n)#vs)" by simp
      also have "… = ejec ys ent (ejec xs ent ((ent n)#vs))" using HI by simp
      also have "… = ejec ys ent (ejec ((ILoad n)#xs) ent vs)" by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C2 by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  next
    fix f assume C3: "a=IApp f"
    show "∀vs. ejec ((a#xs)@ys) ent vs = ejec ys ent (ejec (a#xs) ent vs)"
    proof
      fix vs
      have "ejec ((a#xs)@ys) ent vs = ejec (((IApp f)#xs)@ys) ent vs"
        using C3 by simp
      also have "… = ejec (xs@ys) ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs)))" 
        by simp
      also have "… = ejec ys 
                          ent 
                          (ejec xs ent ((f (hd vs) (hd (tl vs)))#(tl(tl vs))))" 
        using HI by simp
      also have "… = ejec ys ent (ejec ((IApp f)#xs) ent vs)" by simp
      also have "… = ejec ys ent (ejec (a#xs) ent vs)" using C3 by simp
      finally show "ejec ((a#xs)@ys) ent vs = 
                    ejec ys ent (ejec (a#xs) ent vs)" .
    qed
  qed
qed
 
text {*
  La demostración automática del teorema es
*}
 
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
by (induct e) (auto simp add:ejec_append)
 
text {*
  La demostración estructurada del teorema es
*}
 
theorem "∀vs. ejec (comp e) ent vs = (valor e ent)#vs"
proof (induct e)
  fix v
  show "∀vs. ejec (comp (Const v)) ent vs = (valor (Const v) ent)#vs" by simp
next
  fix x
  show "∀vs. ejec (comp (Var x)) ent vs = (valor (Var x) ent) # vs" by simp
next
  fix f e1 e2
  assume HI1: "∀vs. ejec (comp e1) ent vs = (valor e1 ent) # vs"
    and HI2: "∀vs. ejec (comp e2) ent vs = (valor e2 ent) # vs"
  show "∀vs. ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs"
  proof
    fix vs
    have "ejec (comp (App f e1 e2)) ent vs
          = ejec ((comp e2) @ (comp e1) @ [IApp f]) ent vs" by simp
    also have "… = ejec ((comp e1) @ [IApp f]) ent (ejec (comp e2) ent vs)"
      using ejec_append by blast
    also have "… = ejec [IApp f] 
                         ent 
                         (ejec (comp e1) ent (ejec (comp e2) ent vs))" 
      using ejec_append by blast
    also have "… =  ejec [IApp f] ent (ejec (comp e1) ent ((valor e2 ent)#vs))"
      using HI2 by simp
    also have "… = ejec [IApp f] ent ((valor e1 ent)#((valor e2 ent)#vs))"
      using HI1 by simp
    also have "… = (f (valor e1 ent) (valor e2 ent))#vs" by simp
    also have "… = (valor (App f e1 e2) ent) # vs" by simp
    finally 
    show "ejec (comp (App f e1 e2)) ent vs = (valor (App f e1 e2) ent) # vs" 
      by blast
  qed
qed
 
end

RA2017: Deducción natural de primer orden con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha presentado la deducción natural de primer orden Isabelle/HOL. La presentación se basa en los ejemplos del tema 8 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, 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:

RA2017: Deducción natural proposicional con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha presentado la deducción naturalcon Isabelle/HOL. La presentación se basa en los ejemplos del tema 2 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, 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:

RA2017: Razonamiento por casos y por inducción en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Razonamiento automático hemos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado

  • el razonamiento por casos booleanos,
  • el razonamiento por casos booleanos sobre una variable,
  • el razonamiento por casos sobre listas,
  • el razonamiento por inducción sobre números naturales con patrones,
  • el razonamiento sobre definiciones con existenciales,
  • el uso de librerías auxiliares (como Parity) y
  • el uso de otros métodos de demostración (como presburg).

La teoría con los ejemplos presentados en la clase es la siguiente: