ShenDoc 30

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₁ ... X_n) is an s-expr if X₁, ... , X_n are s-exprs.