more comments on subsorting in CoFI Semantics note S-6

[Alexandre Zamulin <zam@cs.usm.my>]

Dear Don,

Please find enclosed some more comments on subsorting.

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$.

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.

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".

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.

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$

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'}} 

Regards,

Alexandre.
----------------------------------------------------------------------
Alexandre Zamulin                              e-mail: zam@cs.usm.my
School of Computer Science                     fax, phone:+60 4 6573335
University Sains Malaysia
11800 Penang, Malaysia
-----------------------------------------------------------------------