1
我定義2種幾乎相同的語言（foo和bar）：如何定義表達式翻譯器？
theory SimpTr
imports Main
begin
type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"
datatype foo_exp =
FooBConst bool |
FooIConst int |
FooLet vname foo_exp foo_exp |
FooVar vname |
FooAnd foo_exp foo_exp
datatype bar_exp =
BarBConst bool |
BarIConst int |
BarLet vname bar_exp bar_exp |
BarVar vname |
BarAnd bar_exp bar_exp
甲瑣碎語義：
datatype foo_val = FooBValue bool | FooIValue int
datatype bar_val = BarBValue bool | BarIValue int
type_synonym foo_env = "foo_val env"
type_synonym bar_env = "bar_val env"
inductive foo_big_step :: "foo_exp × foo_env ⇒ foo_val ⇒ bool"
(infix "⇒f" 55) where
"(FooBConst c, e) ⇒f FooBValue c" |
"(FooIConst c, e) ⇒f FooIValue c" |
"(init, e) ⇒f x ⟹
(body, e(var↦x)) ⇒f v ⟹
(FooLet var init body, e) ⇒f v" |
"e var = Some v ⟹
(FooVar var, e) ⇒f v" |
"(a, e) ⇒f FooBValue x ⟹
(b, e) ⇒f FooBValue y ⟹
(FooAnd a b, e) ⇒f FooBValue (x ∧ y)"
inductive_cases FooBConstE[elim!]: "(FooBConst c, e) ⇒f v"
inductive_cases FooIConstE[elim!]: "(FooIConst c, e) ⇒f v"
inductive_cases FooLetE[elim!]: "(FooLet var init body, e) ⇒f v"
inductive_cases FooVarE[elim!]: "(FooVar var, e) ⇒f v"
inductive_cases FooAndE[elim!]: "(FooAnd a b, e) ⇒f v"
inductive bar_big_step :: "bar_exp × bar_env ⇒ bar_val ⇒ bool"
(infix "⇒b" 55) where
"(BarBConst c, e) ⇒b BarBValue c" |
"(BarIConst c, e) ⇒b BarIValue c" |
"(init, e) ⇒b x ⟹
(body, e(var↦x)) ⇒b v ⟹
(BarLet var init body, e) ⇒b v" |
"e var = Some v ⟹
(BarVar var, e) ⇒b v" |
"(a, e) ⇒b BarBValue x ⟹
(b, e) ⇒b BarBValue y ⟹
(BarAnd a b, e) ⇒b BarBValue (x ∧ y)"
inductive_cases BarBConstE[elim!]: "(BarBConst c, e) ⇒b v"
inductive_cases BarIConstE[elim!]: "(BarIConst c, e) ⇒b v"
inductive_cases BarLetE[elim!]: "(BarLet var init body, e) ⇒b v"
inductive_cases BarVarE[elim!]: "(BarVar var, e) ⇒b v"
inductive_cases BarAndE[elim!]: "(BarAnd a b, e) ⇒b v"
打字：
datatype foo_type = FooBType | FooIType
datatype bar_type = BarBType | BarIType
type_synonym foo_tenv = "foo_type env"
type_synonym bar_tenv = "bar_type env"
inductive foo_typing :: "foo_tenv ⇒ foo_exp ⇒ foo_type ⇒ bool"
("(1_/ ⊢f/ (_ :/ _))" [50,0,50] 50) where
"Γ ⊢f FooBConst c : FooBType" |
"Γ ⊢f FooIConst c : FooIType" |
"Γ ⊢f init : τ⇩1 ⟹
Γ(var↦τ⇩1) ⊢f body : τ ⟹
Γ ⊢f FooLet var init body : τ" |
"Γ var = Some τ ⟹
Γ ⊢f FooVar var : τ" |
"Γ ⊢f a : BType ⟹
Γ ⊢f b : BType ⟹
Γ ⊢f FooAnd a b : BType"
inductive bar_typing :: "bar_tenv ⇒ bar_exp ⇒ bar_type ⇒ bool"
("(1_/ ⊢b/ (_ :/ _))" [50,0,50] 50) where
"Γ ⊢b BarBConst c : BarBType" |
"Γ ⊢b BarIConst c : BarIType" |
"Γ ⊢b init : τ⇩1 ⟹
Γ(var↦τ⇩1) ⊢b body : τ ⟹
Γ ⊢b BarLet var init body : τ" |
"Γ var = Some τ ⟹
Γ ⊢b BarVar var : τ" |
"Γ ⊢b a : BType ⟹
Γ ⊢b b : BType ⟹
Γ ⊢b BarAnd a b : BType"
inductive_cases [elim!]:
"Γ ⊢f FooBConst c : τ"
"Γ ⊢f FooIConst c : τ"
"Γ ⊢f FooLet var init body : τ"
"Γ ⊢f FooVar var : τ"
"Γ ⊢f FooAnd a b : τ"
inductive_cases [elim!]:
"Γ ⊢b BarBConst c : τ"
"Γ ⊢b BarIConst c : τ"
"Γ ⊢b BarLet var init body : τ"
"Γ ⊢b BarVar var : τ"
"Γ ⊢b BarAnd a b : τ"
lemma foo_typing_is_fun:
"Γ ⊢f exp : τ⇩1 ⟹
Γ ⊢f exp : τ⇩2 ⟹
τ⇩1 = τ⇩2"
apply (induct Γ exp τ⇩1 arbitrary: τ⇩2 rule: foo_typing.induct)
apply blast
apply blast
apply blast
apply fastforce
by blast
lemma bar_typing_is_fun:
"Γ ⊢b exp : τ⇩1 ⟹
Γ ⊢b exp : τ⇩2 ⟹
τ⇩1 = τ⇩2"
apply (induct Γ exp τ⇩1 arbitrary: τ⇩2 rule: bar_typing.induct)
apply blast
apply blast
apply blast
apply fastforce
by blast
此外，我所定義從FOO翻譯吧：
primrec FooToBar :: "foo_exp ⇒ bar_exp option" where
"FooToBar (FooBConst c) = Some (BarBConst c)" |
"FooToBar (FooIConst c) = None" |
"FooToBar (FooLet var init body) = (case FooToBar init of
Some barInit ⇒ (case FooToBar body of
Some barBody ⇒ Some (BarLet var barInit barBody) |
_ ⇒ None) | _ ⇒ None)" |
"FooToBar (FooVar var) = Some (BarVar var)" |
"FooToBar (FooAnd a b) = (case (FooToBar a, FooToBar b) of
(Some a1, Some b1) ⇒ Some (BarAnd a1 b1) | _ ⇒ None)"
我試圖證明翻譯轉換FOO表達式吧表達式與相似類型：
inductive type_equiv :: "foo_type ⇒ bar_type ⇒ bool" (infix "∼" 50) where
"FooBType ∼ BarBType" |
"FooIType ∼ BarIType"
lemma FooToBarPreserveType:
"FooToBar fooExp = Some barExp ⟹
Γ1 ⊢f fooExp : t1 ⟹
Γ2 ⊢b barExp : t2 ⟹
t1 ∼ t2"
apply (induct fooExp arbitrary: barExp Γ1 Γ2 t1 t2)
而且還改造保留了表達的語義：
inductive val_equiv :: "foo_val ⇒ bar_val ⇒ bool" (infix "≈" 50) where
"v⇩F = v⇩B ⟹ FooBValue v⇩F ≈ BarBValue v⇩B" |
"v⇩F = v⇩B ⟹ FooIValue v⇩F ≈ BarIValue v⇩B"
lemma FooToBarPreserveValue:
"FooToBar fooExp = Some barExp ⟹
FooEval fooExp fooEnv = Some v1 ⟹
BarEval barExp barEnv = Some v2 ⟹
v1 ≈ v2"
apply (induct fooExp arbitrary: barExp fooEnv barEnv v1 v2)
我甚證明一些歸納案例。但我不能證明FooToBar (FooVar x)的情況。
總體而言不能證明FooVar x與BarVar x具有相似的類型或值。
我想FooToBar一定比較複雜。它還必須涉及某種表達環境或變量映射。你能建議FooToBar更好的簽名嗎？我認爲這樣的翻譯是一件小事，但我找不到任何描述它的教科書。