rhi/blog
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

use :::aside instead of <aside>

Browse source
This commit is contained in:
rhiannon morris 2022-03-16 18:40:12 +01:00
parent 81041fdb30
commit 6a7d65d421
1 changed files with 47 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

82
posts/2022-03-14-digitle-in-maude.md
View file

@ -40,24 +40,31 @@ 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 module, and saying that any time `M` or `N` show up in equations or rewrite
rules they stand for single numbers. rules they stand for single numbers.
<aside> :::aside
**why is importing called `protecting`?** in maude, sorts (approximately, **why is importing called `protecting`?** in maude, sorts (approximately,
types) aren't necessarily closed. you can add a new constructor, or equations 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 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 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}$. between them. like to get `ℤ/4ℤ` you can just do something like
but when you're importing a module, most of the time you don't want to do any ```maude
of that. so there are three ways of importing a module to express how much you fmod NAT4 is
intend to mess with it. `protecting` says you are not adding new constructors including NAT .
or conflating existing ones. `extending` lets you add new constructors, but eq 4 = 0 .
not new equations. `including` lets you do whatever. since i'm just using endfm
_normal_ numbers, `protecting` is what i want. ```
an important caveat is that it is not possible for maude itself to check you but when you're importing a module, most of the time you don't want to do any
are telling the truth here, but it can ask `yices` or `cvc4` for help. please of that. so there are three ways of importing a module to express how much you
don't press me for more detail i have never used this intend to mess with it. `protecting` says you are not adding new constructors
</aside> 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 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 have. it's a _multiset_: the number of copies of each number matters, but the
@ -93,13 +100,13 @@ 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 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. _anywhere_, without needing extra rules to shuffle the list around manually.
<aside> :::aside
**the name `__` is pretty weird!** generally operator names are written with an **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 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 `_+_`. 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 other (in a context where a `Pool` value is expected, anyway), so it's just
two underscores. two underscores.
</aside> :::
from here, we *could* just define the rewrite rules and be done. something like from here, we *could* just define the rewrite rules and be done. something like
this would work: this would work:
@ -111,9 +118,14 @@ rl [mul] : M N => M * N .
crl [div] : M N => M quo N if M rem N = 0 . crl [div] : M N => M quo N if M rem N = 0 .
``` ```
<aside> :::aside
**`sd`** is "symmetric difference"---e.g. `sd(1, 4) = sd(4, 1) = 3`. **`sd`** is "symmetric difference"---e.g. `sd(1, 4) = sd(4, 1) = 3`. \
</aside> (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 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 `comm`; they don't have to be next to each other), and replace them with the
@ -200,10 +212,10 @@ op _,_ : Steps Steps -> Steps [assoc id: nil prec 20] .
var Ss : Steps . var Ss : Steps .
``` ```
<aside> :::aside
**`prec N`** is parsing/printing precedence (higher is looser, same as coq, **`prec N`** is parsing/printing precedence (higher is looser, same as coq,
opposite of haskell/agda/idris). opposite of haskell/agda/idris).
</aside> :::
so solution traces are written like so solution traces are written like
`2 + 9 → 11,4 × 8 → 32,11 × 75 → 825,825 - 32 → 793` `2 + 9 → 11,4 × 8 → 32,11 × 75 → 825,825 - 32 → 793`
@ -235,11 +247,11 @@ eq (N Ps & Ss) has N = true .
eq S has N = false [otherwise] . eq S has N = false [otherwise] .
``` ```
<aside> :::aside
it could even skip the `false` line with a slightly different signature but 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 then i would have to explain more about the sort & kind system... this is good
enough. enough.
</aside> :::
the new rewrite rules (delete the other ones) have the same behaviour for the the new rewrite rules (delete the other ones) have the same behaviour for the