Skip to content

Commit 78e3724

Browse files
woodrushwoodrush
authored
Merge pull request #6 from woodrush/lisplambda
Add Binary Lambda Calculus interpreters written in LambdaLisp
2 parents 9c89414 + f5eba8a commit 78e3724

File tree

5 files changed

+704
-3
lines changed

5 files changed

+704
-3
lines changed

‎README.md

+16-3
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44

55

66
LambdaLisp is a Lisp interpreter written as an untyped lambda calculus term.
7+
It basically runs a large subset of Common Lisp as shown in the [Features](#features) section.
78
The entire lambda calculus expression is viewable as a PDF [here](https://woodrush.github.io/lambdalisp.pdf).
89

910

@@ -14,7 +15,7 @@ which takes a string `x` as an input and returns a string as an output.
1415
The input `x` is the Lisp program and the user's standard input,
1516
and the output is the standard output.
1617
Characters are encoded into lambda term representations of natural numbers using the [Church encoding](https://en.wikipedia.org/wiki/Church_encoding),
17-
and strings are encoded as a list of characters with lists expressed as lambdas in the [Mogensen-Scott encoding](https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding),
18+
and strings are encoded as a list of characters with lists expressed as lambdas in the [Scott encoding](https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding),
1819
so the entire computation process solely consists of the beta-reduction of lambda terms,
1920
without introducing any non-lambda-type object.
2021

@@ -254,14 +255,14 @@ Supported special forms and functions are:
254255
- defun, defmacro, lambda (&rest can be used)
255256
- quote, atom, car, cdr, cons, eq
256257
- +, -, *, /, mod, =, >, <, >=, <=, integerp
257-
- read (reads Lisp expressions), print, format (supports `~a` and `~%`), write-to-string, intern, stringp
258+
- read (reads Lisp expressions), read-char, peek-char, print, format (supports `~a` and `~%`), write-to-string, intern, stringp
258259
- let, let*, labels, setq, boundp
259260
- progn, loop, block, return, return-from, if, cond, error
260261
- list, append, reverse, length, position, mapcar
261262
- make-hash-table, gethash (setf can be used)
262263
- equal, and, or, not
263264
- eval, apply
264-
- set-macro-character, peek-char, read-char, `` ` `` `,` `,@` `'` `#\`
265+
- set-macro-character, `` ` `` `,` `,@` `'` `#\`
265266
- carstr, cdrstr, str, string comparison with =, >, <, >=, <=, string concatenation with +
266267
- defun-local, defglobal, type, macro
267268
- malloc, memread, memwrite
@@ -508,6 +509,18 @@ Runnable with:
508509
make test-self-host
509510
```
510511

512+
## Lambda Calculus Interpreter Written in LambdaLisp
513+
The [examples-advanced](./examples-advanced/) directory features lambda calculus interpreters written in LambdaLisp itself.
514+
This means that we have a lambda calculus interpreter written in Lisp, which is written in lambda calculus, that runs on a lambda calculus interpreter.
515+
516+
Furthermore, the interpreter [lisplambda-bit.lisp](./examples-advanced/lisplambda-bit.lisp)
517+
is capable of running [uni.blc](https://www.ioccc.org/2012/tromp/uni.blc),
518+
the bit-oriented BLC self-interpreter from the IOCCC 2012 "Most functional" entry written by John Tromp.
519+
uni.blc is a bit-oriented BLC interpreter written in bit-oriented BLC itself.
520+
From the standard input, it takes a program and a standard input, and evaluates the result of the program applied with the standard input.
521+
522+
This means that we have a lambda calculus interpreter written in lambda calculus itself, which runs on a lambda calculus interpreter written in Lisp, which is written in lambda calculus, that runs on a lambda calculus interpreter.
523+
511524

512525
## How it Works
513526
Implementation details are introduced in [this blog post](https://woodrush.github.io/blog/lambdalisp.html).

‎examples-advanced/krivine.lisp

+122
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
(defparameter **lambdalisp-suppress-repl** t) ;; Enters script mode and suppresses REPL messages
2+
3+
;; Reads a lambda calculus term from the standard input and
4+
;; evaluates its head normal form, based on the Krivine machine.
5+
;; The lambda calculus term is provided as a Binary Lambda Calculus term.
6+
;; The transition process of the Krivine machine is visualized as the term is evaluated.
7+
;;
8+
;; Specifications:
9+
;; - All characters except 0 and 1 are ignored.
10+
;; - BLC is a prefix code. As soon as the interpreter accepts a valid BLC code,
11+
;; the interpreter starts evaluating the code.
12+
;;
13+
;; Usage:
14+
;; $ ( cat bin/lambdalisp.blc | bin/asc2bin; cat examples-advanced/krivine.lisp;
15+
;; echo "01 0010 0010" ) | bin/uni
16+
;; Code: 0100100010
17+
;; Parsed: ((L . 0) (L . 0))
18+
;; Krivine machine transitions:
19+
;; ----
20+
;; t: ((L . 0) (L . 0))
21+
;; p: ()
22+
;; e: ()
23+
;; ----
24+
;; t: (L . 0)
25+
;; p: (((L . 0)))
26+
;; e: ()
27+
;; ----
28+
;; t: 0
29+
;; p: ()
30+
;; e: (((L . 0)))
31+
;; ----
32+
;; t: (L . 0)
33+
;; p: ()
34+
;; e: ()
35+
;; ----
36+
;; Result: (L . 0)
37+
38+
39+
(defun read-print-01char ()
40+
(let ((c (read-char)))
41+
(cond
42+
((or (= "0" c) (= "1" c))
43+
(format t c)
44+
c)
45+
(t
46+
(read-print-01char)))))
47+
48+
(defun parsevarname-stdin ()
49+
(let ((c (read-print-01char)))
50+
(cond
51+
((= "0" c)
52+
0)
53+
(t
54+
(+ 1 (parsevarname-stdin))))))
55+
56+
(defun parseblc-stdin ()
57+
(let ((c (read-print-01char)))
58+
(cond
59+
((= c "0")
60+
(setq c (read-print-01char))
61+
(cond
62+
((= c "0")
63+
(cons 'L (parseblc-stdin)))
64+
;; 1 case
65+
(t
66+
(list (parseblc-stdin) (parseblc-stdin)))))
67+
;; 1 case
68+
(t
69+
(parsevarname-stdin)))))
70+
71+
(defun nth (n l)
72+
(cond
73+
((= 0 n)
74+
(car l))
75+
(t
76+
(nth (- n 1) (cdr l)))))
77+
78+
(defun krivine (term)
79+
(let ((tmp nil) (et term) (ep nil) (ee nil))
80+
(format t "----~%")
81+
(loop
82+
(format t "t: ~a~%" et)
83+
(format t "p: ~a~%" ep)
84+
(format t "e: ~a~%" ee)
85+
(format t "----~%")
86+
(cond
87+
;; Variable
88+
((integerp et)
89+
(setq tmp (nth et ee))
90+
(setq et (car tmp))
91+
(setq ee (cdr tmp)))
92+
;; Abstraction
93+
((eq 'L (car et))
94+
;; If the stack is empty, finish the evaluation
95+
(cond ((eq nil ep)
96+
(return-from krivine et)))
97+
(setq et (cdr et))
98+
(setq ee (cons (car ep) ee))
99+
(setq ep (cdr ep)))
100+
;; Empty term
101+
((eq nil et)
102+
(return-from krivine et))
103+
;; Application
104+
(t
105+
(setq ep
106+
(cons
107+
(cons (car (cdr et)) ee)
108+
ep))
109+
(setq et (car et)))))))
110+
111+
(defun main ()
112+
(let ((parsed nil) (result nil))
113+
(format t "~%")
114+
(format t "Code: ")
115+
(setq parsed (parseblc-stdin))
116+
(format t "~%")
117+
(format t "Parsed: ~a~%" parsed)
118+
(format t "Krivine machine transitions:~%")
119+
(setq result (krivine parsed))
120+
(format t "Result: ~a~%" result)))
121+
122+
(main)

‎examples-advanced/krivine2.lisp

+113
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
(defparameter **lambdalisp-suppress-repl** t) ;; Enters script mode and suppresses REPL messages
2+
3+
;; Reads a lambda calculus term from the standard input and
4+
;; evaluates its head normal form, based on the Krivine machine.
5+
;; The lambda calculus term is provided as a Binary Lambda Calculus term.
6+
;; The transition process of the Krivine machine is visualized as the term is evaluated.
7+
;;
8+
;; The same as krivine.lisp, except the code is specified with the variable `code`,
9+
;; defined after this comment.
10+
11+
(defparameter code "01 0010 0010")
12+
13+
(defun parsevarname (s n cont)
14+
(cond
15+
((= nil s)
16+
(error "Parse error: Unexpected EOF in variable name"))
17+
((= "0" (carstr s))
18+
(cont (cdrstr s) n))
19+
((= "1" (carstr s))
20+
(parsevarname (cdrstr s) (+ 1 n) cont))))
21+
22+
(defun lexblc (s)
23+
(cond
24+
((eq s "")
25+
nil)
26+
((= (carstr s) "0")
27+
(cond
28+
((eq nil (cdrstr s))
29+
(error "Parse error: Unexpected EOF"))
30+
((= (carstr (cdrstr s)) "0")
31+
(cons 'L (lexblc (cdrstr (cdrstr s)))))
32+
((= (carstr (cdrstr s)) "1")
33+
(cons 'A (lexblc (cdrstr (cdrstr s)))))
34+
(t
35+
(lexblc (cdrstr s)))))
36+
((= (carstr s) "1")
37+
(parsevarname (cdrstr s) 0
38+
(lambda (s n)
39+
(cons n (lexblc s)))))
40+
(t
41+
(lexblc (cdrstr s)))))
42+
43+
(defun parseblc (lexed cont)
44+
(cond
45+
;; Abstraction
46+
((eq 'L (car lexed))
47+
(parseblc (cdr lexed) (lambda (t1 pnext) (cont (cons 'L t1) pnext))))
48+
;; Appliation
49+
((eq 'A (car lexed))
50+
(parseblc (cdr lexed)
51+
(lambda (t1 pnext)
52+
(parseblc pnext
53+
(lambda (t2 pnext)
54+
(cont (list t1 t2) pnext))))))
55+
;; Variable
56+
((integerp (car lexed))
57+
(cont (car lexed) (cdr lexed)))
58+
(t
59+
(error "Parse error"))))
60+
61+
(defun nth (n l)
62+
(cond
63+
((= 0 n)
64+
(car l))
65+
(t
66+
(nth (- n 1) (cdr l)))))
67+
68+
(defun krivine (term)
69+
(let ((tmp nil) (et term) (ep nil) (ee nil))
70+
(format t "----~%")
71+
(loop
72+
(format t "t: ~a~%" et)
73+
(format t "p: ~a~%" ep)
74+
(format t "e: ~a~%" ee)
75+
(format t "----~%")
76+
(cond
77+
;; Variable
78+
((integerp et)
79+
(setq tmp (nth et ee))
80+
(setq et (car tmp))
81+
(setq ee (cdr tmp)))
82+
;; Abstraction
83+
((eq 'L (car et))
84+
;; If the stack is empty, finish the evaluation
85+
(cond ((eq nil ep)
86+
(return-from krivine et)))
87+
(setq et (cdr et))
88+
(setq ee (cons (car ep) ee))
89+
(setq ep (cdr ep)))
90+
;; Empty term
91+
((eq nil et)
92+
(return-from krivine et))
93+
;; Application
94+
(t
95+
(setq ep
96+
(cons
97+
(cons (car (cdr et)) ee)
98+
ep))
99+
(setq et (car et)))))))
100+
101+
(defun main ()
102+
(let ((lexed nil) (parsed nil) (result nil))
103+
(format t "~%")
104+
(format t "Input: ~a~%" code)
105+
(setq lexed (lexblc code))
106+
(format t "Lexed: ~a~%" lexed)
107+
(parseblc lexed (lambda (term _) (setq parsed term)))
108+
(format t "Parsed: ~a~%" parsed)
109+
(format t "Krivine machine transitions:~%")
110+
(setq result (krivine parsed))
111+
(format t "Result: ~a~%" result)))
112+
113+
(main)

0 commit comments

Comments
 (0)