Maude-help mailing list

[Francisco Durán <narudocap AT gmail.com>]

Hi Robert,

Answers below...

> On 31 Oct 2022, at 17:06, Robert Jacobson <rljacobson AT gmail.com> wrote:
> 
> 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. 
>       • 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?

The "in <module-name> :" part is optional in most Maude commands. You can 
always add it. If you don't use it, Maude assumes that the module to use to 
execute the command is the "current" one (i.e., the last entered one or the 
one selected with the select command). If the current one is ok for you, 
fine, otherwise you have to explicitly specify the module to use. 

>       • 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.

All declarations must be inside modules. There is not a "top level".

>       • 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.)

By redefining I suppose you mean entering a module with the same name. In 
this case, the previous version of the module is replaced with the new one. 

This has nothing to do with module importation. Maude keeps many modules in 
the current session, each with different names, which can be imported from 
other modules. Note that from this collection of modules already loaded in 
the system, any can be selected (we can set as current module any of the ones 
in the system with a "select" command), or use to execute different commands 
(e.g., red in <module-name> : true ., where <module-name> is the name of any 
module in the system's session). 

>       • Can I "clear" a definition? E.g. if I want to "undefine" 
> PARSING-EX2 as if it was never defined in the first place.

I suppose that PARSING-EX2 is the name of a module. Then, no, you cannot 
undefine it. You can load or create another module with the same name, 
resulting in its redefinition. 

>       • 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.)

You will have to advance a little bit in your readings to get to equational 
attributes, but yes, you can. You can define lists or sets, and have matching 
module associativity, commutativity and/or identity. You can have variables 
of a type List or Set, and do things like the ones you ask about. 

Hope to have been of help. 

Cheers,

Francisco


> Best,
> 
> Robert