In the interpretation of bags as sequences, presented in the Specware language manual, the bags are regarded as a quotient of the sequences modulo the permutation relation. The mediator imports the target, the specification for sequences, and introduces the notion of permutations that enables the interpretation to be described.
In this interpretation, there are two morphisms , from the source specification BAG and the target specification SEQ, respectively, into the mediator BAG-AS-SEQ. In parsing the specification, it must be established that the axioms of the source and target theories are mapped into theorems of the mediator.
This is straightforward in the case of the target morphism, which is simply the import morphism. Each axiom of the target theory SEQ is mapped into an axiom of the mediator, which is of course a theorem.
In the case of the source morphism, the theorem-proving problems are substantial. For example, the uniqueness axiom for bags,
(implies
(equal (insert-bag e b) (insert-bag e c))
(equal b c))
asserts that if the results of inserting the same element into two bags are equal, the two bags must already be equal. This axiom maps into the following sentence in the mediator:
(implies
(equal (insert-b-as-s e b) (insert-b-as-s e c))
(equal b c))
This theorem is superficially similar to the axiom, but b and
c are equivalence classes of sequences, modulo the
permutation relation. The operation
(insert-b-as-s e c) inserts an element at the beginning of one
of the sequences in the class c (via the sequence operation
prepend) , and then yields the
equivalence class corresponding to the resulting sequence. The
equality relation on classes corresponds to the permutation relation
on the underlying sequences. Hence the theorem may be paraphrased as
saying that, if the results of inserting the same element at the
beginning of two sequences are permutations, the two sequences are
already permutations. Thus a simple axiom on bags maps into a
substantive theorem on permutations of sequences in the mediator.
This section has described what theorems need to be proved, and from what axioms. The next sections tell how to control and assist the theorem prover.