ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (1)

数学ガールのゲーデル巻を読んでると、「定義1」から「定義46」までなんだか
プログラムを読んでるみたいですよね？ですよね？

数学ガール/ゲーデルの不完全性定理 (数学ガールシリーズ 3)

しかも関数型っていうか関数そのものですね
なんか証明の中に定義が46個並んでるのは壮観な感じですが
プログラムの中に関数が46個っていうとなんてことない気もします

なーんてことを思ってたらじゃあちょっと書いてみるかという気に
書いたからどうなるってこともない気はするんですけど
ややこしくて理解が難しいのは多分その先の表現定理が出てきてからだし
どう考えたってマトモに動くはずもないし

でもまあやってみようかと
どこまで行けるかな
書くだけなら行けると思うけど

「10.8 《冬》証明可能性へ至る長い長い旅」

このあたりから
必要なら戻って

「10.8.1 装備を整える」

まずは∀x≦M[...]の定義から
こんな感じですかね
それっぽいunicode文字は使っていこうかと思ってます

(define (∀≦ max f)
  (let loop ((x 0))
    (cond ((> x max) #t)
          ((not (f x)) #f)
          (else (loop (+ x 1))))))

ちょっと動かしてみます
3行書いたら動かしてみるくらいじゃないと不安なんです

> (∀≦ 3 (λ (x) (< x 4)))
#t
> (∀≦ 3 (λ (x) (< x 3)))
#f

うん大丈夫

ところでxは0から始まるべきなのか1から始まるべきなのか
ちょっと自信がありませんがとりあえず0で進みます
辻褄が合わないところが出てきたら戻す

ここでsyntax-parse登場
ていうかここで使ってみようと思って先に勉強してたわけです

(require (for-syntax syntax/parse))

(define ≦ #f)

(define-syntax (∀ stx)
  (syntax-parse stx
    #:literals (≦)
    [(_ v:id ≦ max:expr body:expr)
     #'(∀≦ max (λ (v) body))]))

literalは何か定義しないとエラーになってしまいます
とりあえず定義されていれば値はなんでもいいようなので#fにして進みます

> (∀ x ≦ 3 (< x 4))
#t
> (∀ x ≦ 3 (< x 3))
#f

おー
ちょっとそれっぽくなりました
≦は完全に飾りですが
これからたくさん使うので、ラムダラムダ書かずに済むのはありがたいのでは

とりあえずここまでで満足！