Download TEL (Version 0.9) Report and User Manual

 F:;:P [s=t] = F:;:P #fs: (P " t)g
if NCV (s) [ V (t) D(P ),
F and V (s) are disjoint, and
(P #fs: (P " t)g) " s u P " t exists and is proper.
The type checker treats equations asymmetrically to enforce a certain programming style: only the left-hand side can contain variables for which types
have not been derived so far. Of course, the logical semantics and the execution
of equations are symmetric.
Furthermore, an equation type checks only if the least type terms of the left
and the right-hand side have a proper inmum. The reason for this requirement
is that in TEL two terms can denote the same value only if their least type
terms have a proper common lower bound.
Disequations are checked as follows:
F:;:P [s\=t] = F:;:P
if V (s) D(P ) and F:O:P [s=t] is dened.
Boolean conditions are abbreviations for equations:
F:;:P [s] = F:;:P [true=s]
if the top symbol of s is a variable or a function.
To check relational conditions, we need a further auxiliary function. Given a
relation p with the domain
t1 x
x tk x
?tk+1 x
x
?tn
and type terms s1 ; . . . ; sk (k 0), the least domain of p for s1 ; . . . ; sk is dened
as follows:
least domain(p; (s1 ; . . . ; sk )) :=
minf(t1 ; . . . ; tn ) j t1 s1 ^ ^ tk sk g.