Prev Up
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.  
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.  
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).

CoFI Note: L-9 --Version 1.0-- 21 March 1998.
Comments to

Prev Up