Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha95/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha95/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This is a pure alpha release. Bug fixes --------- (1) A bug in the lexing of tokens beginning with . after a . that might have, but didn't end a statement or command. Illustrated by mod X is sorts S T . op a_.b : T -> [S] [prec 0] . op . : -> T . mb [set] : a . .b : S . endm and mod X is sorts S T . op a_.b : T -> [S] [prec 0] . op . : -> T . endm red a . .b . Here the . is being split off of the .b token. Bug reported by Traian. (2) A bug in the AC matcher, where for under certain circumstances a binding could be forgotten, resulting is false matchers. Provoked by this example adapted from an example of Jose, communicated by Camilo Rocha : fmod HF-SETS is sorts Magma Set . subsort Set < Magma . op _,_ : Magma Magma -> Magma [ctor assoc comm] . op {_} : Magma -> Set [ctor] . op 0 : -> Set [ctor] . vars M : Magma . endfm match {M,{M}} <=? {{0,{0},{{0}}},{0,{0},{{{0}}}},{0,{0},{{0,{0}}}},{0,{{0}},{{{0}}}},{0,{{0}},{{0,{0}}}},{0,{{{0}}},{{0,{0}}}},{0,{0},{{0}},{{{ 0}}}},{0,{0},{{0}},{{0,{0}}}},{0,{0},{{{0}}},{{0,{0}}}},{0,{{0}},{{{0}}},{{0,{0}}}},{0,{0},{{0}},{{{0}}},{{0,{0}}}}} . This bug has existed since I added an optimization to allow red-black tree matching in the non-greedy case, in Maude80a, May 29 2003! (3) A bug where an attribute clash error in a instantiation could cause a crash. Provoked by an example from Emmanuel Castro . Since the bug causes memory corruption it is hard to find a small example that crashes consistantly across all recent binaries. Other improvements ------------------ (1) Order sorted ACU unification was incomplete in a couple of ways. Firstly a unsorted unifier Q could fail to have a sorting while a less general unsorted unifier P that was not generated could have a sorting. Thus sortings of P would be missed. For example: fmod FOO is sorts Small Big . subsort Small < Big . op f : Big Big -> Big [assoc comm id: 1f] . op 1f : -> Small . op h : Small -> Big . endfm unify X:Big =? h(f(Y:Big, Z:Big)) . Here no solution is fould but unifying one of Y or Z with 1f forces the collapse and finds a solution: unify X:Big =? h(f(Y:Big, Z:Big)) /\ Y:Big =? 1f . Note that here an extra function symbol h was used force f(Y:Big, Z:Big) to the Small sort; making X Small would allow the Diophantine phase of the ACU unification algorithm to realized that X could not be assigned f(...) and the collapse would happen there. Secondly an unsorted unifier Q might only have sortings that disallow a collapse to a less general unifier P which it was covering. For example: fmod FOO is sorts Small Big . subsort Small < Big . op f : Big Big -> Big [assoc comm id: 1f] . op f : Small Small -> Small [ditto] . op 1f : -> Big . endfm unify X:Small =? f(Y:Big, Z:Big) . Here we find a sorting X:Small --> f(#1:Small, #2:Small) Z:Big --> #1:Small Y:Big --> #2:Small but then collapse is no longer possible and unifiers such as: X:Small --> #1:Small Y:Big --> #1:Small Z:Big --> 1f are not covered. With complex identities, this situations can occur in more subtle ways: fmod FOO is sorts Small Big . subsort Small < Big . op a : -> Small . op g : Big -> Big . op f : Big Big -> Big [assoc comm id: g(a)] . op f : Small Small -> Small [assoc comm id: g(a)] . op 1f : -> Small . endfm unify X:Small =? f(g(Y:Small), Z:Small) . Here the orginal solved form has no valid sorting but the collapse version does: X:Small --> #1:Small Z:Small --> #1:Small Y:Small --> a fmod FOO is sorts Small Big . subsort Small < Big . op a : -> Big . op g : Big -> Big . op g : Small -> Small . op f : Big Big -> Big [assoc comm id: g(a)] . op f : Small Small -> Small [assoc comm id: g(a)] . op 1f : -> Small . endfm unify X:Small =? f(g(Y:Big), Z:Small) . Here the maximal sorting: X:Small --> f(#2:Small, g(#1:Small)) Z:Small --> #2:Small Y:Big --> #1:Small prevents a collapse. Both of these phenomena happen because f collapses down; that is there exists a sort S such that f(X:S, 1f) has a sort greater than S. These means there are terms will different sorts in the congruence class. Historically we allowed this as long as the most collapsed representative has the least sort because of container examples like SET as declared in the prelude. Here there is a collapse down from NeSet to Elt and a similar thing happens with LIST. Identifying elements with singleton sets is a dubious thing to do (I recently fielded a query from a user complaining that Maude sets couldn't be given mathematical set semantics), however it is an well entrenched programming technique since it allows a single basis case for the empty set rather than having another basis case for the singleton set. Interestingly identity collapses in the number hierarchy do not collapse down, as long as all the appropriate sort declarations are given. Joe Hendrix proposed a theory tranformation to solve this problem that adds extra sorts to hold the identities so that collapse down does not happen: subsort Id < Set . op empty : -> Id . op _,_ : Set Id -> Set [ditto] . op _,_ : NeSet Id -> NeSet [ditto] . op _,_ : Elt Id -> Elt [ditto] . Now _,_(E:Elt, empty) has sort Elt and there is no collapse down when it collapses to E:Elt. Free variables receiving the sort Id would need to be replaced by the constant empty to get a solution in the original theory. The problem with this approach is complex identities; although additional sorts can be added to hold subterms of identities, this approach becomes impractical once iter operators are thrown into the mix: fmod FOO is sorts Small Big . subsort Small < Big . op a : -> Small . op g : Big -> Big [iter] . op f : Big Big -> Big [assoc comm id: g^1000000(a)] . op f : Small Small -> Small [assoc comm id: g^1000000(a)] . op 1f : -> Small . endfm unify X:Small =? f(g(Y:Big), Z:Small) . has an order sorted unifier X:Small --> #1:Small Z:Small --> #1:Small Y:Big --> g^999999(a) Also fmod FOO is sorts Small Big . subsort Small < Big . op a : -> Big . op g : Big -> Big [iter]. op g : Small -> Small [ditto] . op f : Big Big -> Big [assoc comm id: g^1000000(a)] . op f : Small Small -> Small [assoc comm id: g^1000000(a)] . op 1f : -> Small . endfm *** lose generalization of collapsed version unify X:Small =? f(g(Y:Big), Z:Small) . has a maximal sorting: X:Small --> f(#2:Small, g(#1:Small)) Z:Small --> #2:Small Y:Big --> #1:Small which no longer covers the unifier X:Small --> #1:Small Z:Small --> #1:Small Y:Big --> g^999999(a) In this version I've adopted a brute force approach to solving the problem. Whenever a signature has a collapse down issue, a flag is set for that symbol. Then at unification time, the BDD algorithm that avoids generating unifiers that are redundant by collapses is skipped, and the power set of the Diophantine basis is expanded out, only respecting computed constraints and not (lack of) generality. Surprisingly there are examples where even the empty set of basis elements needs to be considered: fmod FOO is sorts Small Big . subsort Small < Big . op f : Big Big -> Big [assoc comm id: 1f] . op 1f : -> Small . op h : Small -> Big . endfm unify X:Big =? h(f(Y:Big, Y:Big)) . The downside of this technique is that it possible to produce a doubly exponential avalanch of redundant unifiers since we are now doing a search that is very close to AC unification. fmod FOO is sorts Small Big . subsort Small < Big . op f : Big Big -> Big [assoc comm id: 1f] . op 1f : -> Small . endfm unify f(U:Big, V:Big, W:Big) =? f(X:Big, Y:Big, Z:Big) . Here Alpha94a finds the single most general unifier but the new version includes an additional 511 redundant unifiers before it finds the mgu. (2) srewrite now uses hash consing, just like search and model checking. (3) I've reimplemented the memo attribute so that it also uses a varient of hash consing. I'm interested to know if this yields any improvements in time or storage for memo heavy code such as the NPA. Steven