Re: question from Zamulin about the CASL semantics of subsorting

[Anne Haxthausen <ah@it.dtu.dk>]

Dear Alexandre,

Thanks a lot for all your comments to the CASL semantics of subsorting
in CoFI document S6. Here are our replies.

Best regards,
   Maura Cerioli, 
   Till Mossakowski and 
   Anne Haxthausen
-------------------------
>Page 38:
>
>$\IsoRel{s}{s'}$ iff both $s\leq_S s'$ and $s'\leq_S s$ for all
>$s,s'\in S$
>
>Since one cannot first declare both $s\leq_S s'$ and $s'\leq_S s$ and 
>then conclude that $\IsoRel{s}{s'}$, then it is better not to write "iff" 
>here. I suggest to write:
>
>If $\IsoRel{s}{s'}$, then both $s\leq_S s'$ and $s'\leq_S s$ for all
>$s,s'\in S$.
We think that the point is that "iff" is the full requirement, that
apparently makes the IsoRel redundant. But, if you look at the definition
as a fixed point, you see that the IsoRel is needed in the extensions and
for uniformity we add it to signatures as well.
Indeed, if you consider the followng example Fool
    sorts s,s'
     s< s'
     s'<s
that is uncorrect, without IsoRel, because if we get IsoRel as derived from
the signature, then we would have that  (E stands for emptyset)
({s,s'},E,E,{s<s',s'<s}) |- Fool |> ({s,s'},E,E,{s<s',s'<s})
that's correct, while using IsoRel we have
({s,s'},E,E,{s<s',s'<s},{s=s'}) |- Fool |> ({s,s'},E,E,{s<s',s'<s},E)
but this is not sufficient to deduce ({s,s'},E,E,{s<s',s'<s},{s=s'}) as
semantics for Fool, because the right-hand side is smaller.

---------------------------
>Page 38:
>
>"A subsorted extension ... relative to an extended subsorted signature .. "
>
>I seems to me that the use of both "extension" and "extended" is quite 
>confusing. I would sugest to replace "extended" in "extended subsorted 
>signature" with some other word.
>

Yes, that is confusing. How about the term "augmented" or "safe".
Do anybody have a better proposal?

---------------------------
>Page 38:
>
>"Analogously, a subsorted enrichment $(\Delta,\Psi)$ relative to an
>extended subsorted signature $\Sigma =
>(S',\TF',\PF',P',\leq'_S,\ISOREL')$ consists of a subsorted
>extension $\Delta = (S,\TF,\PF,P,\leq_S,\ISOREL)$ relative to $\Sigma$ \st\
>$((S,\TF,\PF,P),\Psi)$ is a (many-sorted) enrichment relative
>to the signature $(S',\TF',\PF',P')$."
>
>Is everything OK with this sentence? It sounds to me like "a subsorted 
>enrichment ... consists of subsorted extension".

The sentence should have been:

Analogously, a subsorted enrichment $(\Delta,\Psi)$ relative to an
extended subsorted signature $\Sigma =
(S',\TF',\PF',P',\leq'_S,\ISOREL')$ consists of a subsorted
extension $\Delta = (S,\TF,\PF,P,\leq_S,\ISOREL)$ relative to $\Sigma$ 
and a set of sentences $\Psi$
\st\
each $\psi \in \Psi$ is a sentence over 
$(S' \cup S, \TF' \cup TF,\PF' \cup PF, P' \cup P, 
  \RTclosure{\leq'_S\cup\leq_S})$ 

---------------------------
Page 40:

>(s,s'),(s',s)\in
>              \RTclosure{\preceq_S\cup\leq_S}\textrm{\ iff } \IsoRel{s}{s'}
>
>It seems to me that you should add to this $for all s, s' \in (S \cup 
>\{s^1, ... , S^n\}$ like you did it in page 45.
Yes

>It also seems to me that the condition can be written in a simpler way: 
> 
>$(s^{n+1}, s^i) \in
>              \RTclosure{\preceq_S\cup\leq_S}\textrm{\ iff } 
>\IsoRel{s^i}{s^{n+1} for i = 1, ... n$

That's true for the basic part, because if the newly introduced sorts
creates a new cycle, then they are made isomorphic too.
But, this is not anymore true if compound identifiers are taken into account.
eg if you have a signature Sigma with sorts s,s',f[s],f[s'] and subsort relation
f[s]<f[s'] and use it to process the declaration s'<s, then you get the
extension Delta with all components empty, but the subsorting relations
that consists of s'<s and f[s']<f[s].
But Delta is not, technically speaking an extension of Sigma, because
uniting it with Sigma does not result in a signature, as both f[s']<f[s]
and f[s]<f[s'] though f[s'] and f[s] are not in the IsoRel.
Thus, we would prefer to leave the more complex condition also for the
basic part.

---------------------------
Page 45:

>{(s^1,s^2),(s^2,s^1)\in
>              \RTclosure{\{(s',s)\}\cup\leq_S}}\textrm{\ iff}\\
>        \multicolumn{1}{r}{\IsoRel{s^1}{s^2}\textrm{\  for all\ 
>}s^1,s^2\in S}
>
>It seems to me that this condition also can be written in a simpler way:
>
>{(s, s') \in \RTclosure{\{(s',s)\}\cup\leq_S}}\textrm{\ iff} 
>{\IsoRel{s}{s'}} 

Same comment as to page 45