In natural semantics, computing the value of an expression in a language amounts to proving that a particular proposition holds. A proposition holds when it can be formally derived from the set of rules that constitute the Typol program. Thus, the proposition:
X is half a man.
would hold if we had expressed the fact that:
Centaur is half a man.
somewhere in a set of Typol rules. The symbol X is a variable. For the expression to hold, X must:
A proposition in Typol has the syntax:
<expression_s> [ <symbol> <expression_s> ]
where <expression_s> is a list of expressions separated by commas. These expressions are terms. They are patterns that represent fragments of an abstract syntax tree. These patterns contain operator names from the formalism and may contain metavariables that stand for subtrees. An atomic tree pattern is the name of the atomic operator followed by an appropriate value.
The <symbol> and second <expression_s> are optional. The
symbols that appear in semantic equations have no intrinsic meaning,
they only separate Typol identifiers (variables, syntactic operators,
phyla, programs, types, ...). However, the turnstyle () has a
conventional meaning that it retains in Typol.
To express the above proposition in Typol, we might write:
X : half a man.
which would hold given a set of rules that included:
Centaur : half a man.
In Exp, evaluating an arithmetic expression amounts to proving that the expression may be reduced to a single integer value. An Exp proposition should express the relationship between the original expression and the final integer value. In English, the proposition might be ``the value of expression exp is val.'' In Typol, we have adopted the notation exp : val.