无聊的日记

第1章 2026年7月28日

今日回看之前写的生命游戏实现:

(define conway-kernel
  (<< (Array #(1 1 1 1 0 1 1 1 1))
      (rho2 3 3)))
(define (neighbor grid)
  (<< conway-kernel
      (Convolve2 grid '(1 1))))
(define (step grid)
  (Materialize2
   ((Zip-with
     (λ (x n)
       (if (= x 1)
           (if (or (= n 2) (= n 3)) 1 0)
           (if (= n 3) 1 0))))
    grid (neighbor grid))))

(define kernel
  (array '(3 3) (const 1)))
(define (sum9 grid)
  (<< kernel (Convolve2 grid '(1 1))))
(define (step^ grid)
  (Materialize2
   ((Zip-with
     (λ (x n)
       (if (or (= n 3)
               (and (= x 1) (= n 4)))
           1 0)))
    grid (sum9 grid))))

第2章 2026年8月27日

昨日阅读和翻译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))
(define (VAR u)
  (lambda (env)
    (define t (type-of u env))
    (cons t (assume u (&true (reify t))))))
(define (CONS a b)
  (lambda (env)
    (define pa (a env))
    (define pb (b env))
    (define ta (car pa))
    (define tb (car pb))
    (define ca (cdr pa))
    (define cb (cdr pb))
    (define type `(conj ,ta ,tb))
    (cons type
          (&rull $conjI ca cb
                 (&true (reify type))))))
(define (CAR a)
  (lambda (env)
    (define pa (a env))
    (define ta (car pa))
    (define ca (cdr pa))
    (match ta
      ((conj ,t1 ,t2)
       (cons t1 (&rull $conjE1 ca
                       (&true (reify t1))))))))
(define (CDR a)
  (lambda (env)
    (define pa (a env))
    (define ta (car pa))
    (define ca (cdr pa))
    (match ta
      ((conj ,t1 ,t2)
       (cons t2 (&rull $conjE2 ca
                       (&true (reify t2))))))))
(define (LAM u t body)
  (lambda (env)
    (define pbody
      (body (extend-env u t env)))
    (define tbody (car pbody))
    (define cbody (cdr pbody))
    (define type `(-> ,t ,tbody))
    (cons type
          (&rull (&implI u) cbody
                 (&true (reify type))))))
(define (APP a b)
  (lambda (env)
    (define pa (a env))
    (define pb (b env))
    (define ta (car pa))
    (define tb (car pb))
    (define ca (cdr pa))
    (define cb (cdr pb))
    (match ta
      ((-> ,t1 ,t2)
       (unless (equal? t1 tb)
         (error 'APP "type mismatch"))
       (cons t2 (&rull $implE ca cb
                       (&true (reify t2))))))))
(define (CASE a u1 b1 u2 b2)
  (lambda (env)
    (define pa (a env))
    (define ta (car pa))
    (define ca (cdr pa))
    (match ta
      ((disj ,t1 ,t2)
       (let* ((pb1 (b1 (extend-env u1 t1 env)))
              (pb2 (b2 (extend-env u2 t2 env)))
              (tb1 (car pb1))
              (tb2 (car pb2))
              (cb1  (cdr pb1))
              (cb2  (cdr pb2)))
         (unless (equal? tb1 tb2)
           (error 'CASE "branch type mismatch"))
         (cons tb1 (&rull (&disjE u1 u2) ca cb1 cb2
                          (&true (reify tb1)))))))))
(define (INL tb a)
  (lambda (env)
    (define pa (a env))
    (define ta (car pa))
    (define ca (cdr pa))
    (define type `(disj ,ta ,tb))
    (cons type (&rull $disjI1 ca
                      (&true (reify type))))))
(define (INR ta b)
  (lambda (env)
    (define pb (b env))
    (define tb (car pb))
    (define cb (cdr pb))
    (define type `(disj ,ta ,tb))
    (cons type (&rull $disjI2 cb
                      (&true (reify type))))))
(define (ND proof)
  (cdr (proof '())))