Concerning Referential Transparency

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

Dear all,

here are some observations (or a small study note?) spawned by Andrzej's
remark on referential transparency (see below).

The reason why referential transparency is lost is because a SPEC-NAME
denotes a closed specification, ie., a pair (\Sigma,M), while a
specification expression yields an open spec, ie., a partial function
mapping (\Sigma',M') to (\Sigma'',M'') such that \Sigma' \subseteq
\Sigma'' and M'' | \Sigma' \subseteq M'. The restrictions are required
to give semantics to persistent extensions, free specifications and
for the current definition of instantiation of generic specifications.

When a SPEC-NAME is used as a SPEC, one has to interpret a closed
specification (\Sigma,M) as an open specification, ie. as a function
mapping (\Sigma',M') to (\Sigma'',M'').

I think there are two obvious choices:

	i) [| SPEC-NAME qua SPEC |](\Sigma',M') = (\Sigma,M) 

	ii) [| SPEC-NAME qua SPEC |](\Sigma',M') = (\Sigma,M) + (\Sigma',M')

In the first solution the local environment is ignored.  But, since
\Sigma is not necessarily included in \Sigma', this solution does not
work.

The second forms the union of the closed specification denoted by
SPEC-NAME with the environment. This seems to me the right but not so
obvious(?) choice to give semantics to:

Sp1 = sort s, const c:s

Sp2 = extend sort s', const c':s' by Sp1

Then [|Sp2|] = sort s,s', const c:s, c':s'.

A different solution would allow SPEC-NAME to refer to the open
specification denoted by the expression Sp in the definition of
SPEC-NAME:

	[| SPEC-NAME qua SPEC |](\Sigma',M') = [|Sp|](\Sigma',M'), 

where SPEC-NAME is defined by "spec-defn SPEC-NAME Sp"

This solution would give referential transparency. One could require
Sp to be self-contained, that is, Sp should yield a correct
specification wrt. the empty environment.  In this case [|SPEC-NAME|]
could always be interpreted as a closed specification by applying it
to (\emtpyset,1).

One problem with this solution is that if [|SPEC-NAME|] denotes an
open specification it may be undefined for some local environments,
although it is defined for the empty environment (cf.  Andrzej's
example with translation).  This may seem counter-intuitive, because,
if a specification is named, the specification is checked for
well-formedness and using this specification should give no unexpected
'syntax' error within Sp, as it would happen in Andrzej's example.

On the other hand, if [|SPEC-NAME|] denotes a closed specification,
the union with the local environment may also be undefined, for
example, if Sp defines a total function and the local environment a
partial function with the same profile.

I think in the current situation solution ii) would be the best.

Greetings,
	Hubert

Andrzej wrote:
[..]
> 10) p.27, sect.9, 2nd paragraph:
> 
> I'm afraid this is not "quite true": if my understanding of things is
> correct, we do not have referential transparency now (see trivial
> examples below).
> 
> The point is that, as rightly explained in sect.6.2, p.20, just after
> the first group of clauses, naming a specification is a semantically
> meaningful operation, which fixes the "local environment" for the
> specification expression to be empty. Consequently, the structure of
> the expression is not "visible" anymore.
> 
[..]
> **********************************************************************
> Examples of the lack of referential transparency
> **********************************************************************
> 
> For instance (sorry for awkward concrete syntax),
> 
>  SP1 = [sort s, const a: s] translated by {s |-> s'}
> 
> is a legal declaration, yielding a spec with a single sort s' and a
> constant a: s'.
> 
> Then also:
> 
>   SP2 = extend [sort s] by SP1
> 
> yields a legal specification with two sorts s and s' and a constant
> a:s'.
> 
> However, the expression
> 
>   extend [sort s] by
>         ( [sort s, const a: s] translated by {s |-> s'} )
> 
> is not legal.
>
> Moreover, even if everything is well-formed, we may loose equivalence
> of the specifications involved.
> 
> For instance:
> 
>  SP3 = free [sort s, const a: s]
> 
> yields a specification with a unique (up to iso) one-element model.
> Then:
> 
>  SP4 = extend [sort s, const a:s] by SP3
> 
> is equivalent to SP3.
> 
> But
> 
> SP5 = extend [sort s, const a:s] by free [sort s, const a:s]
> 
> admits any algebra as a model!
> **********************************************************************
> 


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