| title | tags | author | slide |
|---|---|---|---|
Coq で半環 |
Coq |
mathink |
false |
- Coq で半環を定義した
- 足し算とかけ算で半環になることを示した。
- 自然数に ∞ を追加して、その上で最小値と足し算が半環になることを示した。
「へー、 Coq で半環定義して遊べるんだー」
前半のコードの解説はしません。 読めば大体わかるような書き方をしてい(るつもりではあり)ますが、何か質問があれば https://twitter.com/mathink までお寄せください。
基本的に順番通りにコードをコピペすれば動きます。 また、全部ひっくるめたやつを https://gist.github.com/mathink/fe8f36b9cca0697fc5b5 に置きました。
Setoid をベースにして議論を行ないます。 半環を定義する前に、必要な道具である
- Setoid :: 同値関係を等価性と見做して扱う構造
- Map :: Setoid の間のモルフィズム
- Binop :: Setoid 上の二項演算
- Associative など :: Binop に関する性質
- Monoid :: Setoid ベースのモノイド
を定義します。一気にどうぞ。 とりあえず、必要なものがここに書いてあるんだなぁと思ってくれれば OK です。
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.
Structure Setoid :=
{
carrier:> Type;
equal: relation carrier;
prf_Setoid:> Equivalence equal
}.
Existing Instance prf_Setoid.
Notation Setoid_of eq := (@Build_Setoid _ eq _).
Notation "(== :> S )" := (equal (s:=S)).
Notation "(==)" := (== :> _).
Notation "x == y" := (equal x y) (at level 70, no associativity).
Notation "x == y :> S" := (equal (s:=S) x y)
(at level 70, y at next level, no associativity).
Class isMap (X Y: Setoid)(f: X -> Y) :=
map_subst:> Proper ((==) ==> (==)) f.
Structure Map (X Y: Setoid) :=
{
map_body:> X -> Y;
prf_Map:> isMap map_body
}.
Existing Instance prf_Map.
Notation makeMap f := (@Build_Map _ _ f _).
Notation "[ x .. y :-> p ]" :=
(makeMap (fun x => .. (makeMap (fun y => p)) ..))
(at level 200, x binder, y binder, right associativity,
format "'[' [ x .. y :-> '/ ' p ] ']'"): map_scope.
Delimit Scope map_scope with map.
Class isBinop (X: Setoid)(op: X -> X -> X) :=
binop_subst:> Proper ((==) ==> (==) ==> (==)) op.
Structure Binop (X: Setoid) :=
{
binop:> X -> X -> X;
prf_Binop:> isBinop binop
}.
Existing Instance prf_Binop.
Class Associative `(op: Binop X): Prop :=
associative:>
forall (x y z: X), op x (op y z) == op (op x y) z.
Class LIdentical `(op: Binop X)(e: X): Prop :=
left_identical:> forall x: X, op e x == x.
Class RIdentical `(op: Binop X)(e: X): Prop :=
right_identical:> forall x: X, op x e == x.
Class Identical `(op: Binop X)(e: X): Prop :=
{
identical_l:> LIdentical op e;
identical_r:> RIdentical op e
}.
Existing Instance identical_l.
Existing Instance identical_r.
Coercion identical_l: Identical >-> LIdentical.
Coercion identical_r: Identical >-> RIdentical.
Class LInvertible `{Identical X op e}(inv: Map X X): Prop :=
left_invertible:>
forall (x: X), op (inv x) x == e.
Class RInvertible `{Identical X op e}(inv: Map X X): Prop :=
right_invertible:>
forall (x: X), op x (inv x) == e.
Class Invertible `{Identical X op e}(inv: Map X X): Prop :=
{
invertible_l:> LInvertible inv;
invertible_r:> RInvertible inv
}.
Coercion invertible_l: Invertible >-> LInvertible.
Coercion invertible_r: Invertible >-> RInvertible.
Class Divisible `(op: Binop X)(divL divR: Binop X): Prop :=
{
divisible_l:>
forall (a b: X), op (divL a b) a == b;
divisible_r:>
forall (a b: X), op a (divR a b) == b
}.
Class Commute `(op: Binop X): Prop :=
commute:>
forall a b, op a b == op b a.
Module Monoid.
Class spec (M: Setoid)(op: Binop M)(e: M) :=
proof {
associative:> Associative op;
identical:> Identical op e
}.
Structure type :=
make {
carrier: Setoid;
op: Binop carrier;
e: carrier;
prf: spec op e
}.
Module Ex.
Existing Instance associative.
Existing Instance identical.
Existing Instance prf.
Notation isMonoid := spec.
Notation Monoid := type.
Coercion associative: isMonoid >-> Associative.
Coercion identical: isMonoid >-> Identical.
Coercion carrier: Monoid >-> Setoid.
Coercion prf: Monoid >-> isMonoid.
Delimit Scope monoid_scope with monoid.
Notation "x * y" := (op _ x y) (at level 40, left associativity): monoid_scope.
Notation "'1'" := (e _): monoid_scope.
End Ex.
End Monoid.
Export Monoid.Ex.Module と Class と Structure、そして Export の合わせ技は慣れると(私にとっては)読み易いんですが、慣れてないとどうなんでしょう？
こうやってベターっと載せるのは、反感をk
以上の道具を用いて半環の定義を行います。
半環は、加法については可換なモノイドの、乗法については(可換とは限らない)モノイドの構造を持った代数系であり、更に加法についての単位元 0 が乗法の零元になっているものです。
この条件をそのまま書き下せば Coq においても半環が定義できます。
spec が 半環であること を記述している部分です。
Module SemiRing.
Class spec (S: Setoid)(add: Binop S)(z: S)(mul: Binop S)(e: S) :=
proof {
add_monoid: isMonoid add z;
add_commute:> Commute add;
mul_monoid: isMonoid mul e;
zero_l:
forall a: S, mul z a == z;
zero_r:
forall a: S, mul a z == z
}.
Structure type :=
make {
carrier: Setoid;
add: Binop carrier;
z: carrier;
mul: Binop carrier;
e: carrier;
prf: spec add z mul e
}.
Module Ex.
Existing Instance add_monoid.
Existing Instance add_commute.
Existing Instance mul_monoid.
Existing Instance prf.
Notation isSemiRing := spec.
Notation SemiRing := type.
Coercion add_commute: isSemiRing >-> Commute.
Coercion carrier: SemiRing >-> Setoid.
Coercion prf: SemiRing >-> isSemiRing.
Delimit Scope semiring_scope with srng.
Notation "x + y" := (add _ x y): semiring_scope.
Notation "x * y" := (mul _ x y): semiring_scope.
Notation "'0'" := (z _): semiring_scope.
Notation "'1'" := (e _): semiring_scope.
End Ex.
Import Ex.
End SemiRing.
Export SemiRing.Ex.
最後の方にある記法の定義は大切なのでよく見ておきましょう。 こういった記号はとても乱用されるので、スコープで制限して時と場合に応じて使い分けられるようにしています。 モノイドでも同じことをやっているので、参照してみてください。
半環の定義を記述できたので実際に半環を構成してみましょう。 一つ目はわかりやすい例、足し算とかけ算です。
証明は省略していきますが、どれも簡単なので大丈夫です。
とりあえず Arith ライブラリをインポートしておきましょう。
以降、既に示されている性質を使えば証明が楽になるためです(省略しますが)。
Require Import Arith.
さて、これから半環を構成していきます。
まず、nat が Setoid であることを述べておきます。
Canonical Structure nat_setoid := Setoid_of (@eq nat).
等価性は Coq が標準で提供している = で構いません。
次に、足し算が nat_setoid 上の二項演算となっていることを述べましょう。
一般に、 Setoid 上での演算は等価性について well-defined でなければなりませんから、この確認は必要です。
今回は等価性が = なので、 Program コマンドを使えば証明は大体 Coq がやってくれます。
Program Instance plus_is_binop: isBinop (X:=nat_setoid) plus.
Canonical Structure plus_binop := Build_Binop plus_is_binop.
そして、足し算が 0 を単位元とするモノイドとなることを以下で示します。 省略していますが、モノイド則に対応したゴールが二つ生成されるので、証明が必要です。
Program Instance plus_is_monoid: isMonoid plus_binop 0.
かけ算についても同様に、二項演算であることを確かめたのち、1 を単位元とするモノイドになっていることを示します。
Program Instance mult_is_binop: isBinop (X:=nat_setoid) mult.
Canonical Structure mult_binop := Build_Binop mult_is_binop.
Program Instance mult_is_monoid: isMonoid mult_binop 1.
これで半環を構成する準備が大体出来ました。 以下のように半環の定義をしていきます。
大体、というのは、半環は加法について可換ですので、最後に足し算の可換性についての証明が必要になるからです。
すごく簡単なので特に触れません(plus_comm を apply すりゃいいです)。
Program Instance plus_mult_is_semiring: isSemiRing plus_binop 0 mult_binop 1.
Canonical Structure plus_mult_semiring: SemiRing := SemiRing.make plus_mult_is_semiring.
ついでに零元に関する証明も生じますが、これまた簡単なので省略です。
これで、足し算とかけ算のなす半環の構成が終わりました。
作ったので試してみましょう。 ちょっとした準備として、次の省略記法を用意しておきます。
Notation pms := plus_mult_semiring.
以下で幾つかの計算を行なっています。
加法と乗法がそれぞれ足し算とかけ算なので、本当に半環としての計算が行なわれているのか心配になるでしょうが、計算の結果が pms、先程定義した半環になっているので、どうやら問題はなさそうです。
Open Scope semiring_scope.
Compute (3 + 2).
(* = 5 *)
(* : pms *)
Compute (3 * 2).
(* = 6 *)
(* : pms *)
Compute (0 + 4).
(* = 4 *)
(* : pms *)
Compute (0 * 4).
(* = 0 *)
(* : pms *)
二つ目の例は、最小値を取る演算を加法、足し算を乗法とした半環です。 min-plus 代数とかトロピカル半環とか呼ばれる構造です。
この時利用するのは通常の自然数ではなく、自然数に ∞ を加えた構造を利用します。 ですので、まずはこれを表す型を定義しましょう。
Inductive nat_inf :=
| num: nat -> nat_inf
| inf: nat_inf.
Notation "! n" := (num n) (at level 0).
nat_inf は inf という新たなコンストラクタと、通常の自然数をラップする num というコンストラクタから構成されています。
これは option nat と同型なのですが、そのまま option nat を使ってしまうと実際に計算を行うときにちょっと面倒なことになるので、このように新たな型を定義しておきます。
その面倒の説明はここでは割愛しておきます。とりあえず、タイプ量が増えて見た目が悪くなるのです。
また、記法を簡略化するために !n で num n を表せるようにしておきます。
まずは最小値と足し算の定義です。
nat を拡張して nat_inf を作ったので、min と plus もそれに合わせて拡張する必要があります。
考えるべきところは inf が関わる場合のみで、そうでなければ元の演算を使えばよいです。
Require Import Min.
Definition min_inf (n m: nat_inf): nat_inf :=
match n, m with
| inf, _ => m
| _, inf => n
| !n, !m => !(min n m)
end.
Definition plus_inf (n m: nat_inf): nat_inf :=
match n, m with
| inf, _ | _, inf => inf
| !n, !m => !(plus n m)
end.
演算を定義したので、前の例と同様の流れで半環構造を与えていきます。
まず、 nat_inf を通常の = で Setoid と見做します。
Canonical Structure nat_inf_setoid := Setoid_of (@eq nat_inf).
次に、 min_inf、最小値演算が二項演算であり、 inf を単位元とするモノイドであることを示します。
Program Instance min_inf_is_binop: isBinop (X:=nat_inf_setoid) min_inf.
Canonical Structure min_inf_binop := Build_Binop min_inf_is_binop.
Program Instance min_inf_is_monoid: isMonoid min_inf_binop inf.
また、 plus_inf も二項演算であり、 !0 を単位元とするモノイドです。
Program Instance plus_inf_is_binop: isBinop (X:=nat_inf_setoid) plus_inf.
Canonical Structure plus_inf_binop := Build_Binop plus_inf_is_binop.
Program Instance plus_inf_is_monoid: isMonoid plus_inf_binop !0.
以上の事実を利用することで、最小値と足し算による半環が構成できました。
Program Instance min_plus_is_semiring: isSemiRing min_inf_binop inf plus_inf_binop !0.
Canonical Structure min_plus_semiring := SemiRing.make min_plus_is_semiring.
せっかく構成したので試してみましょう。 前回同様に省略記法を導入しておきます。
Notation mps := min_plus_semiring.
そして、以下が計算結果たちです。
+ が最小値に、 * が足し算になっていることがわかると思います。
また、 inf も上手く機能していることもわかります。
Open Scope semiring_scope.
Compute (!3 + !2).
(* = !(2) *)
(* : mps *)
Compute (!3 * !2).
(* = !(5) *)
(* : mps *)
Compute (!1 + !2).
(* = !(1) *)
(* : mps *)
Compute (!1 * !2).
(* = !(3) *)
(* : mps *)
Compute (inf + !4).
(* = !(4) *)
(* : mps *)
Compute (inf * !4).
(* = inf *)
(* : mps *)
Compute (!0 + inf).
(* = !(0) *)
(* : mps *)
Compute (!0 * inf).
(* = inf *)
(* : mps *)
Coq で半環を定義して、実例を二つ構成して使ってみました。
なお、この二つの半環は併用(というか、足し算かけ算の半環の計算結果を最小値足し算の半環に流用)できます。
こんな感じに色々面白い計算が書けそうですね。
Compute (!(5 + 2) + !6).
(* = !(6) *)
(* : mps *)
Compute (inf * !(3 + 1)).
(* = inf *)
(* : mps *)
ただし、足し算かけ算の半環を定義していなくても同じものが書けます。
Coercion を使うことで '!' をつけずに書くことが、概ね、できるようになります。 以下の例を見れば「概ね」の意味もわかることでしょう。
Coercion num: nat >-> nat_inf.
Notation "x '|' X" := (x:X) (at level 15, no associativity, format "x '|' X").
Compute (!3 + 2).
(* = !(2) *)
(* : mps *)
Fail Compute (3 * !2).
Compute (3|mps * 2).
(* = !(5) *)
(* : mps *)
Compute (1|mps + inf).
(* = !(2) *)
(* : mps *)
Compute (inf * 0).
(* = inf *)
(* : mps *)
Compute ((4 * 3)|mps + inf).
(* = !(12) *)
(* : mps *)
Compute (0 + (4 * 3)).
(* = 12 *)
(* : pms *)
+ や * がどの半環での演算なのかは第一引数で推論されます。
ゆえに、第一引数が数の場合、pms 上の演算と見做されてしまうために、第二引数が mps の数だと型が合わないというエラーが起きてしまいます。
ですから、第一引数が inf ならそういう心配はないのですが、大抵の場合 mps だと明示しなければなりません。
結局、 ! を使ったほうがよいということになるのですね。
ちなみに x|X というのは x:X の結合度を上げるためのものです。
そうしないと、 3|mps * 2 を (3:mps) * 2 と書かなければならなくなります。