more comments on CoFI Semantics note S-6

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

[Nearly all of the following relate to Basic Specifications.  My
responses are in brackets.  -- Don Sannella]

Hi,

This is a comment for pages 25-26. You have at the bottom of page 25:

\rulesection{\staticsem{\Sigma,f,\ws,n}{\gram{COMPONENT}}{s',(\Delta,\Psi)}}
$f$ is required to be a total function in $\Sigma$ with profile
$\ws = (w,s)$ and $1 \leq n \leq |w|$.
$s'$ is a sort in $\Sigma$ and
$(\Delta,\Psi)$ is an enrichment relative to $\Sigma$.

It seems to me that it would be useful to indicate that $s'$ is an element 
of $w$. It is the same at the beginning of the next page.

[Agreed.  I will add some explanatory comments here and for CONSTRUCT
a few lines earlier.  Maybe elsewhere too.]

I am returning now to your answer regarding (S',F') and (S,F).

> [In the notation used -- which isn't defined anywhere but is inspired
> by the notation used in the Definition of Standard ML (MIT Press,
> 1990) -- this change wouldn't make any difference.  (S,F) here just
> indicates the notation to be used for constraints, with primes and/or
> subscripts added where required.]

I agree that, principally, it does not make difference which of the 
notations is to be used. However, it seems to me that you sacrifice 
nothing and help the reader at the same time if you are consistent and do 
not change the notation at least at the same page. The same remark refers to 
the use of "n" in page 25:

\rulesection{\staticsem{\Sigma,f,\ws,n}{\gram{COMPONENT}}{s',(\Delta,\Psi)}}

and "m" in the next page.

[Okay, I will try to avoid the potential confusion.  Certainly this
will be easy on p25-26.]

Some more comments:

Page 10, 37. I have found three slightly different notations for a term:

f_\ws\ang{t_1,\ldots,t_n} (page 10)

f_{(w,s)}\ang{t_1,\ldots,t_n}} (page 10 and many other pages)

f_{w,s}\ang{t_1,\ldots,t_n}} (page 37)

Does it make sense to have all the three?

[Since (w,s) is an alternative form of ws (p4 near top), the first two
are equivalent.  I agree that there is no need for both the second and
the third.]

Page 30: p \in P \ang{s_1,\ldots,s_n}

Possibly, it make sense to explain that $P \ang{s_1,\ldots,s_n}$ means
$P(\ang{s_1,\ldots,s_n})$?

[I use parentheses for grouping and simple juxtaposition for function
application.  I get this convention from ML.  Since <s1,...,sn> is
already grouped, the parentheses in P(<s1,...,sn>) are redundant.
Similarly, in f \in TF(<s1,...,sn>,s) (on p32 near the top) the
parentheses are for grouping and not function application.  I agree
that this should be explained somewhere.  In the final version of the
semantics, I plan to add a section at the beginning about the form of
the semantics with an explanation of the meta-language used, for which
the remarks on p2-3 and p17 are a start.]

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