日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

定性空間表現 PLCA のモデル化と妥当性の証明について
後藤 瑞貴

高橋 和子

定性空間推論の枠組みの１つである PLCA 表現の妥当性を検証する．PLCA 表現は点，線，閉路，範囲を，位置や大きさを指定しない定性的なオブジェクトとしてとらえ，それらの関係で図形を記号表現する方法である．PLCA
表現の性質やその上に記述された操作の妥当性や与えられた PLCA 表現に対して２次元平面図形が存在するための条件については証明されている．しかしながら，これらの証明については手作業で行われており，正しさが確実に保証されているとはいえない．本発表では，証明支援系 Coq を用いて PLCA 表現を体系としてモデル化し，その妥当性を証明する．表現の定義は帰納的にモデル化できるように変更した．また，２次元平面図形との関係を証明する際に出現した問題についても議論する．

象をモデル化して証明を行う定理証明器を使用する．

1 はじめに定理証明器には Coq [1]，Isabelle/HOL [2]，PVS [3]，コンピュータ上で図形などを扱う場合に，ポリゴンACL2 [4]，Agda [5] などがある．定理証明器はそれぞを使って形を表現し，頂点の座標を使って正確にオブれベースとなる論理をもっていて，その論理によってジェクトを記述することで必要な情報を数値計算で求証明を進めることができる．一般に帰納的定義と帰納める手法が一般的である．このような定量的な方法法によって証明を行うものが多く，型理論に基づいては画像処理やコンピュータグラフィクスで使われるが検証するものもある．定理証明器で証明されたものはその中で定性的な情報も必要とすることがある．例

机上で証明されたものに比べて非常に信頼性が高い

えば，領域のオブジェクト同士が接している，重なっため，検証に用いられることがよくある．ている，もしくは内包しているなどである．こういっ本研究では定性空間推論の１つである PLCA 表現た情報については定性的に処理できるのが好ましい．

[6] [7] の妥当性を定理証明器を使って証明し，PLCA従って，定性空間推論の手法を用いて推論を行うこと表現をより確固で信頼性の高いものにすることを目標

で計算時間の削減が期待できる．しかし，一般的ににしている．PLCA 表現はその枠組みの１つであり，提案されている定性空間推論システムの妥当性は机点 (Point)，線 (Line)，閉路 (Circuit)，範囲 (Area)

上での証明はされているが，すべての場合についての４つのオブジェクトで定性的に図形を表現し，それの厳密な証明がなされているわけではない．従って，らの関係を推論するものである．定理証明器には Coq

形式的な方法で妥当性を調べる必要がある．形式的を使用し，帰納的アプローチによって証明を試みる．に検証する方法として，ここではコンピュータ上で対P，L，C，A はもともと集合として定義されているが，本研究では集合の要素数をカウントすることを念On modeling and proving validity of qualitative spatial representation PLCA.
Mizuki Goto, 関西学院大学大学院理工学研究科, Graduate School of Science and Technology, Kwansei
Gakuin University.
Kazuko Takahashi, 関西学院大学理工学部, School of Science and Technology, Kwansei Gakuin University.

頭に入れているためリストで表現し，重複する要素が存在しないように定義した．PLCA 表現を帰納的に定義したのち，その定義が PLCA 表現として満たすべき制約条件を充足することを一部を除き証明した．
本発表は以下のように構成される．第２節で定理証

明器について簡単に触れ，第３節で PLCA 表現について説明する．そして第４節で帰納的に PLCA 表現を定義する方法について述べる．第５節では証明を行い，第６章で結論を述べる．

2 Coq
本研究に使用した Coq は対話型定理証明器であり，直観主義論理に基づいている定理証明器である．逐一手動で式変形を行い，証明の状況を使用者に全て提示されるようになっているため，手順を考えて証明を組み立てることができる．しかし，デメリットとしてライブラリが少なく自分で定義する量が多くなることがある．一方で Isabelle/HOL などは強力な自動推論機構を持つ．PLCA 表現の検証は必ず証明できる目算がなかったため，自動的に証明を進める定理証明器は好ましくない．よって手動で証明を行いかつ，理解しやすい Coq を本研究の定理証明器に採用した．

2. 1 Coq の表記法
Coq では帰納的定義は以下のように表記される．
Inductive nat : Set := 0 : nat | S : nat → nat.
nat(natural number) は帰納的に定義されておりターミネータとなる 0 と後者関数である S(Successor) の２つコンストラクタからなる．Set とは型の上位に存在する型で帰納的定義は必ず Set か Type か Propを型にとらなければならない．今回の nat は命題(Proposition) ではなく Type ほど上位の型ではないので Set となっている．
次にリスト構造を表す List の定義は以下の通りである．

同値関係は Definition を使って行う．

Definition three := S (S (S 0)).
これは three という型が nat の３と等しいことを表している．

3 PLCA 表現
PLCA 表現は領域同士の接続関係を扱うための最低限の情報をもっている．

3. 1 オブジェクト
ここでは PLCA 表現に現れる４つのオブジェクトについて詳しく説明する．

3. 1. 1 Point(点)Point とはいわゆる一般的な点を指す．
3. 1. 2 Line(線)Line とはある Point から Point への直線または曲線を表す．つまり，持っている情報は始点と終点のみである．また，Line は有向線であり，始点と終点が反転したものは別の線として区別する．今後，Lineは２つの点のペアとして () を使って表現する．

3. 1. 3 Circuit(閉路)Circuit とは Line のリストであり，その線が閉路のように環状に並んだものを指す．Circuit であるためにはいくつか制約がある．まず，Line リストは必ず長さが１以上でなくてはならない．これは線が存在しない閉路は考えられないためである．そして，リストの要素にあたる Line は終点と次の要素 (Line) の始点が一致していなければならない．すなわち[(p0 , p1 ), (p1 , p2 ), (p2 , p3 ), (p3 , p4 ), ...., (pn−1 , pn )]ただし，p0 = pn である．Circuit には Line 同様，向きが存在する．つまり，右回りと左回りの Circuit はInductive List(A : Type) : Type :=内向きと外向きの２つとして区別する．つまり，右回| nil : List A

りか左回りかによって内向きか外向きか決めることが| cons : A → List A → List A.

できる．

見やすくするために改行しているが，改行することで Coq 上で意味合いが変わることはない．リストはType 型を引数にもち，その Type 型の A のリストを作る．cons は一般的に::と表記しリスト同士の結合は++と表記する．なお，::，++は中置演算子である．

3. 1. 4 Area(範囲)
Area とはある範囲の中の存在する閉路を集めたものであり，Circuit のリストで表現される．これもCircuit と同じく，リストの長さが１以上でなければならない．そして，同じ Area に含まれるどの CircuitA のそれぞれの集合は以下のようになる．
P = {p1 , p2 , p3 , p4 , p5 , p6 }L = {l1 , l2 , l3 , l4 , l5 , l6 , l7 }C = {c1 , c2 , outermost}A = {a1 , a2 }4 妥当性
与えられた PLCA 表現
図1

ありえない PLCA 表現

E =< P, L, C, A, outermost >が妥当な PLCA 表現であるためには３つ制約条件を満たす必要がある．以下はその条件であり，証明を行うにあたって [6] の表現方法を意味を変えることなくいくつか変更した．

4. 1 Point-Line 間の制約
全ての点はある線に含まれる．点が線に含まれるとはその点が始点か終点のどちらかであることを表す．

∀p ∈ P ∃l ∈ L (p ∈ l)

(1)

全ての線の始点，終点は点集合に含まれる．
図2∀l ∈ L (p ∈ l ⇒ p ∈ P )PLCA 表現の例

も他の Circuit と点または線で接してはならない．この条件を例を使って説明する．もし領域 a 内に異なる閉路 c1 , c2 があり，これらが１点で接しているとす4. 2 Line-Circuit 間の制約
全ての線はある閉路に含まれる．線が閉路に含まれるとは線が閉路を構成する線の一部であることを表す．

る (図 1). しかし，PLCA は外側をまとめて１つの閉路で表現すべきであるため，この例は条件を満たさない．

(2)∀l ∈ L ∃c ∈ C (l ∈ c)

(3)

全ての閉路に含まれるいずれの線も L に含まれる．

∀c ∈ C (l ∈ c ⇒ l ∈ L)

3. 1. 5 PLCA 表現(4)

点集合，線集合，閉路集合，範囲集合そして図形上ある線を含む２つの閉路があった場合，それらは同で一番外側の閉路を表す outermost の組を PLCA 表

じ閉路である．つまり，ある線を含む閉路は１つしか現という．点集合を A，線集合を L，閉路集合を C，ない．

範囲集合を A とすると，PLCA 表現 E は

E =< P, L, C, A, outermost >∀l ∈ L ∀c1 c2 ∈ C(l ∈ c1 ∧ l ∈ c2 ⇒ c1 = c2)(5)となる．
ただし，L は有向線の集合ではなく無向線としての線

4. 3 Circuit-Area 間の制約集合である．つまり，「L にある線が含まれる」とは集

outermost 以外の全ての閉路はある範囲に含まれる．

合 L にはそのままの形で含まれているか，逆向きで閉路が範囲に含まれるとは閉路が範囲を構成する閉含まれているかのどちらかであることを示す．

路の一部であることを表す．

図 2 は PLCA 表現の例を表している．P，L，C，∀c ∈ C, ∃a ∈ A, (c ̸= outermost ⇒ c ∈ a)(6)

全ての範囲が持ついずれの閉路も C に含まれる．

∀a ∈ A, (c ∈ a ⇒ c ∈ C)

(7)

outermost でないある閉路を含む２つの範囲があった

点，終点，通った点のリスト，経路を持つ．
構成子は以下の通りにした．

nil path

場合，それらは同じ閉路である．つまり，ある閉路をある Point が P に含まれるならその Point を始含む閉路は１つしかない．

点，終点とする長さ０の PATH がある．

∀c ∈ C ∀a1 a2 ∈ A∀p ∈ P ⇒ P AT H P L p p (p :: nil) nil(c ̸= outermost ⇒ c ∈ a1 ⇒ c ∈ a2⇒ a1 = a2)(8)step path

5 帰納的な PLCA 表現

ある PATH が存在し，さらにその PATH に含

本節では式の定義を Coq のコードで記述する．

まれない別の Point x ∈ P があったとき，x とPLCA 表現はグラフ表現と対応づけて考えられる．

PATH の始点との Line l ∈ L を経路に加えたも従って，PLCA 表現の定義は帰納的にオブジェクトのも PATH になる．

である Point または Line の数が増えるように行うのが自然と考えられる．しかし，１つずつ Point また∀P, L, ∀p1, p2, p3 ∈ P, ∀l ∈ L, ∀pl, ll,は Line を追加していくとグラフ上に突如 Circuit や

P AT H P L p2 p1 pl ll ⇒ p3 ∈/ pl ⇒Area が現れる性質を持つので，単純な帰納的なグラ

P AT H P L p3 p2 (p3 :: pl) ((p3, p2) :: ll)

フの定義ができない．従って，ある操作によって同時閉路とは一般的に始点と終点が同じ PATH であるに４つのオブジェクトを追加していくような帰納的定といえるが，この PATH だけでは閉路を構成できな義が必要となる．

いため

5. 1 オブジェクトの定義∀P L pl ll ∀x y ∈ P

定理証明器で定義した各オブジェクトは以下の通り

P AT H P L x y pl ll ∧ (x, y) ∈ L ∧ length ll ≥ 2である．

を満たす場合，((y, x) :: ll) を閉路とした．

Definition Point := nat
Definition Line := Point ∗ Point
Definition Circuit := list Line
Definition Area := list Circuit

5. 3 PLCA 表現の定義
構成子は３つとし，引数は P，L，C，A とした．

e outermost
e outermost とはベースケースに相当する構成

5. 2 PATH
Circuit は list Line として定義されているが Circuit としての性質を満たしている必要がある．そのため，PATH という述語を用意することで，Circuitの性質を持っている list Line に特定できるようにした．PATH とはある２つの Point 間を結ぶループをもたない経路が存在することを表している．経路とはLine のリストであり，経路の長さは０の場合も許される．

PATH は帰納的に定義され，引数として P，L，始子であり，outermost となる閉路およびその閉路と線を共有する閉路の２つだけ存在する．Pと L は閉路を構成する点と線のみとなり，A はoutermost の内側にある範囲のみとなる．
connect circuit
outermost 以外のある閉路に含まれる２つの点を結ぶ新たな経路を作った時，その経路を追加することによって変化したオブジェクトを更新する．

isolate circuit
ある範囲に含まれる全ての閉路と線または点を6 証明
第 5 節の帰納的な PLCA 表現が正しいことを証明する．P，L，C，A は集合であるが，定理証明器ではリストとして定義したので「P，L，C，A が重複する要素が存在しないこと」と「a ∈ A となる a が重複する要素を含まないこと」，さらに「outermostがいずれの範囲に属さないこと」も加えて証明した．
また，PLCA のもつ制約条件 (1) 〜 (8) の内，(5) を図3除いて全て証明が完了した．
e outermost

以下の補題は第 4 節で説明した制約条件を Coq で記述したものである．

6. 1 P から L への制約条件 (1)Lemma PL limitation :∀ (P : set Point)(L : set Line) (C : set Circuit)(A : set Area)(e : E P L C A) (p : Point),
set In p P →(∃ l : Line, InL l L ∧ Point In Line p l )set という型は list と同値定義されているため，P，
図4

e outermost ⇒ connect circuit

L，C，A はリストである．set In もまた，リストの包含関係を示す In の関数と同じであるが，集合ということを強調するためにこちらを使用した．In a A で要素a がリスト A に含まれることを指す．Point In Lineとはある点が線の始点または終点であることを表す．

Line はリストではないため In の関数が使えない．
従って，このような関数を導入した．

6. 2 L から P への制約条件 (2)Lemma LP limitation :∀ (P : set Point)(L : set Line) (C : set Circuit)
図5e outermost ⇒ isolate circuit(A : set Area)(e : E P L C A) (p : Point)(l : Line),
set In l L → Point In Line p l → set In p P共有しない新たな閉路を追加する．
構成子が e outermost のみの場合は図 3 のようになる．そして，図 3 に connect circuit を適用すると
図 4 のようになり，図 3 に isolate circuit を適用す
ると図 5 のようになる．

6. 3 L から C への制約条件 (3)Lemma LC limitation :∀ (P : set Point)(L : set Line) (C : set Circuit)(A : set Area)(e : E P L C A) (l : Line),
InL l L → (∃ c : Circuit, In l c ∧ set In c C )InL とは線が無向線として L に含まれることを意味

する．

れ補題は PLCA 表現に対する帰納法で証明するのだ
が，ベースケースが証明できても帰納段階において他

6. 4 C から L への制約条件 (4)の補題を必要とした．表 1 はそれらの関係を表にし

Lemma CL limitation :たものである．ベースケースとなる e outermost は∀ (P : set Point)(L : set Line) (C : set Circuit)

何も必要としないため問題ないが，それ以外の場合(A : set Area)(e : E P L C A) (l : Line)(c : Circuit),

は帰納段階における仮定がたりないため証明できな

set In c C → In l c → InL l L

い．例えば，(2) の isolate circuit は帰納における仮定があるため証明できる．しかし，connect circuit

6. 5 ある線を含む閉路はただ１つである．(5)

では (4)，(7) が足りない．同様のことが以下５つのLemma Circuit only one :補題で発生した．全てまとめてから帰納法を適用する∀ (P : set Point)(L : set Line) (C : set Circuit)

ことでベースケースはもちろん，connect circuit や(A : set Area)(e : E P L C A) (l : Line)(c1 c2 : Circuit),

isolate circuit も仮定の過不足なく証明できた．

7 おわりにset In c1 C → set In c2 C →PLCA 表現を帰納的に定義する方法を示すことでIn l c1 → In l c2 → c1 = c2

証明可能なモデルへ変換した．そして，それが３つの制約条件のうち一部を除き全てを満たすことを証6. 6 C から A への制約条件 (6)明した．また，PLCA 表現の上で曖昧なところを一Lemma CA limitation :部発見し，修正を試みた．今回，帰納的に定義した∀ (P : set Point)(L : set Line) (C : set Circuit)

PLCA 表現が元の定義と意味的に等しいことを確か(A : set Area)(e : E P L C A) (c : Circuit),めることが今後の課題である．また，PLCA 表現の

set In c C → c ̸= (outermost e) →グラフを連結グラフに変換する関数を定義した上で，(∃ a : Area, In c a ∧ set In a A)

その関数の性質を証明し，P，L，C，A の集合の要素の関係式 [2] について厳密な証明を与えることも考6. 7 A から C への制約条件 (7)えている．

Lemma AC limitation :8 謝辞∀ (P : set Point)(L : set Line) (C : set Circuit)

本研究は科研費 25330274 の補助を受けて行われた．

(A : set Area)(e : E P L C A) (a : Area)(c : Circuit),

参 考 文 献set In a A → In c a → set In c C
6. 8 ある閉路を含む範囲はただ１つである．(8)Lemma Area only one :∀ (P : set Point)(L : set Line) (C : set Circuit)(A : set Area)(e : E P L C A) (c : Circuit)(a1 a2 : Area),
set In a1 A → set In a2 A →In c a1 → In c a2 → a1 = a2(2)，(4)，(5) そして，(7) の他に「集合 A が重複する要素を含まないこと」(9) と，「集合 A の要素 aが重複する要素を含まないこと」(10) を加えた６つの補題は単独で証明することができなかった．それぞ[1] Bertot, Y. and Casteran, P. : Interative Theorem
Proving and Program Development, Springer, 2004.
[2] Nipkow, T. Paulson, C, L. and Wenzel, M.: Isabelle/HOL A Proof Assistant for Higher-Order
Logic, Springer, 2008.
[3] Crow, J., Owre, S., Rushby, J., Shankar, N. andSrivas, M.: A Tutorial Introduction to PVS, 1995.
[4] Kaufmann, M. and Moore, S. J.: ACL2-Tutorial,
1997.
[5] Norell, U.: Dependently Typed Programming in
Agda, Advanced Functional Programming 2008,
pp.230-266, 2008.
[6] 住友孝郎 : 定性空間推論における新しい枠組みの提案, 関西学院大学理工学研究科修士論文, 2006.
[7] Takahashi, K., Sumitomo, T. and Takeuti,I.: OnEmbedding a Qualitative Representation in a TwoDimensional Plane ，Spatial Cognition and Computation, Vol.8, No.1-2, pp.4-26, April, 2008.

表1

それぞれの補題に PLCA 表現に対する帰納法を適用した場合に必要となる補題証明する補題

e outermost

connect circuit

isolate circuit

(2)

None

(2)，(4)，(7)

(2)

(4)

None

(4)，(7)

(4)

(7)

None

(7)，(8)，(9)，(10)

(7)

(8)

None

(2)，(4)，(7)，(10)(2)，(4)，(7)，(8)，(9)

(9)

None

(2)，(4)，(7)，(9)(2)，(4)，(7)，(9)

(10)

None

(2)，(4)，(7)，(8)，(9)(2)，(4)，(7)，(10)(2) + (4) + (7)(2) + (4) + (7)(8) + (9) + (10)(8) + (9) + (10)(2) + (4) + (7)(8) + (9) + (10)None