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

Re: comments

Dear Alexandre,

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

I agree that the name and symbol are okay. The symbol for overriding
union, at least in the 1999 version, is the symbol for union with a
small backslash at the bottom to indicate the asymmetric nature of
overriding union.
However, still I would prefer not to use overriding union but some
operator on functions for the special case of f \union id_S.

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

Can you give a reference? I think that the notation XF \in {TF,PF} is
correct here, because
XF is either the function TF or PF but not an element in the union of TF
and PF. That is, the expanded version of XF'(ws) = XF_1(ws) \cup
XF_2(ws) on page 49 is:

PF'(ws) = PF_1(ws) \cup PF_2(ws) and
TF'(ws) = TF_1(ws) \cup TF_2(ws)

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

I think Till should answer this question :-)

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

This notation seemed obvious to us when writing this down. Since a
relation R is just a set of tuples, lets say R \subseteq S x S, then
f(R) denotes the application of the canonical extension of a function
f:S ->S' to a function from 2^(S x S) to 2^(S' x S') to R, which might
not be so obvious at all :-)

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

Agreed.

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

The production for symbol maps is 
SYMB-MAP ::= symb-map SYMB SYMB 
and for symbols
SYMB ::= SORT | FUN-SYMB | PRED-SYMB 
where
SORT ::= ID
FUN-SYMB ::= fun-symb FUN-NAME FUN-TYPE?
PRED-SYM ::= pred-symb PRED-NAME PRED-TYPE?

Thus to check that in "symb-map s1 s2" s2 is a symbol denoting a sort
name, it is sufficient to see if s2 is 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}')$

I think this is the same situation as above. In writing "XF \in {TF,
PF)" no decorations are used and it is understood that the decorations
are added when replacing XF by TF or PF. Note that in XF'(ws) = XF_1(ws)
\cup XF_2(ws) we had different decorations for each occurence of XF,
while in this case we have only one. 

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/