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)
Agdaによる「プログラミング言語の基礎概念」 - 導出システムReduceNatExpのメタ定理 [Agda]
定理2.15から定理2.20はEvalNatExpについてのメタ定理だが、特に難しい証明ではなかったので省略する。 導出システムReduceNatExpについてのメタ定理を見ていく。
module igarashi2-reducenatexp where
open import Data.Nat using (ℕ; zero; suc)
open import Data.Bool
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; cong; subst)
open import Data.Product
using (_×_; proj₁; proj₂; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import igarashi1
open import igarashi2
定理2.21 簡約の前進性
定理2.21は「任意の算術式eに対し、それがペアノ自然数でないならば、ある算術式e'が存在し、e—→e'である。」というものだ。 「それがペアノ自然数でないならば」をAgdaの型でどう表現するかが問題である。
Expの定義はこういうものだった。
data Exp : Set where
`_ : ℕ → Exp
_+_ : Exp → Exp → Exp
_*_ : Exp → Exp → Exp
こんな風にコンストラクタだけを取り出して等式で判定することはできない。
∀ {e : Exp} → constructor-of e ≢ `_ → ...
存在量化を使って「『何らかのnがあって e ≡ ` n』ではない」とするならば等式が書けそうだ。
theorem2-21 : ∀ {e : Exp}
→ ¬ ∃[ n ](e ≡ ` n)
-----------------
→ ∃[ e' ] (e —→ e')
しかし否定から初めてAgdaでどうやって証明を進めればいいのかよくわからない。
そこで、Expにはペアノ数以外には加算と乗算しかないので、「ペアノ自然数でないならば」を「加算か乗算であるならば」を言い換えることにしよう。 「何らかのe1,e2があってe ≡ e1 + e2」か「何らかのe1,e2があってe ≡ e1 * e2」 であるとすると:
theorem2-21 : ∀ {e : Exp}
→ ∃[ e1 ] (∃[ e2 ](e ≡ e1 + e2))
⊎ ∃[ e1 ] (∃[ e2 ](e ≡ e1 * e2))
-----------------
→ ∃[ e' ] (e —→ e')
となる。これが一番素直な定式化ではないかと思う。 証明に関してはCtrl+c, Ctrl+, をひたすら繰り返すとここまで場合分けができるから:
theorem2-21 (inj₁ ⟨ ` x1 , ⟨ ` x2 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₁ ⟨ ` x , ⟨ e1 + e2 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₁ ⟨ ` x , ⟨ e1 * e2 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₁ ⟨ e1 + e2 , ⟨ e3 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₁ ⟨ e1 * e2 , ⟨ e3 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₂ ⟨ ` x1 , ⟨ ` x2 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₂ ⟨ ` x , ⟨ e1 + e2 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₂ ⟨ ` x , ⟨ e1 * e2 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₂ ⟨ e1 + e2 , ⟨ e3 , refl ⟩ ⟩) = {!!}
theorem2-21 (inj₂ ⟨ e1 * e2 , ⟨ e3 , refl ⟩ ⟩) = {!!}
あとはひたすら埋める(あとで見たときのわかりやすさのため中括弧引数を補った)。
theorem2-21 {`x1 + `x2} (inj₁ ⟨ ` x1 , ⟨ ` x2 , refl ⟩ ⟩)
with theorem2-3 {x1} {x2} -- 加算の閉包性
... | ⟨ x3 , x1+x2=x3 ⟩ = ⟨ ` x3 , R-PLUS x1+x2=x3 ⟩
theorem2-21 {` x + (e1 + e2)} (inj₁ ⟨ ` x , ⟨ e1 + e2 , refl ⟩ ⟩)
with theorem2-21 (inj₁ ⟨ e1 , ⟨ e2 , refl ⟩ ⟩)
... | ⟨ e3 , e1+e2—→e3 ⟩ = ⟨ ` x + e3 , R-PLUSR e1+e2—→e3 ⟩
theorem2-21 {` x + (e1 * e2)} (inj₁ ⟨ ` x , ⟨ e1 * e2 , refl ⟩ ⟩)
with theorem2-21 (inj₂ ⟨ e1 , ⟨ e2 , refl ⟩ ⟩)
... | ⟨ e3 , e1*e2—→e3 ⟩ = ⟨ ` x + e3 , R-PLUSR e1*e2—→e3 ⟩
theorem2-21 {(e1 + e2) + e} (inj₁ ⟨ e1 + e2 , ⟨ e , refl ⟩ ⟩)
with theorem2-21 (inj₁ ⟨ e1 , ⟨ e2 , refl ⟩ ⟩)
... | ⟨ e3 , e1+e2—→e3 ⟩ = ⟨ e3 + e , R-PLUSL e1+e2—→e3 ⟩
theorem2-21 {(e1 * e2) + e} (inj₁ ⟨ e1 * e2 , ⟨ e , refl ⟩ ⟩)
with theorem2-21 (inj₂ ⟨ e1 , ⟨ e2 , refl ⟩ ⟩)
... | ⟨ e3 , e1*e2—→e3 ⟩ = ⟨ e3 + e , R-PLUSL e1*e2—→e3 ⟩
theorem2-21 {` x1 * ` x2} (inj₂ ⟨ ` x1 , ⟨ ` x2 , refl ⟩ ⟩)
with theorem2-7 {x1} {x2} -- 乗算の閉包性
... | ⟨ x3 , x1*x2=x3 ⟩ = ⟨ ` x3 , R-TIMES x1*x2=x3 ⟩
theorem2-21 {` x * (e1 + e2)} (inj₂ ⟨ ` x , ⟨ e1 + e2 , refl ⟩ ⟩)
with theorem2-21 (inj₁ ⟨ e1 , ⟨ e2 , refl ⟩ ⟩)
... | ⟨ e3 , e1+e2—→e3 ⟩ = ⟨ ` x * e3 , R-TIMESR e1+e2—→e3 ⟩
theorem2-21 {` x * (e1 * e2)} (inj₂ ⟨ ` x , ⟨ e1 * e2 , refl ⟩ ⟩)
with theorem2-21 (inj₂ ⟨ e1 , ⟨ e2 , refl ⟩ ⟩)
... | ⟨ e3 , e1*e2—→e3 ⟩ = ⟨ ` x * e3 , R-TIMESR e1*e2—→e3 ⟩
theorem2-21 {(e1 + e2) * e} (inj₂ ⟨ e1 + e2 , ⟨ e , refl ⟩ ⟩)
with theorem2-21 (inj₁ ⟨ e1 , ⟨ e2 , refl ⟩ ⟩)
... | ⟨ e3 , e1+e2—→e3 ⟩ = ⟨ e3 * e , R-TIMESL e1+e2—→e3 ⟩
theorem2-21 {(e1 * e2) * e} (inj₂ ⟨ e1 * e2 , ⟨ e , refl ⟩ ⟩)
with theorem2-21 (inj₂ ⟨ e1 , ⟨ e2 , refl ⟩ ⟩)
... | ⟨ e3 , e1*e2—→e3 ⟩ = ⟨ e3 * e , R-TIMESL e1*e2—→e3 ⟩
加算乗算の場合で左辺だけ再帰しているのがアンバランスに見えるかもしれないが、 ここで証明したいのは何か1通りでも簡約があればよいということだから、これでよい。
定式化の方法についてもう少し考えてみよう。 A⇒Bは¬A∨Bとも書き換えられるから、 「ペアノ自然数でないならば、ある算術式e'が存在し、e—→e'である。」を 「ペアノ自然数であるか、ある算術式e'が存在し、e—→e'である。」 と言い換えることもできる。
これに従うと次のようになる。
theorem2-21' : ∀ {e : Exp}
-----------------
→ ∃[ n ] (e ≡ ` n) ⊎ ∃[ e' ] (e —→ e')
そうすると証明はこう書ける。
theorem2-21' {` x} = inj₁ ⟨ x , refl ⟩
theorem2-21' {e1 + e2} with theorem2-21' {e1}
... | inj₂ ⟨ e3 , e1—→e3 ⟩ = inj₂ ⟨ e3 + e2 , R-PLUSL e1—→e3 ⟩
... | inj₁ ⟨ n , refl ⟩ with theorem2-21' {e2}
... | inj₂ ⟨ e4 , e2—→e4 ⟩ = inj₂ ⟨ ` n + e4 , R-PLUSR e2—→e4 ⟩
... | inj₁ ⟨ m , refl ⟩ with theorem2-3 {n} {m} -- 加算の閉包性
... | ⟨ o , n+m=o ⟩ = inj₂ ⟨ ` o , R-PLUS n+m=o ⟩
theorem2-21' {e1 * e2} with theorem2-21' {e1}
... | inj₂ ⟨ e3 , e1—→e3 ⟩ = inj₂ ⟨ e3 * e2 , R-TIMESL e1—→e3 ⟩
... | inj₁ ⟨ n , refl ⟩ with theorem2-21' {e2}
... | inj₂ ⟨ e4 , e2—→e4 ⟩ = inj₂ ⟨ ` n * e4 , R-TIMESR e2—→e4 ⟩
... | inj₁ ⟨ m , refl ⟩ with theorem2-7 {n} {m} -- 乗算の閉包性
... | ⟨ o , n*m=o ⟩ = inj₂ ⟨ ` o , R-TIMES n*m=o ⟩
Agdaで... |
は一番近くのwithに結びつくことになっているのでinj₁とinj₂を適宜入れ替えている。
定理2.22 合流
「任意の算術式e₁,e₂,e₃に対して、e₁—→e₂かつe₁—→e₃ならば、 ある算術式e₄が存在して、e₂—→e₄かつe₃—→e₄である。」
これは解けていない。 いま思っている疑問は、 e₁—→e₂,e₁—→e₃がR-PLUS/R-TIMESを使った簡約で「e₂≡e₃でペアノ自然数」になるとき、 e₂(≡e₃)からe₄を作れる簡約が存在しないのではないだろうか。 —→ではなくて—*→であればMR-ZEROが使えるので成立しそうなのだが。
定理2.23 決定的簡約の一意性
これは場合分けをCtrl+c, Ctrl+cで行ったあとはかんたん。
theorem2-22 : ∀ {e e' e'' : Exp}
→ e —→ᵈ e'
→ e —→ᵈ e''
---------
→ e' ≡ e''
theorem2-22 (DR-PLUS x) (DR-PLUS y) with theorem2-2 x y
... | refl = refl
theorem2-22 (DR-TIMES x) (DR-TIMES y) with theorem2-6 x y
... | refl = refl
theorem2-22 (DR-PLUSL r1) (DR-PLUSL r2) with theorem2-22 r1 r2
... | refl = refl
theorem2-22 (DR-PLUSR r1) (DR-PLUSR r2) with theorem2-22 r1 r2
... | refl = refl
theorem2-22 (DR-TIMESL r1) (DR-TIMESL r2) with theorem2-22 r1 r2
... | refl = refl
theorem2-22 (DR-TIMESR r1) (DR-TIMESR r2) with theorem2-22 r1 r2
... | refl = refl
定理2.24
決定的簡約はふつうの簡約に含まれる。場合分けしたあとはすべてCtrl+c, Ctrl+aで自動証明できる。
theorem2-24 : ∀ {e e' : Exp}
→ e —→ᵈ e'
--------
→ e —→ e'
theorem2-24 (DR-PLUS x) = R-PLUS x
theorem2-24 (DR-PLUSL x) = R-PLUSL (theorem2-24 x)
theorem2-24 (DR-PLUSR x) = R-PLUSR (theorem2-24 x)
theorem2-24 (DR-TIMES x) = R-TIMES x
theorem2-24 (DR-TIMESL x) = R-TIMESL (theorem2-24 x)
theorem2-24 (DR-TIMESR x) = R-TIMESR (theorem2-24 x)
定理2.25 弱正規化可能性
証明したいのはこれだ。
theorem2-25 : ∀ {e : Exp}
-------
→ ∃[ n ] (e —*→ ` n)
しかしこれを証明するにはこのような補題が加算乗算それぞれについてあったほうがよいことに気づく。
lemma2-25-1 : ∀ {e1 e2 : Exp} {n1 n2 : ℕ}
→ e1 —*→ ` n1
→ e2 —*→ ` n2
-----------
→ e1 + e2 —*→ ` n1 + ` n2
さらにこの補題の補助として—→のR-PLUSLとR-PLUSRの—*→版を定義しておく。 これらはありがたいことに場合分け後は全自動で証明できる。
MR-PLUSL : ∀ {e₁ e′₁ e₂ : Exp}
→ e₁ —*→ e′₁
--------------
→ e₁ + e₂ —*→ e′₁ + e₂
MR-PLUSL MR-ZERO = MR-ZERO
MR-PLUSL (MR-ONE x) = MR-ONE (R-PLUSL x)
MR-PLUSL (MR-MULTI x y) = MR-MULTI (MR-PLUSL x) (MR-PLUSL y)
MR-PLUSR : ∀ {e₁ e₂ e′₂ : Exp}
→ e₂ —*→ e′₂
--------------
→ e₁ + e₂ —*→ e₁ + e′₂
MR-PLUSR MR-ZERO = MR-ZERO
MR-PLUSR (MR-ONE x) = MR-ONE (R-PLUSR x)
MR-PLUSR (MR-MULTI x y) = MR-MULTI (MR-PLUSR x) (MR-PLUSR y)
これを使って補題の加算版を証明する。
lemma2-25-1 : ∀ {e1 e2 : Exp} {n1 n2 : ℕ}
→ e1 —*→ ` n1
→ e2 —*→ ` n2
-----------
→ e1 + e2 —*→ ` n1 + ` n2
lemma2-25-1 e1—*→`n1 e2—*→`n2
with MR-PLUSL e1—*→`n1 | MR-PLUSR e2—*→`n2
... | x | y = MR-MULTI x y
乗算についても同様に補題を作る。
MR-TIMESL : ∀ {e₁ e′₁ e₂ : Exp}
→ e₁ —*→ e′₁
--------------
→ e₁ * e₂ —*→ e′₁ * e₂
MR-TIMESL MR-ZERO = MR-ZERO
MR-TIMESL (MR-ONE x) = MR-ONE (R-TIMESL x)
MR-TIMESL (MR-MULTI x y) = MR-MULTI (MR-TIMESL x) (MR-TIMESL y)
MR-RIMESR : ∀ {e₁ e₂ e′₂ : Exp}
→ e₂ —*→ e′₂
--------------
→ e₁ * e₂ —*→ e₁ * e′₂
MR-RIMESR MR-ZERO = MR-ZERO
MR-RIMESR (MR-ONE x) = MR-ONE (R-TIMESR x)
MR-RIMESR (MR-MULTI x y) = MR-MULTI (MR-RIMESR x) (MR-RIMESR y)
lemma2-25-2 : ∀ {e1 e2 : Exp} {n1 n2 : ℕ}
→ e1 —*→ ` n1
→ e2 —*→ ` n2
-----------
→ e1 * e2 —*→ ` n1 * ` n2
lemma2-25-2 e1—*→`n1 e2—*→`n2
with MR-TIMESL e1—*→`n1 | MR-RIMESR e2—*→`n2
... | x | y = MR-MULTI x y
補題の準備ができたので証明したかった定理にとりかかる。
theorem2-25 : ∀ {e : Exp}
-------
→ ∃[ n ] (e —*→ ` n)
eの形式によって場合分けを行う。 eがすでにペアノ自然数の場合はゼロ回の簡約でたどり着く。
theorem2-25 {` n} = ⟨ n , MR-ZERO ⟩
加算の場合。まずは2つの構成要素の算術式に再帰的に定理を適用する。
theorem2-25 {e1 + e2}
with theorem2-25 {e1}
... | ⟨ n1 , e1—*→`n1 ⟩
with theorem2-25 {e2}
... | ⟨ n2 , e2—*→`n2 ⟩
ここで手に入った簡約ステップを使って先の補題を適用する。
with lemma2-25-1 e1—*→`n1 e2—*→`n2
... | e1+e2—*→`n1+`n2
最終的には1つのペアノ自然数に簡約されてほしいわけだからR-PLUSでn1+n2を簡約すればよい。 R-PLUSを使うためにはNatJudgementが必要だから加算の閉包性を使って:
with theorem2-3 {n1} {n2} -- +-closure
... | ⟨ n3 , n1+n2=n3 ⟩
R-PLUSを適用して、最後にすべてをつなぎ合わせる。
with MR-ONE (R-PLUS n1+n2=n3)
... | `n1+`n2—*→`n3 = ⟨ n3 , MR-MULTI e1+e2—*→`n1+`n2 `n1+`n2—*→`n3 ⟩
乗算についても同様に行う。
theorem2-25 {e1 * e2}
with theorem2-25 {e1}
... | ⟨ n1 , e1—*→`n1 ⟩
with theorem2-25 {e2}
... | ⟨ n2 , e2—*→`n2 ⟩
with lemma2-25-2 e1—*→`n1 e2—*→`n2
... | e1*e2—*→`n1*`n2
with theorem2-7 {n1} {n2} -- *-closure
... | ⟨ n3 , n1*n2=n3 ⟩
with MR-ONE (R-TIMES n1*n2=n3)
... | `n1*`n2—*→`n3 = ⟨ n3 , MR-MULTI e1*e2—*→`n1*`n2 `n1*`n2—*→`n3 ⟩
Agdaによる「プログラミング言語の基礎概念」 - 導出システムNatのメタ定理 [Agda]
第1章で定義した導出システムNatについてのメタ定理を証明していく。
module igarashi2 where
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; cong; subst)
open import Data.Product
using (_×_; proj₁; proj₂; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import igarashi1
定理2.1 加算の単位元
定理2.1はゼロが加算の単位元であることを左右それぞれ証明する。
-- +-identityˡ
theorem2-1-1 : ∀ {n : ℕ}
----------------
→ NatJudgement (0 plus n is n)
theorem2-1-1 {n} = P-ZERO {n}
-- +-identityʳ
theorem2-1-2 : ∀ {n : ℕ}
----------------
→ NatJudgement (n plus 0 is n)
theorem2-1-2 {zero} = P-ZERO {0}
theorem2-1-2 {suc n} = P-SUCC {n} {0} {n} (theorem2-1-2 {n})
これらの証明は実のところ全部自動でできる。
Agdaで証明を始めるときには型を書いたあと全体がHoleであるような証明をまず書いてしまうとよい。theorem2-1-2の場合はまずこのように書く。
theorem2-1-2 = ?
ここでCtrl+c, Ctrl+c, Enterすると引数を追加してくれる(中括弧引数と小括弧引数がある場合はまず小括弧引数が補完され、2回めに中括弧引数が保管される)。
theorem2-1-2 {n} = { }0
ここでCtrl+c, Ctrl+c, n, Enterすると引数nについて場合分けを行うということになり、引数の定義(この場合ペアノ自然数の定義)に従って場合分けをやってくれる。
theorem2-1-2 {zero} = { }0
theorem2-1-2 {suc n} = { }1
この状態から2つのHoleに対してCtrl+c, Ctrl+aで自動証明してくれる。
定理2.2
定理2.2は加算の結果が一意であることを示す。
theorem2-2 : ∀ {n1 n2 n3 n4 : ℕ}
→ NatJudgement (n1 plus n2 is n3)
→ NatJudgement (n1 plus n2 is n4)
----------------
→ n3 ≡ n4
theorem2-2 {zero} {_} {_} {_} P-ZERO P-ZERO = refl
theorem2-2 {suc _} {_} {_} {_} (P-SUCC d1) (P-SUCC d2) =
cong suc (theorem2-2 d1 d2)
これも証明の過程を見ていこう。 まずCtrl+c, Ctrl+c, Enterを繰り返すと、ここまで行く。
theorem2-2 {n1} {n2} {n3} {n4} x x₁ = { }0
ここでいったんx₁をASCIIの範囲の文字に直しておく。 これはユニコード文字が含まれているとその引数を場合分けしたいときにCtrl+c, Ctrl+cに続けて変数名を入力できないためだ。
theorem2-2 {n1} {n2} {n3} {n4} x y = { }0
n1で場合分けする。
theorem2-2 {zero} {n2} {n3} {n4} x y = { }0
theorem2-2 {suc n1} {n2} {n3} {n4} x y = { }1
1つ目のHoleに移動してCtrl+c, Ctrl+c, xでxを場合分けすると次のようになる。
theorem2-2 {zero} {n2} {n3} {n4} P-ZERO y = { }0
theorem2-2 {suc n1} {n2} {n3} {n4} x y = { }1
場合分けが増えていないが、これは1つ目のケースではP-ZEROしかありえないということをAgdaが推論してくれたためだ。 残りについても行うとこうなる。
theorem2-2 {zero} {n2} {.n2} {.n2} P-ZERO P-ZERO = { }0
theorem2-2 {suc n1} {n2} {.(suc _)} {.(suc _)} (P-SUCC x) (P-SUCC y) = { }1
ここで1つ目のHoleに移動してCtrl+c, Ctrl+,を押すとGoalがn2 ≡ n2であることがわかる。 ≡の左右が同じ値であるような型については常にreflをエビデンスとして与えることができる。 Ctrl+c, Ctrl+aでも埋めてくれる。
theorem2-2 {zero} {n2} {.n2} {.n2} P-ZERO P-ZERO = refl
2つ目のHoleに移動してCtrl+c, Ctrl+,を押すとこのような表示になる。
Goal: suc n₃ ≡ suc n₄
————————————————————————————————————————————————————————————
y : NatJudgement (n1 plus n2 is n₄)
x : NatJudgement (n1 plus n2 is n₃)
ここでxとyをtheorem2-2に再帰的に適用すればn₃ ≡ n₄が手に入ることがわかる。 n₃ ≡ n₄からsuc n₃ ≡ suc n₄を得るにはcongを使うことができる。 cong f x≡yの形で、x≡yの両辺に関数fを適用した等式を作ることができる。 以上を総合すると次のように書けばいいことになる。
theorem2-2 {suc n1} {n2} {.(suc _)} {.(suc _)} (P-SUCC x) (P-SUCC y) =
cong suc (theorem2-2 x y)
定理2.3 加算の閉包性
定義2.3は自然数の加算の結果として何かしらの自然数が存在すること。数学用語でいえば「閉じている」ということを証明する。
theorem2-3 : ∀ {n1 n2 : ℕ}
----------------
→ ∃[ n3 ] (NatJudgement (n1 plus n2 is n3))
theorem2-3 {zero} {n2} = ⟨ n2 , P-ZERO ⟩
theorem2-3 {suc n1} {n2} with theorem2-3 {n1} {n2}
... | ⟨ n , d ⟩ = ⟨ suc n , P-SUCC d ⟩
ここではAgdaの存在量化の構文を使って型を書いている。 ⟨ n2 , P-ZERO ⟩
は ∃[ n3 ] (NatJudgement (n1 plus n2 is n3))
型の値なのである。 Agdaの値とはその型が表現する命題のエビデンスとして提示するものだった。 そしてある値n3が存在することをエビデンスとして示すためにはその具体的な値を構成して提示する必要がある。。 そういうわけでAgdaの存在量化型 ∃[ x ] P xの値は、値xとP xの組ということになる。
最初の場合わけではn1=0だから、PはNatJudgement 0 plus n2 is n3である。この型の値はP-ZEROコンストラクタで構築することができるが、そのときNatJudgement 0 plus n2 is n2となるから、提示したかったn3とはn2のことである。
2つ目の場合わけではwithを使っている。withは関数定義以外の場所でパターンマッチを行いたいときに用いる。 再帰的にtheorem2-3を呼ぶと組が得られるが、それを分解して取り出して使いたいのでパターンマッチをする必要がある。
ところでこの証明を
theorem2-3 = ?
から初めてCtrl+c, Ctrl+c, Enterするとこうなる。
proj₁ theorem2-3 = { }0
proj₂ theorem2-3 = { }1
これは組の片方ずつを別々に書いた表現なのだが、ちょっとわかりにくいので手動で
theorem2-3 = ⟨ ? , ? ⟩
と書いてしまったほうがよい。この場合最後に使うのは組のコンストラクタであるとわかっているからとりあえずそれを書いておいて、コンストラクタを適用する値はHoleにしておいて後回しにできる。
また中括弧引数も何故かこの状態から空欄Enterでは補完してくれないのでCtrl+c, Ctrl+c, n1とCtrl+c, Ctrl+c, n2で補完する(あるいはこれも手で書いてしまう)。
theorem2-3 {n1} {n2} = ⟨ { }0 , { }1 ⟩
定理2.4 加算の可換性
次の定理2.4は加算の可換性を証明する。補題を経由して証明している。
-- +-succʳ
lemma2-4 : ∀ {n1 n2 n3 : ℕ}
→ NatJudgement (n1 plus n2 is n3)
----------------
→ NatJudgement (n1 plus suc n2 is suc n3)
lemma2-4 {zero} {n2} {.n2} P-ZERO = P-ZERO
lemma2-4 {suc n1} {n2} {suc n3} (P-SUCC d) = P-SUCC (lemma2-4 d)
-- +-comm
theorem2-4 : ∀ {n1 n2 n3 : ℕ}
→ NatJudgement (n1 plus n2 is n3)
----------------
→ NatJudgement (n2 plus n1 is n3)
theorem2-4 {zero} {n2} {.n2} P-ZERO = theorem2-1-2
theorem2-4 {suc n1} {n2} {suc n3} (P-SUCC d) = lemma2-4 (theorem2-4 d)
定理2.5 加算の結合性
定義2.5は次のような命題の証明である。
theorem2-5 : ∀ {n1 n2 n3 n4 n5 : ℕ}
→ NatJudgement (n1 plus n2 is n4)
→ NatJudgement (n4 plus n3 is n5)
----------------
→ ∃[ n6 ] (NatJudgement (n2 plus n3 is n6)
× NatJudgement (n1 plus n6 is n5))
これは何を言っているかちょっとわかりにくいのだが、加算の結合性を表している。 つまり (n1 + n2) + n3 ならば n1 + (n2 + n3) であるということを中間的な変数を使って表している。 ここで使っている × は命題の論理積を表す型である。この型の値はそれぞれの命題の値の組である。
lemma2-5-1 : ∀ {n1 n2 : ℕ}
→ n2 ≡ n1
-------
→ NatJudgement (0 plus n1 is n2)
lemma2-5-1 refl = P-ZERO
lemma2-5-2 : ∀ {n1 n2 n3 n4 n5 n6 : ℕ}
→ NatJudgement (n1 plus n2 is n3)
→ NatJudgement (n4 plus n2 is n5)
→ NatJudgement (n4 plus n3 is n6)
----------------
→ NatJudgement (n1 plus n5 is n6)
lemma2-5-2 {n1} {n2} {n3} {zero} {.n2} {.n3} d1 P-ZERO P-ZERO = d1
lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 with theorem2-4 d4 -- +-comm
... | d5 with P-SUCC d5
... | d6 with theorem2-4 d6 -- +-comm
... | d7 = d7
-- +-assoc
theorem2-5 : ∀ {n1 n2 n3 n4 n5 : ℕ}
→ NatJudgement (n1 plus n2 is n4)
→ NatJudgement (n4 plus n3 is n5)
----------------
→ ∃[ n6 ] (NatJudgement (n2 plus n3 is n6)
× NatJudgement (n1 plus n6 is n5))
theorem2-5 {zero} {n2} {n3} {.n2} {n5} P-ZERO d2 with theorem2-3 {n2} {n3}
... | ⟨ n6 , d ⟩ = ⟨ n6 , ⟨ d , lemma2-5-1 (theorem2-2 d2 d) ⟩ ⟩
theorem2-5 {suc n1} {n2} {n3} {n4} {n5} d1 d2 with theorem2-3 {n2} {n3}
... | ⟨ n6 , d ⟩ = ⟨ n6 , ⟨ d , lemma2-5-2 d1 (theorem2-4 d) (theorem2-4 d2) ⟩ ⟩
withのパターンマッチは主に構造を持つデータ(組や場合分けのあるデータ)を取り出すときに使うが、lemma2-5-2では単純な値をパターンマッチで受けている。 ここを少し説明したい。
Agdaで証明を書くとき、普通に関数適用の構文で書くと、「最後に適用される関数・コンストラクタ」を最初に書くことになる。 これは証明の末尾から遡って考えるということだ (このときまだわかっていない部分はHoleにすることができる)。
Goal: Z
————————————————————————————————————————————————————————————
x : X
y : Y
例えばこういう文脈だったとしてZ型を構築できるのは何だろうと考えて、それが例えばZConsというコンストラクタだと思ったら
_ = ZCons ?
と書いておく。Holeが新しいGoalになるからそこからまた遡る。
しかし証明を順方向に考えたいときもある。 手元にあるxとyに何かを適用してZ型の値に近づけていけないだろうかということだ。 こういう思考モードのときにはwithでその関数適用をしておくと手持ちの駒を増やしていくことができる。
lemma2-5-2の2つ目の場合分けでは最初このような文脈になる。
lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) = { }0
Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)
帰納を使うほうの場合分けだからとりあえず再帰をしてみようと思ってこのように書く。
lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 = { }0
すると再帰適用の結果が新たな前提として利用できるようになる。
Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d4 : NatJudgement (n1 plus n5 is n6)
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)
Goalを見ると、n5とn6にsucをつけたものが必要になりそうだ。 項にsucをつけるのはP-SUCCが使えそうだが、P-SUCCの形式にアダプトするにはd4をひっくり返した形式でなければならない。
lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 with theorem2-4 d4 -- +-comm
... | d5 = { }0
Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)
d5 : NatJudgement (n5 plus n1 is n6)
d4 : NatJudgement (n1 plus n5 is n6)
得られた NatJudgement (n5 plus n1 is n6)
にP-SUCCを適用すると NatJudgement (suc n5 plus n1 is suc n6)
が得られる。
lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 with theorem2-4 d4
... | d5 with P-SUCC d5
... | d6 = { }0
Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)
d4 : NatJudgement (n1 plus n5 is n6)
d6 : NatJudgement (suc n5 plus n1 is suc n6)
d5 : NatJudgement (n5 plus n1 is n6)
ここまで来ると NatJudgement (suc n5 plus n1 is suc n6)
をひっくり返せばGoalが得られることがわかる。 もう一度可換性を使う。
lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 with theorem2-4 d4
... | d5 with P-SUCC d5
... | d6 with theorem2-4 d6 -- +-comm
... | d7 = { }0
Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)
d4 : NatJudgement (n1 plus n5 is n6)
d5 : NatJudgement (n5 plus n1 is n6)
d7 : NatJudgement (n1 plus suc n5 is suc n6)
d6 : NatJudgement (suc n5 plus n1 is suc n6)
d7がGoalそのものだからCtrl+c, Ctrl+aで自動補完できる。 このようにwithを連鎖させると順方向で証明を進めやすくなる。
定理2.6
定理2.6は乗算の結果が一意であることを示す。
theorem2-6 : ∀ {n1 n2 n3 n4 : ℕ}
→ NatJudgement (n1 times n2 is n3)
→ NatJudgement (n1 times n2 is n4)
----------------
→ n3 ≡ n4
theorem2-6 {zero} {n2} {.0} {.0} T-ZERO T-ZERO = refl
theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2)
with theorem2-6 y1 x1
... | refl
with theorem2-2 y2 x2
... | refl = refl
reflばかりになるのがちょっとわかりにくい。 まずCtrl+c, Ctrl+cの場合分けで次の状態まで行く。
theorem2-6 {zero} {n2} {.0} {.0} T-ZERO T-ZERO = { }0
theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2) = { }1
1つ目は自動で証明できる。2つ目の文脈は次のようになる。
Goal: n3 ≡ n4
————————————————————————————————————————————————————————————
y2 : NatJudgement (n2 plus n₄ is n4)
y1 : NatJudgement (n1 times n2 is n₄)
x2 : NatJudgement (n2 plus n₃ is n3)
x1 : NatJudgement (n1 times n2 is n₃)
x1とy1に再帰的にtheorem2-6を適用できそうだということがわかる。
theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2)
with theorem2-6 y1 x1
... | x = { }0
Goal: n3 ≡ n4
————————————————————————————————————————————————————————————
y2 : NatJudgement (n2 plus n₄ is n4)
x2 : NatJudgement (n2 plus n₃ is n3)
x : n₄ ≡ n₃
y1 : NatJudgement (n1 times n2 is n₄)
x1 : NatJudgement (n1 times n2 is n₃)
ここで次に目をつけたいのはx2とy2に定理2.2を適用できないかということだ。 すでにn₄ ≡ n₃であるということはわかっているが、 x2とy2の形式はtheorem2-2と一致していないのでこのままでは適用できない。
そこでCtrl+c, Ctrl+c, xでxを場合分けする。するとこうなる。
theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2)
with theorem2-6 y1 x1
... | refl = { }0
Goal: n3 ≡ n4
————————————————————————————————————————————————————————————
y2 : NatJudgement (n2 plus n₃ is n4)
x2 : NatJudgement (n2 plus n₃ is n3)
y1 : NatJudgement (n1 times n2 is n₃)
x1 : NatJudgement (n1 times n2 is n₃)
等式のエビデンスはつねにreflなのでxはreflになった。 それとともに x : n₄ ≡ n₃ も文脈から消えてx2とy2が同じ形式になってくれた。 このように等式で終わるエビデンスはパターンマッチを使ってreflで受けるようにするとよい (そうでなければsubstを使って式変形することになるが、これは書きにくい)。
定理2.2を同様に適用すると次のようになるが、この時点でGoalがn3 ≡ n3になるのでreflを与えれば良いことがわかる。
theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2)
with theorem2-6 y1 x1
... | refl
with theorem2-2 y2 x2
... | refl = { }0
定理2.7 乗算の閉包性
定理2.7は乗算が閉じていることを示す。
theorem2-7 : ∀ {n1 n2 : ℕ}
----------------
→ ∃[ n3 ] (NatJudgement (n1 times n2 is n3))
theorem2-7 {zero} {n2} = ⟨ zero , T-ZERO ⟩
theorem2-7 {suc n1} {n2} with theorem2-7 {n1} {n2}
... | ⟨ n4 , d1 ⟩ with theorem2-3 {n2} {n4}
... | ⟨ n3 , d2 ⟩ = ⟨ n3 , T-SUCC d1 d2 ⟩
定理2.8 乗算の右ゼロと左ゼロ
定理2.8は左右に0をかけると0になることを示す。
-- *-zeroˡ
theorem2-8-1 : ∀ {n : ℕ}
----------------
→ NatJudgement (0 times n is 0)
theorem2-8-1 {n} = T-ZERO
theorem2-8-2 : ∀ {n : ℕ}
----------------
→ NatJudgement (n times 0 is 0)
-- *-zeroʳ
theorem2-8-2 {zero} = T-ZERO
theorem2-8-2 {suc n} = T-SUCC theorem2-8-2 P-ZERO
定理2.9 乗算の可換性
定理2.9は乗算の交換法則の証明である。これは難しかった。 補題として乗算の右辺にsucをつけるもの(T-SUCCとは逆)を証明する必要があるのだが、この証明自体苦労した。
-- *-succʳ
lemma2-9 : ∀ {n1 n2 n3 n4 : ℕ}
→ NatJudgement (n1 times n2 is n3)
→ NatJudgement (n1 plus n3 is n4)
----------------
→ NatJudgement (n1 times suc n2 is n4)
この証明について、式を変形していく発想で行ったので、その注釈をつけながら見ていく。
lemma2-9 {zero} {n2} {.0} {.0} T-ZERO P-ZERO = T-ZERO
lemma2-9 {suc n1} {n2} {n3} {suc n4}
(T-SUCC {n1} {n2} {m1} {n3} n1×n2=m1 n2+m1=n3)
(P-SUCC n1+n3=n4)
n1で場合分けするが1つ目は容易なので説明を省く。 2つ目についてn1をsuc n1、n4をsuc n4と置き換えたので、補題の型から、次の式を出発点とすることになる。
suc n1 + (suc n1 × n2)
| |
suc n4 n3
前提の1つ目の乗算をT-SUCCで分解したことにより、次の式が得られる。
suc n1 + (n2 + (n1 × n2))
| | |
suc n4 n3 m1
前提の2つ目の加算をP-SUCCで分解したことにより、次の式を得る。
n1 + (n2 + (n1 × n2))
| | |
n4 n3 m1
まずはこの式全体をひっくり返す。
with theorem2-4 n1+n3=n4 -- +-comm
... | n3+n1=n4
このような式になったということだ。
(n2 + (n1 × n2)) + n1
| | |
n3 m1 n4
結合法則を使って括弧の対応を変える。
with theorem2-5 n2+m1=n3 n3+n1=n4 -- +-assoc
... | ⟨ m2 , ⟨ m1+n1=m2 , n2+m2=n4 ⟩ ⟩
n2 + ((n1 × n2) + n1)
| | |
n4 m1 m2
内側の加算をひっくり返す。
with theorem2-4 m1+n1=m2 -- +-comm
... | n1+m1=m2
n2 + (n1 + (n1 × n2))
| | |
n4 m2 m1
こうすると補題を再帰適用することができるようになる。
with lemma2-9 n1×n2=m1 n1+m1=m2 -- *-succʳ
... | n1×suc_n2=m2
n2 + (n1 × suc 2)
| |
n4 m2
全体にP-SUCCを適用する。
with P-SUCC n2+m2=n4
... | suc_n2+m2=suc_n4
するとこの式が得られる。
suc n2 + (n1 × suc 2)
| |
suc n4 m2
ここまで来るとT-SUCCと手持ちの式を使ってGoalを作ることができる。
= T-SUCC n1×suc_n2=m2 suc_n2+m2=suc_n4
suc n1 × suc n2
|
suc n4
この補題を使うともともと証明したかった乗算の交換法則を証明することができる。
-- *-comm
theorem2-9 : ∀ {n1 n2 n3 : ℕ}
→ NatJudgement (n1 times n2 is n3)
----------------
→ NatJudgement (n2 times n1 is n3)
theorem2-9 {zero} {n2} {zero} T-ZERO = theorem2-8-2 -- *-zeroʳ
theorem2-9 {suc n1} {n2} {n3} (T-SUCC {n1} {n2} {m3} d1 d2)
with theorem2-9 d1
... | d3 = lemma2-9 d3 d2
定理2.10 乗算の結合性
加算乗算システムについての最後のメタ定理として、乗算の結合性を証明する。 だが、証明しようとすると加算と乗算の分配法則が必要なことに気づくのでまずはそれからだ。
補題 加算と乗算の分配
-- *-distrib-+
lemma2-10 : ∀ {n1 n2 n3 n4 n5 : ℕ}
→ NatJudgement (n1 plus n2 is n4)
→ NatJudgement (n4 times n3 is n5)
-------------------------------
→ ∃[ n6 ] (∃[ n7 ] (NatJudgement (n1 times n3 is n6)
× NatJudgement (n2 times n3 is n7)
× NatJudgement (n6 plus n7 is n5)))
lemma2-10 {zero} {n2} {n3} {.n2} {n5} P-ZERO n2×n3=n5
= ⟨ 0 , ⟨ n5 , ⟨ T-ZERO , ⟨ n2×n3=n5 , P-ZERO ⟩ ⟩ ⟩ ⟩
lemma2-10 {suc n1} {n2} {n3} {suc n4} {n5}
(P-SUCC {n1} {n2} {n4} n1+n2=n4)
(T-SUCC {n4} {n3} {m1} {n5} n4×n3=m1 n3+m1=n5)
場合分けの2つ目の出発点とゴールは次のようになる。
(suc n1 + n2) × n3 → (suc 1 × n3) + (n2 × n3)
| | | | |
suc n4 n5 n6 n5 n7
P-SUCCとT-SUCCの分解によって次の式が得られる。
n3 + ((n1 + n2) × n3)
| | |
n5 n4 m1
さっそくだが右側の部分に再帰的に分配法則を適用する。
with lemma2-10 n1+n2=n4 n4×n3=m1
... | ⟨ m2 , ⟨ n7 , ⟨ n1×n3=m2 , ⟨ n2×n3=n7 , m2+n7=m1 ⟩ ⟩ ⟩ ⟩
n2 × n3はゴールでいうn7に対応するからこの時点でそのように名前をつけた。
n3 + ((n1 × n3) + (n2 × n3))
| | | |
n5 m2 m1 n7
ゴールではn2 × n3が独立して現れるからこれを外に出したい。 結合法則を利用したいところだが、定義2.5とは向きが異なるので交換法則を使って形を合わせる。
with theorem2-4 n3+m1=n5
... | m1+n3=n5
((n1 × n3) + (n2 × n3)) + n3
| | | |
m2 m1 n7 n5
with theorem2-4 m2+n7=m1
... | n7+m2=m1
((n2 × n3) + (n1 × n3)) + n3
| | | |
n7 m1 m2 n5
with theorem2-5 n7+m2=m1 m1+n3=n5
... | ⟨ n6 , ⟨ m2+n3=n6 , n7+n6=n5 ⟩ ⟩
(n2 × n3) + ((n1 × n3) + n3)
| | | |
n7 n5 m2 n6
これでn2 × n3が外に出せた。 直観的にn2 × n3じゃない方の部分はGoalのn6になるはずなのでそういう名前にしておく。
この右側の部分はT-SUCCが使えそうな形に見えるがやはり向きが合わないので入れ替えて合わせる。
with theorem2-4 m2+n3=n6
... | n3+m2=n6
(n2 × n3) + (n3 + (n1 × n3))
| | | |
n7 n5 n6 m2
with T-SUCC n1×n3=m2 n3+m2=n6
... | suc_n1×n3=n6
(n2 × n3) + (suc n1 × n3)
| | |
n7 n5 n6
n6をGoalの形式にすることができた。 全体をひっくり返せばGoalになる。
with theorem2-4 n7+n6=n5
... | n6+n7=n5 = ⟨ n6 , ⟨ n7 , ⟨ suc_n1×n3=n6 , ⟨ n2×n3=n7 , n6+n7=n5 ⟩ ⟩ ⟩ ⟩
これで乗算の結合性を証明する準備ができた。
乗算の結合性
-- *-assoc
theorem2-10 : ∀ {n1 n2 n3 n4 n5 : ℕ}
→ NatJudgement (n1 times n2 is n4)
→ NatJudgement (n4 times n3 is n5)
----------------
→ ∃[ n6 ] (NatJudgement (n2 times n3 is n6)
× NatJudgement (n1 times n6 is n5))
この命題はこういうことを言っている。
(n1 × n2) × n3 → n1 × (n2 × n3)
| | | |
n4 n5 n5 n6
例によってn1で場合分けする。
theorem2-10 {zero} {n2} {n3} {zero} {zero} T-ZERO T-ZERO
with theorem2-7 {n2} {n3}
... | ⟨ n , d ⟩ = ⟨ n , ⟨ d , T-ZERO ⟩ ⟩
theorem2-10 {suc n1} {n2} {n3} {n4} {n5} (T-SUCC {n1} {n2} {m1} {n4} n1×n2=m1 n2+m1=n4) n4×n3=n5
2つめの場合分けの出発点とゴールは次の通り。
(suc n1 × n2) × n3 → suc n1 × (n2 × n3)
| | | |
n4 n5 n5 n6
T-SUCCの分解でこの式が得られる。
(n2 + (n1 × n2)) × n3
| | |
n4 m1 n5
早速分配法則を使う。
with lemma2-10 n2+m1=n4 n4×n3=n5
... | ⟨ n6 , ⟨ m2 , ⟨ n2×n3=n6 , ⟨ m1×n3=m2 , n6+m2=n5 ⟩ ⟩ ⟩ ⟩
(n2 × n3) + ((n1 × n2) × n3)
| | | |
n6 n5 m1 m2
右側にもn2 × n3を作るとよさそうだ。 そこで結合法則を再帰的に適用する。
with theorem2-10 n1×n2=m1 m1×n3=m2
... | ⟨ m3 , ⟨ n2×n3=m3 , n1×m3=m2 ⟩ ⟩
(n2 × n3) + (n1 × (n2 × n3))
| | | |
n6 n5 m2 m3
ここでm3は明らかにn6と同じなのだがAgdaはそれを認識していない。 定理2.6を使って同じであることを教えてあげる。
with theorem2-6 n2×n3=n6 n2×n3=m3
... | refl
最後に全体にT-SUCCを適用すればGoalが作れる。
with T-SUCC n1×m3=m2 n6+m2=n5
... | suc_n1×n6=n5 = ⟨ n6 , ⟨ n2×n3=n6 , suc_n1×n6=n5 ⟩ ⟩
Agdaによる「プログラミング言語の基礎概念」 - 自然数の加算・乗算・比較 [Agda]
定理証明支援系は入門しようとしてみて挫折というのを何度か繰り返しているのだけどAgdaを始めてみたらようやく何か掴み取れそうかなという気がしてきた。
個人的にはHaskellよりMLに慣れ親しんでいるので最初はなんとなくIsabelleやCoqをやってみようかという気になっていたのだけど、いまのところこれらのツールを使いこなせていない。 自分にはAgdaのほうがずっとわかりやすくて、結局のところ使えそうだと感じたものに縋り付くしかない。
Agdaの難点としてIsabelleやCoqのように専用のIDEがなくてEmacsの利用を事実上強制される点があるが、これについてはSpacemacsを使うことで多少軽減できる。 SpacemacsにはAgda Layerもある。
Agdaの練習として、まずは五十嵐淳「プログラミング言語の基礎概念」(以下五十嵐(2011)と表記)の最初の方の例―自然数の加算・乗算・比較―をAgdaで実装してみようと思う。
なおここではAgdaでどう書くかということに主に触れ、本で説明されていることについては書かないので、そちらは本を読んでほしい。
導出システム Nat
module igarashi1 where
open import Data.Nat using (ℕ; zero; suc)
自然数の表現形式としてペアノ数を使う。 自分で容易に定義できるが、ここではAgdaが提供しているものをインポートして使う。 ℕが自然数の型名、zeroとsucがコンストラクタである。 zeroの代わりに0、suc zeroの代わりに1などと書くこともできる。
次に自然数に関する判断を表現するための形式を定義する。
data NatSentence : Set where
_plus_is_ : ℕ → ℕ → ℕ → NatSentence
_times_is_ : ℕ → ℕ → ℕ → NatSentence
dataはSMLでいうdatatypeみたいな代数的データ型を定義するもので、_plus_is_と_times_is_はそのコンストラクタだ。 _は引数のプレースホルダーで、この場合3つの引数をとる。 Agdaではこのようなdisfix/mixfixを自分で定義することができる。
ここで定義したのはただの形式だ。だから間違った形式も構築することができる。
_ : NatSentence
_ = 2 plus 3 is 1
ありうる形式のうち内容として正しいものだけ導出できるような推論規則を定義しよう。
data NatJudgement : NatSentence → Set where
P-ZERO : ∀ {n : ℕ}
----------------
→ NatJudgement (zero plus n is n)
P-SUCC : ∀ {n₁ n₂ n₃ : ℕ}
→ NatJudgement (n₁ plus n₂ is n₃)
----------------
→ NatJudgement (suc n₁ plus n₂ is suc n₃)
T-ZERO : ∀ {n : ℕ}
----------------
→ NatJudgement (zero times n is zero)
T-SUCC : ∀ {n₁ n₂ n₃ n₄ : ℕ}
→ NatJudgement (n₁ times n₂ is n₃)
→ NatJudgement (n₂ plus n₃ is n₄)
----------------
→ NatJudgement (suc n₁ times n₂ is n₄)
Agdaでは述語を定義するのにindexed datatypeというのを使う。 NatJudgementはNatSentenceをindexとするindexed datatypeである。
少々混乱するがP-SUCCの箇所を例に取ると、 NatJudgement (n₁ plus n₂ is n₃) や NatJudgement (suc n₁ plus n₂ is suc n₃) は型である。 一方P-SUCCはコンストラクタだ。
NatJudgementという型はNatSentence型の値をいわば引数にとって新しい型を作る。 NatJudgement : NatSentence → Set はそういうことを言っている。 Setは型という意味だ。
一方P-SUCCというコンストラクタは NatJudgement (n₁ plus n₂ is n₃) 型の値を引数にとって NatJudgement (suc n₁ plus n₂ is suc n₃) 型の値を作る。
横棒は何かというとコメント行だ。Agdaでは--以降をコメントとみなす。 ここでは推論規則っぽさを出すための飾りとして使っている。
NatJudgement NatSentence 型はその型が表現する述語が内容として正しい判断であると主張していることになる。 それを証明するにはその型の値が存在することを示せば良い。 つまりいずれかのコンストラクタを使ってその型の値を構築すればよい。
_ : NatJudgement (0 plus 5 is 5)
これは正しい判断だろうか。
P-ZERO : ∀ {n : ℕ}
----------------
→ NatJudgement (zero plus n is n)
という定義を見てみると、n=5としてP-ZEROコンストラクタを使えば NatJudgement (0 plus n is 5)型の値を作ることができる。 つまりこれが正しい判断であることを示すことができる。
_ = P-ZERO {5}
いままで ∀ {n : ℕ} の部分に触れていなかったが、中括弧で定義された引数に対してコンストラクタを適用する場合は引数を中括弧で囲む必要がある。 実を言うと中括弧引数は省略してもAgdaがいい感じに推論してくれる。 したがって実はこのように書いてもよかった。
_ : NatJudgement (0 plus 5 is 5)
_ = P-ZERO
またP-ZEROを使えば示せるということをEmacsのAgda modeに自動でやってもらうことができる。
_ : NatJudgement (0 plus 5 is 5)
_ = ?
このように値を埋めたい部分に?とだけ書いておく。これはHoleと呼ばれる。 この状態でEmacsでCtrl+c, Ctrl+lと打ってAgdaをロードすると次のようになる。
_ : NatJudgement (0 plus 5 is 5)
_ = { }0
Agda modeがHoleを認識した。 この状態でEmacsでCtrl+c, Ctrl+aと打つと自動でHoleを埋めてくれる。
_ : NatJudgement (0 plus 5 is 5)
_ = P-ZERO
ただしあらゆる場面で常に自動でできるわけではない。
他にもいくつか例を挙げる。これらもCtrl+c, Ctrl+aだけで済む。
_ : NatJudgement (2 plus 3 is 5)
_ = P-SUCC (P-SUCC (P-ZERO {3}))
_ : NatJudgement (2 times 2 is 4)
_ = T-SUCC (T-SUCC T-ZERO
(P-SUCC (P-SUCC P-ZERO)))
(P-SUCC (P-SUCC P-ZERO))
導出システム CompareNat
次に自然数の大小比較の判断をする推論規則を定義する。まずは形式。
data CompareNatSentence : Set where
_is-less-than_ : ℕ → ℕ → CompareNatSentence
ここでis-less-thanはただの中置演算子である。 is less thanのような間に何も引数が入らない分裂した演算子は定義できないためハイフンを入れた。
次に推論規則だが、五十嵐(2011)に従って三通りの方式を定義する。
data CompareNat1Judgement : CompareNatSentence → Set where
L-SUCC : ∀ {n : ℕ}
----------------
→ CompareNat1Judgement (n is-less-than suc n)
L-TRANS : ∀ {n₁ n₂ n₃ : ℕ}
→ CompareNat1Judgement (n₁ is-less-than n₂)
→ CompareNat1Judgement (n₂ is-less-than n₃)
----------------
→ CompareNat1Judgement (n₁ is-less-than n₃)
data CompareNat2Judgement : CompareNatSentence → Set where
L-ZERO : ∀ {n : ℕ}
----------------
→ CompareNat2Judgement (zero is-less-than suc n)
L-SUCCSUCC : ∀ {n₁ n₂ : ℕ}
→ CompareNat2Judgement (n₁ is-less-than n₂)
----------------
→ CompareNat2Judgement (suc n₁ is-less-than suc n₂)
data CompareNat3Judgement : CompareNatSentence → Set where
L-SUCC : ∀ {n : ℕ}
----------------
→ CompareNat3Judgement (n is-less-than suc n)
L-SUCCR : ∀ {n₁ n₂ : ℕ}
→ CompareNat3Judgement (n₁ is-less-than n₂)
----------------
→ CompareNat3Judgement (n₁ is-less-than suc n₂)
同じ内容の判断をそれぞれのやり方で導出する。この辺も自動でできる。
_ : CompareNat1Judgement (zero is-less-than 2)
_ = L-TRANS (L-SUCC {0}) (L-SUCC {1})
_ : CompareNat2Judgement (zero is-less-than 2)
_ = L-ZERO {1}
_ : CompareNat3Judgement (zero is-less-than 2)
_ = L-SUCCR (L-SUCC {0})
導出システム EvalNatExp
続けて算術式の評価と簡約をやってみよう。 これもまずは形式―シンタクスの定義から始める。 次のようにExp型を定義する。
infix 10 `_
infixl 8 _+_
infixl 9 _*_
data Exp : Set where
`_ : ℕ → Exp
_+_ : Exp → Exp → Exp
_*_ : Exp → Exp → Exp
これはいわば抽象構文木を定義しているのだが、Agdaの演算子定義の自由度の高さによりほとんど構文そのもののように書ける。 ただし自然数のリテラルそのものをExp型とすることはできないので、それは前置バックティックのコンストラクタとした。
この算術式の評価を行う導出システムを次のように定義する。
-- EvalNatExp
infix 7 _⇓_
data _⇓_ : Exp → ℕ → Set where
E-CONST : ∀ {n : ℕ}
--------------
→ ` n ⇓ n
E-PLUS : ∀ {n₁ n₂ n : ℕ} {e₁ e₂ : Exp}
→ e₁ ⇓ n₁
→ e₂ ⇓ n₂
→ NatJudgement (n₁ plus n₂ is n)
--------------
→ e₁ + e₂ ⇓ n
E-TIMES : ∀ {n₁ n₂ n : ℕ} {e₁ e₂ : Exp}
→ e₁ ⇓ n₁
→ e₂ ⇓ n₂
→ NatJudgement (n₁ times n₂ is n)
--------------
→ e₁ * e₂ ⇓ n
評価は式のシンタクスと自然数の値の間の関係だからこの述語の型は Exp → ℕ → Set となる。
評価の例を次に挙げる。これらの例もCtrl+c, Ctrl+aで自動化できる。
_ : ` 0 + ` 2 ⇓ 2
_ = E-PLUS (E-CONST {0})
(E-CONST {2})
(P-ZERO {2})
_ : ` 2 + ` 0 ⇓ 2
_ = E-PLUS (E-CONST {2})
(E-CONST {0})
(P-SUCC (P-SUCC (P-ZERO {0})))
_ : ` 1 + ` 1 + ` 1 ⇓ 3
_ = E-PLUS (E-PLUS (E-CONST {1})
(E-CONST {1})
(P-SUCC (P-ZERO {1})))
(E-CONST {1})
(P-SUCC (P-SUCC (P-ZERO {1})))
導出システム ReduceNatExp
次に簡約のための導出システムを定義する。 簡約は式と式の間の関係だから型はExp → Exp → Setになる。
1ステップ分の簡約関係を表す_—→_を次のように定義する。
-- ReduceNatExp
infix 7 _—→_
data _—→_ : Exp → Exp → Set where
R-PLUS : ∀ {n₁ n₂ n₃ : ℕ}
→ NatJudgement (n₁ plus n₂ is n₃)
--------------
→ ` n₁ + ` n₂ —→ ` n₃
R-TIMES : ∀ {n₁ n₂ n₃ : ℕ}
→ NatJudgement (n₁ times n₂ is n₃)
--------------
→ ` n₁ * ` n₂ —→ ` n₃
R-PLUSL : ∀ {e₁ e′₁ e₂ : Exp}
→ e₁ —→ e′₁
--------------
→ e₁ + e₂ —→ e′₁ + e₂
R-PLUSR : ∀ {e₁ e₂ e′₂ : Exp}
→ e₂ —→ e′₂
--------------
→ e₁ + e₂ —→ e₁ + e′₂
R-TIMESL : ∀ {e₁ e′₁ e₂ : Exp}
→ e₁ —→ e′₁
--------------
→ e₁ * e₂ —→ e′₁ * e₂
R-TIMESR : ∀ {e₁ e₂ e′₂ : Exp}
→ e₂ —→ e′₂
--------------
→ e₁ * e₂ —→ e₁ * e′₂
評価の例を挙げる。これらも自動で導出できる。
_ : ` 2 * ` 3 + ` 0 * ` 4 —→ ` 6 + ` 0 * ` 4
_ = R-PLUSL {` 2 * ` 3} {` 6} {` 0 * ` 4}
(R-TIMES -- ` 2 * ` 3 —→ ` 6
(T-SUCC -- 2 times 3 is 6
(T-SUCC -- 1 times 3 is 3
(T-ZERO {3}) -- 0 times 3 is 0
(P-SUCC (P-SUCC (P-SUCC (P-ZERO {0}))))) -- 3 plus 0 is 3
(P-SUCC (P-SUCC (P-SUCC (P-ZERO {3})))))) -- 3 plus 3 is 6
_ : ` 2 * ` 3 + ` 0 * ` 4 —→ ` 2 * ` 3 + ` 0
_ = R-PLUSR {` 2 * ` 3} {` 0 * ` 4} {` 0}
(R-TIMES -- ` 0 * ` 4 —→ ` 0
(T-ZERO {4})) -- 0 times 4 is 0
ある式に複数回(ゼロ回以上)の簡約で別の(ゼロ回のときは同じ)式になるという関係は次のように表現する。
infix 7 _—*→_
data _—*→_ : Exp → Exp → Set where
MR-ZERO : {e : Exp}
--------------
→ e —*→ e
MR-ONE : {e e' : Exp}
→ e —→ e'
--------------
→ e —*→ e'
MR-MULTI : {e e' e'' : Exp}
→ e —*→ e'
→ e' —*→ e''
--------------
→ e —*→ e''
2 * 3 + 4 * 0 —*→ 6 + 0 を導出してみよう。 この辺まで来ると自動では導出できない。 また、かなり長くなるので1ステップずつ分解したほうがよいだろう。
lemma1 : ` 2 * ` 3 + ` 4 * ` 0 —→ ` 6 + ` 4 * ` 0
lemma1 = R-PLUSL {` 2 * ` 3} {` 6} {` 4 * ` 0}
(R-TIMES
(T-SUCC (T-SUCC T-ZERO
(P-SUCC (P-SUCC (P-SUCC P-ZERO))))
(P-SUCC (P-SUCC (P-SUCC P-ZERO)))))
lemma2 : ` 6 + ` 4 * ` 0 —→ ` 6 + ` 0
lemma2 = R-PLUSR
(R-TIMES
(T-SUCC (T-SUCC (T-SUCC (T-SUCC T-ZERO
P-ZERO)
P-ZERO)
P-ZERO)
P-ZERO))
これらの1ステップ簡約を組み合わせるともともと導出したかった判断が書ける。
_ : ` 2 * ` 3 + ` 4 * ` 0 —*→ ` 6 + ` 0
_ = MR-MULTI (MR-ONE lemma1) (MR-ONE lemma2)
先に定義した—→は簡約の仕方が一意に決まらないので非決定的簡約と言われる。 最後に五十嵐(2011)に従って簡約を決定的(1通りの導出に定まる)にしたシステムを示す。
infix 7 _—→ᵈ_
data _—→ᵈ_ : Exp → Exp → Set where
DR-PLUS : ∀ {n₁ n₂ n₃ : ℕ}
→ NatJudgement (n₁ plus n₂ is n₃)
--------------
→ ` n₁ + ` n₂ —→ᵈ ` n₃
DR-TIMES : ∀ {n₁ n₂ n₃ : ℕ}
→ NatJudgement (n₁ times n₂ is n₃)
--------------
→ ` n₁ * ` n₂ —→ᵈ ` n₃
DR-PLUSL : ∀ {e₁ e'₁ e₂ : Exp}
→ e₁ —→ᵈ e'₁
--------------
→ e₁ + e₂ —→ᵈ e'₁ + e₂
DR-PLUSR : ∀ {n₁ : ℕ} {e₂ e'₂ : Exp}
→ e₂ —→ᵈ e'₂
--------------
→ ` n₁ + e₂ —→ᵈ ` n₁ + e'₂
DR-TIMESL : ∀ {e₁ e'₁ e₂ : Exp}
→ e₁ —→ᵈ e'₁
--------------
→ e₁ * e₂ —→ᵈ e'₁ * e₂
DR-TIMESR : ∀ {n₁ : ℕ} {e₂ e'₂ : Exp}
→ e₂ —→ᵈ e'₂
--------------
→ ` n₁ * e₂ —→ᵈ ` n₁ * e'₂
infix 7 _—*→ᵈ_
data _—*→ᵈ_ : Exp → Exp → Set where
MR-ZERO : {e : Exp}
--------------
→ e —*→ᵈ e
MR-ONE : {e e' : Exp}
→ e —→ᵈ e'
--------------
→ e —*→ᵈ e'
MR-MULTI : {e e' e'' : Exp}
→ e —*→ᵈ e'
→ e' —*→ᵈ e''
--------------
→ e —*→ᵈ e''
lemma3 : ` 2 * ` 3 + ` 4 * ` 0 —→ᵈ ` 6 + ` 4 * ` 0
lemma3 = DR-PLUSL
(DR-TIMES
(T-SUCC (T-SUCC T-ZERO (P-SUCC (P-SUCC (P-SUCC P-ZERO))))
(P-SUCC (P-SUCC (P-SUCC P-ZERO)))))
lemma4 : ` 6 + ` 4 * ` 0 —→ᵈ ` 6 + ` 0
lemma4 = DR-PLUSR
(DR-TIMES
(T-SUCC (T-SUCC (T-SUCC (T-SUCC T-ZERO P-ZERO) P-ZERO) P-ZERO)
P-ZERO))
lemma5 : ` 6 + ` 0 —→ᵈ ` 6
lemma5 = DR-PLUS (P-SUCC (P-SUCC (P-SUCC (P-SUCC (P-SUCC (P-SUCC P-ZERO))))))
_ : ` 2 * ` 3 + ` 4 * ` 0 —*→ᵈ ` 6
_ = MR-MULTI (MR-MULTI (MR-ONE lemma3) (MR-ONE lemma4)) (MR-ONE lemma5)
JIRAやConfluenceのアドオンをGoogle App Engineで動かす [Java]
https://bitbucket.org/tkob/acspring-gcloud-quickstart
いまAtlassianのクラウド製品のアドオンを作るときはAtlassian Connectという作法に従って、Webアプリケーション(Atlassian製品の外で動作する)をアドオンとしてつくって製品と連携するということになっています。それをJavaで作るときはAtlassian Connect Spring BootというSpring BootベースのフレームワークがAtlassian公式として公開されています。
https://bitbucket.org/atlassian/atlassian-connect-spring-boot
JIRAアドオンを気軽に作ろうと思うとこれを動かすためのサーバーを見つけないといけません。ここで無料のサーバーで動かしたい…と思うと、今だとGCPのフリーティアーが候補になると思います。
1つの候補はCompute Engineのf1-microインスタンスを使うことですが、ここで問題になるのはAtlassian ConnectではHTTPS通信を必須としていることで、GCEの場合だと追加でドメイン取得が必要となります。
もう1つの可能性はApp Engineのスタンダード環境を使うことですが、(1) Spring BootはJava8以降が要件であること (2) フリーティアーで使えるストレージはCloud Datastoreしかない(Atlassian Connect Spring BootはSpring Dataを使ってインストール先ホストを保存するのだが、Cloud Datastore用のSpring Dataがない)という点が問題でした(appspot.comドメインはHTTPSが使えます)。
(1)については最近までGAEスタンダード環境ではJava7のみだったのが最近Java8対応したことで解消されました。(2)については自分で作ることで解消しました。1つ前の記事のSpring Data Google Cloud Datastoreがそれです。
手順にしたがってMavenアーキタイプからプロジェクトを作るとサンプルアプリが動くようになっていて、このアプリはJIRAから課題を取得してDatastoreに保存し、それを集計して表示するということをやっています(なお、Datastoreは集約関数が利用できないため本来こうした集計には向いていません。使い方の例としてそのようにしています)。
Spring Data Google Cloud Datastoreを作った。 [Java]
https://github.com/tkob/spring-data-gclouddatastore
その名の通りSpring Dataの作法でGoogle Cloud DatastoreのデータをCRUDするものです。クエリメソッド(インターフェイスにfindByFooOrderByBarなどメソッド定義するとそのメソッド名に従った実装を提供する機能)にも対応しています。
Isabelleの練習 - 命題論理の自然演繹 [Isabelle]
「PPLサマースクール2017 Isabelle/HOL による証明とプログラミング」 http://ppl.jssst.or.jp/index.php?ss2017 を受講しに行っていた。結果として自分がIsabelleを咀嚼するのはまだかかりそうだという感想だったが、もっと初歩的なことをやって練習していくことにしたい。
題材としては論理学の教科書に出てくるような自然演繹による証明をIsabelleでやってみることにする。
自然演繹というのは、命題論理の証明を「P,Q... |- R」のように前提P,Q,...から帰結Rが出てくるものとするとP,Q,...に対してあらかじめ用意されたルールを適用して変形することで最終的にRが出てくれば証明完了というものだ。
Isabellの証明はtheoryという構造の中に書く。jEditで次のようなファイルを作ってNaturalDeduction.thyというファイル名で保存する。
theory NaturalDeduction
imports Main
begin
(* ... *)
end
ファイル名とtheoryの名前は一致しなければならない。また、jEditは特に拡張子を自動でつけてくれないが、拡張子がないと証明ファイルとして認識されないので注意しなければならない。
"imports Main"とは何か、はよくわかっていないが気にしないことにする。#include <stdio.h>のようなものだろう。
コメントはMLスタイルで、「(*」と「*)」で囲む。
1つ目の例題として、"P∩Q, R |- Q∩R"を証明してみよう。なお、この記事で使う例題はすべてHuth and Ryan (2004) "Logic in Computer Science"から採っている。
これを証明するにはまずP∩QからQを取り出し(P∩Qが成立するということはQ単独でも成立する)、QとRからQ∩Rを作る(QとRが成立するということはQ∩Rも成立する)必要がある。
問題はIsabelleでそのようなルールが何という名前で提供されているかだが、既存の定理を探すにはfind_theoremsというコマンド(?)を使う。
find_theorems "_ ∧ _ ⟹ _"
find_theorems "_ ⟹ _ ∧ _"
このように書くと検索結果の最初のほうに出てくるconunct2とconjIが求めているものだとわかる。
HOL.conjunct2: ?P ∧ ?Q ⟹ ?Q
HOL.conjI: ?P ⟹ ?Q ⟹ ?P ∧ ?Q
さて、"P∩Q, R |- Q∩R"という定理を表明するにはこのように書けばいいようだ。
theorem Example_1_4:
(*fixes P Q*)
assumes 1: "P ∧ Q"
assumes 2: "R"
shows "Q ∧ R"
つまり前提をassumes、帰結をshowsのところに書く。前提はassumes 1: "P ∧ Q" and 2: "R"と書いてもいいようだ。
コメントアウトしているfixes P Qは「任意のPとQをとった時に」という意味だがこれは書かなくても暗黙の裡にそうなるそうだ。
「1:」とかいうのは前提などに後で使うための名前を付けている。
これだけだと問題を表現しただけで、証明ではない。証明は続けて書くのだが、こうなる。
proof-
have 3: "Q" using 1 by (rule conjunct2)
show 4: "Q ∧ R" using 3 2 by (rule conjI)
qed
proofのあとにハイフンをつけるのは…なんだっけ。セミナーで説明してもらったと思うのだがあまり理解できず、忘れてしまった。ともかくこの例ではハイフンを消すとエラーになる。
前提からこういう事実が導けますというのをhaveとかshowで宣言する。haveとshowの違いは、途中に来るのがhaveで最後に来る(証明したかった)ものがshowだと考えればよいようだ。
1から3はconjunct2で変形できるのでby (rule conunct2)になる。usingがIsabelle的にどういう機能なのかきちんと理解していないのだが、とりあえずこの例ではルールの引数を指定するようなイメージのものだと解釈できる。3と2を使ってconjIを使うと4が出せる。
なお、jEditのOutputパネルでProof stateを表示しておくとproofの先頭にカーソルを置くと
proof (state)
goal (1 subgoal):
1. Q ∧ R
と表示され、show 4:...の行末では
goal:
No subgoals!
となる。「No subgoals!になったらそこにqedと書く」と思っておけばよいようだ。
次に二重否定の除去(~~PからPを導く)と導入(Pから~~Pを導く)を扱う例を書きたい。
find_theorems "¬¬ _ ⟹ _"
theorem notnotI: "P ⟹ ¬¬P" by auto
検索により二重否定の除去はnotnotDが使えるとわかる。二重否定の導入は見つからなかったので独自に定理として作る。by autoで自動的に証明できてしまうのだが、それがなぜかは気にしないことにする。
これらを使うと"P, ~~(Q∩R) |- ~~P∩R"の証明が書ける。
theorem Example_1_5:
assumes 1: "P"
assumes 2: "¬¬(Q∧R)"
shows "¬¬P∧R"
proof-
have 3: "¬¬P" using 1 by (rule notnotI)
have 4: "Q∧R" using 2 by (rule notnotD)
have 5: "R" using 4 by (rule conjunct2)
show 6: "¬¬P∧R" using 3 5 by (rule conjI)
qed
次にmodus ponensとmodus tollensを使った証明をしたい。いずれもそのものはIsabelleの中にないようなので定理として作っておく。
theorem mp: "(P⟹Q) ⟹ P ⟹ Q" by auto
theorem mt: "(P⟹Q) ⟹ ¬Q ⟹ ¬P" by auto
"P⇒(Q⇒R), P, ~R |- ~Q"はMPとMTを順に適用することで証明できる。
theorem Example_1_7:
assumes 1: "P⟹(Q⟹R)"
assumes 2: "P"
assumes 3: "¬R"
shows "¬Q"
proof-
have 4: "Q⟹R" using 1 2 by (rule mp)
show 5: "¬Q" using 4 3 by (rule mt)
qed
次は==>を導入するような式変形ルールを使う。これはいままでのルールとはちょっと違って「Pを仮定したときにQが導けるならばP==>Qを導いてよい」というものだ。これをIsabelle上で行うには、"P==>Q"の証明の中でassume Pを使って最後にshow Qを行えばよい。
"~Q⇒P |- P⇒~~Q"を証明する例が次のものだ。
theorem Example_1_9:
assumes 1: "¬Q⟹¬P"
shows "P⟹¬¬Q"
proof-
assume 2: "P"
have 3: "¬¬P" using 2 by (rule notnotI)
show 4: "¬¬Q" using 1 3 by (rule mt)
qed
==>がいくつもあるような証明を行うときは入れ子構造になる。
theorem Example_1_11:
shows "(Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"
proof-
assume 1: "Q⟹R"
show "(¬Q⟹¬P) ⟹(P⟹R)"
proof-
assume 2: "¬Q⟹¬P"
show "P⟹R"
proof-
assume 3: "P"
have 4: "¬¬P" using 3 by (rule notnotI)
have 5: "¬¬Q" using 2 4 by (rule mt)
have 6: "Q" using 5 by (rule notnotD)
show 7: "R" using 1 6 by (rule mp)
qed
qed
qed
これは前提がないので"|- (Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"ということである。いままでhaveやshowで宣言した式の証明をするのにbyを使ってきたが、ここではbyの代わりに入れ子のproofを書いている。
ただし上の例はフラットに書いても同じことができる。
theorem Example_1_11':
shows "(Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"
proof-
assume 1: "Q⟹R"
assume 2: "¬Q⟹¬P"
assume 3: "P"
have 4: "¬¬P" using 3 by (rule notnotI)
have 5: "¬¬Q" using 2 4 by (rule mt)
have 6: "Q" using 5 by (rule notnotD)
show 7: "R" using 1 6 by (rule mp)
qed
連言、二重否定、条件とやったので今度は選言を使う。選言には「PがいえるならばP∪Qも言える」というもの(導入)と、「P∪Qが言えて、Pの場合とQの場合でいずれもRが導けるならば、Rを導いてよい」(除去)の2つがある。
前者はIsabelleに既にあり、後者はなかったので独自の定理を作る。
find_theorems "_ ⟹ _ ∨ _"
theorem disjE: "P∨Q ⟹ (P⟹R) ⟹ (Q⟹R) ⟹ R" by auto
これらを両方使うと"Q⇒R |- P∪Q ⟹ P∪R"の証明が書ける。
theorem Example_1_16:
assumes 1: "Q⟹R"
shows "P∨Q ⟹ P∨R"
proof-
assume 2: "P∨Q"
show "P∨R"
proof-
have 34: "P⟹(P∨R)"
proof-
assume 3: "P"
show 4: "P∨R" using 3 by (rule disjI1)
qed
have 57: "Q⟹(P∨R)"
proof-
assume 5: "Q"
have 6: "R" using 1 5 by (rule mp)
show 7: "P∨R" using 6 by (rule disjI2)
qed
show "P∨R" using 2 34 57 by (rule disjE)
qed
qed
次に"P⟹(Q⟹P)"を証明することを考えてみる。この場合Pは前提としているんだからQは関係なくPを前提しているということからそのままPが出てくるはずだ。Huth and Ryan (2004)ではこのルールをcopyと呼んでいる。適当に入力してあたりをつけてみたところ、Isabelleでは「by assupmtion」と書けばいいようだ。
theorem Example_copy:
shows "P⟹(Q⟹P)"
proof-
assume 1: "P"
show "Q⟹P"
proof-
assume 2: "Q"
show 3: "P" using 1 by assumption
qed
qed
次の証明では「Pと~Pが両方出てきたら矛盾している」と例の「矛盾からは何でも出てくる」を使う。前者はnotE、後者はFalseEとしてIsabelleで用意されている。
theorem Example_1_20:
assumes 1:"¬P∨Q"
shows "P⟹Q"
proof-
have a: "¬P⟹(P⟹Q)"
proof-
assume a2: "¬P"
show "P⟹Q"
proof-
assume a3: "P"
have a4: "False" using a2 a3 by (rule notE)
show "Q" using a4 by (rule FalseE)
qed
qed
have b: "Q⟹(P⟹Q)"
proof-
assume b2: "Q"
show "P⟹Q"
proof-
assume b3: "P"
show "Q" using b2 by assumption
qed
qed
show "P⟹Q" using 1 a b by (rule disjE)
qed
最後に「Pと仮定して矛盾が導かれるならばPではない(~Pを導ける)」を使う。これはIsabelleではnotIという名前である。
theorem Example_1_21:
assumes 1: "P⟹Q"
assumes 2: "P⟹¬Q"
shows "¬P"
proof-
have 36: "P⟹False"
proof-
assume 3: "P"
have 4: "Q" using 1 3 by (rule mp)
have 5: "¬Q" using 2 3 by (rule mp)
show 6: "False" using 5 4 by (rule notE)
qed
show "¬P" using 36 by (rule notI)
qed
以上Isabelleで命題論理の自然演繹の証明をいくつか書いてみた。「~のようだ」が多い記事になったことは申し訳なく思う。
CSV parsing for Standard ML [SML]
Standard ML用の新しいXMLパーサー [SML]
Standard ML用のXMLパーサーを作った。
SMLの世界にはSMLで書かれたXMLパーサーが(知っている範囲では)すでに2つある。 1つはfxpという、かなり昔からあるもので、これはDTDの検証も行うフルセットのXML1.0準拠もの、 もう1つはSMLNJ-LIBの中にあるXMLストラクチャで、これはかなり非力なものだ。
UXMLは非検証のXMLプロセッサーとしてXML1.0になるべく準拠しようとしている。
現段階ではUTF-8しか受け入れない点と𐀀
以上の文字を受け入れない点
(これはUXMLが依存しているSMLNJ-LIBのUTF8ストラクチャの制約)、
そしてXML1.0の整形条件違反のかなりの部分を報告しない(受け入れてしまう)点が
非準拠であるが、現実的な処理では十分に使える状態になっていると思う。
他の2つのXMLプロセッサーにない点として、 名前空間をサポートしている点と、XPathライクなナビゲーションAPIを持つ点がある。
使用するにはタグv.0.1.0を取得するか、Smackageから利用してほしい。
Smackageを使う場合、.smackage/sources.localにuxml git git://github.com/tkob/uxml.git
という行を追加し、SML/NJのCMファイルからは`$SMACKAGE/uxml/v0.1.0/uxml.cm
のように参照する。
REPLのセッションをそのまま単体テストにする [Rehearsal]
REPLを持ったプログラミング言語処理系における原始的かつボトムアップな開発手順について考えよう。
まず小さな関数(だとか)を書く。 思った通りにかけているだろうか? そこでREPLを起動してソースをロードし、関数に対して入力を与え、結果を見る。 正常系は問題ない。 そこで異常な入力に対するハンドリングを関数内に追加して、異常処理がうまくいくことを見る。 でもさっきの正常系の処理が変わったりしていないだろうか。 そこでESCに続けてkを何度か押して(またはCtrl+Pを何度か押して)履歴から正常系の入力の式を復元してもう1回確認してみる。 関数の実装がちょっと気に入らないので変更する。 さっきまで動いていた分はまだ正しく動くだろうか。 そこでまた履歴から入力式を復元して叩いてみる。
この試行錯誤の中には「テスト」をしている箇所がある。 でもそれは揮発的だ。 REPLの履歴とプログラマの短期記憶の中だけにあって、しばらくすると消えてしまう。
テスト駆動開発、あるいは単に「単体テストを書く」ことは不揮発なテストによってコードの品質を保とうとする習慣である。 そこではREPLでアドホックにテストをするのではなくてテスティングフレームワークの定める形でテストコードを書く。 テストはことあるごとに自動で繰り返し実行される。 コードの変更が何かを壊していたらすぐにわかるし、いま現在のコードがすべてのテストを通過しているという確証を得ることができる。
では我々はそもそも最初からREPLなんて使うべきではなかったのだろうか。
長期的に見てテスティングフレームワークを使用すべきことは明らかだ。 でもREPLにも良い点はある。敷居の低さだ。 REPL上の作業ではプログラム実行とプログラマの頭の中は実際には 「とにかく入力を与えてみて、結果を見る。その次に結果が妥当かどうかを考え、妥当であればよしとする」 という関係になっている場合が多い。 これはある種の教義を信奉する人にとっては悪い習慣とみなされるだろうが、 ともかく「良い習慣」より敷居が低いことは事実だ。
問題はREPL上の作業とテスティングフレームワークで単体テストを書くこととの間の距離だ。 敷居の低いREPLで行った「テスト」を不揮発にしたくなった段階で、その距離が問題になる。 さっきまでのREPLに打っていた式ではなくて、テスティングフレームワーク上のアサーションを書かなければならなくなるのだ。
Rehearsal は、ここにフィットするテスティングフレームワークだ。 Rehearsalにおける単体テストはREPLのセッションそのものである。 例えばSML/NJでgreet.smlというテスト対象のプログラムを作り、次のようなREPLセッションを行ったとする。
このセッションを不揮発にするには、コピーアンドペーストで次のファイルを作る。
これを t/greet.t
というファイル名で保存したとすると、テストを再実行するには次のコマンドを打つ。
このコマンドはもちろんMakefileなどに書いておけばよい。
RehearsalはREPLがなんであるかは問わない。シェルでもよいしPythonでもScalaでもよい。 出力はPerlのTAPという形式に従っているが、JUnit XML形式の出力ができるのでJenkinsなどに集計させることもできる。
Reharsalのテストスクリプトの文法はMarkdownに合わせている。 だからドキュメントとしてのテストを書いて読みやすい形式に変換することもできるし、 「Markdownで書かれたその言語のチュートリアル」をそのままテストとして実行することもできる。 (例: Ruby, Python)
REPLをそのままテストにすることの良い副作用として、プリティプリンタが得られる点がある。 例えばSMLでは(Javaのような言語とは違って)値を文字列に変換する関数は一般的には手に入らず、自分で書かなければならない。 また、SMLのテスティングフレームワークであるSMLUnitでは、 テストが失敗した場合の表示のためにアサートする値に対してプリティプリンタをセットで与えなければならない (期待値と実際の値の比較をエラーメッセージの中に含むために使われる)。 これは合理的ではあるもののREPLと単体テストの間の距離を一層離すことにつながっている。
一方でSMLでもREPLを使うならばそのような面倒くささはない。 REPLは自身のプリティプリンタによって値を表示していて、 プログラマがREPLでテストをするときはREPLが出してくれたものを目で見て妥当性を判断しているからだ。
このようにRehearsalのアプローチはREPLの気軽さを損ねずに自動的な回帰テストの利点を取り入れることができる。 こうした方法が「とにかく自動的な回帰テストを回し始める最初の一歩」を容易にすると考えている。