Maude (My Incompleted Notes)
I happened across these while browsing my files. Needless to say they are incomplete and you should probably just read the Maude manual.
I won't lie. I'm kind skipping over the theory that underpins Maude. I find rewriting interesting, but the theory is lost on me without trying to use it for something familiar. So, this will server as my notes over the Maude language as I try to build my way to a game of tic-tac-toe.
This is not a tutorial for Maude. It's hardly a proper summary. The manual is 615 pages long and even ask you to refer to external libraries on some sections.
Btw, if you are writing a manual for a language, please keep it self-contained. Don't go off introducing libraries and external dependencies unless you are talking about how to use those.
The CLI
Maude is distributed as a self-contained executable. When you run it from the command line you'll be greated with it's shell / REPL.
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 3.5 built: Sep 25 2024 12:00:00
Copyright 1997-2024 SRI International
Sun Dec 8 10:13:22 2024
Maude>
From here you can directly enter modules or load a file into you current session. By convention, module names are in SCREAM-KABAB-CASE.
Maude> fmod SIMPLE-NAT is
sort Nat .
op zero : -> Nat .
op s_ : Nat -> Nat .
op _+_ : Nat Nat -> Nat .
vars N M : Nat .
eq zero + N = N .
eq s N + M = s (N + M) .
endfm
Maude> load my-nat.maude
Program files can additionally contain commands for the Maude session.
Reducing
To evalute equations in Maude, you use the reduce command.
reduce in SIMPLE-NAT : s s zero + s s s zero.
SIMPLE-NAT
When using reduce the in $MODULE-NAME : can be ommited. Maude will default to the last module loaded into your session. Additionally, Maude will search for modules in the following order:
- The directories specified by
MAUDE_LIB - The directory containing the exectuable
- The current directory
Finally when starting a session, Maude will load it's prelude which includes some default modules.
Rewriting
I forgot what supposed to be here. This was originally put together some fevered night December, 2024
...
Maudeisms
Maude makes use of a lot of termonolgy. These modules define terms and syntax (operators) and rules (equations) for tranforming these terms and syntax into new terms and new syntax. Additionally, they define the relationships (sorts and subsorts) between these operators and restrict how equations can be used. Finally, if an operator is unable to be rewritten, Maude will leave a hole in your program (kinds).
A Kind in Maude simbolizes a valid-but-errornous state. It's a program which has inputs which the equation can accept, but has no rules to reduce it. To, illustrait this, the following example will be analyzed:
fmod KINDS-AND-SORTS is
sorts X Y Z W .
subsort X < Z .
subsort Y < Z .
op x : -> X . op y : -> Y .
op z : -> Z . op w : -> W .
op _+_ : X Y -> W .
eq x + y = w .
endfm
The above code defines 4 groups (sorts) X, Y, Z, and W. It then defines that X is member of Z and Y is a member of Z. W exist as an isolated sort with no relationships (subsorts). The graph of these sorts looks as followed:
Z
/ \
X Y W
It then goes on to define 4 terms to use in our equations. Then it defines a + operation that takes an X term and a Y term, producing a W term. Finally, we define a single equation: "When _+_ is given x and y rewrite it to be w".
With that basis defined, lets look at some expression we can write in this module. We'll start with a valid and nonerroneous equation:
Maude> reduce in KINDS-AND-SORTS : x + y . reduce in KINDS-AND-SORTS : x + y . rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) result W: w
Maude applies the singular rewrite it has valiable x + y = w. Reporting the expression has the type W with the "value" w. What would happen if we replace x or y with z?
Maude> reduce in KINDS-AND-SORTS : z + y . reduce in KINDS-AND-SORTS : z + y . rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second) result [W]: z + y Maude> reduce in KINDS-AND-SORTS : x + z . reduce in KINDS-AND-SORTS : x + z . rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second) result [W]: x + z Maude> reduce in KINDS-AND-SORTS : z + z . reduce in KINDS-AND-SORTS : z + z . rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second) result [W]: z + z
Here, Maude was unable to reduce the expression it was given. However, the Maude manual describes this as giving "the benefit of doubt". If an expression could exist, it's allowed to exist. x + z could exist. This allows you to interpret an incomplete result as an error or as deferred execution.
"If I could rewrite this, then the result would be some value in the sort W."
But, if we change x or y to a w, then Maude will reject our program.
Maude> reduce in KINDS-AND-SORTS : w + x . Warning: <standard input>, line 18: didn't expect token +: w + <---*HERE* Warning: <standard input>, line 18: no parse for term. Maude> reduce in KINDS-AND-SORTS : y + w . Warning: <standard input>, line 19: didn't expect token w: y + w <---*HERE* Warning: <standard input>, line 19: no parse for term. Maude> reduce in KINDS-AND-SORTS : w + w . Warning: <standard input>, line 20: didn't expect token +: w + <---*HERE* Warning: <standard input>, line 20: no parse for term.
In this case, Maude see no path forwards. _+_ cannot accept any member of the sort W as an input. Thus, this program fails to parse.
Functional Modules
Functional modules are a collection of [...]. Sorts define groups which operators can exist within. Operators of symbols which you can use in equations. Equations are the rules defining how you transform a collection of operators. Memberships define operators that should be treated as a specialized sort.
Equations are expected to be function in the mathematical sense: they map inputs to outputs one-to-one. If equations have multiple solutions, you will have inconsistent behavior.
System Modules
System modules basically extend from functional modules. They add the ability to rewrite subsections your program in ways that equations cannot. Additionally, rules happen concurrently.,
Important Modules
Just use including. The manual basically says the other modes are useless, and they are defined in perlexing and needlessly abstract terms. I shit you not, they aren't even checked:
The user must be aware that, as explained later, the Maude system does not check that these constraints are satisfied, that is, the different modes of importation can be understood as promises by the user, which would need to be proved by him/herself.
Keywords
A quick collection of keywords Maude programs.
| keyword | functionality |
|---|---|
fmod |
Defines a "functional module" these are modules that only contain equations, relationships, and data definitions. |
mode |
Defines a "system module", they extend functional modules with rules and state transisions. These two features operate concurrently unlike equations. |
sort/sorts |
Definies a type or group that terms can be a member of. |
subsort/subsorts |
Define a relationship between two types/groups in your program. |
op/ops |
Defines a operator which is a symbol can can have zero or more inputs associated with it. A operator with no inputs is called a constant. |
var/vars |
Declares variables for you to use in your equations. |
eq |
Defines an unconditional equation. |
mb |
Declares an unconditional membership based on an expression. |
Tic Tac Toe
Future and relative to when all of the above was written here. I some how figured out enough Maude to implement a game of tic-tac-toe. It makes use of basically everything?
Raw source here.
omod TIC-TAC-TOE is
including STD-STREAM .
including NAT .
sorts Player X O .
subsorts X O < Player .
op Xs : -> X . op Os : -> O .
op next-player : Player -> Player .
eq next-player(Xs) = Os .
eq next-player(Os) = Xs .
sorts Cell Row Grid .
op ___ : Cell Cell Cell -> Row .
op _ : -> Cell [format (! o)] .
op x : -> Cell [format (b! o)] .
op o : -> Cell [format (r! o)] .
op is-empty : Cell -> [Bool] .
eq is-empty(_) = true .
eq is-empty(x) = false .
eq is-empty(o) = false .
op to-cell : Player -> Cell .
eq to-cell(Xs) = x .
eq to-cell(Os) = o .
sort GameState .
ops read-row
read-column
show-grid
wait-show-grid
wait-make-turn
check-win
: -> GameState .
class GameClass
| turn : Player
, state : GameState
.
class RowClass
| index : Nat
, cells : Row
.
ops Game Row1 Row2 Row3 : -> Oid .
op RowX : -> Oid .
op play : -> Configuration .
var S : String .
var O : Oid .
var P : Player .
vars N M : Nat .
vars R1 R2 R3 : Row .
vars C1 C2 C3 C4 C5 C6 C7 C8 C9 : Cell .
op has-won : Row Row Row -> [Bool] .
ceq has-won((C1 C1 C1), R2, R3) = true
if C1 =/= _ .
ceq has-won(R1, (C1 C1 C1), R3) = true
if C1 =/= _ .
ceq has-won(R1, R2, (C1 C1 C1)) = true
if C1 =/= _ .
ceq has-won((C1 C2 C3), (C1 C5 C6), (C1 C8 C9)) = true
if C1 =/= _ .
ceq has-won((C1 C2 C3), (C4 C2 C6), (C7 C2 C9)) = true
if C2 =/= _ .
ceq has-won((C1 C2 C3), (C4 C5 C3), (C7 C8 C3)) = true
if C3 =/= _ .
ceq has-won((C1 C2 C3), (C4 C1 C6), (C7 C8 C1)) = true
if C1 =/= _ .
ceq has-won((C1 C2 C3), (C4 C3 C6), (C3 C8 C9)) = true
if C3 =/= _ .
eq has-won(R1, R2, R3) = false .
op to-string(_) : Cell -> String .
eq to-string(_) = " _ " .
eq to-string(x) = " x " .
eq to-string(o) = " o " .
op to-string(_) : Player -> String .
eq to-string(Xs) = "Xs" .
eq to-string(Os) = "Os" .
--- serious? the new line is in the string ._.
op to-index(_) : String -> Nat .
eq to-index("1\n") = 1 .
eq to-index("2\n") = 2 .
eq to-index("3\n") = 3 .
op show-row : Oid Nat -> Msg .
op show-row-iter : Nat -> Msg .
op print-cells : String -> Msg .
op wait-for-print-cells : Nat -> Msg .
ops turn-row turn-column : Nat -> Msg .
op target-row : Row Nat -> Msg .
eq play = <>
< Game : GameClass | turn : Xs, state : show-grid >
< Row1 : RowClass | index : 1, cells : _ _ _ >
< Row2 : RowClass | index : 2, cells : _ _ _ >
< Row3 : RowClass | index : 3, cells : _ _ _ >
.
rl [show-grid] :
< Game : GameClass | state : show-grid >
=>
< Game : GameClass | state : wait-show-grid >
show-row(Row1, 3)
show-row(Row2, 2)
show-row(Row3, 1)
show-row-iter(3)
.
rl [show-row] :
show-row-iter(N)
show-row(O, N)
< O : RowClass | cells : (C1 C2 C3) >
=>
< O : RowClass | cells : (C1 C2 C3) >
print-cells(to-string(C1) + to-string(C2) + to-string(C3))
wait-for-print-cells(N)
.
rl [print-cells] :
print-cells(S)
wait-for-print-cells(s N)
< Game : GameClass | >
=>
write(stdout, Game, S + "\n")
< Game : GameClass | >
show-row-iter(N)
.
rl [start-turn] :
< Game : GameClass | state : wait-show-grid >
show-row-iter(0)
=>
< Game : GameClass | state : read-column >
getLine(stdin, Game, "Enter column: ")
.
rl [column-retry] :
< Game : GameClass | state : read-column >
gotLine(Game, O, S)
=>
if S == "1\n" or S == "2\n" or S == "3\n" then
< Game : GameClass | state : read-row >
turn-column(to-index(S))
getLine(stdin, Game, "Enter row: ")
else
< Game : GameClass | state : read-column >
getLine(stdin, Game, "Enter column: ")
fi
.
rl [column-retry] :
< Game : GameClass | state : read-row >
gotLine(Game, O, S)
=>
if S == "1\n" or S == "2\n" or S == "3\n" then
< Game : GameClass | state : wait-make-turn >
turn-row(to-index(S))
else
< Game : GameClass | state : read-row >
getLine(stdin, Game, "Enter row: ")
fi
.
rl [update-column-1] : turn-column(1)
turn-row(N)
< O : RowClass | index : N, cells : (C1 C2 C3) >
< Game : GameClass | turn : P, state : wait-make-turn >
=>
if is-empty(C1) then
< O : RowClass | index : N, cells : (to-cell(P) C2 C3) >
< Game : GameClass | turn : P, state : check-win >
else
< O : RowClass | index : N, cells : (C1 C2 C3) >
< Game : GameClass | turn : P, state : read-column >
getLine(stdin, Game, "Enter column: ")
fi
.
rl [update-column-1] : turn-column(2)
turn-row(N)
< O : RowClass | index : N, cells : (C1 C2 C3) >
< Game : GameClass | turn : P, state : wait-make-turn >
=>
if is-empty(C2) then
< O : RowClass | index : N, cells : (C1 to-cell(P) C3) >
< Game : GameClass | turn : P, state : check-win >
else
< O : RowClass | index : N, cells : (C1 C2 C3) >
< Game : GameClass | turn : P, state : read-column >
getLine(stdin, Game, "Enter column: ")
fi
.
rl [update-column-1] : turn-column(3)
turn-row(N)
< O : RowClass | index : N, cells : (C1 C2 C3) >
< Game : GameClass | turn : P, state : wait-make-turn >
=>
if is-empty(C3) then
< O : RowClass | index : N, cells : (C1 C2 to-cell(P)) >
< Game : GameClass | turn : P, state : check-win >
else
< O : RowClass | index : N, cells : (C1 C2 C3) >
< Game : GameClass | turn : P, state : read-column >
getLine(stdin, Game, "Enter column: ")
fi
.
rl [check-win] :
< Row1 : RowClass | cells : R1 >
< Row2 : RowClass | cells : R2 >
< Row3 : RowClass | cells : R3 >
< Game : GameClass |
turn : P, state : check-win >
=>
if has-won(R1, R2, R3) then
write(stdout, Game, to-string(P) + " Wins!\n")
else
< Row1 : RowClass | cells : R1 >
< Row2 : RowClass | cells : R2 >
< Row3 : RowClass | cells : R3 >
< Game : GameClass |
turn : next-player(P), state : show-grid >
fi
.
rl [clean-up] :
wrote(O, stdout)
=>
none
.
endom