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) 

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 ⟩

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

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 ⟩ ⟩

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

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 + ` 22
_ = E-PLUS (E-CONST {0})
           (E-CONST {2})
           (P-ZERO {2})

_ : ` 2 + ` 02
_ = E-PLUS (E-CONST {2})
           (E-CONST {0})
           (P-SUCC (P-SUCC (P-ZERO {0})))

_ : ` 1 + ` 1 + ` 13
_ = 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)

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

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