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 ().
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.
Any application (X1 ... Xn) is an s-expr if
X1, ... , Xn are s-exprs.