「Coqの型クラスの使い方：バンドル方式とアンバンドル方式」で紹介したスピターズ／ファンデル・ウィーゲンのアンバンドル方式の実例をモノイド以外にもうひとつ。半環（semiring）をやってみます。"Type Classes for Mathematics in Type Theory"にある例を簡略化して紹介します。
アンバンドル方式に全面的に賛同しているわけではないのですが、使ってみないとメリット・デメリットが分からないのでやってみました。アンバンドル方式の背後にあると思われる名付けの問題点とか、ソフトウェアシステム一般における名前の悩みとかについても記してあります。
法則の準備
Definition Op (A: Set) := A->A->A.
↑は、A上の二項演算の型を Op A と書けるようにするだけです。A上の二項演算（Op A のインスタンス）に関する法則を準備しておきます。結合律、左単位律、右単位律、可換律、ベキ等律です。今回は中置演算子記号を導入することはしません。
Definition Associative {A: Set} (op: Op A) := forall(x y z: A), op x (op y z) = op (op x y) z. Definition UnitLeft {A: Set} (op: Op A) (u: A) := forall(x: A), op u x = x. Definition UnitRight {A: Set} (op: Op A) (u: A) := forall(x: A), op x u = x. Definition Commutative {A: Set} (op: Op A) := forall(x y: A), op x y = op y x. Definition Idempotent {A: Set} (op: Op A) := forall(x: A), op x x = x.
スピターズ／ファンデル・ウィーゲンは、DefinitionではなくてClassを使っています。次のような感じ。
Class Associative' {A: Set} (op: Op A) := associative: forall(x y z: A), op x (op y z) = op (op x y) z.
DefinitionとClassの差はよく分かってません。クラスにはなんかメリットがあるのでしょうが、クラスを使うと、クラス名とフィールド名の2つの名前が増えるのがなんかイヤ。そうでなくても、名前管理は頭が痛いのに。
基本的な代数構造の定義
半環の定義に先立って、半群、モノイド、可換モノイド（アーベルモノイド）を定義しておきます。
Class Semigroup {A: Set} (op: Op A) := { assoc: Associative op }. Class Monoid {A: Set} (op: Op A) (u: A) := { monoid__semigroup:> Semigroup op; unit_l: UnitLeft op u; unit_r: UnitRight op u }. Class AbMonoid {A: Set} (op: Op A) (u: A) := { ab_monoid__monoid:> Monoid op u; comm: Commutative op }.
フィールドの使い方は二種類あります。assoc, unit_l, unit_r, commのフィールドは対応する法則を記述するためのフィールドです。法則は事前に名前を定義しておいたので、名前にパラメータを渡すだけで済みます。monoid__semigroup, ab_monoid__monoidのフィールドは、部分構造を識別するフィールドです。「モノイドは半群だよね」「可換モノイドはモノイドだよね」という事情を表しています。
記号「:>」は部分構造のフィールドにつけるとよいらしいですが、僕には正体不明です。型強制（coercion）だと思い込んでいたのですが、違います。型強制では説明できないのは確かです。
余談ですが、Coqの名前はUnicord文字が使えて便利なんですが、'-', '?', '!', '>' などは名前に使えないようです。Unicode文字の非名前文字のチェックもちゃんとやってます。部分構造のフィールド名を monoid->semigroup にしたかったのですがダメでした。部分構造のフィールド名は、忘却関手の名前と思えるので矢印を入れると雰囲気が出るんですけど。
閑話休題： monoid__semigroup, ab_monoid__monoid のようなフィールドを通じて、クラスのあいだに階層構造を設定することが容易なのがクラスを使うメリットです。構造のあいだの多重継承みたいなもんだと理解してもいいでしょう。でも、オブジェクト指向との類似性を追求しても得られるものはないと思います。
分配律の定義
結合律、左単位律、左右の単位律、可換律、ベキ等律は単一の二項演算に対する法則でしたが、分配律には2つのニ項演算が登場します。演算子記号を定義してないので見づらいですが、次が分配律。
Definition DistributiveLeft {A: Set} (op1 op2: Op A) := forall(x y z: A), op2 x (op1 y z) = op1 (op2 x y) (op2 x z). Definition DistributiveRight {A: Set} (op1 op2: Op A) := forall(x y z: A), op2 (op1 x y) z = op1 (op2 x z) (op2 y z).
半環の定義
事前の準備をしてきたので、半環の定義はコンパクトです。
Class Semiring {A: Set} (sum: Op A) (z: A) (mult: Op A) (u: A) := { semiring_sum__ab_monoid:> AbMonoid sum z; semiring_mult__monoid:> Monoid mult u; distrib_l: DistributiveLeft sum mult; distrib_r: DistributiveRight sum mult }.
半環を構成する素材は、バラバラなパラメータとしてクラスに渡します。このバラバラさが「アンバンドル」という呼び名の由来です。
- {A: Set} -- 台集合 A （暗黙パラメータ）
- (sum: Op A) -- A上の二項演算sum（足し算）
- (z: A) -- Aの要素z（ゼロ）
- (mult: Op A) -- A上の二項演算mult（掛け算）
- (u: A) -- Aの要素u（イチ）
足し算と掛け算の法則は、既に定義されている可換モノイド構造AbMonoidと（可換とは限らない）モノイド構造Monoidから“継承”します。
- semiring_sum__ab_monoid により、sumとz（足し算とゼロ）は可換モノイドである。
- semiring_mult__monoid により、multとu（掛け算とイチ）はモノイドである。
半環固有の法則として、sumとmult（足し算と掛け算）に対する左右の分配律を追加します。
- distrib_l -- 左分配律
- distrib_r -- 右分配律
足し算が可換なので、どちらか一方でも済みますが、対称性から左右とも入れておきました。
実例の定義
次の実例（インスタンス）を定義してみます。
- bool上のandb演算とtrueによるモノイド実例
- bool上のorb演算とfalseによるモノイド実例
- bool上のorb演算とfalseによる可換モノイド実例（可換律の証明を加える）
- bool上のandb演算とtrueとorb演算とfalseによる半環実例
Require Import Bool. (* 参考： https://coq.inria.fr/library/Coq.Bool.Bool.html andb_assoc andb_true_l andb_true_r andb_comm orb_assoc orb_false_l orb_false_r orb_comm andb_orb_distrib_r andb_orb_distrib_l *) Instance andbMonoid : Monoid andb true. Proof. split. split. unfold Associative. intros. apply andb_assoc. split. unfold UnitRight. intros. apply andb_true_r. Defined. Instance orbMonoid : Monoid orb false. Proof. split. split. unfold Associative. intros. apply orb_assoc. split. unfold UnitRight. intros. apply orb_false_r. Defined. Instance orbAbMonoid : AbMonoid orb false := {| ab_monoid__monoid := orbMonoid |}. Proof. unfold Commutative. intros. apply orb_comm. Defined. Instance orb_andbSemiring : Semiring orb false andb true := {| semiring_sum__ab_monoid := orbAbMonoid; semiring_mult__monoid := andbMonoid (* 自動検索可能 *) |}. Proof. unfold DistributiveLeft. intros. apply andb_orb_distrib_r. (* Boolライブラリでは、rとlが逆になっている *) unfold DistributiveRight. intros. apply andb_orb_distrib_l. (* Boolライブラリでは、rとlが逆になっている *) Defined.
補足と考察
今回はノーテーションを使わなかったのですが、アンバンドル方式はノーテーションと相性が良くて、演算子オーバーロードが広範囲に使えます。
構造の素材をパラメータで渡すので、複雑な構造になるとパラメータの数は増えます。例えば、ベクトル空間をクラスにするなら、そのパラメータは次のようになります。
- スカラー体の台集合
- スカラー体の足し算
- スカラー体のゼロ
- スカラー体の符号反転（単項マイナス）
- スカラー体の掛け算
- スカラー体のイチ
- スカラー体の逆数（マイナスイチ乗）
- ベクトル可換群の台集合
- ベクトル可換群の足し算
- ベクトル可換群のゼロ
- ベクトル可換群の符号反転（単項マイナス）
2つのベクトル空間のあいだの準同型射を定義するなら、ベクトル空間2つ分だけで22個のパラメータ、ドヒャー。これでは堪らないので、色々な技巧を使ってパラメータを減らす工夫をします。頑張って明示パラメータを減らすと、暗黙に渡るパラメータが何だったか分からなくなったりします。このあたりが、アンバンドル方式のなんか残念なところです。
アンバンドル方式は、Coqが抱えている問題に対するワークアラウンドじゃないのかな、と思います。なので、あちらを立てればこちらが立たず、みたいな。Coqが抱えている問題とは、（おそらく）名前を局所化・相対化できないことです。記述の規模が大きくなると、膨大な名前を管理しなくてはなりません。人間には耐えられない数の名前になります。ほぼ唯一の局所的な名前がパラメータ名なんですね。パラメータ名なら大域名前空間を気にせずに同じ名前を違う場所で使える。パラメータとして渡したモノの名前ならオーバーロードできる（フィールド名はオーバーロードできない）。だからなんでもパラメータにする、というストーリーでしょう、たぶん。
また余談ですが、名前の増加にはシンドイ思いをしたので、人間が使うシステムではいかにして名前の個数を減らせるかはとても重要な課題だと思っています。共通の性質・構造を持つモノを同じ名前で呼べることは、ものすごい節約・効率化・汎用化につながります。
ソースコード
(* -*- coding: utf-8 -*- *) Definition Op (A: Set) := A->A->A. Definition Associative {A: Set} (op: Op A) := forall(x y z: A), op x (op y z) = op (op x y) z. Definition UnitLeft {A: Set} (op: Op A) (u: A) := forall(x: A), op u x = x. Definition UnitRight {A: Set} (op: Op A) (u: A) := forall(x: A), op x u = x. Definition Commutative {A: Set} (op: Op A) := forall(x y: A), op x y = op y x. Definition Idempotent {A: Set} (op: Op A) := forall(x: A), op x x = x. Class Semigroup {A: Set} (op: Op A) := { assoc: Associative op }. Class Monoid {A: Set} (op: Op A) (u: A) := { monoid__semigroup:> Semigroup op; unit_l: UnitLeft op u; unit_r: UnitRight op u }. Class AbMonoid {A: Set} (op: Op A) (u: A) := { ab_monoid__monoid:> Monoid op u; comm: Commutative op }. Definition DistributiveLeft {A: Set} (op1 op2: Op A) := forall(x y z: A), op2 x (op1 y z) = op1 (op2 x y) (op2 x z). Definition DistributiveRight {A: Set} (op1 op2: Op A) := forall(x y z: A), op2 (op1 x y) z = op1 (op2 x z) (op2 y z). Class Semiring {A: Set} (sum: Op A) (z: A) (mult: Op A) (u: A) := { semiring_sum__ab_monoid:> AbMonoid sum z; semiring_mult__monoid:> Monoid mult u; distrib_l: DistributiveLeft sum mult; distrib_r: DistributiveRight sum mult }. Require Import Bool. (* 参考： https://coq.inria.fr/library/Coq.Bool.Bool.html andb_assoc andb_true_l andb_true_r andb_comm orb_assoc orb_false_l orb_false_r orb_comm andb_orb_distrib_r andb_orb_distrib_l *) Instance andbMonoid : Monoid andb true. Proof. split. split. unfold Associative. intros. apply andb_assoc. split. unfold UnitRight. intros. apply andb_true_r. Defined. Instance orbMonoid : Monoid orb false. Proof. split. split. unfold Associative. intros. apply orb_assoc. split. unfold UnitRight. intros. apply orb_false_r. Defined. Instance orbAbMonoid : AbMonoid orb false := {| ab_monoid__monoid := orbMonoid |}. Proof. unfold Commutative. intros. apply orb_comm. Defined. Instance orb_andbSemiring : Semiring orb false andb true := {| semiring_sum__ab_monoid := orbAbMonoid; semiring_mult__monoid := andbMonoid (* 自動検索可能 *) |}. Proof. unfold DistributiveLeft. intros. apply andb_orb_distrib_r. (* Boolライブラリでは、rとlが逆になっている *) unfold DistributiveRight. intros. apply andb_orb_distrib_l. (* Boolライブラリでは、rとlが逆になっている *) Defined.
