Rainy Day Codings：So-net blog

	ブログをはじめるログイン

2020年08月16日｜ 2020年08月22日｜2020年08月23日ブログトップ

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 ⟩

加算の場合。まずは２つの構成要素の算術式に再帰的に定理を適用する。

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

最終的には１つのペアノ自然数に簡約されてほしいわけだから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 ⟩