Maude-help mailing list

[Robert Jacobson <rljacobson AT gmail.com>]

Hi,

I am at the very start of learning Maude. I have skimmed through most of the manual and have read more carefully through the first 5 chapters or so.

1. When do I need to specify the name of a module? Let's follow along with `3.9.4 Parsing` to illustrate. We define a function module PARSING-EX1 and immediately are able to execute `parse 1 + 2 * 3 .` We get a message about ambiguity as we expect. But in the next command in which we use parentheses, we write `parse in PARSING-EX1 : 1 + (2 * 3) .` Why do we have "parse in…" in the second case but not the first? (Presumably the rule is the same for "red in…".) In other examples elsewhere, "red in…" is used for the first command and then elided for subsequent commands. We then define PARSING-EX2, and we use "parse in…" in every case. Is it required in every case?
2. Is there a "top level"? Is it possible to make a definition outside of a module? The examples of defining operators apparently need to be within a module.
3. When I "redefine" a module as I work through examples, is the previous definition lost entirely? (I understand that there are explicit ways to import definitions with protect, extend, etc.)
4. Can I "clear" a definition? E.g. if I want to "undefine" PARSING-EX2 as if it was never defined in the first place.
   
5. Does Maude support sequence variables? For example, using notation analogous to regular expressions, suppose I want to match the pattern `f(a, g(s*), t*)`, with s* and t* sequence variables, against the ground term `f(a, g(b, c), d, e)` to obtain the bindings `s*=(b,c), t*=(d, e)`. Can this be done? (There is a "hack" in which you declare f and g associative, but it isn't pretty.)
   

Best,

Robert