はじめに
ある婚活パーティでは、参加者はそれぞれカップルになりたい人の候補者の名前を書き、お互いに名前を書いた者同士の中からカップルが成立するという方式をとっています。
そこで本記事では、この婚活パーティにおけるカップル生成アルゴリズムが正しい仕様を満たしているかどうかを形式検証ツールの1つであるCoq/SSReflectで実装し、検証します。
特に、生成されたカップルが本当にお互いの名前を書いているのか等、カップル生成アルゴリズムが満たすべき仕様を満たしていることを数学的に証明します。
プログラム全体のソースコード及び証明はこちらにあります。
問題設定
本記事で仮定する「婚活パーティ」のルールを以下に定義します。
婚活パーティのルール
有限の参加者を２つのグループTとSに分けます。
(一般的には女性と男性ですが、LGBTなどの問題を考慮し、ここでは単にグループTとSと呼ぶことにします。)
それぞれの参加者は、一通り他の参加者と会話をしたのち、各参加者は自分が所属していないグループの中から、カップルになりたいと思う人の名前をカップリング希望用紙に複数人書き、婚活パーティの運営者に提出します。
すなわちグループTに所属する人はグループSに所属する人の名前を書き、グループSに所属する人はグループTに所属する人の名前を書きます。
ここで、名前を書く人数に制限はなく、全員でも0人でも構いません。
婚活パーティの運営者は参加者全員のカップリング希望用紙を回収したのち、これらを以下を入出力とするカップル生成アルゴリズムに入力します。
カップル生成アルゴリズムの入出力
- [入力]：参加者全員のカップリング希望用紙
-
[出力]：グループ
Tに所属する人とグループSに所属する人によるペアのリスト
このアルゴリズムの出力として与えられた二人をカップルとして認定します。
その後、誰かとカップルになった参加者にはそれぞれカップルになった相手の名前を伝えて婚活パーティは終了です。
ここで、カップル生成アルゴリズムで出力されるカップルの組み合わせは誰でも良いわけではなく、以下の仕様を満たさなければいけません。
カップル生成アルゴリズムの仕様
- [健全性] 出力されたカップルの相手は、互いにカップリング希望用紙に名前を書いた人であること。
- [一意性] 各参加者に対し、カップル成立する相手はたかだか1人であること。つまり2人以上の人とはカップル成立しないこと。
- [極大性] 互いにカップリング希望用紙に名前を書いているにも関わらず、どちらも誰ともカップル成立しないという状況にはならないこと。言い換えると、カップリング希望用紙にお互いの名前を書いている2人がいた場合、少なくてもどちらか1人は誰かとカップル成立していること。
本記事では、これらの仕様をそれぞれカップル生成アルゴリズムの「健全性」「一意性」「極大性」と呼ぶことにします。
特に極大性は、まさに健全性と一意性を満たすペアの部分集合の包含関係における極大性を主張しています。
さらに、場合によっては以下の仕様も仮定する場合があります。
カップル生成アルゴリズムの追加仕様
- **[優先順位極小性]**カップリング希望用紙にカップリングしたい人の「優先順位」があり、優先順位が上位の人が優先してカップリングする。
ここでいう「優先順位」とは具体的には何か、また「優先順位が上位の人がカップリングする」とは何かが曖昧で、多くのこの方針の婚活パーティではこの詳細が明かされていないです。
そこで、本記事では、この仕様を満たす「優先順位」とは何か、「優先順位が高い人がカップリングする」とは何かを考え、数学的に証明します。
カップル生成アルゴリズムの型
上記の問題設定をもとに、形式検証ツールの１つであるCoq/SSReflectでカップル生成アルゴリズムを実装します。
まずカップル生成アルゴリズムmkCouple'の型を考えます。
具体的には以下のように記述することができます。
Variable (T S:finType).
Check mkCouple'.
(* mkCouple' : (T -> seq S) -> (S -> seq T) -> seq (T * S) *)
T S:finTypeがグループTとSに所属する人の型を表していて、それぞれ有限集合1なのでfinTypeで定義しています。
また、T -> seq SがグループTに所属する人のカップリング希望用紙を表していて、S -> seq Tがその逆です。
具体的には、引数ft:T -> seq Sに対し、グループTに所属する参加者t:Tがカップリング希望用紙に書いた名前のリストがft t:seq Sです。
これらを入力にとって、返すのがTとSのペアのリストなので、返り値の型はseq (T * S)になっています。
しかしながら、追加の仕様を考えるために、型を以下のように変更します。
Variable (R:rel (nat * nat)).
Variable (T S:finType).
Check mkCouple.
(* mkCouple : (T -> seq S) -> (S -> seq T) -> seq (T * S * (nat * nat)) *)
定数R : rel (nat * nat)が追加されていて、返り値がseq (T * S)から(T * S * (nat * nat))になっています。
これはマッチングする優先順位を表していて、追加の仕様である**[優先順位極小性]**を満たすアルゴリズムとして定義する場合に必要になります。
具体的には、返り値(t,s,(nt,ns))に対し、参加者tはカップリング希望用紙のnt番目にsの名前を書いていて、sはns番目にtの名前を書いたことを表しています。このペア(nt,ns)を優先順位と見て、その上の順序関係をRとしているわけです。
ちなみに最初のmkCouple'は
Definition mkCouple' ft fs := map fst (mkCouple (fun _ _ => false) ft fs)
とmkCoupleから定義できます。
カップル生成アルゴリズムの仕様を記述する
カップル生成アルゴリズムmkCoupleは上で説明したような仕様を満たさなければいけません。そこで、それぞれの仕様を形式的に記述します。
健全性
- [健全性] 出力されたカップルの相手は、互いにカップリング希望用紙に名前を書いた人であること。
Lemma mkCouple_kindness (ft:T -> seq S) (fs:S -> seq T) t s nt ns :
(t,s,(nt,ns)) \in mkCouple ft fs -> (t \in fs s) && (s \in ft t).
(t,s,(nt,ns)) \in mkCouple ft fsが出力されたカップルであり、特にtとsによるカップルを表しています。
それぞれカップリング希望用紙に名前があることは、tの希望用紙がft tであり、sの希望用紙がfs sであるため、それぞれt \in fs sとs \in ft tで表せます。
一意性
- [一意性] 各参加者に対し、カップル成立する相手はたかだか1人であること。つまり複数人とはカップル成立しないこと。
Lemma mkCouple_uniquel (ft:T -> seq S) (fs:S -> seq T) t s s' nt nt' ns ns':
(t,s,(nt,ns)) \in mkCouple ft fs ->
(t,s',(nt',ns')) \in mkCouple ft fs ->
[/\ s = s', nt = nt' & ns = ns'].
Lemma mkCouple_uniquer (ft:T -> seq S) (fs:S -> seq T) t t' s nt nt' ns ns':
(t,s,(nt,ns)) \in mkCouple ft fs ->
(t',s,(nt',ns')) \in mkCouple ft fs ->
[/\ t = t', nt = nt' & ns = ns'].
(t,s,(nt,ns))と(t,s',(nt',ns'))がtに対する2つのカップルです。
これが一致することを表現すればいいので、結論が[/\ s = s', nt = nt' & ns = ns']になっています。
これをsに対しても同様に記述します。
極大性
- [極大性] 互いにカップリング希望用紙に名前を書いているにも関わらず、どちらも誰ともカップル成立しないという状況にはならないこと。言い換えると、カップリング希望用紙にお互いの名前を書いている2人がいた場合、少なくてもどちらか1人は誰かとカップル成立していること。
Lemma mkCouple_maximal (ft:T -> seq S) (fs:S -> seq T) t s:
(t \in fs s) && (s \in ft t) ->
has (fun m => (m.1.1 == t) || (m.1.2 == s)) (mkCouple ft fs).
**[極大性]**の後者の表現で定義します。
(t \in fs s) && (s \in ft t)がtとsがお互いにカップリング希望用紙を名前を書いていることを表していて、このとき、m.1.1 = tまたはm.1.2 = sを満たすカップルmが出力されていること、すなわち、tかsのどちらか1人は誰かとカップルになっていることを表しています。
優先順位極小性
- **[優先順位極小性]**カップリング希望用紙にカップリングしたい人の「優先順位」があり、優先順位が上位の人が優先してカップリングする。
Hypothesis (Htrans: transitive R).
Lemma mkCouple_minimal (ft:T -> seq S) (fs:S -> seq T) t s:
(t \in fs s) && (s \in ft t) ->
has (fun m => ((m.1.1 == t) || (m.1.2 == s)) &&
let x := (index s (ft t), index t (fs s)) in
(R x m.2 ==> R m.2 x))
(mkCouple ft fs).
命題としては極大性よりも強い主張をしています。
極大性の命題と同様に、(t \in fs s) && (s \in ft t)がtとsがお互いにカップリング希望用紙を名前を書いていることを表していて、
(m.1.1 == t) || (m.1.2 == s)すなわち、tかsのどちらかが所属するカップルmが出力されることを表しています。
さらにこのカップルmの優先順位m.2は、sとt同士のペアの優先順位であるx := (index s (ft t),index t (fs s))より真に大きくならないことをR x m.2 ==> R m.2 xによって主張しています。
つまり優先順位が高い人がマッチングすることを優先順位を表す二項関係が極小であることとして定義するわけです。
ここで、小さくなることではなく、真に大きくならないことと定義しているのは、優先順位を決定する二項関係Rを広く取るためです。
小さくなること、つまりmが最小の優先順位であることをいうためには、少なくても最小値の存在性、すなわち任意の優先順位が比較可能でなければなりません。
しかしながら、Rに全順序を仮定するのは強すぎます。
特に、ここで使うRには一般には反対称律を仮定する必要はないです。
なぜならば、Rに反対称律を仮定したとしても、2つのカップルc1 := (t1,s1,(nt1,ns1))とc2 := (t2,s2,(nt2,ns2))に対し、それぞれの優先順位(nt1,ns1)と(ns1,ns2)が等しかったとしてもc1 = c2は一般に成り立たたないからです。
例えば、異なるt1とt2のカップリング希望順位1位がそれぞれ異なるs1とs2でかつs1とs2の希望順位1位がそれぞれt1とt2であるとき、カップル(t1,s1)、(t2,s2)の優先順位はどちらも(1,1)になりますが、t1 != t2でありs1 != s2なので、Rをカップル上の順序として見たときには反対称律は成り立ちません。
したがって、元々のR自体に反対称律を仮定することはあまり意味をなさないです。
優先順位極小性を成り立たせるための「優先順位」の十分条件
実は、Rは推移律だけを仮定すればこの命題を証明することができ、これを満たす任意の「優先順位」で**[優先順位極小性]**が成り立つことが言えます。
推移律だけ仮定した順序においても、任意の有限部分集合において極小値、すなわち任意の要素よりも真に大きくはない値の存在性が言えるため、こちらを表す命題R x m.2 ==> R m.2 xで定義しているというわけです。
ちなみに全擬順序、つまり比較可能性と推移性を満たす二項関係ならば、極小値が最小値になり、真に大きくないことと小さいことが同値になります。
(ただしペアに対する反対称律が一般に成り立たないので、最小値の一意性が一般に成り立たないことに注意。)
優先順位極小性が成り立つ「優先順位」の例
例としては以下のようなものが挙げられます。
- 自然数上の辞書式順序。例えばグループ
Tの順位を優先し、それが等しいときにグループSの順位を優先させる二項関係。全順序になる。 - 自然数上の積順序。つまり
(nt,ns) <= (nt',ns')をnt <= nt'かつns <= ns'で定義する二項関係。半順序になる。 - 優先順位
(nt,ns)に対し、それらの和nt+nsで比較する二項関係。反対称律は満たさないが比較可能性を満たす。 - 任意の
x y:nat * natに対してR x y = falseを満たす二項関係R。任意のペアに対して順序がつかず、クイックソートしてもリストの並びが変わらないので、この二項関係を使うことによって事実上、優先順位極小性を仮定しないカップル生成アルゴリズムとみなすことができる。
カップル生成アルゴリズムの実装
カップル生成アルゴリズムを実装はシンプルです。
まず、全ての互いに名前を書いたペアのリストを生成する関数pairsを作り、
これらを順序Rでクイックソート関数qsortを使ってソートします。
最後に、同じ人がいるペアをのぞく関数pUndupすれば完成です。
具体的な実装は以下の通りです。
pairs
Fixpoint pairs_def (fs:S -> seq T) (t:T) (ss:seq S) (nt:nat) :
seq (T * S * (nat * nat)) :=
match ss with
| [::] => [::]
| s :: ss => let st := fs s in
let ns := index t st in
if ns < size st
then (t,s,(nt,ns)) :: pairs_def fs t ss nt.+1
else pairs_def fs t ss nt.+1
end.
Definition pairs (ft:T -> seq S) (fs:S -> seq T) :
seq (T * S * (nat * nat)) :=
flatten (codom (fun t => pairs_def fs t (ft t) 0)).
まず、pairs_defで片方(ここではt)を固定したときに全てのペアになる組み合わせを求めます。ここでss := ft tを表していて、ntを求めるための補助変数です。
具体的には、もしs \in ssのとき、つまりtのカップリング希望リストにsが含まれている場合、fs sつまりsにおけるカップリング希望リストにtが含まれている場合はそれを先頭に追加して再帰します。
あとはこれを全てのtに対して求め、それらのリストをflattenで結合してしまえば関数pairsの完成です。
qsort
実装は「クイックソートは半順序でもソート可能であることをCoq/SSReflectで証明する」内で紹介したのと同じなので省略します。
なぜクイックソートを使うかというと、任意の半順序、というよりも単なる推移的な二項関係であればソート可能だからです。
詳細は「半順序でソートするためのアルゴリズムとは？」をご覧ください。
pUndup
Variable (X:eqType).
Function pUndup (s:seq (T * S * X)) {measure size s} : seq (T * S * X) :=
match s with
| [::] => [::]
| h :: s => h :: pUndup [seq x <- s | h.1.1 != x.1.1 & h.1.2 != x.1.2 ]
end.
Proof.
move => s' h s _. apply /ltP. exact : filter_size.
Defined.
先頭の要素(t,s,(nt,ns)) を取り出し、残りの要素のうち、tかsが一致している要素を除いて再帰します。このとき、コンストラクタのみを除いて再帰するわけではなく減少性が非自明なため、Functionコマンドを使って定義します。
またqsortのときと同様に、自動生成されるpUndupにおける帰納原理pUndup_indの使い勝手が悪いので、新たに帰納原理を証明します。
Lemma my_pUndup_ind (P:seq (T * S * X) -> Prop) :
P [::] ->
(forall h s, P [seq x <- s | h.1.1 != x.1.1 & h.1.2 != x.1.2 ] ->
P (h :: s)) ->
forall s, P s.
Proof.
move => Hnil Hcons s.
have [n] := ubnP (size s).
elim : n s =>[|n IH][|h s]//=. rewrite ltnS => Hsize. apply /Hcons /IH.
exact : leq_ltn_trans (filter_size _ _) Hsize.
Qed.
証明の方針は「Coq/SSReflectで{}を使わずに完全帰納法を適用する」のクイックソートにおける帰納原理と同様です。
mkCouple
これらを組み合わせれば、カップル生成アルゴリズムmkCoupleの完成です。
Definition mkCouple (ft:T -> seq S) (fs:S -> seq T) :
seq (T * S * (nat * nat)) :=
pUndup (qsort (fun x y => R x.2 y.2) (pairs ft fs)).
仕様を満たすことを証明する
上で定義したmkCoupleが仕様を満たすことを証明します。
そのための補題をいくつか用意します。
pairsに関する補題
まず、pairsに関する補題です。
pairsの返り値のリストに入っているペアが満たすべき必要十分条件が以下の通りです。
Lemma ex_pairsP (ft:T -> seq S) (fs:S -> seq T) (t:T) (s:S):
reflect (exists nt ns, (t,s,(nt,ns)) \in pairs ft fs)
((t \in fs s) && (s \in ft t)).
(t \in fs s) && (s \in ft t)すなわちtとsがお互いにカップリング希望を出していることとexists nt ns, (t,s,(nt,ns)) \in pairs ft fsすなわちpairs ft fsのリストに含まれていることが同値になります。
ここで、「ntとnsが存在すること」とありますが、具体的な値の1つは以下のようにindex s (ft t)とindex t (fs s)になります。
Lemma pairs_index (ft:T -> seq S) (fs:S -> seq T) (t:T) (s:S):
(t \in fs s) && (s \in ft t) ->
(t,s,(index s (ft t),index t (fs s))) \in pairs ft fs.
ここで「１つ」と言ったのは、マッチング希望用紙に同じ名前を複数書く場合があるからです。
名前が重複しないことを仮定しても良いのですが、重複したペアはのちにpUndupで消えるので、ここでは仮定していません。
qsortに関する補題
クイックソートqsortに関しては返り値がソートされていることと元のリストの置換になっていることを示せれば十分です。
Fixpoint mysorted T (R:rel T) (s:seq T) :=
if s is x :: s' then all (fun y => R y x ==> R x y) s' && mysorted R s'
else true.
Lemma qsort_sorted T (R:rel T) s : transitive R -> mysorted R (qsort R s).
Lemma perm_qsort (T:eqType) (R:rel T) s: perm_eq (qsort R s) s.
ついでに、二項関係fun _ _ => falseでソートしても元のリストと変わらないことも示しておきます。
Lemma qsort0 T (s:seq T) : qsort (fun _ _ => false) s = s.
pUndupに関する補題
それぞれの仕様に関する補題を示していきます。
健全性
pUndupしたリストが部分集合、特に部分列になっていることを示します。
Lemma pUndup_subseq s : subseq (pUndup s) s.
一意性
pUndupしたリストが一意性を満たすことを示します。
Lemma pUndup_uniquel s x y:
x \in pUndup s -> y \in pUndup s -> x.1.1 = y.1.1 -> x = y.
Lemma pUndup_uniquer s x y:
x \in pUndup s -> y \in pUndup s -> x.1.2 = y.1.2 -> x = y.
極大性
pUndupしたリストが極大性を満たすことを示します。
Lemma pUndup_maximal s x:
x \in s -> has (fun m => (m.1.1 == x.1.1) || (m.1.2 == x.1.2)) (pUndup s).
優先順位極小性
これは、pundupの定義だけでは示せないので、別の補題を示します。
まず、述語behindを定義します。
Fixpoint dropuntil (X:eqType) x (s:seq X) :=
match s with
| [::] => [::]
| h :: s' => if x == h then s else dropuntil x s'
end.
Definition behind (X:eqType) (s:seq X) f b := b \in dropuntil f s.
behind s f bが意味するところは、リストsの中の最初に現れるfより後ろにbが存在することです。
特に[:: f; b]がsの部分列であるか、f = bかつfがsに含まれることと同値になります。
Lemma behindP (X:eqType) (s:seq X) f b:
reflect (subseq [:: f; b] s || (f == b) && (f \in s)) (behind s f b).
behindを使ってpUndupの極小性を表します。
Lemma pUndup_minimal s x:
x \in s ->
has (fun m => ((m.1.1 == x.1.1) || (m.1.2 == x.1.2)) && behind s m x)
(pUndup s).
つまり、pUndup_maximal s xが表しているのは、ペアx = (t,s,(nt,ns))に対し、tとsのどちらかが一致するmよりあとにxがリストsに存在することを表しています。
今考えたいのはソートされたリストsなので、mの後にxが存在することとmがxより真に小さくないことが言えます。
あとはこれらを組み合わせてカップル生成アルゴリズムmkCoupleが仕様を満たすことを示します。
mkCoupleが仕様を満たすことを示す。
上の補題を使ってそれぞれ証明します。
健全性
Lemma mkCouple_kindness (ft:T -> seq S) (fs:S -> seq T) t s nt ns :
(t,s,(nt,ns)) \in mkCouple ft fs -> (t \in fs s) && (s \in ft t).
Proof.
move /(mem_subseq (pUndup_subseq _)).
by rewrite (perm_mem (perm_qsort _ _))=>/mem_pairs.
Qed.
一意性
Lemma mkCouple_uniquel (ft:T -> seq S) (fs:S -> seq T) t s s' nt nt' ns ns':
(t,s,(nt,ns)) \in mkCouple ft fs ->
(t,s',(nt',ns')) \in mkCouple ft fs ->
[/\ s = s', nt = nt' & ns = ns'].
Proof.
move => H H'. by case : (pUndup_uniquel H H' (erefl _)).
Qed.
Lemma mkCouple_uniquer (ft:T -> seq S) (fs:S -> seq T) t t' s nt nt' ns ns':
(t,s,(nt,ns)) \in mkCouple ft fs ->
(t',s,(nt',ns')) \in mkCouple ft fs ->
[/\ t = t', nt = nt' & ns = ns'].
Proof.
move => H H'. by case : (pUndup_uniquer H H' (erefl _)).
Qed.
極大性
Lemma mkCouple_maximal (ft:T -> seq S) (fs:S -> seq T) t s:
(t \in fs s) && (s \in ft t) ->
has (fun m => (m.1.1 == t) || (m.1.2 == s)) (mkCouple ft fs).
Proof.
case /ex_pairsP =>[nt][ns].
rewrite -(perm_mem (perm_qsort (fun x y => R x.2 y.2) _)).
exact : pUndup_maximal.
Qed.
優先順位極小性
Hypothesis (Htrans: transitive R).
Lemma mkCouple_minimal (ft:T -> seq S) (fs:S -> seq T) t s:
(t \in fs s) && (s \in ft t) ->
has (fun m => ((m.1.1 == t) || (m.1.2 == s)) &&
let x := (index s (ft t), index t (fs s)) in
(R x m.2 ==> R m.2 x))
(mkCouple ft fs).
Proof.
move => /pairs_index ts. move : (ts).
rewrite -(perm_mem (perm_qsort (fun x y => R x.2 y.2) _))
=>/pUndup_minimal.
apply : sub_has => m /=/andP[->]/behindP/orP[|/andP[/eqP->_]];
[|exact /implyP].
have sndtrans : transitive (fun x y: (T * S * (nat * nat)) => R x.2 y.2)
:= fun _ _ _ xy yz => Htrans xy yz.
move =>/subseq_mysorted. move =>/(_ _ (qsort_sorted _ sndtrans))/=.
by rewrite !andbT.
Qed.
まとめ
婚活パーティにおけるカップル生成アルゴリズムを形式検証しました。
また、婚活パーティにおける「優先順位が高い人がマッチングする」ということの意味を確認しました。
具体的には、「優先順位」とは$\mathbb{N} \times \mathbb{N}$上の推移性を満たす二項関係であり、
「優先順位が高い人がマッチングすること」は優先順位による極小値をとるペアがカップルになるということがわかりました。
-
有限性を仮定しないと無限のカップルが生成される場合が考えられるため、一般に停止しない関数になります。 ↩