CHURCH-REPL
A simple REPL for lambda calculus
Use:
when calling churchrepl and new REPL will be opened.
churchrepl [-f --file file [file ...]] [-v --verbose]
Flags:
(optional) Read definitions and expressions from a file before loading the normal REPL.
-f|--file file [file ...]
(optional) print debugging and verbose output.
-v|--verbose
Church repl file structure:
The EBNF grammar is as follows*:
(* Lambda Program *) program = {line}; line = (define | function); define = "@" alias ":" function; function = lambda | application; lambda = ("位" | "\") variable "." expr; application = '(' expr expr ')'; expr = (lambda | application | variable | alias ) ; variable = /[a-z]/; alias = /[_A-Z][_A-Z0-9]*/;
A simple example program:
@ID: 位x.x @APPLY: 位f.位x.(f x) @TRUE: 位x.位y.x @FALSE: 位x.位y.y @ZERO: 位f.位x.x @SUCC: 位n.位f.位x.(f ((n f) x)) @ONE: (SUCC ZERO) @TWO: (SUCC ONE) @THREE: (SUCC TWO) @FOUR: (SUCC THREE) (SUCC ZERO) (SUCC ONE) (SUCC TWO) (SUCC THREE) (SUCC FOUR)
Note: The 位 (lambda, unicode u03bb) is equivalent to a backslash as far as this program is concerned. When using the repl it may be easier to use a backslash.