To some extent, Lisp just extends and thus includes lambda calculus. Indeed, short functions already permit:
|(+ $ 1) # λx.x+1
(|(+ $ 1) 3) # (λx.x+1) 3
(|(+ $ 1)
(|(+ $ 2) 3)) # (λx.x+1) ((λy.y+2) 3)
Going a bit further, a simple macro gives us more or less everything:
(defmacro λ `Executable lambda calc: ((λ x . + 5 x) 5)` [v dot & args]
(if (= 1 (length args))
~(fn [,v] ,(first args)) # to handle e.g. identity: ((λ x . x) 5)
~(fn [,v] (,;args))))
((λ x . + 1 x) 3) # (λx.x+1) 3
((λ x . + x 1)
((λ y . + y 2) 3)) # (λx.x+1) ((λy.y+2) 3)
# n.b. these versions are the same:
(def K (λ x . (λ y . x)))
(def K (λ x . λ y . x))
On the basis of this macro, you can implement anything you want:
(def TRUE (λ x . λ y . x))
(def FALSE (λ x . λ y . y))
(def IF (λ p . λ a . λ b . (p a) b)) # evaluates both branches
(def AND (λ p . λ q . (p q) p))
(def OR (λ p . λ q . (p p) q))
(def NOT (λ p . λ a . λ b . (p b) a))
(def ZERO (λ f . λ x . x))
(def SUCC (λ n . λ f . λ x . f ((n f) x)))
(def ONE (SUCC ZERO))
(def TWO (SUCC ONE))
(def PLUS (λ m . λ n . λ f . λ x . (m f) ((n f) x)))
# church encodings are funcs which require slight translation:
(defn church->bool [b] ((b true) false))
(defn church->int [n] ((n inc) 0))
(church->int (((PLUS TWO) (SUCC TWO))))
(def Z # Y combinator but with a thunk
(λ f . ((λ x . f (λ v . ((x x) v)))
(λ x . f (λ v . ((x x) v))))))
(def factorial
(λ self . λ n .
(if (= n 0)
1 # not church encoding <(^.^)>
(* n (self (- n 1))))))
((Z factorial) 5)
But we should build a real interpreter uses term rewriting:
(import spork/argparse :as arg)
# Alternative models of computation:
# SKI combinators (SASL was implemented in SKI in 1978)
# Turing machines
# Random access memory stack machines
# SSA https://www.cs.princeton.edu/~appel/papers/ssafun.pdf
# Uniform circuit models
# Lambda Calc has only 3 core forms:
# β-reduction - handled by Janet
# Alpha conversion - handled by lexical scope
# Eta reduction - λx. (f x) ≡ f
# But also: δ--reduction
# And typing...
# Haskell's GHC is similar to System F https://en.wikipedia.org/wiki/System_F
# Aaron Stump's https://cedille.github.io/ and Cedille 2
# Aaron Stump's https://gitlab.com/astump97/dcs
# Lambda calculus can be implemented with with:
# single lisp macro (like above)
# graph rewriting (this implementation)
# CESK machine (efficient!)
# de Bruijn indexing
(defn- fold-app "Fold a sequence of atoms into left-associative applications"
[atoms]
(reduce (fn [f a] [:app f a]) (first atoms) (slice atoms 1)))
(defn- fold-lam "Fold a binder list over a body into nested single-parameter abstractions"
[binders body]
(var acc body)
(each v (reverse binders) (set acc [:lam v acc]))
acc)
(def prims "Map primitive operators to binary functions for δ-reduction"
{:+ + :- - :* * :/ /
:% mod
:< (fn [a b] (if (< a b) 1 0))
:= (fn [a b] (if (= a b) 1 0))})
(defn free-vars
"Collects the free variable names of `t` into `acc`"
[t &opt acc]
(default acc @{})
(case (first t)
:lit acc
:var (do (put acc (t 1) true) acc)
:app (do (free-vars (t 1) acc) (free-vars (t 2) acc) acc)
:lam (do (each k (keys (free-vars (t 2)))
(unless (= k (t 1)) (put acc k true)))
acc)))
(var fresh-counter 0)
(defn- fresh-name
"Returns a fresh name derived from `base` to avoid variable capture"
[base]
(++ fresh-counter)
(keyword (string base "$" fresh-counter)))
(defn subst
"Substitutes `s` for free occurrences of `x` in `t`, avoiding capture"
[t x s]
(case (first t)
:lit t
:var (if (= (t 1) x) s t)
:app [:app (subst (t 1) x s) (subst (t 2) x s)]
:lam (let [y (t 1) body (t 2)]
(cond
(= y x) t # x shadowed; stop
(get (free-vars s) y) # y would capture; rename
(let [y2 (fresh-name y)]
[:lam y2 (subst (subst body y [:var y2]) x s)])
[:lam y (subst body x s)]))))
(defn- delta
"Returns the δ-contractum of `(f a)` if it is a saturated primitive, else nil"
[f a]
(when (and (= :app (first f))
(= :var (first (f 1)))
(get prims ((f 1) 1))
(= :lit (first (f 2)))
(= :lit (first a)))
[:lit ((prims ((f 1) 1)) ((f 2) 1) (a 1))]))
(defn step
"Rewrites the leftmost-outermost redex once; returns nil if `t` is in normal form"
[t]
(case (first t)
:lit nil
:var nil
:lam (if-let [b (step (t 2))] [:lam (t 1) b])
:app (let [f (t 1) a (t 2)]
(if (= :lam (first f))
(subst (f 2) (f 1) a) # β-rule
(or (delta f a) # δ-rule
(if-let [f2 (step f)] [:app f2 a] # reduce function (congruence)
(if-let [a2 (step a)] [:app f a2]))))))) # reduce argument
(defn normalize
"Rewrites `t` to a fixpoint, stopping after `fuel` steps to bound divergence"
[t &opt fuel]
(default fuel 1000)
(var fuel2 fuel)
(var cur t)
(forever
(def nxt (step cur))
(when (or (nil? nxt) (zero? fuel2)) (break))
(set cur nxt)
(-- fuel2))
cur)
(defn unparse
"Renders AST `t` back into surface syntax"
[t]
(case (first t)
:lit (string (t 1))
:var (string (t 1))
:lam (string "(λ " (t 1) " . " (unparse (t 2)) ")")
:app (string "(" (unparse (t 1)) " " (unparse (t 2)) ")")))
(defn from-data
"Converts a quoted surface form into an AST term"
[form]
(cond
(number? form) [:lit form]
(symbol? form) [:var (keyword form)]
(tuple? form)
(if (or (= (form 0) 'λ) (= (form 0) (symbol "\\")))
(let [dot (find-index |(= $ (symbol ".")) form)]
(fold-lam (map keyword (slice form 1 dot))
(fold-app (map from-data (slice form (inc dot))))))
(fold-app (map from-data form)))))
(defn run-data
"Normalizes and renders a quoted form, no string parsing"
[form &opt fuel]
(unparse (normalize (from-data form) fuel)))
(defn trace-data
"Returns the rendered sequence of terms from `form` to normal form"
[form &opt fuel]
(default fuel 1000)
(var fuel2 fuel)
(def out @[])
(var cur (from-data form))
(array/push out (unparse cur))
(forever
(def nxt (step cur))
(when (or (nil? nxt) (zero? fuel2)) (break))
(set cur nxt)
(array/push out (unparse cur))
(-- fuel2))
out)
(defmacro lc
"Normalizes a lambda term written as literal syntax: (lc (λ x . + 5 x) 5)"
[& form]
~(run-data ',form))
(defn main
[_ & args]
(def settings
(arg/argparse
"Execute Lambda calculus by rewriting terms to normal form"
"trace" {:kind :flag :short "t" :help "Print every reduction step"}
"fuel" {:kind :option :short "n" :help "Max reduction steps (default 1000)"}
:default {:kind :accumulate :help "The .lc source file to reduce"}
args))
(when (nil? settings) (os/exit 1))
(def pos-args (settings :default))
(when (or (nil? pos-args) (empty? pos-args))
(print "Error: No source file provided.")
(os/exit 1))
(def fuel (if-let [f (settings "fuel")] (scan-number f) 1000))
(def forms (parse-all (slurp (pos-args 0))))
(each form forms
(if (settings "trace")
(each line (trace-data form fuel) (print line))
(print (run-data form fuel)))))
With this, we can execute .lc files with contents like:
((λ x . + 5 x) 5)
(((λ x . (λ y . x)) 1) 2)
(((λ f . (λ x . (f (f x)))) (λ n . + n 1)) 0)
# Build 3 element list 1 2 3, then add the length to the list's sum
((λ PAIR .
((λ FST .
((λ SND .
((λ NIL .
((λ CONS .
((λ FOLDR .
((λ SUM .
((λ LENGTH .
((λ LIST .
((λ P . + (FST P) (SND P))
(PAIR (SUM LIST) (LENGTH LIST))))
(CONS 1 (CONS 2 (CONS 3 NIL)))))
(λ l . FOLDR (λ h acc . + 1 acc) 0 l)))
(λ l . FOLDR + 0 l)))
(λ c n l . l c n)))
(λ h t c n . c h (t c n))))
(λ c n . n)))
(λ p . p (λ a b . b))))
(λ p . p (λ a b . a))))
(λ a b s . s a b))
Using janet lc-interpreter.janet -t example2.lc prints out rewrites until the very end:
# many steps above...
((+ 6) ((+ 1) ((+ 1) (((λ h . (λ acc . ((+ 1) acc))) 3) (((λ c . (λ n . n)) (λ h . (λ acc . ((+ 1) acc)))) 0)))))
((+ 6) ((+ 1) ((+ 1) ((λ acc . ((+ 1) acc)) (((λ c . (λ n . n)) (λ h . (λ acc . ((+ 1) acc)))) 0)))))
((+ 6) ((+ 1) ((+ 1) ((+ 1) (((λ c . (λ n . n)) (λ h . (λ acc . ((+ 1) acc)))) 0)))))
((+ 6) ((+ 1) ((+ 1) ((+ 1) ((λ n . n) 0)))))
((+ 6) ((+ 1) ((+ 1) ((+ 1) 0))))
((+ 6) ((+ 1) ((+ 1) 1)))
((+ 6) ((+ 1) 2))
((+ 6) 3)
9
From here, we could want:
- normal lambda calculus syntax (but I prefer s-expr)
- a compiler (quickly achievable via a wrapper around Janet’s machinery, but how should… main and cmd line args work in lambda calculus?)