From a9c7c078f70c8a8a2ce047fa90926cc9aaf824e2 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Tue, 29 Apr 2025 01:59:11 -0400
Subject: [PATCH] initial commit

---
 nbe.rkt | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 nbe.rkt

diff --git a/nbe.rkt b/nbe.rkt
new file mode 100644
index 0000000..01b6442
--- /dev/null
+++ b/nbe.rkt
@@ -0,0 +1,39 @@
+#lang racket
+(require racket/treelist)
+
+;; Grammar (Λ)
+;; t := λ t | app t t | i
+
+;; Domain
+;; D ≃ Λ + [D → D]
+;; D_ne = var i | app D_ne D
+;; Define as we go
+(define (ap a b)
+  (match a
+    [`(fun ,f) (f b)]))
+
+(define (ren-ne-dom ξ a)
+  (match a
+    [`(var ,i) `(var ,(treelist-ref ξ i))]
+    [`(app ,a ,b) `(app ,(ren-ne-dom ξ a) ,(ren-dom ξ b))]))
+
+(define (ren-dom ξ a)
+  (match a
+    [`(neu ,a) `(neu ,(ren-ne-dom a))]
+    [`(fun ,f) `(fun ,(λ (ξ0 α) (f (compose ξ0 ξ) α)))]))
+
+(define (interp a ρ)
+  (match a
+    [`(var ,i) (treelist-ref ρ i)]
+    [`(λ ,a)  (list 'fun (λ (ξ x) (interp a (treelist-cons (compose ren-dom ρ) x))))]
+    [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))]))
+
+
+
+(define (reflect a)
+  (list 'neu a))
+
+
+(define (reify a)
+  (match a
+    [`(fun ,f) (reify (f (reflect '(var 0))))]))