論壇

昨日阅读和翻译Pfenning的构造性逻辑讲义弄得头昏脑胀, 不仅是因为其言辞精妙深微, 更是因为反复出现的各种自然演绎的图形让我手忙脚乱. 最后我实在忍无可忍, 决心设计和实现一个DSL用于绘制自然演绎. 这个(E)DSL基于Curry-Howard对应, 所以也可以算是一个proof checker. 不过, 它不能绘制原文那些中间步骤 (实际上或许也可以, 但是我有意没有实现), 只是绘制最终的完整的自然演绎图形. 

(define (type-of var env)

  (cond ((assoc var env) => cdr)

        (else (error 'type-of "unknown variable ~s" var))))

(define (extend-env var type env)

  (cons (cons var type) env))

(define (reify t)

  (define (reify t)

    (match t

      ((-> ,t1 ,t2) (&impl (@reify t1) (@reify t2)))

      ((conj ,t1 ,t2) (&conj (@reify t1) (@reify t2)))

      ((disj ,t1 ,t2) (&disj (@reify t1) (@reify t2)))

      (bot $bottom)

      (top $top)

      (,else t)))

  (define (@reify t)

    (match t

      ((-> ,t1 ,t2) (@impl (@reify t1) (@reify t2)))

      ((conj ,t1 ,t2) (@conj (@reify t1) (@reify t2)))

      ((disj ,t1 ,t2) (@disj (@reify t1) (@reify t2)))

      (bot $bottom)

      (top $top)

      (,else t)))

  (reify t))

(struct result (t c) #:transparent)

(define (VAR u)

  (lambda (env)

    (define t (type-of u env))

    (result t (assume u (&true (reify t))))))

(define (GIVEN l t)

  (lambda (env)

    (result t (label l (&true (reify t))))))

(define (CONS a b)

  (lambda (env)

    (match-define (result ta ca) (a env))

    (match-define (result tb cb) (b env))

    (define type `(conj ,ta ,tb))

    (result type

            (&rull $conjI ca cb

                   (&true (reify type))))))

(define (CAR a)

  (lambda (env)

    (match-define (result ta ca) (a env))

    (match ta

      ((conj ,t1 ,t2)

       (result t1 (&rull $conjE1 ca

                         (&true (reify t1))))))))

(define (CDR a)

  (lambda (env)

    (match-define (result ta ca) (a env))

    (match ta

      ((conj ,t1 ,t2)

       (result t2 (&rull $conjE2 ca

                         (&true (reify t2))))))))

(define (LAM u t body)

  (lambda (env)

    (match-define (result tbody cbody)

      (body (extend-env u t env)))

    (define type `(-> ,t ,tbody))

    (result type

            (&rull (&implI u) cbody

                   (&true (reify type))))))

(define (APP a b)

  (lambda (env)

    (match-define (result ta ca) (a env))

    (match-define (result tb cb) (b env))

    (match ta

      ((-> ,t1 ,t2)

       (unless (equal? t1 tb)

         (error 'APP "type mismatch"))

       (result t2 (&rull $implE ca cb

                         (&true (reify t2))))))))

(define (INL tb a)

  (lambda (env)

    (match-define (result ta ca) (a env))

    (define type `(disj ,ta ,tb))

    (result type (&rull $disjI1 ca

                        (&true (reify type))))))

(define (INR ta b)

  (lambda (env)

    (match-define (result tb cb) (b env))

    (define type `(disj ,ta ,tb))

    (result type (&rull $disjI2 cb

                        (&true (reify type))))))

(define (CASE a u1 b1 u2 b2)

  (lambda (env)

    (match-define (result ta ca) (a env))

    (match ta

      ((disj ,t1 ,t2)

       (match-define (result tb1 cb1)

         (b1 (extend-env u1 t1 env)))

       (match-define (result tb2 cb2)

         (b2 (extend-env u2 t2 env)))

       (unless (equal? tb1 tb2)

         (error 'CASE "branch type mismatch"))

       (result tb1 (&rull (&disjE u1 u2) ca cb1 cb2

                          (&true (reify tb1))))))))

(define (ND proof)

  (result-c (proof '())))

当然这里我有意省略了所有并不直接算是这个DSL的实现的次要代码, 那些代码实际上都是用于绘制自然演绎的定义.

以下是一些来源于讲义或是个人随手而写的图形.