add digitle post
This commit is contained in:
parent
ccd9024861
commit
bffa11780e
|
|
@ -0,0 +1,350 @@
|
|||
---
|
||||
title: digitle in maude
|
||||
date: 2022-03-14
|
||||
tags: [maude, computer]
|
||||
...
|
||||
|
||||
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
|
||||
like `s (s (s (s z))) = z` and pow you've got $\mathbb{Z}/4\mathbb{Z}$.
|
||||
|
||||
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
|
||||
</aside>
|
||||
|
||||
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.
|
||||
</aside>
|
||||
|
||||
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`.
|
||||
</aside>
|
||||
|
||||
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).
|
||||
</aside>
|
||||
|
||||
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.
|
||||
</aside>
|
||||
|
||||
|
||||
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
|
||||
```
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
---
|
||||
title: test
|
||||
tags: [a, b]
|
||||
date: 2021-07-25
|
||||
conlang: laantas
|
||||
...
|
||||
|
||||
# hello
|
||||
|
||||
im gecs
|
||||
|
||||
:::example
|
||||
`{#kášńḿł | size=100 ; stroke=4}`
|
||||
:::
|
||||
|
||||
$$\mathbb{wow},\, \mathcal{MATH}$$
|
||||
|
|
@ -88,6 +88,10 @@ hr {
|
|||
height: 0;
|
||||
}
|
||||
|
||||
pre + hr {
|
||||
margin-top: 1.5em;
|
||||
}
|
||||
|
||||
.meta {
|
||||
display: flex;
|
||||
column-gap: 1em;
|
||||
|
|
@ -168,8 +172,11 @@ code {
|
|||
}
|
||||
|
||||
pre {
|
||||
width: min-content;
|
||||
margin: auto;
|
||||
width: min-content;
|
||||
margin: 0.5em auto;
|
||||
padding: 0.5em 0.8em;
|
||||
border: 1px solid var(--root-col);
|
||||
background: hsla(0deg, 0%, 100%, 40%);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -378,6 +385,14 @@ blockquote {
|
|||
}
|
||||
|
||||
|
||||
aside {
|
||||
font-size: 90%;
|
||||
margin: 0.5em 3em;
|
||||
border-left: 2px solid var(--root-col);
|
||||
padding-left: 1em;
|
||||
}
|
||||
|
||||
|
||||
/* syntax highlighting for maude
|
||||
* [todo] does this also look ok for other langs */
|
||||
.maude .pp { color: hsl(343deg, 100%, 40%); font-weight: 500; }
|
||||
|
|
|
|||
Loading…
Reference in New Issue