#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 は最小不動点を持つ。