定理証明手習い (16) 全域

• 全域とは、どんな値を渡しても関数が値を持つということ

この間pairは全域、って話が出てました

組み込み関数は、すべて全域です。
そうだったんですか！

そうだったんですか！

Scheme手習いでは

lのcarは何ですか。
ここで
lは'()です。
答えはありません。

って掟になってたけどこれは全域じゃないってことだよな
素のRacket(r5rsにしても)でやるとエラーになります

全域なら(car '())の値はなんだろう
j-bob-lang.scmより

(define (car x) (if (pair? x) (s.car x) '()))
(define (cdr x) (if (pair? x) (s.cdr x) '()))

'()か
そういえばCommon Lispでは(car '())も(cdr '()))も'()だったっけ？
Schemeと比べてなんか変だなと思ったけど全域であることを大事にしたってことでしょうか

すぐ下にはこう書いてあります

意外かもしれませんが、そうなのですよ。
それじゃあ、(cdr 'grapefruit)の値は何になるっていうんですか？
考慮するのは、コンスしたものに対するcdrの結果だけです。(cdr 'grapefruit)には何かしら値があるはずですが、それが何であるかを知る必要はなく、値があるということだけわかれば十分なのです。

ふーん
理屈上、そんな引数で評価されることはないわけだから何でもいいってことかな
実用的な観点からはエラーにしてほしい気がするけど
理論上は全域じゃないと取り扱いが面倒な感じはする

ここでは、全域というのはいつでも正しい値を返すという意味じゃなくて、
ただいつでも値を返すっていう意味と理解して進みます
組み込み関数もifも必ず値を返すのでそれらを組み合わせただけなら
必ず値を返すはず
値を返さないっていうのは無限ループしちゃってるときくらいですかね

Defunの法則は更新されて最終バージョンに
再帰的であっても全域であれば置き換えていいことになりました