Syntax trees. All logical expressions input to Ref's inference routines are syntax trees produced by the SETL parser (invoked directly from within Ref's code). Such trees may be converted into objects of a different nature, for specific needs of the various inference mechanism; nevertheless, formulae and terms are always submitted in that form to the logical or algebraic manipulation routines which must hence perform recursive walks through them in order to exploit them directly or in order to convert them into different representations. The tags that may appear on the nodes of a syntax tree are discussed in [Click].
Restrictions to the SETL syntax. Virtually every SETL expression also belongs to the realm of Ref (not SETL instructions, although Ref's definitions bear, in their concrete external syntax, a resemblance with them). Two exceptions must be noted: Ref lacks
: f(E1)...(En), f(E1,...,En),
(FORALL x in OM | P(x)),
(FORALL x | P(x)).
Node tags. A syntax tree is represented in the form of a nested tuple, where nesting reflects the descent into subtrees. The first component of each tuple is a string tag encoding the lead operator of the expression represented by that tuple.