will-stop?

今日は「Scheme手習い」の9章に戻ろう。
will-stop? という関数が出てきた。この関数は、ある関数 f がすべての引数に対して値を返すかどうかを教えてくれる(はず)の関数だ。概略はこんな感じ。

(define will-stop?
  (lambda (f)
    ...))

f が値を返すなら、(will-stop? f) は #t を返し、そうでなければ #f を返す。will-stop?は全関数のはずだ。

じゃあ簡単なところで、引数が空リストの場合について、例を挙げてみてみよう。
まず、f が length のとき、(length (quote())) は0になる。ということは (will-stop? length) は #t を返すはずだ。
つぎに、f が eternity のときはどうだろう。eternity はこんな関数だった

(define eternity
  (lambda (x)
    (eternity x)))

eternity はどんな引数に対しても値を返さない。もちろん空リストに対してもだ。ということは (will-stop? eternity) は #f を返すことになる。

さて、3つ目の例はすごく興味深い。

(define last-try
  (lambda (x)
    (and (will-stop? last-try)
         (eternity x))))

この関数に対して (will-stop? last-try) は #t を返すだろうか、それとも #f を返すだろうか。
last-try の引数が空リストのとき、つまり (last-try (quote ())) の値は、(will-sto? last-try) の値に依存する。なぜなら (and …) は1つ目のS式の値が #f なら2つ目以降は評価しないからだ。そして1つ目のS式、つまり (will-sto? last-try) の値は #t か #f のどっちかしかありえない。
そこで、まずは (will-stop? last-try) の値が #f だと仮定してみよう。すると (and #f ...) は常に #f なので、(and #f (eternity (quote()))) の値は #f だということになり、(last-try (quote ())) は停止する。これは、(will-stop? last-try) を #f と仮定したことと矛盾する。
じゃあ、#t と仮定したらどうだろう。すると今度は (eternity (quote ())) の値に依存することになり、停止しない。つまり (will-stop? last-try) は #f のはずで、#t と仮定したことと矛盾してしまう。

結局これはどういうことかというと、ある関数 f が停止するかどうかを判定してくれるはずの will-stop? は実は定義できない、ってことだ。
問答では、「ありがとう Alan M. Turing (1912~1954) と Kurt Godel (1906~1978)」と書いてある。