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

1.2 while プログラム

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

Python 風に書いてみよう。

while !(y == 0):
    ...

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

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

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

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

定理 1.2.1

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

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

input()
while not(A):
    B
    if C:
        E
        break
    D
output()

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

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

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

input()
do_break=False
while not(A) and not(do_break):
    B
    if C:
        E
        do_break = True
    else:
        D
output()

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

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

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

input()
state = 0
while state != 5:
    if state == 0:
        if A:
            state = 5
        else:
            state = 1
    elif state == 1:
        B
        state = 2
    elif state == 2:
        if C:
            state = 4
        else:
            state = 3
    elif state == 3:
        D
        state = 0
    else: // state == 4
        E
        state = 5
output()

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

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

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

系1.2.2

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

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

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

• lambda calculus