Go backward to References
Go up to Top
- University of Bremen
- That means that no ground
term is an instance of more than one left hand-side.
- Uniqueness follows
from the freeness constraints. Note that the free datatype
declarations are equivalent to some free specification.
the semantics of constructor-generated data types in programming
languages is given in a domain-theoretic fashion. But from this,
we usually can build a partial algebra in a canonical way.
- That is, any ground term
consisting of the head operation symbol applied to constructor
terms must match one of the left hand-sides.
- It is also possible to include complete
specifications of partial functions. The complement of
the domain of such a function must completely be specified
with axioms of form not def f(t1,...,tn).
Note: L-9 --Version 1.0-- 21 March 1998.
Comments to email@example.com