[bg] lambda calculus interpreter

tapl/tests/mlish/bg/README.md

@@ -78,3 +78,16 @@ rock-bit* (encode rock-message rock-tree))
 ```
 
 
+`lambda`
+---
+```
+(fresh [e : Λ] → Int)
+(subst [e : Λ] [i : Int] [v : Λ] → Λ)
+(simpl-aux [e : Λ] [i : Int] → (× Int Λ))
+(simpl [e : Λ] → Λ)
+(eval [e : Λ] → Λ)
+I (Lambda 0 (Var 0))
+K (Lambda 0 (Lambda 1 (Var 0)))
+S (Lambda 0 (Lambda 1 (Lambda 2 (App (App (Var 0) (Var 2)) (App (Var 1) (Var 2))))))
+false (App S K)
+```

tapl/tests/mlish/bg/lambda.rkt

@@ -0,0 +1,95 @@
+#lang s-exp "../../../mlish.rkt"
+(require "../../rackunit-typechecking.rkt")
+
+;; Lambda Calculus interpreter
+
+
+;; Problems:
+;; - Cannot use variable in head position of match (gotta exhaust constructors)
+
+;; -----------------------------------------------------------------------------
+
+(define-type Λ
+  (Var Int)
+  (Lambda Int Λ)
+  (App Λ Λ))
+
+(define (fresh [e : Λ] → Int)
+  (match e with
+   [Var i -> (+ i 1)]
+   [Lambda i e -> (+ i (fresh e))]
+   [App e1 e2 -> (+ 1 (+ (fresh e1) (fresh e2)))]))
+
+(define (subst [e : Λ] [i : Int] [v : Λ] → Λ)
+  (match e with
+   [Var j ->
+    (if (= i j)
+      v
+      e)]
+   [Lambda j e2 ->
+    (if (= i j)
+      e
+      (Lambda j (subst e2 i v)))]
+   [App e1 e2 ->
+    (App (subst e1 i v) (subst e2 i v))]))
+
+(define (simpl-aux [e : Λ] [i : Int] → (× Int Λ))
+  (match e with
+   [Var j -> (tup i (Var j))]
+   [Lambda j e ->
+    (match (simpl-aux (subst e j (Var i)) (+ i 1)) with
+     [k e2 ->
+      (tup k (Lambda i e2))])]
+   [App e1 e2 ->
+    (match (simpl-aux e1 i) with
+     [j e1 ->
+      (match (simpl-aux e2 j) with
+       [k e2 ->
+        (tup k (App e1 e2))])])]))
+
+(define (simpl [e : Λ] → Λ)
+  (match (simpl-aux e 0) with
+   [i e2 -> e2]))
+
+(define (eval [e : Λ] → Λ)
+  (match e with
+   [Var i -> (Var i)]
+   [Lambda i e1 -> e]
+   [App e1 e2 ->
+    (match (eval e1) with
+     [Var i -> (Var -1)]
+     [App e1 e2 -> (Var -2)]
+     [Lambda i e ->
+      (match (tup 0 (eval e2)) with
+       [zero v2 ->
+        (eval (subst e i (subst v2 i (Var (+ (fresh e) (fresh v2))))))])])]))
+
+;; -----------------------------------------------------------------------------
+
+(define I (Lambda 0 (Var 0)))
+(define K (Lambda 0 (Lambda 1 (Var 0))))
+(define S (Lambda 0 (Lambda 1 (Lambda 2 (App (App (Var 0) (Var 2)) (App (Var 1) (Var 2)))))))
+(define false (App S K))
+
+;; -----------------------------------------------------------------------------
+
+(check-type
+  (eval I)
+  : Λ
+  ⇒ I)
+
+(check-type
+  (eval (App I I))
+  : Λ
+  ⇒ I)
+
+(check-type
+  (eval (App (App K (Var 2)) (Var 3)))
+  : Λ
+  ⇒ (Var 2))
+
+(check-type
+  (eval (App (App false (Var 2)) (Var 3)))
+  : Λ
+  ⇒ (Var 3))
+