# A Natural Deduction Renderer (?

**URL:** <https://racket.discourse.group/t/a-natural-deduction-renderer/4396>\
**Category:** Show & Tell\
**Created:** [September 21, 2026, 11:23am UTC](https://racket.discourse.group/t/a-natural-deduction-renderer/4396 "2026-09-21T11:23:44Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![ulambda](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/ulambda/32/1495_2.png) [@ulambda](https://racket.discourse.group/u/ulambda)\
**Post date:** [September 21, 2026, 11:23am UTC](https://racket.discourse.group/t/a-natural-deduction-renderer/4396/1 "2026-09-21T11:23:44Z")

</div>

I write a EDSL which checks a proof (in intuitionistic propositional logic) and then generates a corresponding natural deduction. This is based on my SMathML.

```scheme
(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 (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 '())))

```

Here are some examples.

```scheme
(MB (ND (LAM $u `(-> (disj ,$A ,$B) ,$C)
             (CONS (LAM $w $A
                        (APP (VAR $u)
                             (INL $B (VAR $w))))
                   (LAM $x $B
                        (APP (VAR $u)
                             (INR $A (VAR $x))))))))

```

 ![image](https://global.discourse-cdn.com/free1/uploads/racket/original/2X/b/bd7d712728d715851f213a3c97aa09e3a23f2349.png)

```scheme
(MB (ND (LAM $u `(conj (-> ,$A ,$C) (-> ,$B ,$C))
             (LAM $w `(disj ,$A ,$B)
                  (CASE (VAR $w)
                        $x (APP (CAR (VAR $u)) (VAR $x))
                        $y (APP (CDR (VAR $u)) (VAR $y)))))))

```

 ![image](https://global.discourse-cdn.com/free1/uploads/racket/original/2X/3/350807252ab74108ebfaae1377b4e6493a66d53e.png)

```scheme
(let ((Neg (lambda (A) `(-> ,A bot))))
  (MB (ND (LAM $u (Neg `(disj ,$A ,(Neg $A)))
               (APP (LAM $v (Neg $A)
                         (APP (VAR $u)
                              (INR $A (VAR $v))))
                    (LAM $w $A
                         (APP (VAR $u)
                              (INL (Neg $A) (VAR $w)))))))))

```

 ![image](https://global.discourse-cdn.com/free1/uploads/racket/original/2X/2/2f962db2e20e66cc00e7d8fc233f67ea2334e482.png)  
Have fun with it!