From d897ccce099e2f0a292caa6c4df1573cb214c8d7 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Tue, 29 Apr 2025 18:17:49 -0400
Subject: [PATCH] Add README.md

---
 .woodpecker.yaml |  9 ++++++++
 README.md        | 15 +++++++++++++
 nbe-test.rkt     | 12 ++++++++++-
 nbe.rkt          | 55 ++++++++++++++++++++++++++++++++++++++++++++----
 4 files changed, 86 insertions(+), 5 deletions(-)
 create mode 100644 .woodpecker.yaml
 create mode 100644 README.md

diff --git a/.woodpecker.yaml b/.woodpecker.yaml
new file mode 100644
index 0000000..527c342
--- /dev/null
+++ b/.woodpecker.yaml
@@ -0,0 +1,9 @@
+when:
+  - event: [push, pull_request]
+    branch: [main]
+
+steps:
+  - name: build
+    image: racket/racket:8.16-full
+    commands:
+      - racket nbe-test.rkt
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..9b03a45
--- /dev/null
+++ b/README.md
@@ -0,0 +1,15 @@
+# Kripke-style untyped NbE in racket
+[![status-badge](https://woodpecker.electriclam.com/api/badges/4/status.svg)](https://woodpecker.electriclam.com/repos/4)
+An implementation of normalization by evaluation loosely based on [A
+Denotational Account of Untyped Normalization by
+Evaluation](https://www.brics.dk/RS/03/40/BRICS-RS-03-40.pdf) and
+[Abel's thesis on NbE](https://www.cse.chalmers.se/~abela/habil.pdf).
+
+Since the implementation is untyped, the `normalize` function only
+gives you $\beta$-normal forms. However, you can get a little bit of
+$\beta\eta$-equivalence by invoking Coquand's algorithm (`η-eq?`) on
+$\beta$-normal forms.
+
+I'm hoping to expand the repository into a benchmark suite where I can
+visualize the performance trade-off of type-directed NbE compared to
+untyped NbE composed with Coquand's algorithm.
diff --git a/nbe-test.rkt b/nbe-test.rkt
index 51eb93c..e4e34e2 100644
--- a/nbe-test.rkt
+++ b/nbe-test.rkt
@@ -31,6 +31,11 @@
   (tm-abs (tm-abs
            (tm-app b (tm-var 1) (tm-app a (tm-var 1) (tm-var 0))))))
 
+(define (tm-compose a b)
+  (tm-abs (tm-app a (tm-app b (tm-var 0)))))
+
+(define (tm-mult a b) (tm-compose a b))
+
 (define (tm-nat n)
   (if (positive? n)
       (tm-suc (tm-nat (- n 1)))
@@ -40,4 +45,9 @@
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-snd)) tm-fst)
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-fst)) tm-id)
 (check-equal? (normalize (tm-app tm-snd (tm-app tm-pair tm-id tm-fst) tm-fst)) tm-fst)
-(check-equal? (normalize (tm-add (tm-nat 100) (tm-nat 40))) (normalize (tm-add (tm-nat 40) (tm-nat 100))))
+(check-equal? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
+(check-equal? (normalize (tm-mult (tm-nat 3) (tm-nat 2))) (normalize (tm-nat 6)))
+(check-equal? (normalize (tm-mult (tm-nat 11) (tm-nat 116))) (normalize (tm-nat 1276)))
+(check η-eq? (normalize (tm-add (tm-nat 499) (tm-nat 777))) (normalize (tm-add (tm-nat 777) (tm-nat 499))))
+(check βη-eq? (tm-mult (tm-nat 888) (tm-nat 999)) (tm-nat 887112))
+(check β-eq? (tm-mult (tm-nat 888) (tm-nat 999)) (tm-nat 887112))
diff --git a/nbe.rkt b/nbe.rkt
index 841cef8..5be4b12 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -3,9 +3,9 @@
 ;; t := λ t | app t t | i
 
 ;; Domain
-;; D ≃ neu D_ne | fun [D → D]
-;; D_ne = var i | app D_ne D
-;; Define as we go
+;; D := neu D_ne | fun [(var -> var) -> D → D]
+;; D_ne := var i | app D_ne D
+
 
 (define (ap a b)
   (match a
@@ -51,6 +51,53 @@
 (define (normalize a)
   (reify (interp a idsub)))
 
+
+(define (subst ρ a)
+  (match a
+    [`(var ,i) (ρ i)]
+    [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
+    [`(λ ,a) `(λ ,(subst (ext (compose (curry subst (λ (i) `(var ,(+ i 1)))) ρ)
+                              '(var 0)) a))]))
+
+(define (idsub-tm i) `(var ,i))
+(define (subst1 b a)
+  (subst (ext idsub-tm b) a))
+
+(define (eval-tm a)
+  (match a
+    [(list 'var _) a]
+    [(list 'λ a) `(λ ,(eval-tm a))]
+    [(list 'app a b)
+     (match (eval-tm a)
+       [(list 'λ a) (eval-tm (subst1 b a))]
+       [v `(app ,v ,(eval-tm b))])]))
+
+(define (eval-tm-strict a)
+  (match a
+    [(list 'var _) a]
+    [(list 'λ a) `(λ ,(eval-tm-strict a))]
+    [(list 'app a b)
+     (match (eval-tm-strict a)
+       [(list 'λ a) (eval-tm-strict (subst1 (eval-tm-strict b) a))]
+       [v `(app ,v ,(eval-tm-strict b))])]))
+
+;; Coquand's algorithm but for β-normal forms
+(define (η-eq? a b)
+  (match (list a b)
+    [`((λ ,a) (λ ,b)) (η-eq? a b)]
+    [`((λ ,a) ,u) (η-eq? a `(app ,(subst (λ (i) `(var ,(+ i 1))) u) (var 0)))]
+    [`(,u (λ ,a)) (η-eq? `(app ,(subst (λ (i) `(var ,(+ i 1))) u) (var 0)) a)]
+    [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (η-eq? u0 u1) (η-eq? v0 v1))]
+    [`((var ,i) (var ,j)) (eqv? i j)]
+    [_ false]))
+
+
+(define (βη-eq? a b)
+  (η-eq? (normalize a) (normalize b)))
+
+(define (β-eq? a b)
+  (equal? (normalize a) (normalize b)))
+
 (define (tm? a)
   (match a
     [`(λ ,a) (tm? a)]
@@ -58,4 +105,4 @@
     [`(var ,i) (exact-nonnegative-integer? i)]
     [_ false]))
 
-(provide reify interp normalize tm?)
+(provide eval-tm eval-tm-strict reify interp normalize tm? η-eq? βη-eq? β-eq?)