so you know digitle right. it’s the countdown numbers round.

- you have six numbers to start with, each picked from 1–10 or 25, 50, 75, 100; and a target.
- you can add, subtract, multiply, or divide any of the numbers you currently have.
- you can only use each number once, and the intermediates have to also all be positive integers. (it is ok to have some numbers left over at the end.)

you probably have not heard of maude though. but it’s cool. it lets you define rewrite systems with a few equational extras like associativity and commutativity. in other words it’s essentially a domain specific language for solving puzzles like this. it also lets you prove stuff like termination of your system, but we are not going to do any of that today.

**i just think maude is neat and this is a nice little example
to show it off.** that’s all this is really.

```
mod DIGITLE is
protecting NAT .
vars M N : Nat .
```

the file starts with a module declaration. everything has to live
inside some module, but this program isn’t big enough to be worth
splitting up so it’s all going into one. since digitle involves numbers,
i’m also importing the `NAT`

module, and saying that any time
`M`

or `N`

show up in equations or rewrite rules
they stand for single numbers.

the first thing i need is a ~~type~~ sort for the pool of
numbers we currently have. it’s a *multiset*: the number of
copies of each number matters, but the order they’re in doesn’t. the
most convenient way to express that is like this.

```
sort Pool .
subsort Nat < Pool .
op nil : -> Pool .
op __ : Pool Pool -> Pool [assoc comm id: nil] .
var Ps : Pool .
```

first i just declare `Pool`

as a sort, without saying
anything about what it looks like. next i say that any `Nat`

is also a `Pool`

(containing one copy of just that number),
by making `Nat`

a subsort of `Pool`

.

in the third and fourth lines, i say that `nil`

is a pool
(with no numbers), and two `Pool`

s written next to each other
are also a `Pool`

. so far, we’ve defined a binary tree. by
making `__`

associative, we’re saying that the exact
bracketing of the appends doesn’t matter, which flattens it to a list.
by saying it’s commutative, we’re saying the order *also* doesn’t
matter.

the last attribute, `id: nil`

, says that
`Ps nil = nil Ps = Ps`

. it also allows a pattern like
`M N Ps`

to match against `1 2`

, setting
`Ps = nil`

.

it feels a bit weird at times to be specifying constructors of a tree
and then telling the language to flatten them after the fact, coming
from languages where you try to design your datatypes to only have one
representation per value. but the benefit of writing it like this
instead of something like `op cons : Nat Pool -> Pool`

is
that maude knows what `assoc`

, `comm`

, and
`id`

mean, so later when i have some equations and rewrite
rules that match on the beginning of a list, it knows that it can
actually pick those numbers from *anywhere*, without needing
extra rules to shuffle the list around manually.

from here, we *could* just define the rewrite rules and be
done. something like this would work:

```
rl [add] : M N => M + N .
rl [sub] : M N => sd(M, N) .
rl [mul] : M N => M * N .
crl [div] : M N => M quo N if M rem N = 0 .
```

the first three rules just pick two numbers from our pool (any two,
because of `comm`

; they don’t have to be next to each other),
and replace them with the result of applying them to one of our
operations. the last one is slightly more complicated, because we can
only divide evenly. `_quo_`

ignores the remainder altogether,
so we need a *conditional rule* which only fires if the remainder
actually is zero.

save what we have so far, plus a terminating `endm`

for
the `mod`

, in a file `digitle.maude`

, and feed it
into the repl:

```
$ maude digitle
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 3.2.1 built: Mar 13 2022 18:56:15
Copyright 1997-2022 SRI International
Mon Mar 14 02:28:22 2022
```

let’s use random
puzzle ALO7b9UK as an example. we have to get to
**793** starting from **75, 4, 7, 9, 8, 2**.
so starting from that list, we want to search for a sequence of rewrites
that leads to a pool containing 793. one solution is all we need.

```
Maude> search [1] (75 4 7 9 8 2) =>* (793 Ps) .
search [1] in DIGITLE : 75 4 7 9 2 8 =>* Ps 793 .
Solution 1 (state 9577)
states: 9578 rewrites: 273357 in 128ms cpu (128ms real) (2135601 rewrites/second)
Ps --> 7
```

ok, so there *is* at least one solution, which leaves 7 unused
(because it is in the assignment for `Ps`

). we can use the
state label `9577`

to replay the sequence that reaches it,
and see which steps it took.

```
Maude> show path 9577 .
state 0, Pool: 2 4 7 8 9 75
===[ rl N M Ps => Ps N + M [label add] . ]===>
state 4, Pool: 4 7 8 11 75
===[ rl N M Ps => Ps N * M [label mul] . ]===>
state 146, Pool: 7 11 32 75
===[ rl N M Ps => Ps N * M [label mul] . ]===>
state 1733, Pool: 7 32 825
===[ rl N M Ps => Ps sd(N, M) [label sub] . ]===>
state 9577, Pool: 7 793
```

squinting at the available numbers each time, along with the rule labels, we can just about make out what it did to get to a solution:

- 2 + 9 =
**11** - 4 × 8 =
**32** - 11 × 75 =
**825** - 825 − 32 =
**793**⭐⭐

ok that’s cool. but reading the output is a bit annoying. let’s
instead keep track of what we did so that it’s just printed legibly at
the end of `search`

. thanks to maude’s flexible expression
syntax, we can make this look like pretty much whatever we want.

```
sort Op .
ops + - × ÷ : -> Op .
sort Steps .
--- empty list
op nil : -> Steps .
--- a single step, like "3 + 4 → 7"
op ___→_ : Nat Op Nat Nat -> Steps [prec 10] .
--- sequence of steps
op _,_ : Steps Steps -> Steps [assoc id: nil prec 20] .
var Ss : Steps .
```

so solution traces are written like
`2 + 9 → 11,4 × 8 → 32,11 × 75 → 825,825 - 32 → 793`

and that
is also how maude will print them.

the given state at any point is now going to be the available pool of
numbers, *plus* the steps taken so far. this is just a pair,
along with an abbreviation `{Ps}`

to make the
`search`

command look a little nicer.

```
sort State .
op _&_ : Pool Steps -> State .
op {_} : Pool -> State .
eq {Ps} = Ps & nil .
var S : State .
```

one last thing before the expanded rewrite rules is a predicate to
say what we are looking for. this isn’t strictly necessary, you could
just continue to pattern match in the `search`

command like
last time; i just think this looks a bit nicer. but a state “has” a
number `N`

if `N`

occurs anywhere in the pool.
maude supports repeating pattern variables so this is nice and
short.

```
op _has_ : State Nat -> Bool .
eq (N Ps & Ss) has N = true .
eq S has N = false [otherwise] .
```

the new rewrite rules (delete the other ones) have the same behaviour
for the number pool, and also append the current step to the trace.
since we don’t need `show path`

any more i removed the
labels.

```
rl M N Ps & Ss => Ps (M + N) & Ss, (M + N → (M + N)) .
rl M N Ps & Ss => Ps sd(M, N) & Ss, (M - N → sd(M,N)) .
rl M N Ps & Ss => Ps (M * N) & Ss, (M × N → (M * N)) .
crl M N Ps & Ss => Ps (M quo N) & Ss, (M ÷ N → (M quo N)) if M rem N = 0 .
```

now load the updated file into maude and run the search command. i’m
using `s.t.`

(short for `such that`

) to identify
solutions by a boolean expression, the `_has_`

function
above.

```
$ maude -no-banner digitle
Maude> search [1] {75 4 7 9 8 2} =>* S s.t. S has 793 .
search [1] in DIGITLE : {75 4 7 9 2 8} =>* S such that S has 793 = true .
Solution 1 (state 335734)
states: 335735 rewrites: 1114984 in 832ms cpu (830ms real) (1340125 rewrites/second)
S --> (7 793) & (9 + 2 → 11),(8 × 4 → 32),(75 × 11 → 825),(825 - 32 → 793)
```

and now we have our solution nicely printed!

there is one small thing that is still bothering me. if we are trying
`M + N`

, then trying `N + M`

later is just wasting
time. so what if we make all the rules conditional so that the first
argument is never smaller than the second.

```
crl M N Ps & Ss => Ps (M + N) & Ss, (M + N → (M + N)) if M >= N .
crl M N Ps & Ss => Ps sd(M, N) & Ss, (M - N → sd(M,N)) if M > N .
crl M N Ps & Ss => Ps (M * N) & Ss, (M × N → (M * N)) if M >= N .
crl M N Ps & Ss => Ps (M quo N) & Ss, (M ÷ N → (M quo N))
if M >= N /\ M rem N = 0 .
```

and look, it’s five times faster now it’s not repeating itself.

```
Maude> search [1] {75 4 7 9 8 2} =>* S s.t. S has 793 .
search [1] in DIGITLE : {75 4 7 9 2 8} =>* S such that S has 793 = true .
Solution 1 (state 46714)
states: 46715 rewrites: 270529 in 160ms cpu (158ms real) (1690806 rewrites/second)
S --> (7 793) & (9 + 2 → 11),(8 × 4 → 32),(75 × 11 → 825),(825 - 32 → 793)
```

here’s the full file. the `format`

directives i didn’t
discuss: the one in `_,_`

puts a space after the comma, and
the rest do some colours & indenting to make the solution a little
bit prettier. it also contains a predicate `_has!_`

for Hard
Mode, that requires *all* the numbers get used up; and
`_almost has_`

, which finds any almost-solution within 10 of
the target, and uses language features that maybe i will discuss if i
ever write a second post about maude.

```
mod DIGITLE is
protecting NAT .
var M N : Nat .
sort Pool .
subsort Nat < Pool .
op nil : -> Pool .
op __ : Pool Pool -> Pool [assoc comm id: nil] .
var Ps : Pool .
sort Op .
op + : -> Op [format (r o)] .
op - : -> Op [format (g o)] .
op × : -> Op [format (y o)] .
op ÷ : -> Op [format (b o)] .
sort Steps .
op nil : -> Steps .
op ___→_ : Nat Op Nat Nat -> Steps [prec 20 format (d d d d ! o)] .
op _,_ : Steps Steps -> Steps [assoc id: nil prec 10 format (d d s d)] .
var Ss : Steps .
sort State .
op _&_ : Pool Steps -> State [format (d d n++i --)] .
op {_} : Pool -> State .
eq {Ps} = Ps & nil .
var S : State .
op _has_ : State Nat -> Bool .
eq (N Ps & Ss) has N = true .
eq S has N = false [otherwise] .
op _has!_ : State Nat -> Bool .
eq (N & Ss) has! N = true .
eq S has! N = false [otherwise] .
op _almost has_ : State Nat -> [Bool] .
ceq (M Ps & Ss) almost has N = true if sd(M,N) <= 10 .
crl M N Ps & Ss => Ps (M + N) & Ss, (M + N → (M + N)) if M >= N .
crl M N Ps & Ss => Ps sd(M, N) & Ss, (M - N → sd(M,N)) if M > N .
crl M N Ps & Ss => Ps (M * N) & Ss, (M × N → (M * N)) if M >= N .
crl M N Ps & Ss => Ps (M quo N) & Ss, (M ÷ N → (M quo N))
if M >= N /\ M rem N = 0 .
endm
```