Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

You're right; MAP and ARRAY are not confluent or even ground confluent. If 
you 
use them for programming in the natural way then you will not encounter 
nonconfluent situations. I can't think of any way of getting ground 
confluence that does not destroy efficiency which is their raison d'etre.

Of course other predefined stuff (RATs spring to mind) is not confluent but 
hopefully ground confluent. Order-sorted confluence checking modulo theories 
is tricky - membership equational confluence checking modulo theories even 
more so.

I have been thinking about an optional more elaborate specification for some 
of the builtin and/or predefined stuff that would not only be confluent but 
also omega-complete and which would be of use in theorem proving applications 
where one is less concerned with efficiency; but omega-complete, confluent 
and terminating rewrite systems are not possible for many data types of 
interest. Still omega-completeness is one of my pet projects and I may 
include something in the next public release.

Steven

On Tuesday 20 June 2006 21:30, Scott wrote:
> 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.
>
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help