From bffa11780e12ebefbb9e1e41bc3efa1d5ae38877 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Tue, 15 Mar 2022 04:42:38 +0100 Subject: [PATCH] add digitle post --- posts/2022-03-14-digitle-in-maude.md | 350 +++++++++++++++++++++++++++ posts/test.md | 16 -- style/page.css | 19 +- 3 files changed, 367 insertions(+), 18 deletions(-) create mode 100644 posts/2022-03-14-digitle-in-maude.md delete mode 100644 posts/test.md diff --git a/posts/2022-03-14-digitle-in-maude.md b/posts/2022-03-14-digitle-in-maude.md new file mode 100644 index 0000000..3661133 --- /dev/null +++ b/posts/2022-03-14-digitle-in-maude.md @@ -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. + + + +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. + + + +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 . +``` + + + +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 . +``` + + + +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] . +``` + + + + +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 +``` diff --git a/posts/test.md b/posts/test.md deleted file mode 100644 index 85c584d..0000000 --- a/posts/test.md +++ /dev/null @@ -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}$$ diff --git a/style/page.css b/style/page.css index 48ee047..8be0f5f 100644 --- a/style/page.css +++ b/style/page.css @@ -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; }