A Typol program consists of a list of global declarations (judgements, import clauses, definitions) and a set, or sets, of rules which may be either inference rules or axioms. These rules explain how to deduce sequents from other sequents.
Inference rules have the following form:
Typol semantics state that when we have proved all of the premises, we
have proved the conclusion and thus the rule. The numerator is a list
of sequents, the conclusion a single sequent, and the subject of the
conclusion is called the subject of the rule. The inference rule:
may be interpreted as follows:
The value of the tree (whose associated operator is plus) with descendentsand
is
where
is the result of the evaluation of
is the result of the evaluation of
This rule has three premises, two of which are recursive calls to
evaluate the descendents of the subject tree, and the third actually
adds the resulting integers. The subject of this rule is the pattern
.
Axioms are rules without premises and therefore serve to stop recursive deduction. In Exp, we use the axiom:
which may be interpreted as The value of the integer N is itself. The word integer that appears in the axiom and previous inference rule is the name of the atomic operator in the abstract syntax.