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
のより良い署名を提案できますか?私はそのような翻訳者は些細なことだと思うが、それを説明する教科書は見つからない。