comments on CoFI Semantics note S-6

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

Hi,

I have a couple of comments to CoFi Note: S6.

[All of these relate to Basic Specifications, which I wrote.  My
responses are in brackets.  Thanks to Alexandre for his careful
reading!  Would the rest of you please send any comments on the
semantics that you might have?   -- Don Sannella]

1. Page 4:

An extension $\Delta = (S,\TF,\PF,P)$ relative to a signature
$\Sigma = (S',\TF',\PF',P')$ is required to be such that
$\Sigma\cup\Delta$ is a signature.

Since you have here some unions of functions (TF'\cup TF, PF'\cup PF, 
P'\cup P), it would be useful to give a formal definition of such a 
union. I am afraid that not many readers will understand what happens 
when, say, both function TF' and TF have tuples with the same function 
profile. In which way such functions are united?

[There is a comment on the top of p3 saying that union will be used
for various kinds of semantics objects, with "the evident
interpretation".  My intention was that for functions f and g,
	(f u g)(x) = f(x) u g(x)
which I think is fairly evident.  But now I see that I have not been
careful enough in section 2 to ensure that TF(ws)=emptyset where
appropriate, and likewise for PF and P.  This will have to be fixed.]

2. Page 7:

It seems to me that the phrase

where $\ang{s_1,\ldots,s_n}^M = \ang{s_1^M,\ldots,s_n^M}$.

should be rewritten as follows:

where $\ang{s_1,\ldots,s_n}^M = s_1^M \times\ldots\times s_n^M$.

[Yes!]

3. Page 12:

(S,F) & \in & \Constraint = \Sorts \times \Funs \\

It seems to me that there should be (S',F') instead of (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.]

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