Isabelle Tutorial その17

6.4 Well-Founded Relations and Induction

整礎性は手続きの停止性と関係します。例えば複雑な再帰関数の定義にはその停止性を保証するための整礎関係を示す必要があり、また多くの数学的帰納法は整礎帰納法の特別な場合です。

関係 $\prec$ が整礎であるとは、関係 $\prec$ が無限下降列を持たないことです。

$\cdots \prec a_{2} \prec a_{1} \prec a_{0}$

多くの場合、関係が整礎であるかどうかはその構造から求められます。一般的な方法は $x \prec y \Leftrightarrow f \, x < f \, y$ を満たすような自然数を返す評価関数 $f$ を示すことです。

Isabelle/HOLには関係less_thanが定義されています。次の二つの定理は、less_thanの振る舞いと、それが整礎であることを表わしています。

((?x, ?y) : less_than) = (?x < ?y)　　　　(less_than_iff)
wf less_than　　　　　　　　　　　　　　　(wf_less_than)

評価の考えを関係の逆像に広げることができます。関数fによる関係rの逆像に無限下降列があるならば、rにも無限下降列があります。Isabelle/HOLには次の定理が証明されています。

inv_image ?r ?f == {(x, y). (?f x, ?f y) : ?r}　　　　(inv_image_def)
wf ?r ==> wf (inv_image ?r ?f)　　　　　　　　　　　　(wf_inv_image)

関係measure sizeが、原始再帰や、データ型上の構造的帰納法を正当化します。measureは次のように定義されています。

measure == inv_image less_than　　　　(measure_def)
wf (measures ?fs)　　　　　　　　　　 (wf_measure)

最も重要な構造の一つに、辞書順の組み合わせがあります。これは、次のように定義されています。

?ra <*lex*> ?rb == {((a, b), a', b'). (a, a') : ?ra | a = a' & (b, b') : ?rb}　　　　(lex_prod_def)
[| wf ?ra; wf ?rb |] ==> wf (?ra <*lex*> ?rb)　　　　　　　　　　　　　　　　　　　　(wf_lex_prod)

帰納法には様々な形がありますが、どれも次に示す整礎帰納法の特別な場合です。

$\begin{array} [\forall y. y \prec x \rightarrow P(y)] \\ \vdots \\ P(x) \\ \overline{P(y)} \end{array}$

Isabelleではこれを次のように表わしています。

[| wf ?r; !!x. ALL y. (y, x) : ?r --> ?P y ==> ?P x |] ==> ?P ?a　　　　(wf_induct)

6.5 Fixed Point Operators

不動点演算子は集合を再帰的に定義します。最小不動点は帰納的定義に、最大不動点は余帰納的定義に対応します。

定理は単調関数にのみ使用できます。Isabelleにおける単調性の定義は全ての順序関係にオーバーロードされています。

mono ?f = (ALL x y. x <= y --> ?f x <= ?f y)　　　　(mono_def)

不動点演算子の場合、順序関係は部分集合関係になります。これに加えて、単調性には次の導入規則と破壊規則が定義されています。

(!!x y. x <= y ==> ?f x <= ?f y) ==> mono ?f　　　　(monoI)
[| mono ?f; ?x <= ?y |] ==> ?f ?x <= ?f ?y　　　　　(monoD)

最小不動点で最も重要な性質はそれが不動点であることであり、そこから次のような帰納ルールも定義されています。

mono ?f ==> lfp ?f = ?f (lfp ?f)　　　　　　　　　　　　　　　　　　　　 (lfp_unfold)
[| ?a : lfp ?f; mono ?f; !!x. x : ?f (lfp ?f Int {x. ?P x}) ==> ?P x |]
==> ?P ?a　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　(lfp_induct_set)

最大不動点も同様ですが、こちらは余帰納ルールが定義されています。

mono ?f ==> gfp ?f = ?f (gfp ?f)　　　　　　　　　　　　　　　　　 　　(gfp_unfold)
[| mono ?f; ?a : ?X; ?X <= ?f (?X Un gfp ?f) |] ==> ?a : gfp ?f　　　　(coinduct_set)

最大不動点を使って定義されている最も知られた概念はバイシミュレーションでしょう。プロセス代数におけるバイシミュレーションの証明には余帰納法を使用します。