Re: subsorting relationsubsorting relation

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

Dear Sasha,

> At the beginning of Section 3.1 of the Summary it is written: 
> 
> A subsorted signature \Sigma = (S, TF, PF, P, \leq_S) consists of 
> a many-sorted signature (S, TF, PF, P) together with a pre-order 
> \leq_S of subsort embedding on the set S of sorts. 
> 
> >From this, it follows that we have a pre-order \leq_T if we have a 
> signature (T, TF, PF, P). At the same time, in the Semantics the 
> subscript S has no relation to the actual name of the set of sorts (it 
> just stands for Sorts). I discussed the problem with Don (he is here 
> in Novosibirsk at the moment) and the proposition is to remove the 
> subsctipt to avoid the ambiguity.
> 
> What do you think of this?

I agree.

Till

[[[
I also guess that this is okay. So, unless somebody protests strongly
--- this is relevant e.g. for the subsorting part --- then I suggest
we adopt this for the current and future versions of the semantics.

Best regards,

Andrzej Tarlecki
]]]