帰納法と再帰

自然数やリストの構造を使って、無限個の場合を扱います。

15.1 Nat は二つの構成子からできる

自然数 Nat は、零の Zero と、ひとつ大きい自然数 Succ(n) で組み立てられます。Nat は最初から入っている帰納型で、定義は次のとおりです。

inductive Nat: Type {
  Zero: Nat
  Succ(n: Nat): Nat
}

この定義で、0、1、2、... を、有限回の構成子の適用として表せます（2 は Succ(Succ(Zero)) で、数のリテラル 2 とも書けます）。帰納法は、Zero の場合と Succ(k) の場合に分けて、すべての自然数を扱う技術です。

15.2 まずは加算で考える

標準ライブラリ std/Nat.taut にある、「零を左に足しても数は変わらない」という定理を、自分で書いてみます。plus は、+ と同じ演算の別名です。

import std::Nat
import std::Std

theorem add_zero_left(n: Nat): plus(Zero, n) = n {
  match n: plus(Zero, n) = n {
    Zero => Refl
    Succ(k) => Eq::congr(Succ, add_zero_left(k))
  }
}

✓ theorem add_zero_left : ∀ n: Nat. plus(Zero, n) = n

tauto check src/ch15-add.taut

match n: 命題 { ... } の : のあとは、n ごとに変わる、証明したい命題です。基底部の Zero では、両辺が計算で一致するので Refl です。帰納段階の Succ(k) では、より小さい k について同じ定理 add_zero_left(k) を呼んで帰納法の仮定を手に入れ、Eq::congr(Succ, ...) で両側を一つ増やします。

15.3 帰納法は「有限回の反復」ではない

ここで示したのは、0 からいくつかの数を試した、という事実ではありません。自然数のすべての構造について成り立つ証明を、構築しています。これが、大量のテストと証明の本質的な違いです。

ただし、プログラムを実行するときの固定幅の整数は、自然数 Nat と違って上限があります。証明した性質を実行時の整数に移すときは、変換やオーバーフローの条件を別に考える必要があります。

15.4 構造再帰と整礎再帰

Tauto には、パターンの一部への呼び出しで進む構造再帰と、呼び出しのたびに量が小さくなることを証明して進む整礎再帰があります。後者では、decreasing_by measure(...) と、減少の証明を使います。

import std::WellFounded
import std::Nat

fn id_nat(n: Nat): Nat { n }

fn half(n: Nat): Nat decreasing_by measure(id_nat) => theorem half::eq {
  match n: Nat {
    Zero => Zero
    Succ(m) => match m: Nat {
      Zero => Zero
      Succ(k) => Succ(half(k, Nat::le_succ(k)))
    }
  }
}

✓ def id_nat : (Nat) -> Nat
✓ def half : (Nat) -> Nat

half は n を二つずつ減らすので、「直下の子だけを見る」単純な再帰ではありません。再帰呼び出し half(k, Nat::le_succ(k)) の末尾の引数が、「k は元の n より小さい」という証明です。=> theorem half::eq は、half の定義を表す定理を生成します。

再帰呼び出しに証明を渡さないと、カーネルが受理しません。

演習 15.1：リストの長さを数える関数は、リストの構造に関する帰納法と、どのように対応しているでしょうか。