#9?

論理式 p(x, y) を、 p(x, νx) と置き換えたものをプログラム（の仕様）と考える。

while 文は if 文と再帰で書き直せる。つまり

P = while c do A

とすれば、

P = if c then A; P else skip

と等価。

プログラムは、一般に再帰 p=φ(x, νx, p) の形で書かれる。φ を汎関数と考えれば、プログラムは論理式の変換空間 φ 上の不動点である。

関数 f を保守的拡張(conservative extension)して、この空間を完備半順序集合 (CPO; complete partial odered set) にしたい。ドメインに不定値 ⊥ を追加して、⊥ が最小になるように順序 ⊑ を適当に定める。

CPO とは順序、最小元をもち、単調増加列が上限を持つような集合のこと。

定理： CPO は最小不動点を持つ。