still more comments on CoFI Semantics note S-6

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

[The first comment relates to Basic Specifications, and my response is
in brackets.  The others relate to Subsorts, for which I defer to
Maura and Anne.  -- Don Sannella]

I do not quite understand the semantics of the sort declaration in 
the datatype declaration. I read in page 25:

"Note that $s$ will be a sort in $\Sigma$ because of non-linear
visibility."

"$s$ is required to be a sort in $\Sigma$."

I understand that according to the rule at the beginning of the page, a 
datatype declaration relative to a signature $\Sigma$ either declares a new 
sort $s$ or uses a sort from $\Sigma$. If this is really so, then the 
meaning of the above two phrases is unclear to me.

[It declares a new sort s, but then s is already in Sigma, because of
non-linear visibility.  In more detail: consider a BASIC-SPEC
containing a DATATYPE-DECL      datatype-decl s ...
In the rule at the top of p25, s will be declared.  This declaration
of s makes its way to the rule on p18, which "ties the knot" in the
premise by feeding the declared symbols (Delta) in together with those
in the environment (Sigma). The same goes for the comments concerning
f on the bottom half of p25.]

Page 35 (bottom):

\TF^{\#}(w,s') & = & \left\{
\begin{array}{ll}
\TF(w,s')\cup\{\Embs\}&\mbox{\rm if }
w=s \mbox{\rm\ and }s\leq_S s'\\
\TF(w,s')&\mbox{\rm otherwise }
\end{array}\right. \\
\PF^{\#}(w,s) & = & \left\{
\begin{array}{ll}
\PF(w,s)\cup\{\Proj\}&\mbox{\rm if }
w=s' \mbox{\rm\ and }s\leq_S s'\\
\PF(w,s)&\mbox{\rm otherwise }
\end{array}\right. \\

According to the definition, both TF and PF are partial functions. 
Therefore, either of them can be undefined for some (w,s). What is 
produced by \TF(s,s')\cup\{\Embs\} or by \PF(s',s)\cup\{\Proj\} if 
\TF(s,s') or \PF(s',s) does not exist?

It seems to me that the following definition is safer:

\TF^{\#} = TF \cup \{(<s>,s')\mapsto\{Embs\}\mid s\leq_S s'\}
\PF^{\#} = PF \cup \{(<s'>,s)\mapsto\{Proj\}\mid s\leq_S s'\}
\P^{\#} = P \cup \{<s'>\mapsto\{\Smember\mid s\leq_S s'\}\}

However, you still need to give a formal definition of the function union 
operation because the explanation you gave me in response to my first 
comment does not work in case of partial functions.

It also seems to me that a similar problem arises in many cases when you 
write: 

for all $\ws \in \FinSeq{S} \times S$, TF(ws)...

since $\FinSeq{S} \times S$ is infinite.

A minor remark: the meaning of w=s is perfectly understandable; however, 
strictly speaking, one should write w=<s> since w is a sequence.
 
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
-----------------------------------------------------------------------