claustrophobia

一般λがなんか書くとか

プログラムの停止性とRanking関数

大学・大学院時代の研究テーマは、「プログラムの停止性の自動検証」 ー つまり任意の入力に対しプログラムが停止するかを自動で検証する手法についてだったのですが、プログラムの停止性の特徴付けとして有名なものにRanking関数(Ranking function)があります。

Ranking関数とはつまり、関係が定義された構造(Σ, →)から何らかのwell-ordered structure(W, >)への準同型 f のことで、つまり

a,b∈Σ, a→b ⇒  f(a) > f(b)

が成り立つような写像fのことを言います。大体はwell-ordered setとして(N, >)が使われます。

 

プログラムの停止性とRanking関数の関連について、詳しくはByron Cookの資料(サマースクールのテキスト?)が簡潔にまとまっていていい感じです。適当にググれば出てきます。

http://research.microsoft.com/en-us/um/cambridge/projects/terminator/principles.pdf

関連部分だけ軽く説明すると、プログラムを

  1. S: プログラムの状態
  2. R: プログラムの遷移関係
  3. I: 初期状態

の3つ組(S,R,I)で表したとき、プログラムの停止性は「IからRで到達可能な状態(R*(I)と書く)とRからなる構造(R*(I), R)がwell-founded structureである」ことと定義されます。

さて、(R*(I),R)にRanking関数があれば、(S,R,I)が停止することが言えます。なので、停止性検証の主流な手法の一つとして、そのプログラムに対するRanking関数を見つけてやる、という方法があります。

 

で、前々からちょくちょく考えてたのが「逆は成り立つのか?」ということで、つまりプログラムが停止するとき、そのプログラムに対するRanking関数は必ず存在するか?ということです。well-foundedだがwell-orderedでない集合なんていくらでもある訳で(例えば偶奇が異なる数同士は比較できないように制限した自然数の集合とか)実際どうなんだろうなぁと思っていたのですが、どうやら選択公理を仮定すればwell-founded relationからwell-orderedへの拡張は可能なようで:

[1503.06514] On the Well Extension of Partial Well Orderings

ということはつまりプログラムが停止するならばRを拡張して適当なwell orderingにできるということで、停止するプログラムには必ずRanking関数が存在する、ということになります。

あと、一般のwell-founded relationからwell-orderingへの拡張には整列可能定理が要りますが、 要はプログラムの状態の集合に適当な整列順序を一つ定義できればいいので、状態集合が加算なら選択公理も必要ないような気がします。

 

と、いうようなことを悶々と考えていたりしました。なお未だに以下の点が疑問です。

  1. このことに明確に言及した文献はないのか。(絶対にあると思う)
  2. computableな(つまりプログラムとして書き下せる)Ranking関数が見つかるための条件は何か。

誰か何か知ってたら教えて下さい。