Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha89h/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha89h/ Alpha release site authentication: User Name: maudeabuser Password: bughunter Bug fixes ---------- (1) A bug in the processing of condition fragments which causes memory corruption when one side of a condition fragment collapses at the top. Reported by Adrián Riesco and illustrated by the following simplified example: fmod FOO is sort Foo . ops a b 1 : -> Foo . op f : Foo Foo -> Foo [id: 1] . ceq a = b if f(1, a) = b . endfm (2) A memory leak in the collapse of AU terms, visible under Purify with the following example: fmod FOO is sort Foo . ops a b 1 : -> Foo . op f : Foo Foo -> Foo [assoc id: 1] . eq f(1, a) = b . endfm Changes -------- (1) For operators in the C, CU, CI and CUI theories, if both arguments are the same, the rewrite, srewrite and search commands and the model checker will only consider one of the arguments for that step since only one rewriting step is made per pass, the choice of argument is irrelevant. This already happened for operators in the AC and ACU theories. The frewrite command still always considers all arguments even if they are identical since multiple rewriting steps can happen in each pass. (2) The command xunify and metalevel operator metaXunify() and metaDisjointXunify() are no longer supported. It appears that simply considering the subterms of the congruence class is not enough for narrowing modulo E. And a more sophisticated notion of unification modulo E doesn't fit within the existing Context framework at the metalevel. (3) A very experimental version of narrowing is supported. The syntax resembles the search command excetp that conditions are not supported: narrow [, ] in : . Here is one of =>+, =>*, or =>! which have the same meanings as they do with search. The major difference between narrow and search is that narrowing steps rather than rewriting steps are performed with rules. Equations still do normal in place rewriting and each state is reduced by equations before another narrowing step is looked for. Another difference is that narrowing proceeds depthfirst rather than breadthfirst. Unbound variables in the rhs of a (nonexec) rule get bound to fresh variables. Free variables in all but the user given initial state are named #n. Checking of states against the pattern_term is done using regular matching. There a large number of limitations on the current implementation: (a) Only operators from theories supported by unification (Free, C, AC, iter) may take part in narrowing. Operators from unsupported theories can occur above the narrowing redexes or within ground terms. (b) No attempt at theory extension needed for completeness in the AC and iter theories is made. (c) No counting the number of narrow steps or equational rewrites. (d) Bad interactions with operator strategies. (e) No support for conditional rules. (f) No support for frozen attribute. (g) No support for ctrl-C interrupts or tracing. (h) No support for continue command. (i) Duplicate states are detected but states that are equivalent up to a change of variables names are not. (j) Ground terms in the lhs of rules should not be reducible by equations or builtin reduction or strange things can happen. (k) Equations that can rewrite variables (i.e. they have a lhs that is, or can collapse to a bare variable) can corrupt unifiers in other paths. (l) The semi-compilation of unconditional rules has been pessimized to avoid conflicts with narrowing. Narrowing is reflected by the new descent function: op metaNarrow : Module Term Term Qid Bound Nat ~> ResultTriple? . It take a module, start term, pattern, search type ('+, '* or '!), bound on narrowing steps and result number and returns a triple containing the state that matched the pattern, its type, and the matching substitution. Steven