今日回看之前写的生命游戏实现:
(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))))昨日阅读和翻译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 '())))今日根据Mike Gordon的Hoare逻辑讲义写了一个最小的验证条件生成器.
(define (subst Q E V)
(cond ((pair? Q) (cons (subst (car Q) E V)
(subst (cdr Q) E V)))
((eq? Q V) E)
(else Q)))
(define (:= V E)
(case-lambda
((P Q) (list `(=> ,P ,(subst Q E V))))
((Q) (values (subst Q E V) '()))))
(define ((IF S C1 C2) P Q)
(append (C1 `(and ,P ,S) Q)
(C2 `(and ,P (not ,S)) Q)))
(define ((WHILE S R C) P Q)
`((=> ,P ,R)
(=> (and ,R (not ,S)) ,Q)
. ,(C `(and ,R ,S) R)))
(define ((PRE R C) Q)
(values R (C R Q)))
(define ((SEQ C . C*) P Q)
(let iter ((RC* (reverse C*))
(R Q) (VC '()))
(if (null? RC*)
(append (C P R) VC)
(let-values (((R VC0) ((car RC*) R)))
(iter (cdr RC*) R (append VC0 VC))))))
(define (Hoare P C Q) (C P Q))(Hoare
'(and (= X x) (= Y y))
(SEQ (:= 'R 'X)
(:= 'X 'Y)
(:= 'Y 'R))
'(and (= Y x) (= X y)))最近三个星期我开始工作, 这是我人生中的第一份工作. 我感觉真的很糟糕, 但是我也学到了许多, 以下是我的感想: