kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

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

「10.8.1 装備を整える」の続き

同様に∃x≦M[...]min x≦M[...]を定義します

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

(define-syntax (∃ stx)
  (syntax-parse stx
    #:literals (≦)
    [(_ v:id ≦ max:expr body:expr)
     #'(∃≦ max (λ (v) body))]))
     
(define (Min≦ max f)
  (let loop ((x 1))
    (cond ((> x max) 0)
          ((f x) x)
          (else (loop (+ x 1))))))

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

minだと名前がカブるのでMinにしました

Min≦Min(f x)を満たすxが見つからなかった場合は0を返します
x=0から開始すると見つからなかったのかx=0で見つかったのかわからないので
x=1から開始することにしました
も同様に修正
カンが悪かった

ところで、Minはどう見てもそっくりですね
関数とマクロを作るマクロを作ればまとめられそうな気がします

(require (for-syntax syntax/parse))
(require (for-syntax racket/syntax))

(define ≦ #f)

(define-syntax (define-equipment stx)
  (syntax-parse stx
    ((_ name term notfound found)
     #:with fname (format-id stx "~a≦" #'name)
     #'(begin
         (define (fname max f)
           (let loop ((x 1))
             (cond ((> x max) (notfound x))
                   ((term (f x)) (found x))
                   (else (loop (+ x 1))))))
         (define-syntax (name stx)
           (syntax-parse stx
             #:literals (≦)
             [(_ v:id ≦ max:expr body:expr)
              #'(fname max (λ (v) body))]))))))

(define-equipment ∀ not (const #t) (const #f))
(define-equipment ∃ identity (const #f) (const #t))
(define-equipment Min identity (const 0) identity)

若干無理やり感ありますができたみたいです
だけだったらもうちょっとシンプルになったと思うんですが、
Minもいっしょにしようとしたんでconstとか使うことに

けっこう調べた知識を総動員したかも
短くはなりましたがあとで見たらわかるかどうかちょっと心配

とりあえずこれくらいで先に進むことにします

定数の定義

; 定数

(define c0 1)
(define cf 3)
(define cnot 5)
(define cor 7)
(define call 9)
(define clp 11)
(define crp 13)

どんな名前にするのがいいのか悩みましたがまあこんなところで
(全角のゼロとかfとか使ってやろうかと思ったけどさすがにやめた)

それでは長旅に出かけましょう