[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: comments

Dear Alexandre,

Alexandre Zamulin wrote:
> 
> 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.

The notation M|_\Sigma is short for M|_\iota, where \iota is the
inclusion
of \Sigma into \Sigma' and M is a \Sigma'-algebra. I agree that some 
elementary definitions are missing and they will appear in
the semantics of CASL 1.0 :-)

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

See the note above. There should be a note saying that \Mset|_\sigma is
the same as
{ M|_\sigma | M \in \Mset }.

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

That is indeed a mistake.

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

I think it should be \Sigma,\Delta \cup \Delta'.

In a judgement of the form \Sigma, \Delta |- restriction ... |> \Delta'
we require that \Delta' is a
signature extension of \Sigma, which implies that a restriction cannot
hide symbols from \Sigma.

Thus writing \Sigma \cup \Delta, \Delta' |- restriction ... |> \Delta'',
cannot hide symbols from \Delta. However, the symbols locally introduced
by a LOCAL-SPEC are those of \Delta and are those which should be hidden
in the result.

> 
> Page 64, 65 (possibly, somewhere else);
> 
> "does not already exists" -> "does not already exist".

Right.

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

A fitting morphism has two components. One component is given directly
with each argument, denoted \sigma_i here and goes from \Sigma^P_i to
\Sigma \cup \Sigma^A_i, and the other one is given by a global symbol
map and applies to the union of all parameters, denoted \sigma_c and
goes from \Sigma^P to \Sigma \cup \Delta^A. 

Only the union of \sigma_i with the restriction of \sigma_c to
\Sigma^P_i
has to yield a signature extension morphism from \Sigma^P_i to \Sigma
\cup \Delta^A_i relative to \Sigma_\bot and only this union is relevant
for parameter passing.

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

No, \sigma = sigmorph(\sigma_1 \cup .. \cup \sigma_n \cup \sigma_c),
that is, the union of all single fitting morphisms together with the
global fitting morphism.

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

Yes.

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

Hmm, why not? \sigma_i and \sigma_c|_{\Sigma^P_i} are signature
extension morphisms relative to \Sigma_\bot, thus their union is a
signature extension morphism relative to \Sigma_\bot. To make the union
a proper signature mophisms the function sigmorph is used. 

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

The definition of \sigma_\Delta is given on page 51 and extended to
compound id's on page 71.

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

Okay, it is better to write "if SYMB-MAP* is empty". The problem with
using SIG-MORPH is, that the semantics
of SIG-MORPH is a signature morphism.
However, in the semantics of instantiation, the fitting morphism is
splitted into two parts, the part for each argument and the common part.
Each of the parts itself need not be a signature morphism, only their
union (see also recommendation 6.2). Thus it only complicates things
further if each part of the fitting morphism yields a signature
morphism.

Instead of SYMB-MAP*? it should read SYMP-MAP*. SYMB-MAP*? is a
remainder of substituting SYMB-MAP* for SIG-MORPH.

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

Right.

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

That is a pity, I was so proud of this part :-) But to be serious,
althougth I wrote it, I find the semantics of instantiation quite
complex myself. One source of confusion is the semantics of signature
morphisms and symbol maps. 
This should get better in the semantics for CASL 1.0, when the semantics
of SYMB-MAP'S yield real symbol maps instead of signature extension
morphisms. 

Regards,
	Hubert

-- 
           Hubert Baumeister
           MPI Informatik, Im Stadtwald, D-66123 Saarbr"ucken, Germany
    Phone: (x49-681)9325-220  Fax: -299
   e-mail: hubert@mpi-sb.mpg.de  
      WWW: http://www.mpi-sb.mpg.de/~hubert/