Footnotes

 

(1)

University of Bremen  

(2)

That means that no ground term is an instance of more than one left hand-side.  

(3)

Uniqueness follows from the freeness constraints. Note that the free datatype declarations are equivalent to some free specification.  

(4)

Usually, 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.  

(5)

That is, any ground term consisting of the head operation symbol applied to constructor terms must match one of the left hand-sides.  

(6)

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(t₁,...,t_n).