AgdaによるTaPL - Typed Arithmetic Expressions [Agda]
「プログラミング言語の基礎概念」(五十嵐2011)をAgdaでやっていた途中だが、 ここで "Types and Programming Language" (Pierce 2002) の第8章 "Typed Arithmetic Expressions" をAgdaでやることにする。
open import Relation.Binary.PropositionalEquality
using (_≡_; refl)
open import Data.Product
using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
Syntax of Terms
この章では同第3章で定義した算術式の言語に型をつける。 これは変数という概念が登場しない言語で、次のように定義される。
infix 10 succ_
infix 10 pred_
infix 9 iszero_
infix 8 if_then_else_
data Term : Set where
true : Term
false : Term
if_then_else_ : Term → Term → Term → Term
zero : Term
succ_ : Term → Term
pred_ : Term → Term
iszero_ : Term → Term
五十嵐(2011)はこれに近いML1という言語を定義しているが、その言語への型付けを扱っていない。 しかし変数がないため型環境について考えなくてよいという単純さがあって、 最初に型付けの証明をするには適当であると思われる。
Value
この言語に対してValueという概念を定義する。
data NumericValue : Term → Set where
NV-zero : NumericValue zero
NV-suc : ∀ {NV : Term}
→ NumericValue NV
-------
→ NumericValue (succ NV)
data Value : Term → Set where
V-true : Value true
V-false : Value false
V-nv : ∀ {NV : Term}
→ NumericValue NV
-------
→ Value NV
これは要するにValueとは真偽値か自然数であるということを言っている。 テストしてみよう。
_ : Value true
_ = V-true
_ : Value false
_ = V-false
_ : Value (succ zero)
_ = V-nv (NV-suc NV-zero)
Syntax of Types
この言語の型を定義する。ブール型と自然数型しかない。
data Type : Set where
Bool : Type
Nat : Type
Typing Rules
次に型付けルールを定義する。コロンはAgdaに使われているので記号としては ⦂ を使う。
infix 4 _⦂_
data _⦂_ : Term → Type → Set where
真偽値の定数は自然とブール型である。
T-TRUE : true ⦂ Bool
T-FALSE : false ⦂ Bool
if式の全体としての型は、then/elseの型になるが、前提として条件部分がBoolであり、then/elseの型が同じである必要がある。
T-IF : ∀ {t₁ t₂ t₃ : Term} {T : Type}
→ t₁ ⦂ Bool
→ t₂ ⦂ T
→ t₃ ⦂ T
---------
→ if t₁ then t₂ else t₃ ⦂ T
自然数型の型付けはペアノ数の構造に従って再帰的に定義される。
T-ZERO : zero ⦂ Nat
T-SUCC : ∀ {t₁ : Term}
→ t₁ ⦂ Nat
→ succ t₁ ⦂ Nat
この言語にはpredecessor関数も定義されている。 形はsuccと同じである。
T-PRED : ∀ {t₁ : Term}
→ t₁ ⦂ Nat
→ pred t₁ ⦂ Nat
iszeroは引数の型が自然数という前提で、全体がブール型になる。
T-ISZERO : ∀ {t₁ : Term}
→ t₁ ⦂ Nat
→ iszero t₁ ⦂ Bool
Inversion of the Typing Relation
この定義を定理の形にしたものがTaPLではinversion lemmaと呼ばれている。 ちょっとつまらないのだが一応全部書き下しておく。
inv1 : ∀ {R : Type}
→ true ⦂ R
---------
→ R ≡ Bool
inv1 T-TRUE = refl
inv2 : ∀ {R : Type}
→ false ⦂ R
---------
→ R ≡ Bool
inv2 T-FALSE = refl
inv3-1 : ∀ {t₁ t₂ t₃ : Term} {R : Type}
→ if t₁ then t₂ else t₃ ⦂ R
---------
→ t₁ ⦂ Bool
inv3-1 (T-IF t₁⦂Bool _ _) = t₁⦂Bool
inv3-2 : ∀ {t₁ t₂ t₃ : Term} {R : Type}
→ if t₁ then t₂ else t₃ ⦂ R
---------
→ t₂ ⦂ R
inv3-2 (T-IF _ t₂⦂R _) = t₂⦂R
inv3-3 : ∀ {t₁ t₂ t₃ : Term} {R : Type}
→ if t₁ then t₂ else t₃ ⦂ R
---------
→ t₃ ⦂ R
inv3-3 (T-IF _ _ t₃⦂R) = t₃⦂R
inv4 : ∀ {R : Type}
→ zero ⦂ R
---------
→ R ≡ Nat
inv4 T-ZERO = refl
inv5-1 : ∀ {t₁ : Term} {R : Type}
→ succ t₁ ⦂ R
---------
→ R ≡ Nat
inv5-1 (T-SUCC t₁⦂Nat) = refl
inv5-2 : ∀ {t₁ : Term} {R : Type}
→ succ t₁ ⦂ R
---------
→ t₁ ⦂ Nat
inv5-2 (T-SUCC t₁⦂Nat) = t₁⦂Nat
inv6-1 : ∀ {t₁ : Term} {R : Type}
→ pred t₁ ⦂ R
---------
→ R ≡ Nat
inv6-1 (T-PRED t₁⦂Nat) = refl
inv6-2 : ∀ {t₁ : Term} {R : Type}
→ pred t₁ ⦂ R
---------
→ t₁ ⦂ Nat
inv6-2 (T-PRED t₁⦂Nat) = t₁⦂Nat
inv7-1 : ∀ {t₁ : Term} {R : Type}
→ iszero t₁ ⦂ R
---------
→ R ≡ Bool
inv7-1 (T-ISZERO t₁⦂Nat) = refl
inv7-2 : ∀ {t₁ : Term} {R : Type}
→ iszero t₁ ⦂ R
---------
→ t₁ ⦂ Nat
inv7-2 (T-ISZERO t₁⦂Nat) = t₁⦂Nat
Uniqueness of Types
定義した型付けルールの一意性を証明する。 つまりTermに何か型がついているとしたらそれは1つの型であるということを示す。 証明はかんたんである。
uniqueness : ∀ {t : Term} {R S : Type}
→ t ⦂ R
→ t ⦂ S
→ R ≡ S
uniqueness T-TRUE T-TRUE = refl
uniqueness T-FALSE T-FALSE = refl
uniqueness (T-IF _ _ t₃⦂R) (T-IF _ _ t₃⦂S) = uniqueness t₃⦂R t₃⦂S
uniqueness T-ZERO T-ZERO = refl
uniqueness (T-SUCC _) (T-SUCC _) = refl
uniqueness (T-PRED _) (T-PRED _) = refl
uniqueness (T-ISZERO _) (T-ISZERO _) = refl
Canonical Forms
次にCanonical Formsという補題を証明する。これは次のようなものだ。
- If v is a value of type Bool, then v is either true or false.
- If v is a value of type Nat, then v is a numeric value according to the grammar in Figure 3-2.
Figure 3-21というのはこの記事でいうと上のNumericValueの定義である。
文章を愚直にAgdaの型に翻訳して証明するとこうなる。
canon1 : ∀ {v : Term}
→ Value v
→ v ⦂ Bool
--------
→ v ≡ true ⊎ v ≡ false
canon1 _ T-TRUE = inj₁ refl
canon1 _ T-FALSE = inj₂ refl
canon1 (V-nv ()) (T-IF y y₁ y₂)
canon1 (V-nv ()) (T-ISZERO y)
canon2 : ∀ {v : Term}
→ Value v
→ v ⦂ Nat
--------
→ v ≡ zero ⊎ ∃[ w ] (v ≡ succ w)
canon2 (V-nv ()) (T-IF _ _ _)
canon2 (V-nv NV-zero) T-ZERO = inj₁ refl
canon2 (V-nv (NV-suc {v} NumericValue-v)) (T-SUCC v⦂Nat) = inj₂ ⟨ v , refl ⟩
canon2 (V-nv ()) (T-PRED _)
ここに出てくる ()
はabsurd patternと呼ばれていて、そのパターンはありえないということを示す。
Safety = Progress + Preservation
型付けルールに関して証明したい性質はProgressとPreservationと呼ばれていて、それぞれ
- 型がついたTermはValueになっているか、さもなくば必ず簡約が存在する
- Term tがt'に簡約されたならばt'はtと同じ型である
ということを言っている。
まだこの言語の簡約について定義していなかったので、定義しておこう。
infix 4 _—→_
data _—→_ : Term → Term → Set where
E-IFTRUE : ∀ {t₂ t₃ : Term}
-----------------------
→ if true then t₂ else t₃ —→ t₂
E-IFFALSE : ∀ {t₂ t₃ : Term}
-----------------------
→ if false then t₂ else t₃ —→ t₃
E-IF : ∀ {t₁ t'₁ t₂ t₃ : Term}
→ t₁ —→ t'₁
-----------------------
→ if t₁ then t₂ else t₃ —→ if t'₁ then t₂ else t₃
E-SUCC : ∀ {t₁ t'₁ : Term}
→ t₁ —→ t'₁
---------
→ succ t₁ —→ succ t'₁
E-PREDZERO :
pred zero —→ zero
E-PREDSUCC : ∀ {nv₁ : Term}
→ pred (succ nv₁) —→ nv₁
E-PRED : ∀ {t₁ t'₁ : Term}
→ t₁ —→ t'₁
---------
→ pred t₁ —→ pred t'₁
E-ISZEROZERO :
iszero zero —→ true
E-ISZEROSUCC : ∀ {nv₁ : Term}
→ iszero (succ nv₁) —→ false
E-ISZERO : ∀ {t₁ t'₁ : Term}
→ t₁ —→ t'₁
---------
→ iszero t₁ —→ iszero t'₁
「型がついたTermはValueになっているか、さもなくば必ず簡約が存在する」 を愚直に表現するとこうなる。
progress' : ∀ {M : Term} {A : Type}
→ M ⦂ A
-----
→ ∃[ N ] (M —→ N) ⊎ Value M
証明は再帰するところとCanoncal Formsの補題を使うところを指定すればほぼ半自動でできる。
progress' T-TRUE = inj₂ V-true
progress' T-FALSE = inj₂ V-false
progress' (T-IF {t₁} {t₂} {t₃} t₁⦂Bool _ _) with progress' t₁⦂Bool
... | inj₁ ⟨ t , t₁—→t ⟩ = inj₁ (⟨ if t then t₂ else t₃ , E-IF t₁—→t ⟩)
... | inj₂ Value-t₁ with canon1 Value-t₁ t₁⦂Bool
... | inj₁ refl = inj₁ ⟨ t₂ , E-IFTRUE ⟩
... | inj₂ refl = inj₁ ⟨ t₃ , E-IFFALSE ⟩
progress' T-ZERO = inj₂ (V-nv NV-zero)
progress' (T-SUCC t₁⦂Nat) with progress' t₁⦂Nat
... | inj₁ ⟨ t , t₁—→t ⟩ = inj₁ ⟨ succ t , E-SUCC t₁—→t ⟩
... | inj₂ (V-nv NumericValue-t₁) = inj₂ (V-nv (NV-suc NumericValue-t₁))
progress' (T-PRED t₁⦂Nat) with progress' t₁⦂Nat
... | inj₁ ⟨ t , t₁—→t ⟩ = inj₁ ⟨ pred t , E-PRED t₁—→t ⟩
... | inj₂ Value-t₁ with canon2 Value-t₁ t₁⦂Nat
... | inj₁ refl = inj₁ ⟨ zero , E-PREDZERO ⟩
... | inj₂ ⟨ t , refl ⟩ = inj₁ ⟨ t , E-PREDSUCC ⟩
progress' (T-ISZERO t₁⦂Nat) with progress' t₁⦂Nat
... | inj₁ ⟨ t , t₁—→t ⟩ = inj₁ ⟨ iszero t , E-ISZERO t₁—→t ⟩
... | inj₂ Value-t₁ with canon2 Value-t₁ t₁⦂Nat
... | inj₁ refl = inj₁ ⟨ true , E-ISZEROZERO ⟩
... | inj₂ ⟨ t , refl ⟩ = inj₁ ⟨ false , E-ISZEROSUCC ⟩
ところでこの証明のinj₁/inj₂というところが読みにくいかもしれない。 progress'の戻り値もcanon1/canon2の戻り値も論理和なので それを受けるときにinj₁/inj₂を使う必要があるのだが、 文脈によって区別して読まなければならない。
こういう場合、汎用的な_⊎_を使うのでなくて、 特化した直和型を作ってしまったほうが読みやすくなることがある。
Canonical Formについては型ごとのCanonical Formを2通りずつ、4通りの直和型を作って:
infix 4 Canon_⦂_
data Canon_⦂_ : Term → Type → Set where
C-true :
Canon true ⦂ Bool
C-false :
Canon false ⦂ Bool
C-zero :
Canon zero ⦂ Nat
C-succ : ∀ {V : Term}
→ Canon V ⦂ Nat
------------------
→ Canon succ V ⦂ Nat
このように補題を証明する。
canon : ∀ {V : Term} {A : Type}
→ Value V
→ V ⦂ A
-------
→ Canon V ⦂ A
これは「VがA型のValueのとき、VはA型のCanonical Formである」と言っている。
canon _ T-TRUE = C-true
canon _ T-FALSE = C-false
canon (V-nv ()) (T-IF _ _ _)
canon _ T-ZERO = C-zero
canon (V-nv (NV-suc NumericValue-NV)) (T-SUCC NV⦂Nat) =
C-succ (canon (V-nv NumericValue-NV) NV⦂Nat)
canon (V-nv ()) (T-PRED _)
canon (V-nv ()) (T-ISZERO _)
Progressについても値の場合と簡約が存在する場合をそれぞれこのようにdataで表現する。
data Progress (M : Term) : Set where
step : ∀ {N : Term}
→ M —→ N
-----------
→ Progress M
done :
Value M
-----------
→ Progress M
そうするとprogressの定理と証明は次のように書ける。
progress : ∀ {M : Term} {A : Type}
→ M ⦂ A
------
→ Progress M
progress T-TRUE = done V-true
progress T-FALSE = done V-false
progress T-ZERO = done (V-nv NV-zero)
progress (T-IF t₁⦂Bool _ _) with progress t₁⦂Bool
... | step t—→N = step (E-IF t—→N)
... | done Value-t₁ with canon Value-t₁ t₁⦂Bool
... | C-true = step E-IFTRUE
... | C-false = step E-IFFALSE
progress {succ t₁} {Nat} (T-SUCC t₁⦂Nat) with progress t₁⦂Nat
... | step t₁—→N = step (E-SUCC t₁—→N)
... | done (V-nv x₁) = done (V-nv (NV-suc x₁))
progress (T-PRED t₁⦂Nat) with progress t₁⦂Nat
... | step t₁—→N = step (E-PRED t₁—→N)
... | done Value-t₁ with canon Value-t₁ t₁⦂Nat
... | C-zero = step E-PREDZERO
... | C-succ CanonV⦂Nat = step E-PREDSUCC
progress (T-ISZERO t₁⦂Nat) with progress t₁⦂Nat
... | step t₁—→N = step (E-ISZERO t₁—→N)
... | done Value-t₁ with canon Value-t₁ t₁⦂Nat
... | C-zero = step E-ISZEROZERO
... | C-succ CanonV⦂Nat = step E-ISZEROSUCC
最後にこれがPreservationの証明である。
preservation : ∀ {M N A}
→ M ⦂ A
→ M —→ N
-----
→ N ⦂ A
preservation (T-IF x x₁ x₂) E-IFTRUE = x₁
preservation (T-IF x x₁ x₂) E-IFFALSE = x₂
preservation (T-IF x x₁ x₂) (E-IF y) = T-IF (preservation x y) x₁ x₂
preservation (T-SUCC x) (E-SUCC y) = T-SUCC (preservation x y)
preservation (T-PRED x) E-PREDZERO = x
preservation (T-PRED x) E-PREDSUCC = inv5-2 x
preservation (T-PRED x) (E-PRED y) = T-PRED (preservation x y)
preservation (T-ISZERO x) E-ISZEROZERO = T-TRUE
preservation (T-ISZERO x) E-ISZEROSUCC = T-FALSE
preservation (T-ISZERO x) (E-ISZERO y) = T-ISZERO (preservation x y)
コメント 0