Day 14

Part 1

Each pair of elements in the input polymer sequence gives rise to a new element which is inserted in the middle of the pair. Given a function step which computes a single step of pair insertion, I can specify a function to compute any number of steps as follows:

steps : ℕ → [Element] → [Element]
steps n = iter n step

Here’s an approach to computing a single step of insertion: from the input list, compute the list of bases to be inserted, then interleave the lists. If I assume that every pair matches some insertion rule, then an input k-list will generate a (k - 1)-list of new elements.

I can specify this as follows:

step : [Element] → [Element]
step es = let ins = list pair_insert (pairs es) in
            interleave es ins

interleave : [α] → [α] → [α]
interleave as       []       = as
interleave []       bs       = bs
interleave (a : as) (b : bs) = a : b : interleave as bs

pairs : [α] → [[α]]
pairs xs = zipWith pair_list xs (tail xs)

pair_list : α → α → [α]
pair_list a b = [a, b]

For convenience, I’m using fixed-length lists of elements instead of tuples. Note that interleave is very nearly the same as zipWith pair_list, except that it appends the remaining tail of a longer list.

pair_insert is the core of this transformation; it takes a pair of elements to the list of new elements they generate:

pair_insert : [Element] → Element
pair_insert p = lookup p rules

where rules is a table of insertion rules described as a mapping [Element] → Element.

Now, it should be possible to fuse the components of step to (1) eliminate the intermediate list ins and (2) produce the result with only a single traversal of the input list.

I’ll do this by inductive synthesis on step, calculating a new, recursive implementation of the function.

The case step [] quickly simplifies to []. The singleton list case is also “degenerate” and follows directly from the definitions of interleave and zipWith:

  step [e]

= { step.1 }

  let ins = list pair_insert (pairs [e]) in
    interleave [e] ins

= { pairs def., zipWith (x ∷ xs) [] = [] }

  let ins = list pair_insert [] in
    interleave [e] ins

= { list, replace ins with its value }

  interleave [e] []

= { interleave.1 }


The recursive case handles lists of length two or greater, and it’s obviously the interesting one. First, I’ll remove the let binding, which might make the final steps of the calculation a little easier to understand.

  step (e₁ ∷ e₂ ∷ es)

= { step.1 }

  let ins = list pair_insert (pairs (e₁ ∷ e₂ ∷ es)) in
    interleave (e₁ ∷ e₂ ∷ es) ins

= { replace ins with its value }

  interleave (e₁ ∷ e₂ ∷ es)
    (list pair_insert (pairs (e₁ ∷ e₂ ∷ es)))

= { pairs.1, zipWith def. }

  interleave (e₁ ∷ e₂ ∷ es)
    (list pair_insert ([e₁, e₂] ∷ pairs (e₂ ∷ es)))

= { list }

  interleave (e₁ ∷ e₂ ∷ es)
             (pair_insert [e₁, e₂]) ∷
               (list pair_insert (pairs (e₂ ∷ es)))

= { interleave.3 }

  e₁ ∷ (pair_insert [e₁, e₂]) ∷
    interleave (e₂ ∷ es) (list pair_insert (pairs (e₂ ∷ es)))

= { step def. }

  e₁ ∷ (pair_insert [e₁, e₂]) ∷ (step (e₂ ∷ es))

which is a recursive equation whose only external dependency is pair_insert. In sum, I’ve calculated:

step []             = []
step [e]            = [e]
step (e₁ ∷ e₂ ∷ es) = e₁ ∷ (pair_insert [e₁, e₂]) ∷ (step (e₂ ∷ es))

This completes the synthesis of step.

All that remains now is to find the “magic number” for part 1: here, it’s the difference of the number of occurrences of the most and least common elements of the sequence after performing ten steps of insertion. This is not very interesting, so I’ve left it to the Haskell source file, where it’s implemented in terms of a few functions from the Data.List library.

Executable Haskell solution

Haskellized test puzzle input

AOC 2021 Index