Re: CoFI semantics

[Hubert Baumeister <hubert@mpi-sb.mpg.de>]

Hi Alexandre,

Alexandre Zamulin wrote:
> 
> Here are a few comments on the semantics of structured specifications
> in note S-6.
> 

Thank you for your comments, they are very helpful.

> 1. Page 48 and in the sequel.
> 
> In the previous chapters the pre-order symbol $\leq_S$ is always suppled
> with a subscript, in this chapter it is never supplied with a sub-script.
> I believe that the difference in notation should be eliminated.
> 

I agree. I propose the semantics of structured specifications adopts
$\leq_S$ to keep the clear distinction of the preorder on sorts from the
overloading relations on functions $\leq_F$ and predicates $\leq_P$.


> 2. Page 48.
> 
> I understand that id_S is the identity function on S; I believe, however,
> that is should be indicated explicitly.

Okay. 

> 
> 3. Page 48.
> 
> \sigma^S\union id_S
> 
> The function union operation here is different from that one used in the
> previous chapters. I believe that it should be defined with the use
> of a different symbol. It should be noted which result is produced if
> both S and \bar{S} contain the same sort symbol.

I agree. However, it seems that \sigma_S \union id_S is the only place
where \union is used with the semantics that 
(f \union g)(s) = if s \in dom(f) then f(s)
                  else if s \in dom(g) then g(s)
                       else undef. 
Maybe we should have an operator ext_S(f), extending a partial function
f to a partial function, whose domain includes S. That is:
ext_S(f)(s) = if s \in dom(f) then f(s) 
              else if s \in S then s 
                   else undef

[..]
> 5. Page 53.
> 
> $\Delta$ is required to be an enrichment relative to $\Sigma$.
> 
> Is \Delata really an enrichment? In the previous chapters an enrichment
> was denoted by (\Delta,\Psi). Denoting it by \Delta in this chapter is
> very confusing.

You are right, it should read "\Delta is required to be a signature
extension relative to \Sigma." (This applies also to other judgements in
the section about structured specifications).

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/