JAIST Repository
https://dspace.jaist.ac.jp/Title

様相論理の証明支援系上の実装

Author(s)矢田部, 俊介

CitationIssue Date

2008‑03‑03

TypePresentation

Text version

publisher

URL

http://hdl.handle.net/10119/8287

RightsDescription

5th VERITE : JAIST/TRUST‑AIST/CVS joint workshop
on VERIfication TEchnologyでの発表資料, 開催：2008年3月3日, 開催場所：北陸先端科学技術大学院
大学・情報科学研究科棟 5F コラボレーションルーム
７, JAIST 21世紀COEシンポジウム 2008「検証進化可能電子社会」と共催

Japan Advanced Institute of Science and Technology

様相論理の証明支援系上の実装
矢田部俊介
産業技術総合研究所システム検証研究センター

2008 年 3 月 3 日

独立行政法人産業技術総合研究所

1/ 16要旨
I 目的: 知識様相論理の意味論を証明支援系に実装
I 二つの問題点(1) 多変数述語を持つ型のデータ型の定義が難しい(2) 充足関数の再帰的定義が停止判定に合格しないI 解決法(1) ベクトルを使用(2) 論理式のデータ型の情報量を増やす
P(x, y) 二変数述語とする。論理式 (∀x)P(x, y) のデータ型としてII

従来: Fml 1 （一変数述語）
今回: V2,1 （二変数のうち一変数が束縛されている）

この増えた情報量によって、帰納法を行うことで、停止判定を合格させる定義が可能になる

独立行政法人産業技術総合研究所

2/ 16使用する証明支援系 Agda

I Agda: Martin-Löf の直観主義的型理論に基づいた証明支援系
I 述語論理のかなりの部分（命題論理のすべてと、述語論理の一部分）をそのまま定義することが可能である。
I 述語論理における論理的帰結関係と全称量化子の取り扱い：

命題 p は p : Set として表現される
命題（集合） A, B に関して、 A → B は、集合 A から B への関数として定義される。
I 全称量化子 (∀x ∈ D) p(x) は、(x : D) → px と、依存型として定義される。
II

独立行政法人産業技術総合研究所

3/ 16

Agda の特徴
I 依存型理論と一般の再帰法 (general recursion) は相性が悪い。

f : ∀x : N → T[x],f s : T[s]s:Nf (2 + 2) は f (4) と型が一致し、また T[2 + 2] は T[4] と型が一致する必要がある。
I この計算が停止しない場合、証明支援系は型付けに失敗する。
II Agda では依存型理論に基づきながら、原始再帰法による定義だけでなく、一般の再帰法による定義を許す。
II

型検査の終了後に、別の検査「停止判定」を行う。
その関数の型の判定に計算が含まれている場合、その計算が停止するかどうかを判定する。

I Agda では停止判定にパスするかどうかが重要
独立行政法人産業技術総合研究所

4/ 16

実装の対象: 知識様相論理の体系の充足関数
I 実装の対象となる体系: 知識様相論理

この知識様相論理の体系は、伝聞に関する知識を表現する様相論理の体系である。
I ネットワーク上の認証の安全性証明への応用が期待される。
II 表記法: 全称量化子を forall 、論理的帰結関係 ⇒I 充足関数は、述語論理の上で再帰的に定義されている: 全称量化子（forall ） のケース⟨s̄, φ, ψ⟩ |=(forall x)P(x)⇐⇒ ⟨s̄, φ ∧ ((∃y)Q(y) → Q), ψ ∧ ((∃y)R(y) → R)⟩ |= P(y)が任意の Q(x), R(x) に成立するI 人間の目には、この再帰法が有限回で停止するのは明らかである（この点が Agda にとっての問題となる）。
独立行政法人産業技術総合研究所

5/ 16

ポイント: 必要なことポイントになるのは、以下の二点が要求されるということである。
I 述語論理の実装：

任意有限個の変数をもつ述語を、変数を束縛する機構（量化子・個体記号の変数への代入操作）を持つデータ型として定義すること。
I 知識様相論理の充足関数の再帰的定義：

量化子を持つ文を代入操作を持つ文に還元することにより、述語論理上で関数を再帰的に定義し、そしてこの定義が帰納的定義になっていることを証明支援系に理解させる（型検査と停止判定にパスする）こと。

独立行政法人産業技術総合研究所

6/ 16

問題点その一：任意有限個の変数を持つ述語のデータ構造を定義することの困難（述語論理）
I 通常、Agda では以下のように述語を構成する。

p が 1 変数述語（domain として D をとる）場合は p : D → Set と型付けする。
I p′ が 2 変数述語の場合は p′ : D → D → Set, etc.
III

しかし、以下のデータ型 Pred n は型検査に合格しない (Ver. 2.0.0)。
III

Pred 0 = Set
Pred n + 1 = D → Pred n

右辺 ( D → Pred n) の値域 (Pred n) が明示的に（Set などの）ソート（Sort）になっていないと合格しない。

I 量化・代入の順番が一通りに限られる（∀y∃xP(x, y) などが明示的に表現できない）

独立行政法人産業技術総合研究所

7/ 16

問題点その二：関数の一般再帰的定義の停止判定にまつわる困難（様相論理）
I |= の定義: 左辺を右辺に還元している⟨s̄, φ, ψ⟩ |=(forall x)P(x)⇐⇒ ⟨s̄, φ ∧ ((∃y)Q(y) → Q), ψ ∧ ((∃y)R(y) → R)⟩ |= P(y)が任意の Q(x), R(x) に成立する

I しかし、証明支援系にとっては、forall x Px も subst y P も、データの複雑さの点では同じ。
I そのため、前者のケース |= forall x p を後者のケース · · · |= subst y Pに還元する上記の再帰的定義は、Agda の停止判定メカニズムが循環的定義であると判断してしまう。
独立行政法人産業技術総合研究所

8/ 16

解決法その一：ベクトルによる述語のデータ型の定義（述語論理）

I 型検査に合格するため、多変数の述語は X → Set の形で定義しなければならない。
I そのため、 n 変数述語の解釈のデータ型 Pred ′ を、I
I

N → Set1 の依存型を持ち、Pred ′ n = D n → Set （ D の元の長さ n のベクトル D n を定義域としSet を値域とする関数）として定義する。

独立行政法人産業技術総合研究所

9/ 16

論理式の定義（述語論理）

オブジェクト

データ型′

データ型のソート

解釈

Q:

Pred (n + 1) :Set1 (Set1 , Set)

述語記号q:PredSym (n + 1) :

Set

論理式

fml q :

Fml (n + 1) :

Set

代入操作

fml-subst t q

Fml n量化

∀x q

Fml n

独立行政法人産業技術総合研究所

10/ 16

ベクトル操作のための関数の定義

I ベクトルを領域として述語を定義する場合は、以下が問題になる。

Q を 2 変数述語とする。片方の変数に t : D を代入した結果は 1 変数述語 Q(x, t) となる。
I しかし q : D2 → Set では、 t : D のみを代入できない。
II 解決策は以下の通り。

ベクトルを操作する関数 gt (k, ⃗t, c) はベクトル ⃗t の k 番目の箇所に、新しい個体 c を付け加える。
I 以下のように述語記号 p : PredSym n + 1 に対して、以下のように解釈 int の値を定める。
III

代入操作: int (fml-subst t p) = (t s : D n) → (int p)(gt (0, t s, t))
全称量化子: int (∀x p) = (t s : D n) → (int p)(gt (0, t s, y))、ただし y はフレッシュな変数（を表す D の元）とする。

独立行政法人産業技術総合研究所

11/ 16

解決法その二：論理式のデータ型の情報量を増やす（様相論理）
I データ型 V : {n : N} → {m ≤ n} → Set を定義する。
IIn: 述語の変数の個数
m: 束縛変数の個数

V は、コンストラクター trans : {n : N} → PredSym n → V n,0 を持つ。

通常の表記

オブジェクト

データ型

解釈

int (q)Pred ′ 2

述語記号qPredSym 2trans qV2,0∀x q(x, )forall x (trans q)

V2,1∀x q(x, t)

subst t forall x (trans q)

V2,2q( , )独立行政法人産業技術総合研究所

12/ 16

充足関数 Sat の定義

I Sat (⃗t, φ, ψ, n, n, P, ()) は、|= の表記法ではII⟨⃗t, φ, ψ⟩ |= P であり、また P : V n,n の閉論理式であることを表現する。

独立行政法人産業技術総合研究所

13/ 16

充足関数の計算の実例(∀x)Q(x, t) に対応する論理式 subst t forall x (trans q) を考える。
1. まず外側の subst t を除去
Sat ((⃗t, φ, ψ, 2, 2, (subst t forall x (trans q)), ())= Sat ((⃗t, φ, ψ, 2, 1, (forall x (trans q)), (t))
2. 次に forall x を除去

Sat ((⃗t, φ, ψ, 2, 1, (forall x (trans q)), (t))= (n : N) → (Q, R : Fml n) →Sat ((⃗t, φ∧((∃y)Q(y) → Q), ψ∧((∃y)R(y) → R), 2, 0, (trans q), (y, t))
3. m = 0 なので終了処理（int (q) : D2 → Set）

Sat ((⃗t, φ ∧ ..., ψ ∧ ..., 2, 0, (trans q), (y, t)) = (int (q))(y, t)
有限ステップの変形で (int (q))(y, t) : Set が値として出力される。
独立行政法人産業技術総合研究所

14/ 16

停止判定に合格する理由

I forall と subst はどちらも V n,m → V n,m+1 の型を持つ。除去することで、添え字が m + 1 から m へと明示的に 1 減る。

Im = 0 のとき、必ず終了処理をして、計算は停止する。

I このことが、再帰法による計算が、有限回で必ず停止することを明示的に保証する。このことは Agda も理解することができ、Agda の停止判定に合格することができた。

独立行政法人産業技術総合研究所

15/ 16まとめ
I 結果: 知識様相論理の意味論を証明支援系に実装した。
I 実装中、二つの問題点が見つかった。

(1) 多変数述語を持つ型のデータ型の定義が難しい(2) 充足関数の再帰的定義が停止判定に合格しない
I 以下のように解決した。

(1) 多変数述語をベクトルを使用して定義した。
(2) 論理式のデータ型の情報量を増やした。
IV n,m として、 n 変数述語のうち m 個の変数が束縛されていることを表現するようにした。
I この増えた情報量によって、帰納法を行うことで、停止判定を合格させる定義が可能になった。

独立行政法人産業技術総合研究所

16/ 16