Basic Specs: are explicit sorts on terms needed?

[Don Sannella <dts@dcs.ed.ac.uk>]

On Tuesday, Anne wrote:

> According to section 1.3, equations are of the form t_s = t'_s' 
> and definedness formulas of the form D(t_s), where t_s and t_s'
> are *sorted* terms (in ESTerm) and not just fully-qualified terms (in FQTerm).
> I do not see any reason for explicitly sorting the terms, as the sort
> of a term can always be derived (cf. the function "sort").

Peter thought that if explicit sorts were omitted, in the presence of
subsorting there would be a problem with transitivity of equality.

Anne replied:

> It is right that 
> we only have transitivity for [CASL] equations over the same sort.
> 
> Example:
> 
> Given signature:
> 
> sorts s, t, u
> subsorts t < s, t < u
> ops a : s, b ; t, c : u
> 
> a = b  and b = c are wellformed with sort s and u, respectively,
> but a = c is illformed.
> 
> If you prefer to keep the transitivity, 
> I would prefer to annotate the equality sign with the sort.

Till responded:

> If you spell this out within FQTerm (fully-qualified terms), and
> allow equations over FQTerm (rather than over ESTerm), you get
> (trying to come close to Don's and Maura's notational form):
> 
> a_s = Em_{t,s}<b_t> and Em_{t,u}<b_t> = c_u are valid equations,
> and a_s = c_u is not, but transitivity is not destroyed,
> since Em_{t,s}<b_t> and Em_{t,u}<b_t> are different terms!

The bottom line is (Till again):

> You always can infer the sort of a fully-qualified term: 
> just look at the (result) sort of the outmost function symbol or variable.
> Therefore it is redundant to use explicitly-sorted terms (ESTerm).
> It is not necessary to annotate the equality sign with the sort either.
> 
> Historical remark: we introduced explicitly-sorted terms at a time
> where we didn't work with fully-sorted terms in the present form,
> but rather with terms which had some qua's around at some places
> but not everywhere. At that time, the sort could not be infered from
> the term.