DOSEIの日記

技術メモ+日常ログ

プログラム論

#10 ?

不動点定理。 f = φ(f) の最小不動点が存在する。 φの最小不動点は ⊔{φk(⊥)}k となる(ように拡張した)。φ の構成法。 例えば階乗 fact(x) := if x=0 then 1 else x⋅fact(x-1) は、 F(f) = if x=0 then 1 else x⋅f(x-1) の不動点である。 このとき最小不動…

#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) の形で書かれる…

#2 1章

いつのまにか最初にやる人が決まっていた模様。とりあえず前回の焼き直し。仕様がすべてである、と。ゲ●ツ思想。

#1 ガイダンス

他専攻(のはず)。検証論。ホーアの理論を学ぶってわけだ。これで私のアサーションプログラム能力も高まるかな。初回は理学部の入試問題。最大公約数の性質の証明、ユークリッドの互除法のアルゴリズムの停止性および妥当性の証明。えー、これ学部生できる…