365 lines
13 KiB
Markdown
365 lines
13 KiB
Markdown
---
|
||
title: digitle in maude
|
||
date: 2022-03-14
|
||
tags: [maude, computer, cool languages]
|
||
summary: |
|
||
a solver for digitle (numbers countdown) in maude, a language
|
||
for rewriting systems.
|
||
...
|
||
|
||
so you know [digitle] right. it's the countdown numbers round.
|
||
|
||
[digitle]: https://c.eev.ee/digitle
|
||
|
||
1. you have six numbers to start with, each picked from 1–10 or 25, 50, 75, 100;
|
||
and a target.
|
||
2. you can add, subtract, multiply, or divide any of the numbers you currently
|
||
have.
|
||
3. 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.
|
||
|
||
[maude]: https://maude.cs.illinois.edu/w/index.php/The_Maude_System
|
||
|
||
**i just think maude is neat and this is a nice little example to show it off.**
|
||
that's all this is really.
|
||
|
||
---
|
||
|
||
```maude
|
||
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.
|
||
|
||
:::aside
|
||
**why is importing called `protecting`?** in maude, sorts (approximately,
|
||
types) aren't necessarily closed. you can add a new constructor, or equations
|
||
between constructor forms, at any time. unlike in languages like haskell or
|
||
rust, constructors don't have to be _free_, which means you can have equations
|
||
between them. like to get `ℤ/4ℤ` you can just do something like
|
||
|
||
```maude
|
||
fmod NAT4 is
|
||
including NAT .
|
||
eq 4 = 0 .
|
||
endfm
|
||
```
|
||
|
||
but when you're importing a module, most of the time you don't want to do any
|
||
of that. so there are three ways of importing a module to express how much you
|
||
intend to mess with it. `protecting` says you are not adding new constructors
|
||
or conflating existing ones. `extending` lets you add new constructors, but
|
||
not new equations. `including` lets you do whatever. since i'm just using
|
||
_normal_ numbers, `protecting` is what i want.
|
||
|
||
an important caveat is that it is not possible for maude itself to check you
|
||
are telling the truth here, but it can ask `yices` or `cvc4` for help. please
|
||
don't press me for more detail i have never used this
|
||
:::
|
||
|
||
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.
|
||
|
||
```maude
|
||
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.
|
||
|
||
:::aside
|
||
**the name `__` is pretty weird!** generally operator names are written with an
|
||
underscore where the arguments go, so the name of the addition operator is
|
||
`_+_`. in this case, there _is_ no operator, it's just two things next to each
|
||
other (in a context where a `Pool` value is expected, anyway), so it's just
|
||
two underscores.
|
||
:::
|
||
|
||
from here, we *could* just define the rewrite rules and be done. something like
|
||
this would work:
|
||
|
||
```maude
|
||
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 .
|
||
```
|
||
|
||
:::aside
|
||
**`sd`** is "symmetric difference"---e.g. `sd(1, 4) = sd(4, 1) = 3`. \
|
||
(it is also [a declaration form][sd] which is why it's purple.
|
||
i don't know how to distinguish the two in pandoc/kate's syntax highlighting
|
||
format sorry)
|
||
|
||
[sd]: https://maude.lcc.uma.es/maude321-manual-html/maude-manualch10.html
|
||
:::
|
||
|
||
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](https://c.eev.ee/digitle/#seed=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:
|
||
|
||
:::twocol
|
||
- 2 + 9 = **11**
|
||
- 4 × 8 = **32**
|
||
- 11 × 75 = **825**
|
||
- 825 − 32 = **793** :star::star:
|
||
:::
|
||
|
||
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.
|
||
|
||
```maude
|
||
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 .
|
||
```
|
||
|
||
:::aside
|
||
**`prec N`** is parsing/printing precedence (higher is looser, same as coq,
|
||
opposite of haskell/agda/idris).
|
||
:::
|
||
|
||
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.
|
||
|
||
```maude
|
||
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.
|
||
|
||
```maude
|
||
op _has_ : State Nat -> Bool .
|
||
eq (N Ps & Ss) has N = true .
|
||
eq S has N = false [otherwise] .
|
||
```
|
||
|
||
:::aside
|
||
it could even skip the `false` line with a slightly different signature but
|
||
then i would have to explain more about the sort & kind system... this is good
|
||
enough.
|
||
:::
|
||
|
||
|
||
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.
|
||
|
||
```maude
|
||
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.
|
||
|
||
```maude
|
||
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.
|
||
|
||
```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
|
||
```
|