計算論を再読し始めた。最初の同値関係と合同関係で躓くんですけど。

1.2 while プログラム

false で回るのは while プログラムじゃないのかよ。と。インフォーマルかもしれんがそう書いてくれ。まぁプログラムのときはそんなことは考えない。なぜなら、通常は not があるからね。

Python 風に書いてみよう。

ところが not は定義されていないからそうはかけない。そして、通常のフォントにない文字を使ってらっしゃる。引き算してマイナスになったらそれは 0 とかいう特殊な関数。フォントがないからかけねーよ。

もう少し、フォント的に親切な本がないか調べてみたけどラムダ計算にしぼった本てあまりないのね。

R って実数の集合じゃないのかよ。ここの R は 二項関係(binary relation)だって。あと自然数は0から始まる:-)、という定義。定義だから仕方がない。

二項関係とはが詳しかった。今はすぐに知識を検索できて便利だなぁ〜。

定理 1.2.1

任意の N プログラム P に対して、fp を計算する while プログラムがある

図3を単純に考えてみよう(Python 風)。

みたいなプログラムになるね。これ、この絵では分かりづらいけどwhile の箱を抜けるときに強引に break で抜けることになる。

だから while プログラムではないと。なるほど。

プログラム書いてもそうなるね。じゃこれを break なしで"必ず"書けるか？ということね。単純には

できた。できた。何をやっているかというと、E を通過したかどうかの状態を持つようにしたということ。

つまり、もとのプログラムは構造上、ステータス管理している。break というのはステータス管理を while の構造に埋め込む構文シュガーだった!という結論。

でもっと一般化すれば、、、げ、Python は switch case がない。

う〜ん。HDL みたいになったぞ。

あと、not をつかっているから、そこだけ変換すると while プログラムになると。そうやって、一つの形式に正規化が可能だと、それだけを考えればいいから(場合分けしなくて良い。そもそもどんな場合分けが存在するかもわからんし)正規化しましょうということだね。

プログラムからも絵からもわかったことは、ここで問われているのは、プログラムの流れが もとのたどってきた方向(前方)と合流するとき、そこに箱を書いて閉じようとしたときに、その箱から出ようとする線を消すことができるか？(= break 消せせるか？)という問題だね。

系1.2.2

複数の while がある while プログラムを while １個に書き直せるか？という問題だね(多分)。これができると、以降の議論がより簡単になると。

証明が載ってないけどステータス使えば全部書きおろせるんだろうね。while が現れるたびに番号つけていって、switch case に書き直せばできそうだね。

それにしても、このウェブページ書いては見たものの、絵がないとわからりづらい。