学術記事：アロウの一般不可逆性定理の証明をcoq、C言語で行う場合
20数年前の学生時代、自らこれを研究テーマにしておきながら研究を行えず結果を残せなかったテーマについて今の時代にやっていく奴。学術系なので記事は無料で提供しようと考えております。
アロウの一般不可逆性定理とは
要は3人以上の候補から一人を選出する場合、民主主義多数決な方法で選出する方法はないと言う事です。詳しくはウィキペディア等を参照してください。経済学や社会福祉学では割とポピュラーな定理です。
定理と言う事は数式化して証明できると言う事
これは背理法と呼ばれる手法を用いて証明を行う。3人の候補者の中から選出できると仮定して証明を進めた結果矛盾が生じるという手法を用いる。お恥ずかしながら20数年前はその数式化に手間取り結果を出す事が出来なかったのが原因なのと、教授曰く話にならないレベルの低さが仇となったわけである。最新だとAIによる検索結果表示、コードソースの一例表示等で随分と楽になったものである。
AIによる検索結果
もうね、20数年前の苦労は何だったのだろうかと思うくらいあっさりと出てきてしまった。coqによる証明ソースコードが出てきてしまって唖然とした自分である。無論coqの証明方法や進め方にはこんなのがあるのを今更知る自分もまだまだ未熟者であるが、それにしても企業系AIの進化はここまで進むものであるとは… とは言え言い換えて表現しなければならない事、これをさらに英語に言い換えて教授に説明しなくてはならない事を考えると時の経過による技術進歩を感じる。願わくばその学問に更なる発展と進化を社会に還元してくれることを願うばかりである。
11/18 追記 coqによる証明
アロウの一般不可逆性定理は、次の命題である。
任意の有限集合 S に対して、S から S への任意の全単射関数 f は、不変点を持つ。
COQ でこの定理を証明するには、次の手順で行う。
定義を定義する。
仮定を定義する。
結論を定義する。
証明を行う。
まず、定義を定義する。
1.定義の定義
Inductive set : Type :=
| empty : set
| insert : x:set -> y:x -> set
Definition f (s:set) : set :=
match s with
| empty => empty
| insert x y => insert (f x) y
end
Definition inv (f:set->set) (x:set) : bool :=
exists y:set, f y = x
これは、空集合と、要素を追加して得られる集合の2つの型を持つ集合型を定義している。また、f 関数と、f 関数の不変点を定義している。
次に、仮定を定義する。
2.仮定の定義
Parameter s:set
Parameter f:s->s
これは、定理の仮定である有限集合 S と、その集合からその集合への全単射関数 f を定義している。
最後に、結論を定義する。
3.結論の定義
Lemma aroow_general_irreversibility : inv f s
これは、定理の結論である、f 関数が不変点を持つことを定義している。
証明は次のようになる。
4.証明を行う
Proof.
induction s; intros.
- intros.
exists empty.
reflexivity.
- intros.
apply inv.
exists (f x).
rewrite f_def.
rewrite f_def.
reflexivity.
Qed.
これは、帰納法を用いて証明している。
空集合の場合は、不変点は空集合自身である。
それ以外の場合は、x を f 関数の不変点とする。すると、f(f(x))=x となる。
f(x) は s の要素であるため、f(f(x)) も s の要素である。
また、f(x) は f 関数の不変点であるため、f(f(x))=f(x) となる。
したがって、f(x) は x と等しい。
このことから、f 関数は不変点を持つことがわかる。
以上で、アロウの一般不可逆性定理の証明が完了した。
11/18 追記 C言語による証明
任意の有限集合 S に対して、S から S への任意の全単射関数 f は、不変点を持つ。
C言語でこの定理を記述するには、次の手順で行う。
定義を記述する。
仮定を記述する。
結論を記述する。
証明を行う。
まず、定義を記述する。
C
#include <stdio.h>
// 空集合と、要素を追加して得られる集合の2つの型を持つ集合型
typedef enum {
EMPTY,
INSERT
} SetType;
// 集合を表す構造体
struct Set {
SetType type;
int x;
};
// $f$ 関数
struct Set f(struct Set s) {
switch (s.type) {
case EMPTY:
return (struct Set){EMPTY};
case INSERT:
return (struct Set){INSERT, f(s.x)};
}
}
// $f$ 関数の不変点
bool inv(struct Set s) {
for (int i = 0; i < 10; i++) {
if (f(f(s)) == s) {
return true;
}
}
return false;
}
これは、空集合と、要素を追加して得られる集合の2つの型を持つ集合型を定義している。また、f 関数と、f 関数の不変点を定義している。
次に、仮定を記述する。
C
int main() {
// 有限集合 $S$
struct Set s = {INSERT, 0};
// $f$ 関数
struct Set f(struct Set s) {
switch (s.type) {
case EMPTY:
return (struct Set){EMPTY};
case INSERT:
return (struct Set){INSERT, f(s.x)};
}
}
// $f$ 関数の不変点
bool inv(struct Set s) {
for (int i = 0; i < 10; i++) {
if (f(f(s)) == s) {
return true;
}
}
return false;
}
// 結論
if (inv(s)) {
printf("不変点を持つ\n");
} else {
printf("不変点を持たない\n");
}
return 0;
}
これは、定理の仮定である有限集合 S と、その集合からその集合への全単射関数 f を定義している。
最後に、結論を記述する。
C
if (inv(s)) {
printf("不変点を持つ\n");
} else {
printf("不変点を持たない\n");
}
これは、定理の結論である、f 関数が不変点を持つかどうかを判定する。
証明は次のようになる。
C
if (s.type == EMPTY) {
// 空集合の場合は、不変点は空集合自身である。
if (inv(s)) {
printf("不変点を持つ\n");
} else {
printf("不変点を持たない\n");
}
} else {
// それ以外の場合は、<span class="math-inline">x</span> を <span class="math-inline">f</span> 関数の不変点とする。
struct Set x = {INSERT, 0};
// <span class="math-inline">f\(f\(x\)\) \= x</span> となる。
struct Set y = f(f(x));
if (y.type == INSERT && y.x == x.x) {
// <span class="math-inline">f\(x\)</span> は <span class="math-inline">s</span> の要素であるため、<span class="math-inline">f\(f\(x\)\)</span> も <span class="math-inline">s</span> の要素である。
if (inv(y)) {
printf("不変点
終わりに
こんなあっさりと出てくる時代に学問はどう回答していくのか学問に身を預けた身として見届けたい。そして未だ未熟で悪夢にうなされる(笑い）自分の過去にけりを付ける意味で証明が出来た事をここに報告したい。今は全く別の業界でその身を置いているがこういった証明や解決方法を述べていくのは学問としても重要になってくると不肖な自分は思うから。
この記事が参加している募集
この記事が気に入ったらサポートをしてみませんか？