Maude-help mailing list

[Scott <scottxyz AT usa.net>]

Hello --

This email asks some questions using Full Maude 2.1.1a about modules
such as MOD:

(fmod MOD(X1 :: TRIV | X2 :: TRIV | X3 :: TRIV | X4 :: TRIV) is
  pr MI(...) .
  ...
endfm)

which might import a module MI parameterized over two copies of TRIV:

(fmod MI(X :: TRIV | Y :: TRIV) ... endfm)

where imported module MI could be instantiated in various ways:

(a) with formal parameters of MOD (now called MOD-FP):

(fmod MOD-FP(X1 :: TRIV | X2 :: TRIV | X3 :: TRIV | X4 :: TRIV) is
  pr MI(X1 | X2) .
  ...
endfm)

or (b) with views defined before MOD (now called MOD-VW) is entered, for
example with view Nat from TRIV to NAT and view Qid from TRIV to QID:

(view Nat from TRIV to NAT is sort Elt to Nat . endv)
(view Qid from TRIV to QID is sort Elt to Qid . endv)

(fmod MOD-VW(X1 :: TRIV | X2 :: TRIV | X3 :: TRIV | X4 :: TRIV) is
  pr MI(Nat | Qid) .
  ...
endfm)

Syntaxes (a) and (b) can't be mixed in the same imported instantiation
of MI -- i.e., we can't import an instantiation of module MI:

(c) instantiated with both a formal parameter of the enclosing module
and with a view such as Qid:

(fmod MOD-FP-VW?(X1 :: TRIV | X2 :: TRIV | X3 :: TRIV | X4 :: TRIV) is
  --- this line won't compile (mixed formal parm and view)
  pr MI(X3 | Qid) .
  ...
endfm)

However, intuitively speaking, could a module like MOD-FP-VW? have a
useful semantics?

-----

So far, we have parameterized modules like MOD over several copies of
TRIV and then we have:

- instantiated imported module MI...

...(a) with two formal parameters (of MOD-FP),

...(b) with a view from TRIV to NAT and a view from TRIV to QID (MOD-
VW),

...(c) (illegally) with a formal parameter (of MOD-FP-VW?) and a view
from TRIV to QID.

Let's look at a slightly more complicated example, involving module MOD-
FUN parameterized over TRIV-FUN:

(fth TRIV-FUN is
  sorts EltA EltB .
  op f : EltA -> EltB .
endfth)

(fmod MOD-FUN(F :: TRIV-FUN | X3 :: TRIV | X4 :: TRIV)
  is
  ...
  eq f ... = ... .
  ...
endfm)

Notice that MOD-FUN has "tighter" semantics than MOD, because MOD-FUN
requires the op f which was not required by MOD.

Now let's say we have a module FOO:

(fmod FOO is
  sorts Foo1 Foo2 .
  op foo : Foo1 -> Foo2 .
endfm)

and a view Foo from TRIV-FUN to FOO:

(view Foo from TRIV-FUN to FOO is
  sort EltA to Foo1 .
  sort EltB to Foo2 .
  op f to foo .
endv)

If we instantiate MOD-FUN with this view:

(fmod MOD-FUN-FOO is
  pr MOD-FUN(Foo | ... | ...) .
endfm)

then MOD-FUN-FOO would contain the operator foo (to which view Foo
mapped op f), and operator foo in MOD-FUN-FOO would be expected to
satisfy the equations for operator f in MOD-FUN.

-----

Combining various aspects of the above situations, let's say we want a
module MOD-FUN-MI:

(fmod MOD-FUN-MI(F :: TRIV-FUN | X3 :: TRIV | X4 :: TRIV)
  is
  pr MI(...) .
  ...
  eq f ... = ... .
endfm)

which is similar to MOD-FUN but also imports the module MI, which is
parameterized as before over two copies of TRIV.

Let us further say we would like to be able to import into MOD-FUN-MI
the module MI with:

- one of the parameters of MI instantiated with a formal parameter of
MOD-FUN-MI, and

- one of the parameters of MI instantiated with "one of the sorts
provided by theory TRIV-FUN bound to interface parameter F of MOD-FUN-
MI" (or, more accurately speaking, instantiated with "a view from TRIV
to TRIV-FUN mapping sort Elt of TRIV to a sort, say EltA, of TRIV-FUN").

As we have seen above with module MOD-FP-VW?, this is not possible,
because this approach "mixes" within the instantiation of MI a reference
to a view and a reference to of a formal parameter of the containing
module MOD-FUN-MI. (However, although this syntax is illegal,
intuitively it seems like it could have a useful semantics.)

-----

The reason we cannot (in the absence of previously defined views from
TRIV-FUN), within an instantiation of MI imported into MOD-FUN-MI "refer
to a sort provided by TRIV-FUN" (or, more accurately speaking, we cannot
"instantiate imported module MI with a view from TRIV to TRIV-FUN
mapping sort Elt of TRIV to a sort, say EltA, of TRIV-FUN") is because
the theory TRIV-FUN in the interface of MOD-FUN-MI is unparameterized.

But we might be able to refer in an imported instantiation of module MI
to "a view from TRIV to TRIV-FUN mapping sort Elt of TRIV to a sort, say
EltA, of TRIV-FUN". For example, we can define two views from TRIV to
TRIV-FUN:

(view EltA from TRIV to TRIV-FUN is sort Elt to EltA . endv)
(view EltB from TRIV to TRIV-FUN is sort Elt to EltB . endv)

and then import MI:

(fmod MOD-FUN-MI(F :: TRIV-FUN | X3 :: TRIV | X4 :: TRIV)
  is
  pr MI(EltA | EltB) .
  ...
  eq f ... = ... .
endfm)

However, we still can't do something like the following:

(fmod MOD-FUN-MI?(F :: TRIV-FUN | X3 :: TRIV | X4 :: TRIV)
  is
  --- this line won't compile (mixed formal parm and view)
  pr MI(X3 | EltB) .
  ...
  eq f ... = ... .
endfm)

Again, this "mixes" within imported instantiated module MI a reference
to a formal parameter of MOD-FUN-MI? and a reference to a view, which is
not legal syntax (although intuitively this may have a useful
semantics).

-----

I have been intrigued by the impossibility of importing module MI with
one of its parameters instantiated with a "trivial" formal parameter of
the containing module (such as X3) and its other parameter instantiated
with a view to a non-trivial formal parameter of the containing module
(such as TRIV-FUN). It seems like this might provide useful semantics in
some situations -- so perhaps it is possible using a different approach.

An approach which might enable us to achieve something like the effect
of "referring", within an imported instantiation of MI, to "one of the
sorts provided by TRIV-FUN" (or, more accurately speaking, to achieve
something like the effect of "instantiating imported module MI with a
view from TRIV to TRIV-FUN mapping sort Elt of TRIV to a sort of TRIV-
FUN"), would be to define a module MOD-FUN-PARM parameterized not over
_unparameterized_ theory TRIV-FUN but rather over _parameterized_ theory
TRIV-FUN-PARM:

(fth TRIV-FUN-PARM(A :: TRIV | B :: TRIV)
  is
  op f : 
A@Elt
 -> 
B@Elt
 .
endfth)

(fmod MOD-FUN-PARM(F :: TRIV-FUN-PARM(J :: TRIV | K :: TRIV)
                 | X3 :: TRIV | X4 :: TRIV)
  is
  pr MI(J | K) .
  pr MI(X3 | K) .
  pr MI(J | X2) .
  pr MI(X2 | X4) .
  ...
endfm)

Now MOD-FUN-PARM is parameterized over TRIV-FUN-PARM (which is itself
parameterized over two copies of TRIV, labelled with formal parameters J
and K in the interface of MOD-FUN-PARM), so the module MOD-FUN-PARM can
import instantiations of MI which "refer to the sorts in TRIV-FUN-PARM"
(or, more accurately speaking, instantiations of MI where each parameter
of MI is instantiated with "a view from TRIV to TRIV-FUN-PARM").

This avoids the problem of "mixing" within imported instantiated module
MI a reference to a formal parameter of the containing module and a
reference to a view, so it achieves something like the semantics which
we attempted to define in (c) or in module MOD-FUN-MI? above.

Note that in order to achieve this, we had to parameterize over theory
TRIV-FUN-PARM (which is itself parameterized). We could not achieve this
by parameterizing over theory TRIV-FUN (which, being unparameterized,
provided no convenient way of referring to "one of its sorts" -- or,
more accurately speaking, to "one of its one-sorted parameter theories
TRIV").

-----

However, do modules MOD-FUN and MOD-FUN-PARM behave the same in terms of
which actual parameter modules can be used for instantiating formal
parameter F? It appears that they do not.

MOD-FUN (and MOD-FUN-MI, like MOD-FUN but also importing MI) requires
TRIV-FUN, which is _unparameterized_. On the other hand MOD-FUN-PARM
requires TRIV-FUN-PARM, which is _parameterized_.

To the best of my understanding, looking at the examples of
parameterized views towards the bottom of this page:

http://maude.cs.uiuc.edu/maude2-manual/html/node169.html

it would not seem to make sense to create a view from TRIV-FUN-PARM to
FOO, because TRIV-FUN-PARM is parameterized and FOO is not. So it
appears that only MOD-FUN could be instantiated with a view to FOO. It
does not appear to be possible to define a view to FOO which could be
used to instantiate MOD-FUN-PARM. Therefore MOD-FUN and MOD-FUN-PARM
have different semantics, and are appropriate for different situations.

-----

So on one hand, MOD-FUN-PARM can do something that MOD-FUN can't do:
MOD-FUN-PARM allows us to refer to the individual sorts (or, more
accurately speaking, to the single-sort theories TRIV labelled J and K)
within its (parameterized) interface theory TRIV-FUN-PARM. One thing
this does is to provide semantics like that of MOD-FUN (i.e., "tighter"
than the semantics provided by modules like MOD parameterized only over
TRIV). In addition, being parameterized over _parameterized_ theory
TRIV-FUN-PARM (rather than over _unparameterized_ theory TRIV-FUN), MOD-
FUN-PARM allows us in imported instantiations of module MI to refer to
the formal parameters J and K of TRIV-FUN-PARM, thereby achieving an
effect similar to the semantics we might intuitively ascribe to the
(illegal) "mixed" syntax in (c) or module MOD-FUN-MI? above, where we
attempted to instantiate an imported module MI with a formal parameter
of its containing module and with a view.

However, MOD-FUN-PARM is only able to do this because because its
interface theory TRIV-FUN-PARM is itself parameterized over two copies
of TRIV -- which according to the previous section would appear to mean
that we could not instantiate MOD-FUN-PARM with a view to FOO (say, from
TRIV-FUN-PARM). This is because FOO is unparameterized while TRIV-FUN-
PARM is parameterized, so it does not seem to make sense to create a
view from TRIV-FUN-PARM to FOO.

-----

On the other hand, as we saw above, MOD-FUN can do something that MOD-
FUN-PARM can't do: MOD-FUN allows us to create a view from
(unparameterized theory) TRIV-FUN to an (unparameterized) module such as
FOO:

(view Foo from TRIV-FUN to FOO is
  sort EltA to Foo1 .
  sort EltB to Foo2 .
  op f to foo .
endv)

and then instantiate MOD-FUN with this view:

(fmod MOD-FUN-FOO is
  pr MOD-FUN(Foo | ... | ...) .
endfm)

However, in this case we cannot have a module like MOD-FUN-MI which
imports an instantiation of module MI where one parameter of MI is
instantiated with a formal parameter of MOD-FUN-MI and the other
parameter of MI is instantiated with (a view from TRIV to TRIV-FUN
mapping sort Elt to) sort EltA of TRIV-FUN. This is because we can't
combine a formal parameter of MOD-FUN-MI and a view in the same
instantiation of module MI, and because MOD-FUN-MI uses unparameterized
interface theory TRIV-FUN (which does not offer any interface theories
of its own which we might mention in the instantiation of MI) rather
than using parameterized interface theory TRIV-FUN-PARM (which does
offer interface theories we can mention in the instantiation of MI).

-----

Probably because of my lack of exposure to more examples of modules
parameterized over theories more complicated than TRIV, I'm often
confused about what is really happening when "importing an instantiated
module". In other words, I'm accustomed to instantiating an imported
module with a view from TRIV, or with a formal parameter (bound to TRIV)
from the interface of the containing module -- but I'm confused about
instantiating an imported module with something more complicated -- such
as with a view from a module other than TRIV, or with a formal parameter
(bound to a theory other than TRIV) from the interface of the containing
module. I'm also confused about how, in an imported instantiated module
such as MI, to "refer to the various sorts" contained in a
unparameterized parameter theory in the interface of the module into
which MI is being imported. Parameterizing MOD-FUN-PARM over
parameterized theory TRIV-FUN-PARM (rather than parameterizing MOD-FUN
over unparameterized theory TRIV-FUN) lets me refer within imported
instantiated module MI to (sorts in the) interface theories of MOD-FUN-
PARM interface theory TRIV-FUN-PARM -- but this creates the obstacle of
no longer being able to instantiate parameter TRIV-FUN-PARM of MOD-FUN-
PARM with a view to an unparameterized module such as FOO. Finally, I
seem to want to instantiate a module such as MI over both a formal
parameter of its containing module and over a view -- which is clearly
illegal syntax in Maude, although intuitively this situation seems to me
to have useful semantics.

What I would like to find out is the following:

Is there a way to define a module which lets us do what MOD-FUN-PARM
lets us do _and_ what MOD-FUN lets us do? In other words, is there a way
to define a module:

- which (like MOD-FUN-PARM) is parameterized over an interface theory
such as TRIV-FUN-PARM providing two sorts and an op from one sort to the
other, and which (also like MOD-FUN-PARM) imports instantiations of a
two-parameter module MI parameterized over TRIV, where one parameter of
imported module MI is instantiated with a formal parameter of MOD-FUN-
PARM and the other parameter of imported module MI is instantiated with
one of the formal parameters of interface theory TRIV-FUN-PARM; _and_

- which (like MOD-FUN) can be instantiated with a view to an
_unparameterized_ module such as FOO?

-----

Thanks for any help!

-- Scott Alexander