結論 完全関数jdは定義できない

証明の方針
完全関数jdが存在するとして,下記の関数fooに
関数jdを適用した場合に起きる矛盾を確認する
 たかだか1つの関数に対してでもjdが値を
返せないならjdは完全関数としては成り立たない
と証明できる

関数foo
(define (foo x)
  (and (jd foo)  (goo x)))
補助関数goo
(define (goo x) (goo x))

証明
(jd foo)の値はその働きから
1. #t  (foo '())が値を持つ場合
2. #f  (foo '())が値を持たない場合
の2通りあり,また,2通りしかない.

仮定1:(jd foo) is #t,つまり(foo '())が値を持つ
(foo '())の結果は
(and (jd foo) (goo x))の値である
仮定1から(and #t (goo x))
(goo x)は任意の引数に対して値を返さない関数であるから
(and #t (goo x)) は値を返さない(無限ﾙｰﾌﾟに陥る)
従って(foo '()) は値を返さない.
これは(jd foo) is #t と矛盾するので,仮定1は成り立たない

仮定2:(jd foo) is #f,つまり(foo '())は値を返さない
(foo '())の結果は
(and (jd foo) (goo x))の値である
仮定2から(and #f (goo x))
その値は(goo x)の値に関わりなく#fとなるので
(and #f (goo x)) is #f
従って(foo '()) は値を返す
これは仮定2と矛盾するので,仮定2は成り立たない

結論
可能な2通りの前提が共に成り立たないので
関数jdは完全関数として定義できるとは言えない.