SSブログ
JIRAやConfluenceのアドオン..｜Agdaによる「プログラミング言語の基礎.. ブログトップ

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)

2020-08-16 21:24  nice!(0)  コメント(0) 

nice! 0

コメント 0

コメントを書く

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

JIRAやConfluenceのアドオン..｜Agdaによる「プログラミング言語の基礎.. ブログトップ

--


シリーズ記事

Essentials of Programming Languages (EOPL)


ScalaCheck を試す


OCaml vs. Scala


Tcl 8.5 の新機能

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