Parameterized views

Suppose we have defined modules LIST{X :: TRIV} and SET{X :: TRIV}, specifying, respectively, lists and sets, and suppose that we need, e.g., the data type of lists of sets of natural numbers. Typically, we would first instantiate the module SET with a view, say Nat, from TRIV to the module NAT mapping the sort Elt to the sort Nat, thus getting the module SET{Nat} of sets of natural numbers. Then, we would instantiate the module specifying lists with a view, say NatSet, from TRIV to SET{Nat}, obtaining the module LIST{NatSet}. But, what if we need now the data type of lists of sets of Booleans? Should we repeat the whole process again? One possibility is to define a combined module SET-LIST{X :: TRIV}. But what if we later want stacks of sets instead of lists of sets?

We can greatly improve the reusability of specifications by using parameterized views. Let us consider the following parameterized view Set from TRIV to SET, which maps the sort Elt to the sort Set{X}.

 (view Set{X :: TRIV} from TRIV to SET{X} is
    sort Elt to Set{X} .
  endv)

With this kind of views we can keep the parameter part of the target module still as a parameter. We can now have lists of sets, stacks of sets, and so on, for any instance of TRIV, by instantiating the appropriate parameterized module with the appropriate view. For example, given the view Nat above, we can have the module LIST{Set{Nat}} of lists of sets of natural numbers, or lists of sets of Booleans with LIST{Set{Bool}}, given a view Bool from TRIV to the predefined module BOOL. Similarly, we can have STACK{Set{Nat}} or STACK{Set{Bool}}.

We can also link the parameter of a module like LIST{Set{X}} to the parameter of the module in which it is being included. That is, we can, for example, declare a module of the form

 (fmod GENERIC-SET-LIST{X :: TRIV} is
    protecting LIST{Set{X}} .
  endfm)

Then, instantiating the parameterized module GENERIC-SET-LIST with a view V from TRIV to another module or theory results in a module with name GENERIC-SET-LIST{V}, which includes the module LIST{Set{V}}. Note that even with parameterized views we still follow conventions for module interfaces and for sort names (see Section 6.3). The only difference is that now, instead of having simple view names, we must consider names of views which are parameterized.

The use of parameterized views in the instantiation of parameterized modules allows very reusable specifications. For example, a very simple way of specifying (finite) partial functions is to see a partial function as a set of input-result pairs. Of course, for such a set to represent a function there cannot be two pairs associating different results with the same input value. We show later in this section (in the module PFUN below) how this property can be specified by means of appropriate membership axioms. Note, however, that since membership axioms cannot be given on associative operators over sorts (see Section 13.2.8), we cannot use either the specification of sets described in Section 6.3.3 or the predefined module in Section 7.12.2. Let us consider instead the following module:^14.3

  (fmod SET-KIND{X :: TRIV} is
    sorts NeKSet{X} KSet{X} .
    subsort X$Elt < NeKSet{X} < KSet{X} .
    op empty : -> KSet{X} [ctor] .
    op _`,_ : KSet{X} KSet{X} ~> KSet{X} [ctor assoc comm id: empty] .
    mb NS:NeKSet`{X`}, NS':NeKSet`{X`} : NeKSet{X} .

    var E : X$Elt .

    *** idempotency
    eq E, E = E .
   endfm)

Here the operator _,_ is declared at the kind level (notice the different form of the arrow in its declaration) together with a membership axiom, that is logically equivalent to the declaration

  op _`,_ : NeKSet{X} NeKSet{X} -> NeKSet{X} .

at the sort level.

We can then specify sets of pairs by instantiating this SET-KIND module with a parameterized view from TRIV to the parameterized module TUPLE[2]{X, Y} defining pairs of elements. The appropriate parameterized view can be defined as follows:

 (view Tuple{X :: TRIV, Y :: TRIV} from TRIV to TUPLE[2]{X, Y} is
    sort Elt to Tuple{X, Y} .
  endv)

A partial function can be lifted to a total function by adding a special value to its codomain, to be used as the result for the input elements for which the function is not defined. For this we make good use of the parameterized module MAYBE, introduced in Section 6.3.3, which adds a supersort and a new element maybe to this supersort; in this application, the constant maybe is renamed to undefined.

We are now ready to give the specification of partial functions. The sets representing the domain and codomain of the function are given by TRIV parameters, and then the set of tuples is provided by the imported module expression SET-KIND{Tuple{X, Y}} with sorts KSet{Tuple{X, Y}} and NeKSet{Tuple{X, Y}}. We define operations dom and im returning, respectively, the domain and image of a set of pairs. The dom operation will be used for checking whether there is already a pair in a set of pairs with a given input value. With these declarations we can define the sort PFun{X, Y} as a subsort of KSet{Tuple{X, Y}}, by adding the appropriate membership axioms specifying those sets that satisfy the required property. Finally, we define operators _[_] and _[_->_] to evaluate a function at a particular element, and to add or redefine an input-result pair, respectively. We use the Core Maude predefined module SET (see Section 7.12.2) for representing the sets of elements in the domain and image of a partial function.

 (fmod PFUN{X :: TRIV, Y :: TRIV} is
    pr SET-KIND{Tuple{X, Y}} .
    pr SET{X} + SET{Y} .
    pr MAYBE{Y} * (op maybe to undefined) .

    sort PFun{X, Y} .
    subsorts Tuple{X, Y} < PFun{X, Y} < KSet{Tuple{X, Y}} .

    vars A D : X$Elt .
    vars B C : Y$Elt .
    var  F : PFun{X, Y} .
    var  S : KSet{Tuple{X, Y}} .

    op dom : KSet{Tuple{X, Y}} -> Set{X} .         *** domain
    eq dom(empty) = empty .
    eq dom((A, B), S) = A, dom(S) .
    op im : KSet{Tuple{X, Y}} -> Set{Y} .          *** image
    eq im(empty) = empty .
    eq im((A, B), S) = B, im(S) .

    op empty : -> PFun{X, Y} [ctor] .
    cmb (A, B), (D, C), F : PFun{X, Y}
      if (D, C), F : PFun{X, Y} /\ not(A in dom((D, C), F)) .

    op _`[_`] : PFun{X, Y} X$Elt -> Maybe{Y} .
    op _`[_->_`] : PFun{X, Y} X$Elt Y$Elt -> PFun{X, Y} .
    ceq ((A, B), F)[ A ] = B if ((A, B), F) : PFun{X, Y} .
    eq F [ A ] = undefined [owise] .
    ceq ((A, B), F)[ A -> C ] = (A, C), F
      if ((A, B), F) : PFun{X, Y} .
    eq F [ A -> C ] = (A, C), F [owise] .
  endfm)

Now, we can instantiate the PFUN module with, for example, the view Nat, in order to get the finite partial functions from natural numbers to natural numbers by means of the module expression PFUN{Nat, Nat}.