GSM.md

提案手法

この章では、行政の性質を証明可能な命題として表現する方法を示す。具体的には、LTS（Labeld Transition System）モデルを用いて、行政を意味するステートマシンGSM（Government State Machine）を定義した。LTSとは、PDL（Propositional Dynamic Logic）やμ計算などの様相論理にて用いられる状態遷移のモデルである。GSMを用いれば、各論理体系において行政の性質を論理命題として記述可能となる。尚、本論文の内容は定理証明支援系のCoqで実装されている。

定義(LTS)

状態の集合Sと、アクションの集合Aが与えられた時、⇒ ⊆ S × A × S となる集合 ⇒ をLTSと呼ぶ

a ∈ A と s,s’ ∈ Sが与えられた時、(s, a, s’) ∈ ⇒ は、状態sがアクションaにより状態s’に遷移し得る事を意味する。

GSM

GSMは、熟議民主制の行政のモデルである。GSMの状態遷移は提案をベースにして行われる。提案内容を委員会が熟議し、可決された場合のみ提案された遷移が実行される。従って、GSMのアクションは図●のように定義される。

Inductive proposal  :=
    | PwithdrawTreasury : currency -> proposal
    | PdepositTreasury : currency -> proposal
    | PwithdrawBudget : admin -> currency -> proposal 
    | PdepositBudget : admin -> currency -> proposal 
    | Pallocate : admin -> currency -> proposal
    | PassignMember : admin -> citizen -> proposal
    | PdismissalMember : admin -> citizen -> proposal    
    | PassignTenureWorker : admin -> citizen -> timestamp -> proposal    
    | PdismissalTenureWorker : admin -> citizen -> proposal
    | Pregister : citizen -> proposal
    | Pderegister : citizen -> proposal
    | PgenAdmin : admin -> proposal 
    | PslashAdmin : admin -> proposal.



Inductive act :=
    | AglobalPropose : proposal -> random -> random -> random -> nat -> act    
    | AglobalDeliberate : act
    | AsubPropose : admin -> proposal -> random -> random -> random -> nat -> act
    | AsubDeliberate : admin -> act.

図● GMS上のアクション

LTSの⇒に相当する関数 trans_ : act -> state -> state と、その補助関数 transv_ : proposal -> state -> state はAPPENDIXに載せている。注意されたいのが、アクションと提案の二層構造になっている点である。trans_　は提案の提出と熟議の実行を定義し、transv_ は提案可能な状態遷移を定義している。また、actにて定義される熟議の提出と熟議の実行が二種類ずつある点にも注目されたい。これはstateの定義に由来する。すなわち、stateにはそれ自身が熟議を行う委員会を持つ一方で、下位組織として持つ各行政機関も委員会を備えている。stateの定義を図○に示す。

Record comitee := mkDlb{
    Dproposal : proposal;
    Dprofessional : citizen;
    Dfacilitator : citizen;
    Ddeliberator : {set citizen};
}.

Record subState := mkSubState {
    SSbudget : currency;
    SSmember : {set citizen};
    SScomitee : option comitee;
    SStenureWorker : {set citizen * timestamp};
}.

Record state := mkState{
    Streasury : currency;
    Smember : {set citizen};
    Scomitee : option comitee;
    Ssubstate : admin -> option subState
}.

図○ GSM上の状態

検証

この章では、様相論理によってGSMの性質を論理命題として記述できる事を確認する。まず様相論理の論理体系を定義する。ここでは、PDLとCTL(Computational Tree Logic)の論理演算を加えた論理体系を用いる。次に、GSM上の命題変数を定義し、GSMでは独裁者が存在しない事を示す命題を記述する。尚、ここでの論理体系は模擬的なものであり、健全性・完全性の確認はできていない。

論理体系

一般的な命題論理に、PDLとCTL(Computational Tree Logic)の論理演算を加えた論理体系を定義した。命題変数の集合をPとし、要素をpで表す。アクションと状態の集合はSとAで表し、その要素をそれぞれsとaで表す。また、LTSの⇒に相当する関数trans : S -> A -> S -> {ture, false}と、命題変数に関する付置関数valuation : P -> S -> {true, false}は所与のものとする。

Φ, Ψ := p | ⊥ | ¬ Φ | Φ ∨ Ψ | [a]Φ | | AG Φ | EG Φ

⊤と∧及び→は、一般的な略記法に従う。特筆すべきは、PDL由来の[a]ΦとCTL由来のAG Φ及びEG Φである。[a]Φは必然性を意味する命題で、アクションaを実行した後のどの状態でも命題Φが成り立つ事を意味する。

s |= [a]Φ iff ∀ s', trans s a s' -> s' |= Φ

AG Φは、EG Φのセマンティックで用いる状態遷移のパスを図▲に示す。

Inductive step (a : act) : state -> state -> Prop :=
    | here s : step a s s
    | there b s t r : trans a s t -> step b t r -> step a s r.    

図▲ 状態遷移のパス

step a s s'は、状態sに対してアクションaを施した後、任意のアクションの繰り返し方を経て状態s'へと至るパスが存在する事を意味する。AG Φは、どのパス上のどの状態においても命題Φが成り立つ事を意味する。EG Φは、パス上の全ての状態でΦが成り立つようなパスが存在する事を意味する。

s |= AG Φ iff ∀ a s', step a s s' -> s' |= Φ
s |= EG Φ iff ∃ a s', s' |= Φ /\ (∀ t, step a s t -> step a t s' -> t |= Φ)

また、AFと¬を用いた略記として、AFを導入する。AF Φは、どのパスにおいても最終的にΦが成り立つ状態に至る事を意味する。

AF Φ := ¬ EG ¬ Φ

独裁者の不在性

図△のような命題変数を定義した。付置関数valuationは、APPENDIXに載せている。isAssigned a mは、行政機関aに市民mが属している事を意味し、isProposed a pは行政機関aに提案pが提出されている事を意味する。

Inductive var :=
    | isAssigned : admin -> citizen -> var
    | isProposed : admin -> proposal -> var 

図△ 命題変数

任意の市民mと行政機関admに対して、mがadmの構成員から罷免できない場合、mが独裁的に振る舞っているとみなす。mの独裁性を形式的に記述したのが、図■である。assignedとproposedは、命題変数のみからなる論理式である。Varが論理式を構成するコンストラクタである事を思い出されたい。undismissableは、罷免提案が熟議で否決される事を示す命題である。また、NotDictatorialでは、論理演算AFを用いている点に注意されたい。AF (¬ undismissable)は、どのパスにおいても最終的に罷免可能となる状態になる事を意味している。

Section Dictatorship.

Variable m : citizen.
Variable adm : admin.

Definition assigned : form := 
    (Var (isAssigned adm m)).

Definition proposed : form :=
    Var (isProposed adm (PdismissalMember adm m)).

Definition deliberate : act :=
    AsubDeliberate adm.

Definition undismissable : form :=
    proposed → [deliberate]assigned.

Definition NotDictatorial : form :=
    assigned → AF (¬ undismissable).

End Dictatorship.

図■ 行政機関の非独裁性

以上より、GSMのいかなる状態においても独裁者が存在しない事を、形式的に記述可能となった。

Definition soundness :=
    forall s m adm, s |= NotDictatorial m adm.