comments

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

Dear Don, Hubert,

Please find enclosed some more comments on structured specifications.

Page 61.

{\modelsem{\Sigma, \Mset, \Gamma_s, \Gamma_m}
          {\gram{union}\;\gram{SP}_1, \ldots, \gram{SP}_n}
          {\{ M \mid M|_{\Sigma \cup \Delta_i} \in \Mset_i,\; 1 \leq i 
\leq n \}}}

A signature morphism should be indicated instead of \Sigma \cup \Delta_i 
in M|_{\Sigma \cup \Delta_i} as in the previous cases (I have not found 
the definition of a construction like M|_\Sigma in this document). The 
same is in pages 62, 64, 66.

Page 62.

$\Mset_i | _{\Sigma \cup \Delta_0 \cup \ldots \cup \Delta_{i-1}} = 
M_{i-1}$ for $1 \leq i \leq n$

a) It seems to me that no notion of a reduct of a class of models is 
defined in the document.

b) A class of models instead of a model M_{i-1} should ne indicated.

Page 63.

\begin{array}{c}
         \staticsem{\Sigma, \Gamma_s}
                   {\gram{SPEC}}
                   {\Delta} \\
         \staticsem{\Sigma\union\Delta,\Gamma_s}
                   {\gram{SPEC'}}
                   {\Delta'}\\
        {\staticsem{\Sigma,\Delta'}
                   {\gram{restriction}\;\gram{hiding}\;\gram{SYMB+}}
                   {\Delta''}}
         \end{array}

According to the second condition in the premise, \Delta' is a signature 
extension relative to \Sigma\union\Delta. It seems to me that 
\Sigma\union\Delta should be used instead of \Sigma in the third 
condition. The same is in the subsequent rule.

Page 64, 65 (possibly, somewhere else);

"does not already exists" -> "does not already exist".

Page 68.

a) "Each fitting argument determines a signature extension 
$\Delta^A_i$ and a signature extension morphism $\sigma_i$ from 
$\Sigma^P_i$ to $\Sigma \cup \Delta^A_i$ relative to 
$\Sigma_\bot$, which, together with $\sigma_c$ restricted to 
$\Sigma^P_i$, must yield a valid signature morphism from 
$\Sigma^P_i$ to $\Sigma \cup \Delta^A_i$."

Do we have two morphisms from $\Sigma^P_i$ to $\Sigma \cup \Delta^A_i$? 
What is the difference between them?

b) "$\sigma_c$ is a signature extension morphism from the union 
$\Sigma^P$ of $\Sigma^P_i$ to $\Sigma \cup \Delta^A$ relative to 
$\Sigma_\bot$ given by $\gram{SYMB-MAP*}$. "

In the picture at the bottom of the page this morphism is denoted by \sigma.

c) "Then the resulting signature extension is given by the union of 
$\Sigma \cup \Delta^A$ with the translation of $\Delta$ by $\sigma$."

What is $\sigma$ here?

d)    \Delta^A \cup \sigma(\Delta)\mbox{ is defined}\\
                  ...
        \sigma = \mathit{sigmor}(\sigma_1 \cup \ldots \cup \sigma_n \cup 
\sigma_c)\\

Is it still the same \sigma?

e)     \mathit{sigmor}(\sigma_i \cup \sigma_c|_{\Sigma^P_i})\colon 
      \Sigma^P_i \rightarrow \Sigma \cup \Delta^A_i

It seems to me that this "sigmor" does not correspond to that given in 
page 48.

f) What is \sigma_\Delta in the picture (alos in pages 69, 70)?

g) It seems to me that it would be better to use SIG-MORPH instead of 
SYMB-MAP* in this page (the notation SYMB-MAP*? is very clumsy, "if 
SIG-MORPH is not present..." is also better than "if SYMB-MAP* is not 
present" since SYMB-MAP* is always present by definition).

h) 

{\staticsem{\Sigma,\Gamma_s}
          {\gram{gen-spec-inst}\; \gram{fa}_1\ldots\gram{fa}_n\; 
\gram{SPEC-NAME}\;\gram{SYMB-MAP*?}}
          {\Delta^A \cup \sigma(\Delta)}

According to the syntax, \gram{fa}_1\ldots\gram{fa}_n\; and 
\gram{SPEC-NAME}\; should be in the reverse order. The same is in page 70.

I would not say that I have understood anything in this page :(((

Regards,

Sasha.

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