データ型とパターン

構造体を使用すれば、複数の独立したデータをひとまとまりにしてまったく新しい型をつくることができます。値の集まりをグループ化する構造体のような型は直積型(product types)と呼ばれます。ただし、多くのドメイン概念は構造体として自然に表現できません。例えば、アプリケーションによっては、ドキュメントの所有者であるユーザー、ドキュメントを編集できるユーザー、ドキュメントの閲覧しかできないユーザーなどユーザーのアクセス権限を追う必要があるかもしれません。電卓であれば、加算、減算、乗算のような二項演算子があります。構造体で複数の選択肢を表現する簡単な方法はありません。

同様に、構造体は決まったフィールドの集まりを追跡する優れた方法ですが、多くのアプリケーションでは任意個の要素を含むことができるデータが必要です。ツリーやリストなどの古典的なデータ構造のほとんどは再帰的な構造を持っています。リストの先頭を除いた部分自体がリストになっていますし、二分木の左右の枝自体が二分木です。前述の電卓の例でいえば、式の構造自体が再帰的です。例えば、加算式内の足される式自体が乗算式であることがあります。

選択することができるデータ型は直和型(sum types)と呼ばれ、それ自体のインスタンスを含めることができるデータ型は再帰データ型(recursive datatypes)と呼ばれます。再帰直和型は、それらに関する文を証明するために数学的帰納法を使用できるため、帰納的データ型(inductive datatypes)と呼ばれます。プログラミングの際、帰納的データ型はパターンマッチングと再帰関数を通じて使用されます。

標準ライブラリでは、組み込み型の多くは実際には帰納的データ型です。例えば、Bool は帰納的データ型です。

inductive Bool where
  | false : Bool
  | true : Bool

この定義には2つの主要な部分があります。初めの行は新しい型の名前(Bool)を提供し、残りの行はそれぞれコンストラクタを記述します。構造体のコンストラクタと同様、帰納的データ型のコンストラクタは、任意の初期化コードやバリデーションコードを挿入する場所ではなく、単なる他のデータのレシーバおよびコンテナにすぎません。構造体とは異なり、帰納的データ型は複数のコンストラクタを持つ可能性があります。今の例では、true と false という2つのコンストラクタがあり、どちらも引数を取りません。構造体宣言がそのフィールドの名前を、宣言された型と同名の名前空間に配置するのと同様に、帰納的データ型はそのコンストラクタの名前を名前空間に配置します。Lean 標準ライブラリでは、true と false はこの名前空間から再エクスポートされるため、それぞれ Bool.true と Bool.false としてではなく、単独で記述できます。

データモデリングの観点から見ると、帰納的データ型が使用される場面の多くは、他の言語における抽象クラスが使用される場面と同じです。C# や Java のような言語では、同様の Bool の定義を書くことができます。

abstract class Bool {}
class True : Bool {}
class False : Bool {}

ただし、これらの表現の詳細はかなり異なります。特に、各非抽象クラスは、新しい型と新しいデータ割り当て方法の両方を作成します。オブジェクト指向の例では、True と False は両方とも Bool よりも具体的な型ですが、Leanでの定義では新しい型 Bool のみが導入されます。

非負整数の型 Nat は帰納的データ型です。

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

ここで、zero は0を表し、succ は他の数値の後続値を表します。succ の宣言で言及されている Nat は、まさにこれから定義しようとしている Nat 型です。後続値(Successor)は「1つ大きい」を意味するため、5の後続値は6、32,185の後続値は32,186です。この定義を使用すると、4はNat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))として表されます。この定義は、名前が異なるだけで Bool の定義に似ています。唯一の本当の違いは、succ の後に (n : Nat) が続くことです。これは、コンストラクタ succ が n という名前の Nat 型の引数を取ることを指定します。名前 zero と succ は、その型と同名の名前空間内にあるため、それぞれ Nat.zero と Nat.succ として参照する必要があります。

n などの引数名は、Lean のエラーメッセージや数学で証明を行うときに提供されるフィードバックに出現することがあります。Lean には、引数を名前で指定するためのオプションの構文もあります。ただし、引数名が API に占める部分はあまり大きくないため、一般に引数名の選択は構造体のフィールド名の選択ほど重要ではありません。

C# または Java では、Nat は次のように定義できます:

abstract class Nat {}
class Zero : Nat {}
class Succ : Nat {
  public Nat n;
  public Succ(Nat pred) {
	n = pred;
  }
}

以前の Bool の例と同様に、これは対応する Lean での定義よりも多くの型を定義します。さらにこの例は、Lean のデータ型コンストラクタが、C# や Java のコンストラクタというよりも抽象クラスのサブクラスに近いことを示唆しています。これは、ここで示されているコンストラクタには、初期化時に実行されるコードが含まれているためです。

直和型は、TypeScript で文字列タグを使用して判別共用体(discriminated unions)を実装することにも似ています。TypeScript では、Nat は次のように定義できます。

interface Zero {
    tag: "zero";
}

interface Succ {
    tag: "succ";
    predecessor: Nat;
}

type Nat = Zero | Succ;

C# や Java と同様に、Zero と Succ はそれぞれ独立した型であるため、この実装では Lean よりも多くの型が含まれることになります。また、Lean のコンストラクタが中身を識別するタグを含む JavaScript または TypeScript のオブジェクトに対応することも示しています。

パターンマッチング

多くの言語では、この種のデータは、最初に instance-of 演算子を使用してどのサブクラスを受け取ったかを確認し、次に与えられたサブクラスで使用可能なフィールドの値を読み取るというように使用されます。instance-of によるチェックは実行するコードを決定し、フィールド自体がデータを提供しながら、このコードで必要なデータが利用可能であることを確認します。Lean では、これらの目的は両方ともパターンマッチングによって同時に達成されます。

パターンマッチングを使用する関数の例として次の isZero を見ましょう。これは、引数が Nat.zero の場合に true を返し、それ以外の場合は false を返す関数です。

def isZero (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => false

match 式には、デストラクトのために関数の引数 n が与えられます。n がコンストラクタ Nat.zero からくる場合、マッチパターンの最初の分岐が選択され、結果はtrue になります。n がコンストラクタ Nat.succ からくる場合、2番目の分岐が選択され、結果は false になります。

isZero Nat.zero の評価は、段階的には次のように進められます。

isZero Nat.zero
===>
match Nat.zero with
| Nat.zero => true
| Nat.succ k => false
===>
true

isZero 5 の評価も同様に行われます。

isZero 5
===>
isZero (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))))
===>
match Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))) with
| Nat.zero => true
| Nat.succ k => false
===>
false

isZero のパターンの2番目の分岐の k は飾りではありません。これにより、succ の引数である Nat が与えられた名前で表示されます。そのより小さい数値を使用して、式の最終結果を計算できます。

ある自然数 \(n\) の後続の数が \(n\) より1大きい(つまり、\(n+1\) )のと同じように、ある数の前の数はその数より 1 小さな数です。pred をある Nat の前の数を見つける関数としたとき、次の例の結果は期待通りでしょう。

#eval pred 5

4

#eval pred 839

838

Nat は負の数を表すことができないため、0 は少し難問です。通常、Nat を使用する場合、普通なら負の数を生成する演算子は 0 を生成するように再定義されます。

#eval pred 0

0

Nat の前者関数を作る最初のステップは、与えられた数を作るためにどのコンストラクタが使用されたかを確認することです。それが Nat.zero だった場合、結果は Nat.zero になります。それが Nat.succ だった場合、その下の Nat を参照するために名前 k が使用されます。そして、この Nat が求めたかった前者であるため、Nat.succ 分岐の結果は k になります。

def pred (n : Nat) : Nat :=
  match n with
  | Nat.zero => Nat.zero
  | Nat.succ k => k

この関数を 5 に適用すると、次の手順が出てきます。

pred 5
===>
pred (Nat.succ 4)
===>
match Nat.succ 4 with
| Nat.zero => Nat.zero
| Nat.succ k => k
===>
4

パターンマッチングは、直和型だけでなく構造体でも使用できます。たとえば、Point3D から \(z\) 座標を取り出す関数は次のように記述できます。

def depth (p : Point3D) : Float :=
  match p with
  | { x:= h, y := w, z := d } => d

この場合、単に z アクセサを使用する方がはるかにシンプルですが、構造体パターンが関数を記述する最もシンプルな方法になる場合もあります。

再帰関数

定義しようとしている名前を参照する定義は、再帰的定義(recursive definitions)と呼ばれます。帰納的データ型は再帰的に書くことができます。実際、succ は別のNat を要求するため、Nat はそのようなデータ型の例です。再帰データ型は、いくらでも大きなデータを表すことができます。制限は使用可能なメモリなどの技術的要因だけです。データ型の定義時に自然数ごとに1つのコンストラクターを書き下すのが不可能であるのと同じく、可能なすべてのパターンマッチのケースを書き出すことも不可能です。

再帰データ型は、再帰関数によって適切に補完されます。Nat に対する単純な再帰関数の例として、引数が偶数かどうかをチェックする次のような関数を考えましょう。このとき、zeroは偶数です。このように、コードの非再帰分岐を基底ケース(base cases)と呼びます。奇数の後続は偶数であり、偶数の後続は奇数です。これは、succ で作られた数は、その引数が偶数でない場合にのみ偶数であることを意味します。

def even (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (even k)

この思考パターンは、Nat 上の再帰関数を記述する場合に典型的なものです。まず、zero に対して何をすべきかを特定します。次に、任意の Nat の結果をその後続に対する結果に変換する方法を決定し、この変換を再帰呼び出しの結果に適用します。このパターンは構造的再帰(structural recursion)と呼ばれます。

多くの言語とは異なり、Lean はデフォルトで、すべての再帰関数が最終的に基本ケースに到達することを保証します。プログラミングの観点から見ると、これにより偶発的な無限ループが排除されます。ただし、この機能は定理証明で特に重要です。定理証明では、無限ループが大きな問題を引き起こすからです。たとえば、Lean は同じ数に対して再帰的に自身を呼び出そうとするバージョンの even は受け入れません。

def evenLoops (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (evenLoops n)

エラーメッセージには、再帰関数が常に基本ケースに到達するかどうかを(実際到達しないが故に) Lean が判断できなかったと書かれています。

fail to show termination for
  evenLoops
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'evenLoops' does not take any (non-fixed) arguments

加算には2つの引数が必要ですが、パターンマッチする必要があるのはそのうちの1つだけです。数 \(n\) に0を足した和は、\(n\) そのものです。\(k\) の後続数を \(n\) に加えた和は、\(k\) を \(n\) に加えた結果の後続数です。

def plus (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => n
  | Nat.succ k' => Nat.succ (plus n k')

plus の定義では、引数 k と関連があるが同一ではないことを示すために k' という名前を選びました。たとえば、plus 3 2 の評価を実行すると、次の手順で行われます。

plus 3 2
===>
plus 3 (Nat.succ (Nat.succ Nat.zero))
===>
match Nat.succ (Nat.succ Nat.zero) with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k')
===>
Nat.succ (plus 3 (Nat.succ Nat.zero))
===>
Nat.succ (match Nat.succ Nat.zero with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k'))
===>
Nat.succ (Nat.succ (plus 3 Nat.zero))
===>
Nat.succ (Nat.succ (match Nat.zero with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k')))
===>
Nat.succ (Nat.succ 3)
===>
5

加算 \(n + k\) は、Nat.succ を \(n\) に \(k\) 回適用したものだと見なせます。同様に、乗算 \(n × k\) は \(n\) を \(n\) 自身に \(k\) 回加算したものだと見なせますし、減算 \(n - k\) は \(n\) の前者を \(k\) 回取ったものだと見なせます。

def times (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => Nat.zero
  | Nat.succ k' => plus n (times n k')

def minus (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => n
  | Nat.succ k' => pred (minus n k')

すべての関数が構造的再帰を使用して簡単に記述できるわけではありません。加算は Nat.succ の反復、乗算は加算の反復、減算は前者関数の反復として理解できるので、除算は減算の反復として実装可能であることが示唆されます。この場合、分子が除数より小さい場合、結果はゼロになります。それ以外の場合、結果は「分子から除数を引いた値を除数で除算したもの」の後者になります。

def div (n : Nat) (k : Nat) : Nat :=
  if n < k then
    0
  else Nat.succ (div (n - k) k)

2番目の引数が 0 でない限り、このプログラムは常に基本ケースに向かって進むため、終了します。しかし、「ゼロに対する返り値を記述し、より小さい Nat での結果をその後続の結果に変換するパターン」に従っていないため、構造的再帰ではありません。特に、関数の再帰呼び出しは、入力コンストラクタの引数ではなく、別の関数呼び出し(今回であれば引き算)の結果に適用されます。したがって、Lean は次のメッセージを表示してこの関数を拒否します。

fail to show termination for
  div
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    div (n - k) k

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    div (n - k) k

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

このメッセージは、div の再帰が停止することを手動で証明する必要があると言っています。このトピックについては、最終章で説明します。