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

相互法則 reciprocity law

起きたら、授業にぎりぎり。霧雨。プログラム論、難しいけど結構楽しい。やっぱりもっと理論的なところ勉強したいなぁ。ところで、 BOSS がプログラムの不動点とかよく知ってるみたいなんだけど…。何でも知ってるなぁ…。不動点っていろんなところで出てくる…