[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[CoFI] Revised proposal for CASL Views, Imports (700 lines)
To: cofi-language@brics.dk
Subject: [CoFI] Revised proposal for CASL Views, Imports (700 lines)
From: "Peter D. Mosses" <pdm@daimi.aau.dk>
Dear CoFI Language Design Task Group Participants,
Please find appended a proposal to adjust the CASL Summary to:
* LET PARAMETERS AND ARGUMENTS EXTEND IMPORTS of generic specs
* CLARIFY THE INTENDED SEMANTICS OF GENERIC VIEWS
* ELIMINATE IMPLICIT FITTING VIEWS
This proposal is based on recent e-mail discussion between Hubert
Baumeister, Till Mossakowski, Peter D. Mosses, Don Sannella, and
Andrzej Tarlecki, concerned mainly with establishing a satisfactory
basis for the formal semantics of generic specifications and views in
CASL.
If this proposal is adopted, the effect on the CASL Summary would be
some small but significant adjustments to Sections 6.2 and 6.3, and
the removal of Section 6.3.2. Minor changes would also be needed in
the abstract and concrete syntax.
As mentioned in Appendix F of the CASL Summary v0.99, the syntax and
semantics of views were there still regarded as TENTATIVE, and the
need for revision was not entirely unexpected. Implicit fitting of
generic views has turned out to be semantically more complicated than
some of us had anticipated. Moreover, the methodological need for
implicit views has been questioned, and since in any case they merely
allow the use of a specification instead of an explicit view - or in
practice: a generic specification instantiation instead of a generic
view instantiation - it seems best to leave them to extensions (or
future versions) of CASL.
For a simple example, suppose we have:
spec ELEM = sort Elem
spec LIST[ELEM] = free type List ::= nil | cons(Elem;List)
spec NAT = free type Nat ::= 0 | succ(Nat)
view NATasELEM: ELEM to NAT = Elem |-> Nat
We may instantiate LIST by writing LIST[view NATasELEM] or
LIST[NAT fit Elem |-> Nat]. Implicit fitting views allowed us to
write also LIST[NAT]. This would no longer be allowed.
Similarly, if we have also the generic view:
view LISTasELEM [ELEM]: ELEM to LIST[ELEM] = Elem |-> List
we may instantiate LIST by writing LIST[view LISTasELEM[view NATasELEM]]
or LIST[ LIST[NAT fit Elem |-> Nat] fit Elem |-> List ]. Implicit
generic fitting views allowed us to write this also as LIST[LIST[NAT]],
and this also would no longer be allowed.
COMMENTS ARE SOLICITED - ESPECIALLY FROM ANYONE WHO OBJECTS TO THE
ELIMINATION OF IMPLICIT FITTING VIEWS! Since we are already in the
vacation period, the deadline for comments on this final detail of the
CASL language design is:
FRIDAY 21 AUGUST 1998
Please send comments to cofi-language@brics.dk AS SOON AS POSSIBLE!
(The formal semantics of CASL v0.99 is nearing completion, and should
not be delayed further by the discussion of this proposal.)
Sorry for the length of this e-mail: I'd have preferred to install it
as a note for web access, but couldn't find the time for it...
Peter
_________________________________________________________________
========= Peter D. MOSSES Associate Professor, PhD
==== ==== BRICS mailto:pdmosses@brics.dk
========= Dept. of Computer Science == pdmosses@daimi.aau.dk
==== ==== University of Aarhus http://www.brics.dk/~pdm
==== ==== Ny Munkegade, bldg. 540 Telephone: +45 8942 3364
==== ==== DK-8000 Aarhus C, Denmark Telefax: +45 8942 3255
_________________________________________________________________
PROPOSED CHANGES TO THE CASL SUMMARY
+ indicates new lines, - indicates lines to be deleted,
! indicates corrected lines, [...] indicates unchanged lines
5 Structuring Concepts
[...]
Fitting may also be
+ achieved by explicit use of named views between the
- achieved by (implicit or explicit) use of named views between the
parameter and argument specifications.
[...]
- * Given another signature Sigma', a mapping of symbols in |Sigma| to
- symbols in |Sigma'| determines the set of all morphisms from Sigma
to
- Sigma' that both extend the given mapping, and are identity on
common
- symbols of Sigma and Sigma', other than those already in the domain
of
- the mapping. (Mapping an operation or predicate symbol implies
mapping
- the sorts in the profile consistently.)
6.2 Specification Definitions
SPEC-DEFN ::= spec-defn SPEC-NAME GENERICITY SPEC
+ GENERICITY ::= genericity IMPORTS PARAMS
- GENERICITY ::= genericity PARAMS IMPORTS
PARAMS ::= params SPEC*
IMPORTS ::= imports SPEC*
A generic specification definition SPEC-DEFN with some parameters and
some imports is written:
spec
+ SN ( given SP''1, ..., SP''m ) [SP1] ... [SPn] =
- SN [SP1] ... [SPn] given SP''1, ..., SP''m =
SP
end
[...]
It defines the name SN to refer to the specification that has
parameter specifications SP1, ..., SPn (if any), import specifications
SP''1, ..., SP''m (if any), and body specification SP. This extends
the
global environment (which must not already include a definition for
SN). The local environment given to the defined specification is
empty, i.e., the specification is implicitly closed.
The well-formedness and semantics of a generic specification are
+ essentially as for the imports, extended by the union of the
+ parameter specifications and then by the body:
+
+ { SP''1 and ... and SP''m } then { SP1 and ... and SPn } then SP
- essentially as for the union of the parameter specifications and the
- imports, extended by the body:
-
- { SP1 and ... and SPn and SP''1 and ... and SP''m } then SP
The difference between declaring parameters and leaving them implicit
in an extension is that each parameter has to be provided with a
fitting argument specification in all references to the specification
name SN. The declared parameters show just which parts of the generic
specification are intended to vary between different references to it.
+ The imports, in contrast, are fixed, and common to the parameters,
+ body, and arguments.
[...]
6.2.1 Specification Instantiation
[...]
+ The signature Sigmai given by the parameter specification SPi
+ and the symbol mapping SM determine a signature
+ morphism from Sigmai to Sigma'i, as explained in Chapter 5. The
+ fitting argument is well-formed only when
+ the signature of the target of this morphism is included in that of
SP'i.
- The signature Sigmai given by the parameter specification SPi, the
- signature Sigma'i given by the the corresponding argument
- specification, and the symbol mapping SM determine a set of signature
- morphisms from Sigmai to Sigma'i, as explained in Chapter 5. The
- fitting argument is well-formed only when this set is a singleton,
- i.e., the fitting argument morphism is well-defined. Note that mapping
- an operation or predicate symbol generally implies non-identity
- mapping of the sorts in the profile.
[...]
+ Each fitting argument FAi is regarded as an extension of the union
+ of the imports and the current environment.
The fitting argument morphism has to be identity on all symbols
! declared by the imports SP''1, ..., SP''m of the generic
specification,
if there are any.
+ Let SP' be the extension of the imports and generic parameters by the
+ body of the specification named SN:
+
+ { SP''1 and ... and SP''m } then { SP1 and ... and SPn } then SP
- Let SP' be the extension of the generic parameters and imports by the
- body of the specification named SN:
-
- { SP1 and ... and SPn and SP''1 and ... and SP''m } then SP
Let FM be the morphism yielded by the fitting arguments FA1, ..., FAn,
extended to a morphism applicable to the signature of SP' (and written
as a list of symbol maps). Then the semantics of the well-formed
instantiation SN[FA1]...[FAn] is the same as that of the
specification:
! SP' with FM and SP'1 and ... and SP'n
+ where each SP'i is the specification of the fitting argument FAi.
Each model of an argument FAi is required to be a model of the
corresponding parameter SPi, otherwise the instantiation is
undefined. The instantiation is also undefined whenever the result is
not a push-out.
6.3 Views
- N.B. Views have only recently been incorporated in CASL, and their
- syntax and semantics have not yet been finalized. In fact the present
- version of this section differs significantly from the previous draft
- version, as it no longer relies on names of specifications to
- determine the applicability of views; it also makes the parameters of
- generic views explicit.
[...]
Generic parameters in a view definition allow the same view to be
instantiated with different fitting arguments, giving compositions of
the morphism defined by the view with other fitting morphisms.
+ The source SP of the view is NOT in the scope of the parameteres
+ SP1,...,SPn, and the instantiation affects only the target SP'.
6.3.1 Fitting Views
FIT-ARG ::= ... | FIT-VIEW
FIT-VIEW ::= fit-view VIEW-NAME
A reference to a non-generic fitting argument view FIT-VIEW is simply
written:
view VN
It refers to the current global environment, and is well-formed as an
argument for a parameter SPi only when the global environment includes
a view definition for VN of type from SP to SP', such that the
signatures of SP and of SPi are the same. The view definition then
provides the fitting morphism from the parameter SPi to the argument
specification given by the target SP' of the view.
If the generic specification being instantiated has imports, the
fitting morphism is then the union of the specification morphism given
by the view and the identity morphism on the imports. The argument
specification is the union of the target of the view and the imports.
+ Each model of SP is required to be model of SPi, otherwise the
+ instantiation is undefined.
- Note that checking whether a view can be used as a fitting morphism
- only depends on the signatures of the involved specifications and thus
- no semantic check is needed to ensure the applicability of a view.
FIT-VIEW ::= ... | fit-view VIEW-NAME FIT-ARG+
A fitting argument view FIT-VIEW involving the instantiation of a
generic view to fitting arguments is written:
view VN[FA1]...[FAn]
It refers to the current global environment, and is well-formed only
when the global environment includes a generic view definition for VN
with parameters that can be instantiated by the indicated fitting
arguments FA1, ..., FAn to give a view of type from SP to SP', such
that the signatures of SP and of SPi are the same.
+ As with non-generic views, each model of SP is required to be a model
+ of SPi, otherwise the instantiation is undefined.
- 6.3.2 Implicit Fitting Views
- [...]
________________________________________________________________________
Finally, here is an extract of the discussion that led to the above
proposal:
(Abbreviations: TM - Till Mossakowski; PDM - Peter Mosses;
DTS - Don Sannella; AT - Andrzej Tarlecki)
AT> 1. I understand that the first issue to resolve is whether or not
AT> imports for generics should also (implicitly) underly parameters, or
AT> only bodies of the generics.
AT>
AT> Here I agree with what seems to be the conclusion reached, namely:
AT> yes, imports precede both parameters and the body, so that
implicitly
AT> parameters extend imports (and consequently, the body does so as
well,
AT> as it extends the parameters, even if they are empty).
AT>
AT> The suggested concrete syntax for this, with the imports placed
AT> between the name introduced and the parameters, decorated
sufficiently
AT> to make this unambiguous, seems fine to me as well.
PDM> i.e. spec SN (given SP') [SP1]...[SPn] = SP
PDM> where the obligatory parentheses around "given SP'" eliminate any
PDM> doubt about whether [SP1]...[SPn] are parameters of SN or arguments
of
PDM> SP'.
AT> The argument for this is that it may be useful from time to time,
and
AT> when the fact that imports are visible within parameters is not
used,
AT> then neither the semantics nor the intuitive understanding of the
AT> generic spec is affected.
AT>
AT> Consequently, i think, at instantiation, actual parameters should
AT> always be implicitly treated as extending the imports, and the
fitting
AT> morphisms should be implicitly extending the identities on imports.
AT>
AT> Is this the current [proposal]?
PDM> Yes - although of course one then has to unite the current
environment
PDM> with the imports to get the environment for the actual parameter,
PDM> which seems a bit complicated. Never mind: the actual parameter
may
PDM> often be a named spec, in which case its environment is irrelevant.
AT> 2. The fitting morphisms are required to be proper specification
AT> morphisms in the "model semantics" of instantiations. Intuitively,
AT> this generates the expected proof obligation for the user.
AT>
AT> Right?
PDM> Right.
AT>
------------------------------------------------------------------------
AT> To be honest, as far as I am concerned, once the above is fixed i am
AT> happy. The rest seems to concern views, about which i have no strong
AT> intuition and in fact I would willingly leave them out, especially
if
AT> they are to be invoked implicitly. Still, i would like to know what
is
AT> going on there, and I would probably try to argue against (or for)
AT> certain decisions, so let me continue.
AT>
-----------------------------------------------------------------------
AT>
AT> 3. Views: these are declared with specific source and target
AT> specifications. Just as for fitting morphisms, the semantics
requires
AT> them to be true specification morphisms, thus generating the
AT> corresponding proof obligation at the time of the view declaration.
AT>
AT> Right?
PDM> Right.
AT> 4. Views can be generic. I thought that this meant essentially only
AT> that the target spec of the view is generic, and that instantiation
of
AT> a view simply meant instantiation of the target (and composing the
AT> morphism appropriately).
AT>
AT> Is this still right?
PDM> Yes.
AT> We are not considering the situation where also the source spec is
AT> parameterized (by the same, or smaller parameter), right?
PDM> Right. Regarding both abstract and concrete syntax, however, it
may
PDM> cause confusion if the parameters SPi of the generic view occur
before
PDM> the source spec SP, i.e., view VN [SP1]...[SPn] : SP to SP' = ...
PDM> One might consider e.g. view SP by VN [SP1]...[SPn] as SP' = ...
PDM> although it would then be awkward if we (in some later version)
wanted
PDM> to allow the "by VN" to be omitted. Never mind.
AT> What about view VN : SP to SP' [SP1]...[SPn] = ... at the risk
that
AT> symbols in SP' might occur before being introduced in one of the
AT> parameters?
AT> I read through the current summary trying to check what it says
about
AT> this, and I realized that essentially there is nothing there about
the
AT> meaning of genericity for views. I guess this has to be clarified in
AT> v.1.0...
AT>
AT> BTW: given that our generic specs may have imports, wouldn't it also
AT> make sense to allow for imports for generic views?
AT>
AT> (I am against, trying to keep the views as simple as possible --- I
AT> would even like to disallow generic views as well...)
PDM> I seem to recall someone [...] arguing that imports were not needed
PDM> here, but I can't find the relevant message. Anyway, the issue
with
PDM> generic views seems to be to find a good balance between
generality,
PDM> uniformity, simplicity, and convenience of use. Personally, I
suspect
PDM> I'd find it annoying to have to define (and provide names for!)
views
PDM> from ELEM to every instantiation of LIST[ELEM] - it would encourage
PDM> people to write the fitting morphism in line, thereby discouraging
PDM> reuse. I doubt that I'd find the lack of imports equally annoying;
if
PDM> sufficiently many users did, they could presumably be added in CASL
PDM> v1.1 without too much bother. But this is all a matter of
methodology...
AT> Okay, so we seem to agree here that no imports in generic views.
TM> I cannot remember that I have argued that imports are not needed
here.
TM> I assume that instantiations of generic views are required
TM> to be pushouts. If the target of the generic view and the actual
parameter
TM> share, say, NAT (for example, because both containg some weight
function
TM> or some bound), then the instantiation of the generic view is
ill-formed
TM> unless the formal parameter contains NAT.
TM> So it would really make sense here to have the possibility to import
NAT.
PDM> This is not yet reflected in the proposal above!
AT> 5. Views can be used in instantiations instead of "fitted actual
AT> parameters", that is, they can replace an actual parameter with its
AT> fitting morphisms.
AT>
AT> However, here i disagree with what is said in the current summary,
AT> that "checking whether a view can be used as a fitting morphism only
AT> depends on the signatures of the involved specifications and thus no
AT> semantic check is needed to ensure the applicability of the view."
If
AT> we were as permissive as that, we might end up with actual parameter
AT> and fitting morphisms (extracted from the view) that do not form a
AT> specification morphism between formal and actual parameter
AT> specifications (as required, see 2 above). In fact, apart from the
AT> syntactic check that the signatures fit (and from the fact that
views
AT> are spec morphisms, see 3 above) we still have to ensure in the
AT> semantics that any model of the source spec of the view is a model
of
AT> the formal parameter spec.
AT>
AT> Right?
PDM> Right. (The sloppy wording in the summary was actually addressing
PDM> syntactic applicability, i.e., well-formedness. Sorry...)
AT> 6. (the point which i still do not like...) Views can be invoked
AT> implicitly, by instantiating a generic specification to an argument
AT> which is just a spec, with no fitting morphism given. This is
AT> accepted, intuitively, if in the global environment there is only
one
AT> view that allows us (or: that the semantics might take) to fit the
AT> formal into the actual parameter spec.
AT>
AT> I understand that the whole discussion recently was about the real
AT> meaning of the above intuition.
AT>
AT> a) we have agreed that this "unique existence" property of the
AT> appropriate view in the global environment must be understood in the
AT> static sense only, that is no "verification" (or model level
AT> semantics) may be involved to determined whether we can identify
such
AT> a view unambiguously or not.
AT>
AT> Consequently, we search for a unique view with the source signature
AT> that is the same as the signature of the formal parameter and the
AT> target signature that is the same as the signature of the actual
AT> parameter.
AT>
AT> Is this still right? (I hope yes...)
PDM> Yes - except that in the case that NO declared view fits, there may
PDM> still be the possibility of a default view, e.g., an inclusion
PDM> morphism, or perhaps even a morphism with some non-identity maps
PDM> determined by the fitting of some identity maps.
AT> Ugghhh. I personally would not go further than inclusions...
DTS> I would just like to register once again that I think the inclusion
of
DTS> this feature (implicit views) is a mistake. This is an obvious
place
DTS> where fancy tools can do better than anything we would want to
design
DTS> into the language.
DTS> I originally said this in a message dated 9 Feb 98 16:04:46 GMT
with
DTS> subject "Re: Semantics of Views" -- I can re-send it to anybody who
DTS> doesn't have it handy. My point there was that the well-formedness
DTS> and/or meaning of phrases can change when things that are not
involved
DTS> in any way in the phrase in question are changed later. Somebody
DTS> (Till? I don't have a copy of the original message) pointed out
that
DTS> the same comment applies with overloaded functions and predicates;
DTS> that is correct and although I would not suggest removing
overloading
DTS> from CASL, this is a strong negative point about overloading that
is
DTS> outweighed by the extreme inconvenience (impossibility?) of doing
DTS> without overloading in the presence of subsorts. Peter replied to
DTS> this in a message dated Wed, 11 Feb 1998 09:01:10 +0100 (MET) with
DTS> subject "Re: CASL v0.99 abstract syntax: SYMB-MAP; named morphisms"
DTS> saying that nobody will want to read the explicit versions and that
my
DTS> suggested fancy tools would do exactly what it is suggested that we
DTS> build into the static semantics. I didn't reply but I think if the
DTS> explicit version just *names* a view that is missing in the
implicit
DTS> version, with the details of that view spelled out elsewhere,
nobody
DTS> will complain about verbosity.
PDM> It is probably
PDM> controversial how far one goes here: different users may have
PDM> different perceptions about what default fittings are "obvious".
PDM> If we go too far, we may fail to catch some errors; if we don't go
far
PDM> enough, users may find it annoying to have to spell out symbol maps
in
PDM> a lot of detail.
DTS> The various complications discussed below and Peter's comment
DTS> reinforce my earlier opinion. The point is not just that fancy
tools
DTS> can do better than whatever we design into the language, but also
that
DTS> the fancy tools will *improve over time* whereas the language
design
DTS> will be fixed.
AT> As I also said many times earlier, I share Don's objections towards
AT> implicit views, and cannot quite see why using a pre-declared view
is
AT> so much less convenient than using its target specification in
AT> instantiation. I understand I was outvoted (was it in Lisbon?) ---
AT> tough. And I agree with Don, that this part of the semantics to
AT> identify the unique implicit view is becoming somewhat monstrous
AT> (Till's procedure seems nice and interesting, but it is a bit
AT> complicated and not easy to explain at all...).
AT> b) The issue then arises to what extend we can use generic views to
AT> implicitly build this implicit views :-)
AT>
AT> Even though it seems to complicate things considerably, once we
AT> stepped into this mess, it seems logical to me to allow for this
AT> iterative default instantiation and fitting as well. Then the issue
of
AT> uniqueness gets really hairy...
AT>
AT> Fortunately, Till provided a recipe for producing the (finite) set
of
AT> potential candidates that might be formed out of views declared in
the
AT> current environment and potentially might be used to fit given
formal
AT> parameter to given actual parameter (I have not checked the details
of
AT> Till's arguments for finiteness and termination of his procedure,
but
AT> I presume these are okay).
AT>
AT> Now, I would say that the instantiation with implicit view is okay
if
AT> Till's procedure leads to exactly one "view expression" that is
build
AT> over the signature morphism between the required signatures. Then we
AT> still have to check (in the model semantics, so generating
appropriate
AT> proof obligations) if the view produced by this "view expression"
AT> satisfies the following:
AT>
AT> i) each model of the actual parameter is a model of the target
AT> specification of the view, and
AT>
AT> ii) each model of the source specification of the view is a model of
AT> the formal parameter.
AT>
AT> If this holds, the instantiation is well-defined. Otherwise it
AT> fails. So, instantiation may be undefined whenever:
AT>
AT> *) either there is none or more than one way to build a "default
view"
AT> between the signatures of the formal and actual parameter given,
AT>
AT> **) or the unique way of building such a view leads to a view that
AT> does not ensure that the models of the actual parameter are reduced
to
AT> the models of the formal parameter (via the reduction within the
view).
AT>
AT> This seems to be in contrast with what Till wrote when he mentioned
in
AT> the last point:
AT>
AT> TM> 5. Check if all these (finitely many) possibilities lead
AT> TM> to a unique signature morphism or not.
AT>
AT> I'm afraid that unique signature morphism here is not enough --- to
AT> have a crisp criterion for the "semantic fitting" we need the
AT> uniqueness of the resulting *specification morphism*. To avoid the
AT> discussion now of how much of specification equivalence we could
AT> encode in this procedure, i would stick to the uniqueness of the
"view
AT> expression", or in other words: require that there is only one
AT> possible diagram of the form Till looks at that can be built here.
AT> As Hubert pointed out in a discussion earlier today, the semantic,
AT> model-level check (and hence generation of proof obligations as
AT> described by i) and ii) above) must of course be done recursively
AT> throughout the entire "view expressions" used, not only at the top
AT> level.
PDM> I guess that Till was referring to the static checking there.
TM> Exactly. For the dynamic checking, one would have to add
TM> 6. Check Andrzej's i) and ii) above.
TM> Andrzej suggests the condition
TM> there is a unique view expression
TM> Since different view expressions may lead to the same signature
TM> morphism, my condition is weaker. My check indeed requires
TM> computing induced signature morphisms and checking whether they are
TM> the same. But this can be done very easily at the static level.
AT> If this would mean that the uniqueness would be harder to achieve
---
AT> tough!
TM> For view expressions, my finiteness argument concerning composites
TM> does not apply.
TM> But there is another argument:
TM> Given a finite number of generic views (with a finite number
TM> of signatures involved), we have to check if there is more than one
TM> composite of generic view expressions between two given signatures.
TM> To do this, use an algorithm similar to transitive closure,
TM> recording, for each pair of signatures, if there is none, one (and
TM> which one) or more than one view expressions between the signatures.
TM> Finally, add only those view expressions as new views (step
TM> 2 of my algorithm) which have a "one" in this "transitive closure"
TM> graph.
AT> Do we share this understanding?
PDM> I hope so!
TM> I am not sure what is better from a methodological point of view:
TM> unique view expressions or unique induced signature morphisms.
TM> From the semantics, both seem to be possible choices.
AT> I think we decided that the views are checked to be specification
AT> morphisms (my point 3) and that this is to be used in the
verification
AT> of the correctness of instantiation of the generics (cf. my point 5)
AT> --- the two methodlogical aspects of views which I think I would
like
AT> to stick to (without them we could reduce the discusion to signature
AT> morphisms in general).
AT>
AT> Then the same should be happening for implicit views. But then we
also
AT> have to check the (model-level) correctness of the view expression
AT> found in the implicit fittting procedure. And the result of this
AT> check may depend on the view expression considered, not only on the
AT> signature morphism.
AT>
AT> (To take a trivial example, suppose that in the environment we have
AT> two views with the same source and target signatures, but with
AT> different specifications. And let the signatures match the formal
and
AT> actual parameter. Then according to Till's "unique morphism"
AT> principle, everything would be okay --- while my "unique view
AT> expression" priciple would reject this situation.)
AT>
AT> Hence, I vote for the uniqueness of the view expression here.
PDM> E.g. two views of NAT as MONOID?
AT> No, more like (I have not learnt the syntax yet :-( sorry!):
AT>
AT> spec ELEM = sort elem
AT> opns e : elem
AT> op: elem * elem -> elem
AT> end
AT>
AT> spec SOME0 = ELEM then vars x : elem
AT> axioms op(e,x) = x
AT> op(x,e) = x
AT>
AT> spec SOME1 = SOME0 then vars x, y : elem
AT> axiom op(x,y) = op(y,x)
AT>
AT> spec NAT = sort nat
AT> opns 0 : nat
AT> plus : nat * nat -> nat
AT> var n, m, k: nat
AT> axioms plus (n, 0) = n
AT> plus(0, n) = n
AT> plus(n,m) = plus(m,n)
AT> plus(n, plus(m,k)) = plus(plus(n,m),k)
AT>
AT> view V : ELEM to NAT = elem |-> nat, e |-> 0, op |-> plus end
AT> view V0: SOME0 to NAT = elem |-> nat, e |-> 0, op |-> plus end
AT> view V1: SOME1 to NAT = elem |-> nat, e |-> 0, op |-> plus end
AT>
AT> All the three views are the same as signature morphism, so we have a
AT> unique implicit signature morphism declared as a view between the
AT> signature of ELEM (which is the same as SOME0, SOME1) and the
AT> signature of NAT (which is the same as NAT0, NAT1). So, which view
do
AT> we take if we try to instantiate, say, SET[NAT]? In this case the
AT> choice does not matter for the semantics --- it so happens.
AT>
AT> But let me try something more complicated.
AT>
AT> spec LIST [SOME0] = sort list[elem]
AT> opns nil: list[elem]
AT> append: list[elem] * list[elem] -> list[elem]
AT> vars l: list[elem]
AT> axioms append(l, nil) = l
AT> appeend(nil,l) = l
AT>
AT> view VL [SOME0] : SOME0 -> LIST[SOME0] =
AT> elem |-> list[elem], e |-> nil, op : |-> append
AT>
AT> Then the semantics of LIST[LIST[NAT]] might depend on the choice
AT> between V, V0 and V1 in the construction of implicit view:
AT>
AT> LIST [ view VL[view V] ] should probably be ill-formed, since the
AT> inner instantiation is ill-formed (at teh model level!)
AT> LIST [ view VL[view V0] ] is okay
AT> LIST [ view VL[view V1] ] is okay as well, and with the same
AT> semantics, i guess.
AT>
AT> Anyway, there is a difference between the first case and the others,
AT> in spite of the fact that all the three generic view instantiations
AT> yield the same signature morphism, in fact: even between the same
AT> specifications!
AT> c) in the case of multiple parameters, i would tend to be very harsh
AT> as well, and require that the uniqueness is established for each
AT> parameter separately, and then compatibility is checked. An
AT> alternative would be to check for the uniqueness of a vector of
AT> compatible views, some of them given explicitly, some of them
"looked
AT> for" in the global environment. In either case i can see no trouble
AT> with the decidability, but of course we have to choose one of the
two
AT> possibilities before we finish the semantics.
________________________________________________________________________