Re: comments

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear Alexandre,

first let me thank you for your careful reading of the CASL-semantics!

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

The parentheses have the following meaning:
Given the notion of set, there is the notion of subset.
Given the notion of signature extension, there is the notion
of sub-signature extension. In order that this "sub"-variant
of the notion of signature extension is not confused with
extension of subsignatures (whatever this would mean),
I used the parentheses: sub-(signature extension)
(opposed to (sub-signature)-extension).
Is there a better way of expressing this?

Now, according to p. 48, "Given a sub-(signature extension) $\Delta_1$ of
$\Delta$" means that both $\Delta_1$ and $\Delta$ are
signature extensions, $\Delta_1 \subseteq \Delta$, and the
inclusion is a signature extension morphism.

Probably "Given a sub-(signature extension) $\Delta_1 \subseteq
$\Delta$" would be more readable.

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

Sorry, there is a mistake. The correct definition on p.50 should read:
\item ${\leq}'={\leq}\intersection (S_1\times S_1)$
\item ${\asymp}'={\asymp}\intersection (S_1\times S_1)$

So subsorting relations and cycles are typically empty in Delta_1,
and Delta' is just Delta_1 with subsorting relations and cycles
inherited from Delta.

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

I hope that the purpose becomes clear now: \Delta' serves to assemble
all the symbols which are not hidden (or which are revealed), and
then the subsorting relations and cycles are inherited from the
original signature.

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

That indicates that we need a more detalied informal explanation of 
what is going on there. Our goal is to write a readable semantics after
all. So I hope this does not discourage you to read further on. 

Greetings,
Till