Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha88a/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha88a/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This is a pure alpha release to fix a number of bugs and to let maude abusers try out a reimplementation of the strategy language. Bug fixes ========== (1) A bug in the mapping of terms from non-algebraic data types, illustrated by: fmod VECTOR is including ARRAY{Nat,String0} . endfm show all . This problem also affected Float0 and Qid0. Bug reported by Peter Simons . (2) A bug where Maude would allow parameterized theories to be entered even though they are not supported: fth TH is sort S . endfth fth TH-TH { X :: TH } is endfth Bug reported by Joe Hendrix . (3) A long standing bug in the unique collapse case of the AU matcher exposed by this example from Traian Florin Serbanuta : fmod BUG is sort S . ops T F : -> S . op ~_ : S -> S . op _&_ : S S -> S [assoc id: T] . op simplify : S -> S . var B : S . eq simplify(B & (~ B)) = F . endfm red simplify(~ T) . (4) A bug in upModule() that produced malformed singleton renaming sets. Exposed by the following example from Paco: fmod FOO is pr NAT * (op 0 to zero) . endfm red in META-LEVEL : metaReduce(upModule('META-LEVEL, false), upTerm(upModule('FOO, false))) . (5) A bug caused by bug fix (2) from alpha86 where metaXmatch() insisted that the pattern be in the same connected component as the top of the subject even though matching can take place below the top. Illustrated by this example from Alberto Verdejo : mod M is inc NAT . sort S . op f : Nat -> S . rl [l1] : 3 => 5 . endm red in META-LEVEL : metaXmatch(upModule('M,false), 'N:Nat, 'f['s_^3 ['0.Zero]], nil, 0, unbounded, 0) . The Great Purge ================ Owing to fears about the unsoundness of _==_ in the presence of non-confluence and related issues a number of features have been modified, replaced or removed altogether. (1) fmod IDENTICAL is expunged due to alleged unsoundness. (2) The lazy sort test operators _:::s have likewise disappeared. (3) MAP and ARRAY have been reimplemented to remove nonconfluence on artifically created pathological examples such as 1 |-> 2, 1 |-> 3 at the cost of some performance (but log time complexity of insertion and look up is retained). Also the prec of _[_] is changed to 23 to allow terms like v[1] < v[2] to parse without parens. (4) TAO-SET turns out not to be strong enough to define a stable (and hence confluent) version of mergesort. Recall that although TAO-SET used the strict inequality syntax it generalized both reflexive and irreflexive orderings. TAO-SET is now replaced by two notions of an order relation: STRICT-WEAK-ORDER transitive irreflexive incomparability transitive TOTAL-PREORDER transitive reflexive total Note that these two notions are complementary - if < is a strict weak order then it's (set theoretic) complement is a total preorder and vice versa. Both kinds of relations capture the notion that the set of elements is split into partitions which are linearly ordered. This situation naturally arises when records are compared on a given field. The C++ Standard Template Library used the notion of strict weak ordering. There are now two versions of sortable lists with these orderings: WEAKLY-SORTABLE-LIST uses STRICT-WEAK-ORDER and WEAKLY-SORTABLE-LIST' uses TOTAL-PREORDER Both provide a stable sort() operator. There are two further notions of linear ordering: STRICT-TOTAL-ORDER adds totality to STRICT-WEAK-ORDER TOTAL-ORDER adds antisymmetry to TOTAL-PREORDER and there are two versions of sortable lists with these orderings: SORTABLE-LIST uses STRICT-TOTAL-ORDER and SORTABLE-LIST' uses TOTAL-ORDER Since these use linear orderings, the issue of stability does not arise. Two sets of view are provided for the standard built in data types; views such as NAT< map from STRICT-TOTAL-ORDER while views such as NAT<= map from TOTAL-ORDER. (5) makeList() in LIST-AND-SET was non-confluent both because no order was specified for putting the elements in the list, and because due to idempotence on sets, the same element could be placed in the list more than once. This is fixed by reimplementing makeList() in two new modules, SORTABLE-LIST-AND-SET which requires a STRICT-TOTAL-ORDER and SORTABLE-LIST-AND-SET' which requires a TOTAL-ORDER. The availability of a linear order allows the resulting list to be unambiguous. Other changes ============== (1) The strategy language as been reimplemented from scratch using a process based approach rather that a set generator based approach. The leaf strategies and combinators supported in alpha88 are implemented together with the combinator: or-else and the tests: match match s.t. xmatch xmatch s.t. (2) More overparsing for operator declarations; in the following 2 cases: op a : Foo . op b : Foo. there is no legal continuation and Maude will decide that an -> has been omitted, issue an appropriate warning ("missing -> in constant declaration.") and recover gracefully. Unfortunately in the case of an attribute: op c : Foo [ctor] . [ctor looks like the start of a legal type name on by the time we have discovered the syntax error it is too late to recover gracefully. (3) fmods SET and SET* get subset and proper subset tests at Jose's request: op _subset_ : Set{X} Set{X} -> Bool . op _psubset_ : Set{X} Set{X} -> Bool . (4) The file term-order.maude contains an fmod TERM-ORDER parameterized by X :: TRIV that defines a strict total order op lt : [X$Elt] [X$Elt] -> Bool . on terms in the kind [X$Elt]. The exact order is implementation dependent. lt is used rather than _<_ to avoid potential conflicts with pre-existing operators such as _<_ on Nat. Feature requested by Jose. Steven