December Adventure 2024
This is my log for December Adventure. I don’t have a clear plan for the contents, we’ll see where it goes :)
The December Adventure is low key. The goal is to write a little bit of code every day in December.
–– Eli Mellen
Dec 31
Big gap for the update, but I didn’t really touch computers over the vacation. So I’ll finish up with AoC 2024 day 23 in Prolog. Just part one though :)
The solution is, like the others, quite short:
We start out by making the connections bidirectional with the link predicate. We then provide the triangle query to find all groups of three computers – to prevent getting duplicates, we establish an ordering for the nodes.
From these found triangles, we filter out any groups that don’t contain a t as the first letter. Solving is then simply counting these t_triangles.
I ran into some problems with the t_triangle predicate producing too many results; the key was once to ensure we stop early.
These small exercises have really taught me a lot of Prolog, really neat!
That’s all, thanks!
Dec 17 & 18
I did AoC 2024 day 17 across two days, but didn’t get to finish part 2 of it. I didn’t bother brute forcing. Also I skipped parsing anything as the inputs were so small
:-
:-
% adv
% bxl
% bst
% jnz
% bxc
% out
% bdv
% cdv
This all works pretty well. The VM is initialized by the atom of load_program, so we solve by running solve1(short). I made sure to use the #=/2 operator from clpz for all assignments since I was hoping for part 2 that I could use constraint solving to find the register A for part 2.
That didn’t really work - at least not well enough!
.10000000000,
I don’t really want to invest too much time into this, but I think this sort of thing is perfect for clpz, SMT solvers or even symbolic execution. After this not going as expected, I saw some people did something similar in Prolog too, but I don’t plan on just copying it entirely :)
Here’s the solution that uses constraint solving. They add “fuel” for limiting computation and “residuals” which consist of all intermediate registers. Clever!
Edit: I ran the code linked above - it immediately solves in SWI-Prolog, but not in Scryer! Perhaps my original code would have worked in SWI?
Dec 14
Didn’t expect to have this much fun with AoC. Did 2024 day 14 today. Again in Prolog because it hasn’t let me down yet.
:-
We start out by defining how to calculate the safety product. We do this by:
- Calculating a position for every robot at an offset of
T(time) - Counting the number of robots in each quadrant given placement relative to the middle, e.g., for quadrant 1,
Xmust be in the left-top quadrant - Calculating safety factor by finding the product of the quadrant counts
The answer is simply just going 100 time steps ahead on a board that is 101x103 tiles.
I didn’t like part 2 that much. I didn’t really know what this tree was going to look like, so I tried a couple of different things. I ended up consulting other solutions to find a way to do it without too much hassle (i.e., brute force). I simply find the first time step that provides a unique configuration of positions. It’s very inefficient in Prolog to do it this way.
:-
It takes a while to find the result. I was hoping that clpz might be of use here, but modeling the problem with T being a finite domain doesn’t help at all since we still have to enumerate all time steps one by one with this technique.
Would like to see a nicer way! Also, parsing is getting nicer. I found out about the | alternative syntax which I didn’t see in the documentation before.
:-
:-
:-
Dec 13
Wanted to do another AoC in Prolog today, 2024 day 13. It seemed like an integer constraint problem, which is easily done with CLP(ℤ).
It was surprisingly easy again today
:-
:-
That’s the solution for both problems! We just define the constraints of the problem:
- Number of A presses and number of B presses must be greater than or equal to 0
- If there is no offset, we also limit the number of presses to 100 for both buttons
- Set up the equations to calculate number of presses
- Use the
labelingpredicate to minimize the cost, where the cost is 3 for button A and 1 for button B - For each configuration, find the minimum cost and sum them over
Extremely satisfying that so much work is handled by so little code.
And parsing input:
:-
:-
:-
Very similar to yesterday, DCGs are making more sense now, but still sort of strange. By the way, the AX-AY is syntax for pairs.
Prolog bonus:
Since the solution is defined in terms of CLP(ℤ), we can use the definitions to generate problems. For example, generating all problems where the minimum cost is 220:
?- constraint(config((AX-AY),(BX-BY), (PX-PY)), 0, 220).
.. .
By unbinding the Solution (220), we can even go through all solutions for all minimum costs. That’s amazing!
Dec 12
I did AoC 2024 day 5 today. This time in (Scryer) Prolog since the ordering part of the problem seemed like a database of facts and checking the pages seemed like querying the database.
I sat down and solved the ordering first, which was very simple without the parsing!
:-
This assumes facts in the shape page_order(X,Y) for all the page orderings, and pages([_]) for page numbers. The predicate in_order works by checking elements of page numbers per update, recursively making sure that each pair of numbers satisfies a page_order to be considered “in order”. Solving puzzle one is all about filtering for pages/1 that are in_order/1 and extracting the middle element of those for summation - here we use the stdlib for lists.
For the second part, we have to fix unordered page numbers. We can apply the same utilities and use a helper:
The structure is somewhat similar - we filter pages/1 for all facts that are not in_order/1, then fix the list by making pairwise swaps (using the fix_list/2 predicate) and finish off with the same middle-item sum of the fixed ordered lists.
There was some tinkering with fix_list to get it to work properly. We just want to keep trying to swap until we see that the list of page numbers is unchanged. The actual swapping itself is quite simple: given input [A,B|Rest], if it is not in order, swap the items in the result. If the items are in order, we recurse.
That was very short and concise! But we also have to consider parsing the input to the puzzle. This is done with DCGs (Definite Clause Grammars).
It looks pretty wild, but if you squint at it hard enough it looks similar to a BNF grammar.
:-
:-
:-
We use char_type/2 from the charsio library to categorize the input we see and assertz any new facts as we parse the input, ignoring any whitespace. I didn’t find an easier way to parse the digits. It still feels kind of foreign for me to use. Markus Triska’s online prolog resource is a great place to find info on this stuff.
Putting this together, we can run the following in the REPL to solve
?- load_input('input/day05'), solve1(Sum1), solve2(Sum2).
Dec 11
A bit of a break from writing, but today I did day 3 of AoC in Roc, which was fun!
parseJunk =
Parser.const (Err {})
|> Parser.skip (String.anyCodeunit)
|> Parser.skip (Parser.chompWhile \b -> b != 'm' && b != 'd')
parseMul =
Parser.const \x -> \y -> Ok (Mul { x, y })
|> Parser.skip (String.string "mul(")
|> Parser.keep String.digits
|> Parser.skip (String.string ",")
|> Parser.keep String.digits
|> Parser.skip (String.string ")")
parseDo =
Parser.const (Ok (Do))
|> Parser.skip (String.string "do()")
parseDont =
Parser.const (Ok (Dont))
|> Parser.skip (String.string "don't()")
parseInput = Parser.oneOf [parseMul, parseDo, parseDont, parseJunk] |> Parser.many
calcPart1 = \vals ->
List.keepOks vals (\x -> x)
|> List.walk
(0, true)
(\(acc, should), current ->
when current is
Mul { x, y } -> (acc + x * y, should)
_ -> (acc, should)
)
calcPart2 = \vals ->
List.keepOks vals (\x -> x)
|> List.walk
(0, true)
(\(acc, should), current ->
when current is
Mul { x, y } -> (acc + x * y, should)
Do -> (acc, true)
Dont -> (acc, false)
_ -> (acc, should)
)
The language is pretty nice considering how WIP it is. Some parts of the dev experience is a little rough but overall it is quite nice!
Dec 08
Continuing from yesterday, I completed the compilation and execution steps and solved the simple part of the correctness proof.
-- From the lean book
(α : Type u) : {_ : Nat} -> Type u where
| nil : @Vect α 0
| cons : α → @Vect α n → @Vect α (n + 1)
deriving Repr
(n: Nat) := @Vect Int n
: stack 0 := @Vect.nil Int
mutual
-- The nats here track number of ints on the stack.
-- Since we don't have heterogeneous stacks, we can do this.
: (s: Nat) → (s': Nat) → Type
| PUSH : Int → Op s (Nat.succ s)
| ADD : Op (Nat.succ (Nat.succ s)) (Nat.succ s)
| EQ: Op (Nat.succ (Nat.succ s)) (Nat.succ s)
| IF : Code s s' → Code s s' → Op (Nat.succ s) s'
deriving Repr
: (s: Nat) → (s': Nat) → Type where
| nil : Code s s
| cons : Op s s' → Code s' s'' → Code s s''
deriving Repr
end
mutual
{s s' : Nat} (c: Op s s') (st : stack s): stack s' :=
match c, st with
| Op.PUSH n, st => Vect.cons n st
| Op.IF c1 c2, Vect.cons b st =>
if intToBool b then exec c1 st else exec c2 st
| Op.ADD, Vect.cons e1 (Vect.cons e2 st) =>
Vect.cons (e1 + e2) st
| Op.EQ, Vect.cons e1 (Vect.cons e2 st) =>
Vect.cons ((e1 == e2).toNat) st
{s s' : Nat} (c: Code s s') (st : stack s): stack s' :=
match c with
| Code.nil => st
| Code.cons op c' => exec c' (exec_op op st)
end
{s s' s'' : Nat} : Code s s' → Code s' s'' → Code s s''
| Code.nil, c => c
| Code.cons x xs, c => Code.cons x (append xs c)
: Exp → Code n (Nat.succ n)
| Exp.val_exp v => Code.cons (Op.PUSH v) Code.nil
| Exp.plus_exp e1 e2 =>
append (compile e1)
(append (compile e2)
(Code.cons Op.ADD Code.nil))
| Exp.comp_exp e1 e2 =>
append (compile e1)
(append (compile e2)
(Code.cons Op.EQ Code.nil))
| Exp.if_exp b e1 e2 =>
append (compile b)
(Code.cons (Op.IF (compile e1) (compile e2)) Code.nil)
#eval exec (compile some_simple_exp) empty_stack
{n : Nat} (e : Exp) (s : stack n) :
exec (compile e) s = Vect.cons (eval e) s := by
induction e with
| val_exp v =>
simp [compile, exec, exec_op]
rfl
| plus_exp e1 e2 ih1 ih2 =>
sorry
| comp_exp e1 e2 ih1 ih2 =>
sorry
| if_exp b e1 e2 ih1 ih2 ih3 =>
sorry
I found out that the old version with the Val t def can progress if we add @[reducible]. I ran into other roadblocks with that approach, though. So for now this is fine!
The proof is yet to be complete, but I’m happy with the progress so far.
Dec 07
I’m going another route with the Lean compiler I was working on yesterday. I just want to do small increments on something that works.
This is what I reduced down to
where
| val_exp : Int → Exp
| plus_exp : Exp → Exp → Exp
| comp_exp : Exp → Exp → Exp
| if_exp : Exp → Exp → Exp → Exp
(n: Int) : Bool := if n == 0 then True else False
: Exp → Int
| Exp.val_exp v => v
| Exp.plus_exp e1 e2 => eval e1 + eval e2
| Exp.comp_exp e1 e2 => (eval e1 == eval e2).toNat
| .if_exp b e1 e2 => if intToBool $ eval b then eval e1 else eval e2
#eval eval (Exp.if_exp (Exp.comp_exp (Exp.val_exp 4) (Exp.val_exp 3)) (Exp.val_exp 42) (Exp.val_exp 5))
The Val t definition above couldn’t really unify easily, it’s clear I shouldn’t be doing that from the type system complaints. Instead this is just a simple interpreter, very simple in fact. I will be adding opcodes for a simple stack machine later. Obviously I can simplify a lot of things because we don’t have heterogeneous stack values in this version of the language. Instead everything is an Int :)
Dec 06
Continued looking at Lean4, wanted to translate the functional pearl I talked about a couple of days ago to Lean, but it didn’t go as smoothly as I expected. “A type-correct, stack-safe, provably correct, expression compiler in Epigram”
This is what I had, translated from the Idris version I made.
| tnat
| tbool
deriving Repr
: TyExp → Type
| .tnat => Nat
| .tbool => Bool
-- Coercions doesn't address the issue
-- instance : Coe (Val TyExp.tnat) Nat where
-- coe x := x
-- instance : Coe Nat (Val TyExp.tnat) where
-- coe x := x
: TyExp → Type
| val_exp : Val t → Exp t
| plus_exp : Exp tnat → Exp tnat → Exp tnat
| if_exp : Exp tbool → Exp t → Exp t → Exp t
: Add (Val tnat) where
add x y := Nat.add x y
/- Error here ^
application type mismatch
Nat.add x
argument
x
has type
Val tnat : Type
but is expected to have type
Nat : Type
-/
{t : TyExp} : Exp t → Val t
| .val_exp v => v
| .plus_exp e1 e2 => (eval e1) + (eval e2)
-- vvvvvv errors too
| .if_exp b e1 e2 => if eval b then eval e1 else eval e2
It seems that type coercions aren’t as easy to use in Lean. I tried to use the Coe typeclass, but it didn’t work as I expected.
Hopefully I’ll get some time to look at this more tomorrow.
Dec 05
Today I decided to dig into Lean4. I started out by solving some of the simple Software Foundations induction exercises.
The syntax is very clean (heh), and the tactic language is similar to Coq (Rocq now?).
I did some basic natural number proofs:
(n : Nat) : n + 0 = n := by
induction n <;> simp
(n: Nat) : n - n = 0 := by
induction n <;> simp
(n m : Nat) : n + m = m + n := by
intros
-- `omega` to take the short path :)
induction n
. induction m <;> simp
. induction m
. simp
. rw [Nat.succ_add, Nat.add_succ]
congr 1
(n m p : Nat) : n + (m + p) = (n + m) + p := by
induction n with
| zero => rw [add_comm, add_comm]
simp
| succ n => omega -- didn't want to think too hard here..
(n: Nat) : n * 0 = 0 := by
induction n <;> simp
(n: Nat) := match n with
| Nat.zero => Nat.zero
| Nat.succ n' => Nat.succ (Nat.succ (double n'))
(n : Nat) : double n = n + n := by
induction n with
| zero => rfl
| succ n ih => simp [double]
rw [ih]
rw [Nat.succ_add, Nat.succ_add, add_assoc]
I am aware of the “Please do not post solutions to the exercises in a public place” notice in the Software Foundations book.
I will refrain from posting every part of my proofs if I continue with this.
It feels very snappy in the VS Code plugin. When comparing the solutions to my Rocq solutions, there are definitely places where the proof is more concise in Lean4. E.g., the minus_n_n proof in Rocq is:
Theorem minus_n_n : forall n,
minus n n = 0.
Proof.
The induction hypothesis is just applied immediately. It seems that the simp in Lean4 may be closer to what simpl + auto does in Rocq in conjunction. Very neat!
Dec 03
Didn’t do a lot today. I updated my nix config a little after updating my flake lock.
I also followed along the API Authentication guide for Phoenix Framework’s mix phx.gen.auth. Was really easy to get working. Not really sure what to do with it though. I have a little playground project going that I want to do some exploration/learning with. Mostly learning about effective domain design and rapid prototyping with LiveView. No code to show though.
Dec 02
Got that correctness proof done! Very exciting. It got a little long, so I’ll rather just link to the commit.
It’s very messy and Idris1 isn’t the best at error messages so I ported to Idris2 and backported once it worked – though both versions are more or less the same.
I also wanted to do something less mind straining, so I did AoC day 1 in Idris2 too
List (Integer, Integer) -> Integer
part1 loc =
let (left, right) = unzip loc
sortedPairs = zip (sort left) (sort right) in
sum . map (abs . uncurry (-)) $ sortedPairs
List (Integer, Integer) -> Integer
part2 locs =
let (left, right) = unzip locs in
sum $ map (\l => l * cast (count_x l right)) left
where
(Eq t, Foldable m) => t -> m t -> Nat
count_x v = count (== v)
String -> List (Integer, Integer)
parse = map parseLine . lines
where
parseLine str = case words str of
[l, r] => (cast l, cast r)
_ => (0, 0)
IO (List String)
readInput = case !getLine of
"" => pure []
line => pure (line :: !readInput)
IO ()
main =
let input = !readInput
pairs = parse (unlines input)
in do
putStrLn $ "Part 1: " ++ show (part1 pairs)
putStrLn $ "Part 2: " ++ show (part2 pairs)
I especially enjoy the !-notation which acts similar to an inline do-block. It’s syntax sugar that roughly provides (!) : m a -> a. It reminds me of the new ! and ? suffix in Roc. I think it’s a great way to make code more readable and is advantageous over the old backpassing syntax we had before.
That’s all for today. I didn’t want to do much more coding after all that Idris stuff :’)
Dec 01
I did a handful of things today. Not a lot of coding, mostly uni work.
Set the blog up and replaced my old simple placeholder site. I’m using zola with Duckquill which I found very pretty. I stumbled into a fair bit of issues with nothing working in the beginning with a blank zola project, setting some post metas and blog extras did the trick.
Today was mostly writing the technical report for ComRaTT which is a part of a preliminary research project I’m working on with my mate kaep. The project is a compiled functional language that borrows the type system of Async RaTT which our supervisor(s) created. I wrote a couple of typst helper methods to help make the paper a little prettier and consistent. Mostly helper methods like
Typst is such a nice break from LaTeX.
I’ve been holding off working on the correctness proof of a primitive, verified compiler in Idris for a couple of days (not related to above). Hopefully holding back will bring out some ideas to crack the problem once I find time to look at it. Idris is pretty cool! We are basing this work on “functional pearls”
Functional pearls are elegant, instructive examples of functional programming. They are supposed to be fun, and they teach important programming techniques and fundamental design principles [..]
Specifically we’re translating “A type-correct, stack-safe, provably correct, expression compiler in Epigram” into Idris and adding exceptions and let bindings. May show some of that in the coming days.
Rest of the evening will be spent with my lovely wife.