## The Syntax of KLambda
is very simple and conforms to a Lisp. Well-formed sentences of Kλ are symbolic expressions (s-exprs).
Any symbol, boolean, string or number is an atom.
Any atom is an s-expr as is () (the empty list).
Any abstraction (lambda X Y) is an s-expr if X is a symbol and Y is an s-expr.
Any local assignment (let X Y Z) is an s-expr if X is a symbol and Y and Z are s-exprs.
Any definition (defun F X Y) is an s-expr if F is a symbol and X is a (possibly empty)
list of non-repeated symbols (formal parameters) and Y is an s-expr. Note definitions are top level
expressions and are not embedded.
Any application (X_{1} ... X_{n}) is an s-expr if
X_{1}, ... , X_{n} are s-exprs. |