chapter {* Tema 10: Caso de estudio: Compilación de expresiones *}
theory T10_Caso_de_estudio_Compilacion_de_expresiones
imports Main
begin
declare [[names_short]]
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 (+) (Const 3) (Var 2)) (λx. x+1) = 6 ∧
valor (App (+) (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 (+)] (λ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 (+) (Const 3) (Var 2)) = [ILoad 2, IConst 3, IApp (+)]"
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]"
apply (induct e)
apply auto
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"
then show "?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"
then show "?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"
then show "?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
