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

代数的データ構造を扱う関数型プログラムの検証法
岡本 大輔

海野 広志

本論文では代数的データ構造を扱う高階関数型プログラムの新しい検証法を提案する．本提案によって，既存手法では扱うことのできなかった複数のデータ構造が関係する関係的仕様を，再帰的に定義される n 項述語を用いて自由に記述し，検証することが可能になる．本手法は，与えられたプログラム検証問題を，Refinement 型を用いて，１階述語論理式で表現される検証条件の妥当性判定問題へと帰着する．しかし，そのようにして生成される検証条件は，再帰的に定義された述語を含んでおり，既存の SMT ソルバによって妥当性を直接判定することはできない．そこで，本論文では，検証条件を再帰述語を含まない形へと繰り返し精度を向上させながら近似する方法を提案し，それによって既存の SMT ソルバを利用した高速な判定を可能にする．さらに，我々は，提案手法を実装していくつかの関数型プログラムの検証を行い，有望な結果を得た．

を再帰的 1 項述語を用いて記述することはできたが，1 はじめに複数のデータ構造間の関係的仕様を上記 mirror のよ

本論文では，代数的データ構造を扱う高階関数型

うな再帰的 n 項述語を用いて記述することはできなプログラムの新しい検証法を提案する．本提案によっかった．このような再帰的 n 項述語を用いることにて，複数の代数的データ構造が関係する関係的仕様

よって初めて表現できる仕様の例としては他にも，正を，再帰的に定義される n 項述語を用いて自由に記述

規表現マッチング関数の「出力文字列は入力文字列のし，検証することが可能になる．例えば，「引数として部分文字列」といった仕様や，単一化関数の「出力さ受け取った二分木と鏡合わせの二分木を返す」といっれた代入を２つの入力項に適用したものが等しい」とた関数の仕様を以下のような Refinement 型 [3, 10]いった仕様など実用上重要なものが無数に存在する．

として記述することができる．

本論文で提案する新しい検証法は，代数的データ(x : tree) → {y : tree | mirror(x, y)}構造を扱う関数型プログラムと，mirror のような再ここで x, y はそれぞれ入力木と出力木を表し，この帰述語を含む Refinement 型として記述された仕様を型はそれらが以下のように再帰的に定義される述語入力として受け取り，プログラムがその型を持つかどmirror を満たすということを意味している．
mirror(Leaf, Leaf).

うか，つまり仕様を満たすかどうかを自動的に判定する．†1 本手法は内部的に，プログラムが型を持つmirror(Node (x, l1 , r1 ), Node (y, l2 , r2 ))かどうかの判定問題を，１階述語論理式で表現され⇐ x = y ∧ mirror(l1 , r2 ) ∧ mirror(r1 , l2 ).

る検証条件の妥当性判定問題へと帰着する．しかし，この述語は，「2 つの二分木がお互いに鏡合わせになっそのように生成される検証条件は，（仕様記述に用いている」という関係的仕様を表している．従来の検証られた）再帰述語を含んでおり，既存の SMT ソルバ

法 [3–5, 7–10] では，1 つのデータ構造に関する仕様によって妥当性を直接判定することはできない．そこで，本論文では，検証条件を再帰述語を含まない形へ代数的データ構造を扱う関数型プログラムの検証法

Daisuke Okamoto, Hiroshi Unno, 筑波大学, Universityof Tsukuba.

†1 ただし，本論文で扱う検証問題は決定不能なため，本論文では半アルゴリズムを提案する．

プログラムP::={fi pei = ei }i

式

e::=

x | e v | (v1 , . . . , vn ) | v.i|

C v | let x = e1 in e2

パターン

p::=x | C p | (p1 , . . . , pn )値v::=

x | x ve | C v | (v1 , . . . , vn )

図1

論理式

ϕ::=

⊤ | ⊥ | A | ¬ϕ | ϕ1 ⇒ ϕ2|

ϕ1 ∧ ϕ2 | ϕ1 ∨ ϕ2|∀x.ϕ | ∃x.ϕ

ホーン節

H=

∀ex.(A1 ∧ · · · ∧ An ⇒ P (t))

原子論理式

A=P (t) | t1 = t2 | t1 ̸= t2

項

t=x | C t | (t1 , . . . , tn ) | t.i

プログラムの構文

図2

論理式とホーン節の構文と繰り返し精度を向上させながら近似する方法を提案し，それによって既存の SMT ソルバを利用した高速な判定を可能にする．
本論文は以下のように構成されている．まず，2 節

この構文にしたがって二分木の代数的データ型および，入力木と鏡合わせの木を出力する関数 flip を定義すると，以下のようになる．

で検証対象の関数型言語と仕様記述言語を導入する．
次に，3 節と 4 節でそれぞれ，検証条件生成法とそのtype tree = Leaf

妥当性判定法を定式化する．5 節で実装について説明| Node of int * tree * tree

し，6 節で関連研究との比較を行う．最後に 7 節で結論を述べる．

flip Leaf = Leaf
flip (Node (x,l,r)) =2 対象言語

let l’ = flip l in

本節では，提案手法が入力として受け取るプログラ

let r’ = flip r in

ムと仕様を記述するための言語をそれぞれ定義する．

2. 1 プログラム記述言語
提案手法が検証対象とする，代数データ構造を扱う
関数型プログラムの構文を図 1 に示す．基本的には関数型言語 ML と同様の値呼び静的型付き関数型言語
だが，プログラムはトップレベル関数定義 f pe = e の集合として記述される．ここで，pe はパターンの有限Node (x,r’,l’)

2. 2 仕様記述言語
提案手法では，複数のデータ構造間に成り立つべき関係的仕様を，ホーン節の集合によって定義される

n 項述語を含む 1 階述語論理式として記述することができる．例えば，1 節で導入された述語 mirror は稿では省略する．また，値の定義において x v
e は，ve2 つのホーン節からなる集合 mirror(Leaf, Leaf),





 ∀x, y, l , r , l , r .

1 1 2 2D=

x = y ∧ mirror(l1 , r2 ) ∧ mirror(r1 , l2 ) ⇒ 







mirror(Node (x, l1 , r1 ), Node (y, l2 , r2 )) によって定義されている．論理式とホーン節の構文をが空列でない場合，関数 x の部分適用であるとする．

図 2 に示す．ここで，⊤ は恒真式を，⊥ は矛盾式を

本言語では，後に Refinemet 型システムを導入する表す．

列を表し，実行時には関数の実引数に対するパターンマッチが行われる．構文中の C は代数データ型のコンストラクタを表すメタ変数である．代数データ型を定義するための構文は ML と同じであるため，本際の技術的な要請から，構文の一部が値に制限されて提案手法においてユーザは，プログラムの各関数のいる．しかし，let 式があるためこの制限によって一仕様を，再帰述語を含む論理式を用いた Refinement

般性は失われない．

型として記述することができる．例えば，前述の flip
関数の Refinement 型は(x : tree) → {y : tree | mirror(x, y)}のように記述される．この型は，flip 関数の引数 x と返値 y が mirror の関係にあるという仕様を表している．一般の場合の，Refinement 型の構文は以下で定義される．
τ ::= {x : δ | ϕ} | (x : τ1 ) → τ2|(x1 : τ1 ) × · · · × (xn−1 : τn−1 ) × τn
ここで，δ はユーザ定義の代数データ型を表す．

3 検証条件の生成
本検証法では，既存手法 [3, 8, 10] と同様に，プロ
図4

グラムが仕様を満たすことをプログラム中の各関数がその仕様を表す Refinement 型で型付けできることとして定式化し，各関数 f が型付け可能かどうかの判定問題を，検証条件の妥当性判定問題へ帰着する．

充足可能性判定手続きの全体像

mirror(l, l′ )∧mirror(r, r′ )∧ |=D∧y = Node(a, r′ , l′ )⇒ mirror(x, y)

そのような検証条件の生成には，図 7 で定義される

x = Node(a, l, r)

Refinement 型検査関係 D; Γ ⊢ f pe = e ↓ τ を用いる．

4 検証条件の妥当性判定

この関係が意味するのは，再帰述語を定義するホーン

本節では，検証条件の妥当性判定のために，再帰的節の集合 D と，各関数に Refinement 型を割り当てに定義された述語を含む 1 階述語論理式の充足可能る型環境 Γ のもとで，関数 f が Refinement 型 τ を性判定手続きを与える．ここで，論理式 ¬ϕ が充足不持つ，ということである．その関係の導出規則内で能であるとき，またそのときに限り ϕ が妥当である

は，式 e のための型検査関係 D; Γ ⊢ e ↓ τ と型推論関ことに注意されたい．

係 D; Γ ⊢ e ↑ τ が補助的に用いられている．ここで，型推論関係は局所型推論 [6] のために導入されており，4. 1 充足可能性判定手続き

これによって，関数内の部分式に型注釈を書かなくて本論文で提案する充足可能性判定手続きの全体像も，関数の型の情報を局所的に伝播することによって，を図 4 に示す．この手続きでは，入力として与えられその型を推論することが可能となる．また，導出規則た論理式 ϕ が充足可能もしくは不能と判定されるま

内では，部分型判定関係 D; Γ ⊢ τ1 <: τ2 も用いられで，ϕ の再帰述語を含まない論理式への過大近似と過ている．これによって，例えば，{x : int | x = 3} の小近似を，繰り返し精度を向上させながら行う．ここような型を {x : int | x > 0} のように弱めて使うこで，過大近似 ⌈ϕ⌉Dk とは，充足不能性を保つ近似であとが可能となる．

る．つまり，⌈ϕ⌉Dk が充足不能であるならば，ϕ も充これらの関係の導出規則を用いて，入力プログラムの足不能である．一方，過小近似 ⌊ϕ⌋Dk とは，充足可能型検査を行うと，図 3 に抜粋した規則において，論理式性を保つ近似である．つまり，⌊ϕ⌋Dk が充足可能であの妥当性判定が必要となる．これらの論理式を本論文でるならば，ϕ も充足可能である．本手法では，⌈ϕ⌉Dkは検証条件と呼んでおり，本手法の検証条件生成が行っや ⌈ϕ⌉D
k の充足可能性判定には外部の SMT ソルバをているのは，これらの検証条件をすべて集めてくること用いる．

である．例えば，2 節で導入した flip 関数を，その Re-finement 型 (x : tree) → {y : tree | mirror(x, y)}に対して型検査すると，以下の検証条件が生成される．

D ∧ x = Leaf |= y = Leaf ⇒ mirror(x, y)

4. 2 近似アルゴリズム
D
論理式の近似を行うアルゴリズム ⌈ϕ⌉Dk , ⌊ϕ⌋k の説明を行う．D は近似される論理式中に出現する再帰Γ(x) = {y : δ | ϕ1 } D ∧ [[Γ]] |= [x/y]ϕ2D; Γ ⊢ x ↓ {y : δ | ϕ2 }TypeOf(C) = δ1 × · · · × δn → δ D; Γ ⊢ v ↓ δ1 × · · · × δn D ∧ [[Γ]] |= [C v/x]ϕD; Γ ⊢ C v ↓ {x : δ | ϕ}D ∧ [[Γ]] |= ϕ1 ⇒ ϕ2D; Γ ⊢ {x : δ | ϕ1 } <: {x : δ | ϕ2 }図3

妥当性判定が必要な型検査規則の抜粋

述語の定義，k は近似を行う際に再帰述語を展開するが妥当であると判定される．

回数の上限を表すパラメータである．提案アルゴリズ

次に，flip 関数のもう片方の検証条件
mirror(l, l′ )∧y = Node(a, r′ , l′ )D∧mirror(r, r′ )∧ |=⇒ mirror(x, y)
x = Node(a, l, r)の妥当性判定について考えよう．この判定は，ϕ′ をムは，論理式 ϕ 中に出現する再帰述語を展開してその定義に置き換えるが，展開後にその述語が再帰的に出現する場合がある．そこで，無限に展開し続けることを回避するため，展開回数の上限 k に達した場合
は，述語の positive (resp. negative) な位置の再帰的出現を，過大近似 ⌈ϕ⌉kD では ⊤ (resp. ⊥) に，過小近似 ⌊ϕ⌋kD では ⊥ (resp. ⊥) に置き換える．このアルゴリズムの完全な定義を図 7 に示す．
例えば，flip 関数から生成される検証条件の片方

D ∧ x = Leaf |= y = Leaf ⇒ mirror(x, y)の妥当性判定は，ϕ を以下の論理式として，D ∧ ϕ の充足不能性判定に帰着される．

ϕ ≡ x = Leaf ∧ y = Leaf ∧ ¬mirror(x, y)
提案手法によって，ϕ の過大・過小近似が繰り返し行われ，以下の論理式が得られる．

⌈ϕ⌉D0

≡

x = Leaf ∧ y = Leaf ∧ ¬⊥⌊ϕ⌋D0≡

x = Leaf ∧ y = Leaf ∧ ¬⊤⌈ϕ⌉D1

≡x = Leaf ∧ y = Leaf ∧≡¬(x = Leaf∧ y = Leaf) ∧∃a1 , a2 . x = Node(a1 , l1 , r1 )∧¬ ∃l1 , r1 .  y = Node(a2 , l2 , r2 )∧ 
∃l2 , r2 .
a1 = a2 ∧ ⊥ ∧ ⊥x = Leaf ∧ y = Leaf ∧⌊ϕ⌋D1¬(x = Leaf∧ y = Leaf) ∧∃a1 , a2 . x = Node(a1 , l1 , r1 )∧¬ ∃l1 , r1 .  y = Node(a2 , l2 , r2 )∧ 
∃l2 , r2 .
a1 = a2 ∧ ⊤ ∧ ⊤k = 0 では ϕ が充足可能だとも充足不能だとも判定できないが，k = 1 では ⌈ϕ⌉D1 が充足不能であるため，ϕ も充足不能だと判定される．したがって，検証条件以下の論理式として，D ∧ ϕ′ の充足不能性判定へと帰着される．

ϕ′≡mirror(l, l′ ) ∧ mirror(r, r′ ) ∧x = Node(a, l, r) ∧ y = Node(a, r′ , l′ ) ∧¬mirror(x, y)

しかし，この充足不能性判定のために，mirror(l, l′ )と mirror(r, r ′ ) の過大近似と mirror(x, y) の過小近似を，いくら k を上げて精度を向上させながら行っても，mirror のそれぞれの出現が独立に近似される
限りは，充足不能だと判定することはできない．そこで，提案手法では，mirror を近似するための未解
釈関数記号 m : int → tree → tree → bool を導入し，その近似的解釈を述語 mirror の定義を k 回展開したもので与えることによって，D ∧ ϕ′ を以下のように近似する．
x = Leaf ∧ y = Leaf∨
a 1 , a2 ,
x = Node(a1 , l1 , r1 )∧
m(x, y) ⇔ ∃ l1 , r1 , .
y=Node(a,l,r)∧
2 2 2
l2 , r 2a1 = a2 ∧ m(l1 , r2 ) ∧ m(r1 , l2 )(m(l, l′ ) ⇔ · · · ) ∧ (m(r, r′ ) ⇔ · · · )∧m(l, l′ ) ∧ m(r, r′ ) ∧ x = Node(a, l, r) ∧ y = Node(a, r′ , l′ )∧¬m(x, y)これは充足不能であり，この近似は充足不能性を保存するので，D ∧ ϕ′ も充足不能であると判定される．

は，プログラムの検証問題を，再帰述語を含む 1 階述5 実装

語論理式の妥当性判定へと帰着するが，本論文では，我々は提案手法のプロトタイプ実装を行った．充足その判定を行うための新しい手続きの提案も行った．

可能性判定のための SMT ソルバには Z3 [2] を用い今後の課題としては，提案手法をより複雑かつ巨大た．そして，本論文で例として使っている flip 関数がなプログラム例に適用して，有効性の評価を行うこと

述語 mirror を用いて記述された仕様を満たしているが挙げられる．また，本論文で提案した妥当性判定手ことや，map 関数の入出力のリストのサイズが変わ続きが必ず停止するようなホーン節集合の部分クラスらないといった仕様の検証を行い，正しく動作していを明らかにすることも重要な課題である．さらに，妥ることを確認した．

当性判定手続きの近似ループの収束を早めるために，過大・過小近似法の改良を行うことを検討している．

6 関連研究これまでに，リファインメント型に基づいた多くの検証手法が提案されてきており [3–5, 7–10] ，これらは代数データ構造を扱う高階関数型プログラムの検証を行うことができる．しかし，これらの手法では，1 つのデータ構造に関する仕様を再帰的 1 項述語を用いて記述することはできたが，本論文の提案手法のように複数のデータ構造間の関係的仕様を再帰的 n 項述語を用いて記述して検証することはできなかった．

Leon [1] は，Scala で書かれた代数データ構造を扱
う 1 階の関数型プログラムの検証が可能なシステムであり，再帰的に定義された関数を用いて仕様を記述し，検証することができるのが特長である．一方，本論文の提案手法では，ホーン節の集合によって定義される述語を用いて仕様を記述することが可能であるため，双方向性や非決定性といった論理プログラミングの特長を活かした，より柔軟な仕様記述が可能であると考えられる．

7 まとめと今後の課題
本論文では，代数的データ構造を扱う関数型プログラムの新たな検証法の提案を行った．本手法の利点は，既存手法では扱うことのできなかった複数のデータ構造間の関係的仕様を再帰述語によって記述して検証することが可能であるという点である．提案手法

参 考 文 献[ 1 ] Blanc, R., Kuncak, V., Kneuss, E., and Suter,
P.: An Overview of the Leon Verification System:
Verification by Translation to Recursive Functions,
SCALA ’13, ACM, 2013, pp. 1–10.
[ 2 ] de Moura, L. and Bjørner, N.: Z3: An Eﬃcient
SMT Solver, TACAS ’08, 2008.
[ 3 ] Freeman, T. and Pfenning, F.: Refinement types
for ML, PLDI ’91, ACM, 1991, pp. 268–277.
[ 4 ] Kobayashi, N., Tabuchi, N., and Unno, H.:
Higher-order multi-parameter tree transducers andrecursion schemes for program verification, POPL
’10, ACM, 2010, pp. 495–508.
[ 5 ] Ong, C.-H. L. and Ramsay, S. J.: Verifying higher-order functional programs with patternmatching algebraic data types, POPL ’11, ACM,2011, pp. 587–598.
[ 6 ] Pierce, B. C. and Turner, D. N.: Local type inference, POPL ’98, ACM, 1998, pp. 252–265.
[ 7 ] Sato, R., Unno, H., and Kobayashi, N.: Towards
a scalable software model checker for higher-orderprograms, ACM, 2013, pp. 53–62.
[ 8 ] Unno, H. and Kobayashi, N.: Dependent Type
Inference with Interpolants, PPDP ’09, ACM, 2009,
pp. 277–288.
[ 9 ] Unno, H., Tabuchi, N., and Kobayashi, N.: Verification of Tree-Processing Programs via HigherOrder Model Checking, APLAS ’10, LNCS,
Vol. 6461, Springer, 2010, pp. 312–327.
[10] Xi, H. and Pfenning, F.: Dependent types inpractical programming, POPL ’99, ACM, 1999,
pp. 214–227.

Γ(x) = {y : δ | ϕ1 } D ∧ [[Γ]] |= [x/y]ϕ2D; Γ ⊢ x ↓ {y : δ | ϕ2 }Γ(x) = (y : τ1′ ) → τ2′ D; Γ ⊢ (y : τ1′ ) → τ2′ <: (y : τ1 ) → τ2D; Γ ⊢ x ↓ (y : τ1 ) → τ2′) × τn′
Γ(x) = (y1 : τ1′ ) × · · · × (yn−1 : τn−1′D; Γ ⊢ (y1 : τ1′ ) × · · · × (yn−1 : τn−1) × τn′ <: (y1 : τ1 ) × · · · × (yn−1 : τn−1 ) × τn

D; Γ ⊢ x ↓ (y1 : τ1 ) × · · · × (yn−1 : τn−1 ) × τn
D; Γ ⊢ v1 ↓ τ1 . . . D; Γ, x1 : τ1 , . . . , xn−1 : τn−1 ⊢ vn ↓ τn
D; Γ ⊢ (v1 , . . . , vn ) ↓ (x1 : τ1 ) × · · · × (xn−1 : τn−1 ) × τn
D; Γ ⊢ v ↑ (x1 : τ1 ) × · · · × (xn−1 : τn−1 ) × τn D; Γ ⊢ [v.1, . . . , v.(i − 1)/x1 , . . . , xi−1 ]τi <: τD; Γ ⊢ v.i ↓ τD; Γ ⊢ v ↑ τ1 D; Γ ⊢ e ↓ (x : τ1 ) → τ2D; Γ ⊢ e v ↓ τ2D; Γ ⊢ e1 ↑ τ1 D; Γ, x : τ1 ⊢ e2 ↓ τ2D; Γ ⊢ let x = e1 in e2 ↓ τ2

TypeOf(C) = δ1 × · · · × δn → δ D; Γ ⊢ v ↓ δ1 × · · · × δnD; Γ ⊢ C v ↓ {x : δ | ϕ}(p1 : τ1 )  Γ′1D ∧ [[Γ]] |= [C v/x]ϕ. . . (pn : τn )  Γ′n D; Γ, Γ′1 , . . . , Γ′n , x1 = p1 , . . . , xn = pn ⊢ e ↓ τD; Γ ⊢ f p1 . . . pn = e ↓ (x1 : τ1 ) → · · · → (xn : τn ) → τ
TypeOf(C) = δ1 × · · · × δn → δ (p : δ1 × · · · × δn )  Γ(C p : {x : δ | ϕ})  Γ, x = C p, ϕ(x : τ )  x : τ(p1 : τ1 )  Γ1 . . . (pn : τn )  Γn((p1 , . . . , pn ) : (x1 : τ1 ) × · · · × (xn−1 : τn−1 ) × τn )  Γ1 , . . . , Γn , x1 = p1 , . . . , xn = pn
D; Γ ⊢ τ1′ <: τ1 D; Γ, x : τ1′ ⊢ τ2 <: τ2′D; Γ ⊢ (x : τ1 ) → τ2 <: (x : τ1′ ) → τ2′D ∧ [[Γ]] |= ϕ1 ⇒ ϕ2D; Γ ⊢ {x : δ | ϕ1 } <: {x : δ | ϕ2 }D; Γ ⊢ τ1 <: τ1′ . . . D; Γ, x1 : τ1 , . . . , xn−1 : τn−1 ⊢ τn <: τn′′D; Γ ⊢ (x1 : τ1 ) × · · · × (xn−1 : τn−1 ) × τn <: (x1 : τ1′ ) × · · · × (xn−1 : τn−1) × τn′
Γ(x) = {y : δ | ϕ}D; Γ ⊢ x ↑ {y : δ | y = x}

Γ(x) = (y : τ1 ) × · · · × (yn−1 : τn−1 ) × τn
D; Γ ⊢ x ↑ (y1 : τ1 ) × · · · × (yn−1 : τn−1 ) × τn

Γ(x) = (y : τ1 ) → τ2
D; Γ ⊢ x ↑ (y : τ1 ) → τ2D; Γ ⊢ v1 ↑ τ1 . . . D; Γ, x1 : τ1 , . . . , xn−1 : τn−1 ⊢ vn ↑ τnD; Γ ⊢ (v1 , . . . , vn ) ↑ (x1 : τ1 ) × · · · × (xn−1 : τn−1 ) × τn

D; Γ ⊢ v ↑ (x1 : τ1 ) × · · · × (xn−1 : τn−1 ) × τn
D; Γ ⊢ v.i ↑ [v.1, . . . , v.(i − 1)/x1 , . . . , xi−1 ]τiD; Γ ⊢ e ↑ (x : τ1 ) → τ2 D; Γ ⊢ v ↓ τ1D; Γ ⊢ e v ↑ [v/x]τ2D; Γ ⊢ e1 ↑ τ1 D; Γ, x : τ1 ⊢ e2 ↑ τ2D; Γ ⊢ let x = e1 in e2 ↑ τ2TypeOf(C) = δ1 × · · · × δn → δ D; Γ ⊢ v ↓ δ1 × . . . δnD; Γ ⊢ C v ↑ {x : δ | x = C v}[[∅]]=⊤[[Γ, x : {x : δ | ϕ}]]=[[Γ]] ∧ ϕ[[Γ, x : (y1 : τ1 ) × · · · × (yn−1 : τn−1 ) × τn ]]
図5=[[Γ, ϕ]]=[[Γ]] ∧ ϕ[[Γ, x : (y : τ1 ) → τ2 ]]

=

[[Γ]]

[[Γ, y1 : τ1 , . . . , yn : τn ]] ∧ x = (y1 , . . . , yn )Refinement 型検査関係の導出規則

⌈⊤⌉kD=⊤⌈⊥⌉kD=⊥⌈t1 = t2 ⌉kD=t1 = t2

⌈t1 ̸= t2 ⌉kD=t1 ̸= t2⊤∨∃ex.t = t′ ∧ ⌈body(H)⌉k−1D



⌈P (t)⌉kD=⌈¬ϕ⌉kD=¬ ⌊ϕ⌋kD⌈ϕ1 ∧ ϕ2 ⌉kD=⌈ϕ1 ⌉kD ∧ ⌈ϕ2 ⌉kD⌈ϕ1 ∨ ϕ2 ⌉kD=⌈ϕ1 ⌉kD ∨ ⌈ϕ2 ⌉kD⌈ϕ1 ⇒ ϕ2 ⌉kD=⌊ϕ1 ⌋kD ⇒ ⌈ϕ2 ⌉kD⌈∀x.ϕ⌉kD=∀x. ⌈ϕ⌉kD⌈∃x.ϕ⌉kD=∃x. ⌈ϕ⌉kD

⌊⊤⌋kD

=

⊤⌊⊥⌋kD=⊥⌊¬ϕ⌋kD=¬ ⌈ϕ⌉kD⌊t1 = t2 ⌋kD=

t1 = t2⌊t1 ̸= t2 ⌋kD=t1 ̸= t2⊥∨∃ex.t = t′ ∧ ⌊body(H)⌋k−1D

⌊P (t)⌋kD=⌊∀x.ϕ⌋kD=∀x. ⌊ϕ⌋kD⌊∃x.ϕ⌋kD=∃x. ⌊ϕ⌋kD⌊ϕ1 ∧ ϕ2 ⌋kD=⌊ϕ1 ⌋kD ∧ ⌊ϕ2 ⌋kD⌊ϕ1 ∨ ϕ2 ⌋kD=⌊ϕ1 ⌋kD ∨ ⌊ϕ2 ⌋kD⌊ϕ1 ⇒ ϕ2 ⌋kD=⌈ϕ1 ⌉kD ⇒ ⌊ϕ2 ⌋kD

head(A1 ∧ · · · ∧ An ⇒ P (t))=P (t)body(A1 ∧ · · · ∧ An ⇒ P (t))=A1 ∧ · · · ∧ An
図6近似アルゴリズム

if k = 0
if k > 0head(H) = P (t )

if k = 0H ∈ D,

if k > 0H ∈ D,{ex} = F V (H),′{ex} = F V (H),′head(H) = P (t )