comments

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

Dear Don, Hubert,

Please find some more comments on structural specification.

First, a comment on the definition of the function union:

>(f \union g)(s) = if s \in dom(f) then f(s)
>                  else if s \in dom(g) then g(s)
>                       else undef.

I found a similar definition with the name "overiding union" and a 
special symbol (the arguments are written in the reverse order: g \union 
f) in the book of Bertrand Meyer "Introduction to the Theory of 
Programming Languages" (Prentice Hall, 1991). I do not know whether the 
operation is conventional in mathematics; however, I believe that the 
name is good.

Page 49 and other pages:

     for $XF\in\{\TF,\PF\}$

In the previous chapters union was used, i.e: $XF\in (\TF \cup \PF)$. I 
believe that it is better to follow the same notation.

Page 50: Generation 
of an extension.

"Given a sub-(signature extension)
 $\Delta_1$ of $\Delta$ (which informally speaking represents
 a set of names only, i.\ e.\ has empty subsorting relations and cycles),
 $\Delta'=\langle\Delta_1\rangle_{\Delta}$ is defined as follows:"

The purpose and definition of this construction is not very clear. First, 
I could not understand whether the phrase in the parentheses referred to 
$\Delta_1$ or to $\Delta$. I then consulted with a native English 
speaker, and he told me that the sentence was ambiguous and it could 
refer to either of them. However, following the presence of the definitions

\item ${\leq}'={\leq}_1\intersection (S_1\times S_1)$
\item ${\asymp}'={\asymp}_1\intersection (S_1\times S_1)$

I concluded that subsorting relations and cycles could be empty in Delta 
and non-empty in Delta' (otherwise, the definitions have no sense). I 
found then that this construction in the form 

\langle\Delta'\rangle_{\Delta}$

was used only in page 58 and \Delta' was defined as follows (the last 
line in the page):

$\Delta'=(\bar{S}',\bar{\TF}',\bar{\PF}',\bar{P}',\emptyset,\emptyset)$,

i.e. with empty subsorting relations and cycles (which is natural since 
neither hiding or revealing a sort can create a subsorting relation or a 
cycle). I stopped thus to understand the definition and the purpose of 
the construction \langle\Delta'\rangle_{\Delta}.
    
Page 51, 56:

   \leq'& = & \sigdelta{\sigma}^S({\leq})\\
   \asymp' & = & \sigdelta{\sigma}^S(\asymp)

Is this notation (I mean the application of a function to a relation) 
conventional?
No need to define it?

Page 55. 

The use of \sigma in this page defined as either

$\sigma\colon\Sigma\union\Delta\rightarrow\Sigma\union\Delta'$ 

or

$\sigma\colon\Delta\rightarrow\Delta'$

is very confusing. Thus, one first reads in the first line of the page:

$\sigma\colon\Sigma\union\Delta\rightarrow\Sigma\union\Delta'$ 

and then finds sigmor(\sigma) in the subsequent rule, which could be 
correct only if \sigma is defined in the second way.

Page 55.

"The second condition ensures that the new sort symbol is actually
a sort identifier (and not a function or predicate symbol)."

It seems to me that the condition actually ensures that the new sort 
symbol is just
an identifier. I would recommend to write:

"The second condition ensures that the new sort symbol is actually
an identifier."

Pages 59-60.

 for $XF\in\{\TF,\PF\}$

It seems to me that there should be

for $\bar{XF}' \in (\bar{TF}' \cup \bar{PF}')$

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