Conditions for free types

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear friends,

in a discussion with Peter, we recognized that the well-formedness
conditions for free datatypes can be interpreted in different
ways.

The many-sorted version of the restriction is (2.1.4.1):

  Moreover, the constructors and selectors must be distinct from each 
  other and from the operations declared in the local environment. 

It could be clarifed a bit:

  Moreover, the constructors and selectors must be distinct
  (as qualified symbols)
  from each other and from the operations declared in the local environment. 

The subsorted version of the restriction is (4.1.2.1):

  Finally, the constructors and selectors of a free datatype must neither
  be in the overloading relation with each other nor with functions in the 
  local environment.

Here, the question is whether a constructor or selector may be 
declared twice with the same profile. Actually, the intention was
that it can be, while the above could be read in a different
way (since the overloading relation is reflexive).
A more exact formulation would be:

  Finally, consider the set of qualified constructor and selector symbols
  declared in a free datatype. Any two different elements of this set must 
  not be in the overloading relation, and no element of this set must be
  in the overloading relation with qualified function symbols in the local
  environment. 

Or:

  Finally, the set of qualified constructor and selector symbols
  declared in a free datatype united with the set of qualified function 
  symbols in the local environment must have a trivial overloading
  relation, i.e. any symbol in this set is only in the overloading relation
  with itself, but not with other symbols from this set.

Greetings,
Till