Dear Maude Abusers, A new alpha release can be accessed at SRI in ~eker/public_html/Maude/Alpha65/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha65/ Currently only linux and solaris are supported. The changes from Alpha64 are: (1) There is a new attribute "frozen" that prevents an operators arguments from being rewritten by rules. Note that using this attribute effectively changes the denotational as well as the operational semantics of the frozen operator by disallowing the congruence proof rule for rl/crls. This is an extension of rewriting logic recently suggested by Jose. The frozen attribute is reflected by op frozen : -> Attr [ctor] . and is supported by all commands and descent functions that use rules. (2) There is a new command set show breakdown on/off . that causes a breakdown of mb applications, equational rewrites and rule rewrites to be printed after the "rewrites:" line but before the "result" line. mb applications are now counted in the main rewrite total. (3) The is a new command line flag "-interactive" that causes Maude to treat stdin/stdout/stderr as a tty and generate prompts even if isatty() returns false. This may be useful if Maude is being controlled by another process via pipes/fifos etc. (4) There is a new command for "position fair" rule rewriting; it has 3 forms: frewrite [nrRewrites, rewritesPerPosition] term . frewrite [nrRewrites] term . frewrite term . frew is an abbreviation for frewrite; the "debug" and "in :" modifiers are supported as they are for rewrite. Unlike rewrite which uses a leftmost outermost strategy for applying rules and reduces the whole term with equations after each succcessful rule rewrite, frewrite attempts to be position fair by making a number of depth first traversals of the term, and on each traversal, each position that existed at the start of the traversal is entitled to at most rewritesPerPosition rule rewrites when its turn comes around. After a rule rewrite succeeds, only the subterm that was rewritten is reduced with equations in order to avoid destroying positions that haven't yet had their turn for the current traversal. Traversals are made until nrRewrites rule rewrites have been made or until no more rewrites are possible. In the 2nd and 3rd forms, rewritesPerPosition defaults to 1. In the 3rd form nrRewrites defaults to infinity. The continue command works with frewrite in the same ways as it works with rewrite. In particular, considerable extra information about the current traversal is saved by the frewrite so that frewrite [n, k] t . continue m . produces the same final answer as frewrite [s, k] t . if s = n + m. The are a couple of caveats with frewrite: (a) If position fair rewriting stops mid traversal (typically the case with the 1st and 2nd forms) then the sort of the (incompletely reduced) result has not been calculated and is printed as "(sort not calculated)". (b) Position fair rewriting is not substitution fair; this is particularly apparent if you have an AC soup of messages and objects. Fair rewriting is reflected by op metaFrewrite : Module Term MachineInt MachineInt ~> ResultPair which is the meta equivalent of the first form of frewrite except that a final (semantic) sort calculation is performed at the end in order to produce a correct ResultPair. (5) Greedy matching is used for rules in situations (currently rewrite/metaRewrite and frewrite/metaFrewrite with non-conditional rules) where only a single matching substitution is required. With A/AC/ACU etc operators this may result in different substitutions being chosen and improved matching speed. (6) rewrite, continue and now frewrite take 64bit rather than 32bit integers. There are also various bug fixes: (1) abort works properly within the rewrite command in some cases where it used to run out of memory or crash. (2) rewrite/metaRewrite (and now frewrite/metaFrewrite) reset the round robin pointers in the rule tables to give reproducible (i.e. functional) results. (3) multiple files specified on the command line are now read in correctly; previously the 2nd and subsequent files would be read in after hitting eofs, even if the eof in question was not from the previous command line file but a file imported by a previous command line file. Steven Various examples: fmod FAIR is pr MACHINE-INT . sort Foo . op i : MachineInt -> Foo . op j : Foo -> Foo [frozen] . op f : Foo Foo -> Foo . var M : NzMachineInt . var X : Foo . rl i(M) => i(M - 1) . rl f(X, i(0)) => X . endfm set trace on . set trace whole on . frew f(f(i(2), i(1)), f(j(i(3)), i(2))) . rew f(f(i(2), i(1)), f(j(i(3)), i(2))) . set trace off . frew [1, 1] f(f(i(2), i(1)), f(j(i(3)), i(2))) . cont 3 . fmod ALL-ONE-STEP-REWRITES is including META-LEVEL . sort TermSet . subsort Term < TermSet . op _|_ : TermSet TermSet -> TermSet [assoc comm id: mt ctor] . op mt : -> TermSet [ctor] . var T : Term . var M : Module . var L : Qid . var N : MachineInt . op findAllRews : Module Term Qid -> TermSet . op findAllRewsAux : Module Term Qid MachineInt -> TermSet . eq findAllRews(M, T, L) = findAllRewsAux(M, T, L, 0) . eq findAllRewsAux(M, T, L, N) = if metaXapply(M, T, L, none, 0, maxMachineInt, N) :: Result4Tuple then (getTerm(metaXapply(M, T, L, none, 0, maxMachineInt, N)) | findAllRewsAux(M, T, L, N + 1)) else mt fi . endfm set show breakdown on . red findAllRews(mod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . op 'g : 'Foo -> 'Foo [none] . none none rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo . rl ['k] : 'a.Foo => 'c.Foo . endm, 'f['a.Foo, 'g['a.Foo]], 'k) . red findAllRews(mod 'FOO is protecting 'BOOL . sorts 'Foo ; 'Bar . subsort 'Bar < 'Foo . op 'a : nil -> 'Foo [none] . op 'b : nil -> 'Foo [none] . op 'c : nil -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [assoc comm] . op 'g : 'Foo -> 'Foo [frozen] . none none rl ['k] : 'f['X:Foo, 'Y:Foo] => 'X:Foo . rl ['k] : 'a.Foo => 'c.Foo . endm, 'f['a.Foo, 'g['a.Foo]], 'k) . fmod TEST is pr META-LEVEL . op m : -> Module . eq m = (mod 'FAIR is protecting 'MACHINE-INT . sorts 'Foo . none op 'i : 'MachineInt -> 'Foo [none] . op 'f : 'Foo 'Foo -> 'Foo [none] . none none rl ['k] : 'i['M:NzMachineInt] => 'i['_-_['M:NzMachineInt, '1.NzMachineInt]] . rl ['k] : 'f['X:Foo, 'i['0.MachineInt]] => 'X:Foo . endm) . op t : -> Term . eq t = 'f['f['i['2.NzMachineInt], 'i['1.NzMachineInt]], 'f['i['3.NzMachineInt], 'i['2.NzMachineInt]]] . endfm red metaFrewrite(m, t, 1, 1) . red metaFrewrite(m, t, 2, 1) . red metaFrewrite(m, t, 3, 1) . red metaFrewrite(m, t, 4, 1) . red metaFrewrite(m, t, 5, 1) . red metaFrewrite(m, t, 6, 1) . red metaFrewrite(m, t, 7, 1) . red metaFrewrite(m, t, 8, 1) . red metaFrewrite(m, t, 9, 1) . red metaFrewrite(m, t, 10, 1) . red metaFrewrite(m, t, 11, 1) . red metaFrewrite(m, t, 0, 1) . set show breakdown off .