前回は自然数とその上の足し算を定義しました。 今回は、自然数の性質についての証明をどのようにAgdaで書いていくかをやります。

型と命題、項と証明

自然数の定義はこうでした。

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

これは次のように、公理を課している読むこともできます。

  1. $0$ は自然数である
  2. $n$ が自然数のとき、 $\mathrm{suc}(n)$ ($=n+1$) も自然数である

あるものが自然数である、と言うためには、この２つのルールしか使わない、 ということを課したということになります。 つまり、その証明は、この２つのルールを組み合わせたものです。 例えば、$3$ が自然数であるということには、

  • $0$ は自然数である (ルール1)
  • よって、ルール2より、$0+1 = 1$ は自然数である
  • さらにルール2より、$2$ は自然数である
  • さらにルール2より、$3$ は自然数である

という証明がつけられます。 そしてこれは、そのまま次のような項として表せます。

  • zero : Nat
  • suc zero : Nat
  • suc (suc zero) : Nat
  • suc (suc (suc zero)) : Nat

ルール1を適用したことを zero 、ルール2を適用したことを suc という記号を使って表すのです。 証明は項によって表すことができ 1、さらに、ある項は証明を表していると 考えることができます。 このような、

型つきの項 ↔ 命題の証明

という対応を、 カリーハワード同型 といいます。

依存型と述語

項に依存する型を依存型といいます。これだけだとわかりにくいので、噛み砕いて言います。

suc は項を受け取って項を返します。いわゆる普通の関数はこれです。 Haskellには、型を受け取って型を返すものがあります。たとえば Maybe や IO 、 [] (リストのやつ)などがそうです。これらは型関数と言われることもあります。 Haskellのポリモーフィズムは（普通はそうは考えませんが）型を受け取って項を返す 存在だといえます。 例えば id : a -> a は、Int 型の引数を与えるとき、型 Int を（暗黙に）受け取って id : Int -> Int という項(ラムダ式の項)になります。

依存型は、項を受け取って型を返す 存在です。これはHaskellにはありません。 例えばこんなのがかけます。

data Even : Nat -> Set where
  zeroIsEven : Even zero
  soIsTwoAdded : ∀ {n} -> Even n -> Even (suc (suc n))

依存型に対応する論理の対象は、述語です。 Even n という型は、n は偶数であると読みます。偶数であることの証明で使えるルールは

  1. $0$ は偶数である
  2. どんな $n$ に対しても、$n$ が偶数ならば、$n+2$ も偶数である

の２つで、これを次のように表します。

  1. zeroIsEven は Even 0 の証明
  2. soIsTwoAdded は 任意の n に対して Even n であることから Even (suc (suc n))を導く

Even n は n によって値をもったりもたなかったりすることに注意してください。 例えば zeroIsEven : Even 0 と soIsTwoAdded : Even 0 -> Even 2 を使って soIsTwoAdded zeroIsEven : Even 2 を作ることはできますが、 Even 1 という型をもった値は作れません。 これは、Even 1 という命題が偽である(i.e. 証明が作れない)ということに対応しています。

再帰と帰納法

自然数の順序の述語 $\leq$ を考えます。

data _≤_ : Nat -> Nat -> Set where
  z≤n : ∀ {n} -> zero ≤ n
  s≤s : ∀ {n m} -> n ≤ m -> suc n ≤ suc m

これは次のように読みます。

  1. どんな自然数 $n$ に対しても、$0 \le n$ である
  2. $n \le m$ ならば $n + 1 \le m + 1$ である

この順序がちゃんと反射律を満たしていることを証明してみましょう。 Agda で書く前に、普通の数学で証明してみます。帰納法で証明します。

$\forall n. n \le n$を示したい。 まず、ルール1より、$0 \le 0$ である。 $n$ で$n \le n$ が成り立つと仮定すると、$n + 1$について、 ルール2より、$n + 1 \le n + 1$ である。 よって、帰納法により、すべての $n$ について、$n \le n$.

これを Agda で書くと、以下のようになります。

reflexive : ∀ n -> n ≤ n
reflexive zero    = z≤n
reflexive (suc n) = s≤s (reflexive n)

∀ n は n : _ の略記なので（_ は型推論により Nat になる）、 reflexive : (n : Nat) -> n ≤ n と書いても同じです。

suc n のとき、reflexive n を再帰的に使っていることに注意してください。 これは、$n + 1$ の証明に $n$ のときの仮定を使っていることに対応します。

例えば、reflexive 3 (3 ≤ 3 の証明になる) を計算するとき、

  1. reflexive (suc 2) にパターンマッチされ、s≤s (reflexive 2) になる
  2. reflexive 2 が reflexive (suc 1) にパターンマッチされ、s≤s (reflexive 1) になる
  3. reflexive 1 が reflexive (suc zero) にパターンマッチされ、s≤s (reflexive zero) になる
  4. reflexive zero が z≤n になる

というふうになり、その値は s≤s (s≤s (s≤s (z≤n))) となり、 確かにその型は 3 ≤ 3 となっています。

つまり、帰納法の証明は、再帰関数によって行えるのです。

まとめ

駆け足で Agda での証明を説明しました。かなり説明不足な部分があると思うので、 わからないところはコメントでお願いします。

参考文献

  1. 細かいことを言うと、項によって表せる証明は直観主義論理のものに限られます。 ↩