Maude-help mailing list

["Scott" <scottxyz AT usa.net>]

Hello --

A map typically models a collection of (key |-> value) pairs where a given key
occurs only once in the collection, and hence maps to a unique value.

The op _,_ in fmod MAP in prelude.maude for Maude 2.2:

fmod MAP{X :: TRIV, Y :: TRIV} is
  sorts Entry{X,Y} Map{X,Y} .
  subsort Entry{X,Y} < Map{X,Y} .

  op _|->_ : X$Elt Y$Elt -> Entry{X,Y} [ctor] .
  op empty : -> Map{X,Y} [ctor] .
  op _,_ : Map{X,Y} Map{X,Y} -> Map{X,Y} 
  [ctor assoc comm id: empty prec 121 format (d r os d)] .
  op undefined : -> [Y$Elt] [ctor] .

  var D : X$Elt .
  vars R R' : Y$Elt .
  var M : Map{X,Y} .

  op insert : X$Elt Y$Elt Map{X,Y} -> Map{X,Y} .
  eq insert(D, R, (M, D |-> R')) = (M, D |-> R) .
  eq insert(D, R, M) = (M, D |-> R) [owise] .

  op _[_] : Map{X,Y} X$Elt -> [Y$Elt] .
  eq (M, D |-> R)[D] = R .
  eq M[D] = undefined [owise] .
endfm

constructs a new Map from two given Maps. This op has been declared to be
total, but it appears that it should actually have been declared to be
partial. 

To see why, we can apply op _,_ to two given Maps WHICH BOTH INCLUDE THE SAME
KEY. The result is not a "map" in the typical sense above, because the same
key now maps to two different values.

For example:

fmod MAP-NAT-NAT is
  pr MAP{Nat,Nat} .
endfm

red ( 1 |-> 2 , 1 |-> 3 )[1] .

The reduction above could rewrite to either 2 or 3 (although the Maude
interpreter appears to always arbitrarily choose the first alternative due to
sort order of the stored data). Does this mean that module MAP is
non-confluent and needs to be corrected?

The operator _;_ in module ARRAY in prelude.maude (Maude 2.2) is also declared
to be total, but it appears that it should actually be declared to be partial
as well, for the same reason.

Thank you for any help.

-- Scott Alexander

PS - The module PFUN(X | Y) (in chapter 15 of the Maude 2.1.1 manual) uses a
different approach to specify partial functions (which are the same as maps),
modeling a partial function as a subsort of SET-KIND(Tuple(X |Y)) and using
membership axioms to check whether a SET-KIND(Tuple(X | Y)) is also a PFUN(X |
Y). MAP seemed more elegant because it avoids using membership axioms and it
avoids using requirement theory DEFAULT for parameter Y, instead defining op
undefined : -> [Y$Elt]. I work a lot in the category FinSet of finite sets and
partial functions, so I am eager to find a compact and efficient specification
for MAP or PFUN.