SSブログ

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という補題を証明する。これは次のようなものだ。

  1. If v is a value of type Bool, then v is either true or false.
  2. 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と呼ばれていて、それぞれ

  1. 型がついたTermはValueになっているか、さもなくば必ず簡約が存在する
  2. 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)

nice!(0)  コメント(0) 

nice! 0

コメント 0

コメントを書く

お名前:
URL:
コメント:
画像認証:
下の画像に表示されている文字を入力してください。

この広告は前回の更新から一定期間経過したブログに表示されています。更新すると自動で解除されます。