This one involves literal folding! Given a 2D grid (yet again) with a set of marked coordinates, I want to fold it along a given row or column. Since the grid is “transparent”, the marks on each side of the “crease” will “show through”, giving a new set of marked coordinates (on a smaller grid). The first part of this puzzle is to find the number of marks on the grid after a single fold–the first one given in the puzzle input.
I’ll once again use a grid type, this time with boolean entries indicating whether a given coordinate is marked.
for S ⊆ (ℕ × ℕ),
Grid Bool ≅ S → Bool
hbounds : Grid α → (ℕ × ℕ)
Coordinates are column-major and (0, 0) is the top left entry. Grids can be of all sizes. hbounds g gives the maximum column and row indices for g.
Now I have to think about what it means to fold a Grid onto itself. For simplicity, I’ll write separate transformations for row and column folds. To avoid confusion, I’m going to call these crease operations.
crease_row : ℕ → Grid Bool → Grid Bool
crease_col : ℕ → Grid Bool → Grid Bool
crease_row r g can be thought of as being composed of three steps:
first, split the grid g into two grids on row r, second, “flip
over” one of the segments, and third, overlay them. Here’s the
specification (; is right-to-left composition):
-- Specification
crease_row : ℕ → Grid Bool → Grid Bool
crease_row k = split_row k ; orient_v ; overlay
split_row : ℕ → Grid α → (Grid α × Grid α)
orient_v : (Grid α × Grid α) → (Grid α × Grid α)
overlay : (Grid Bool × Grid Bool) → Grid Bool
These functions will mostly be described abstractly, in terms of how they map indices to elements. This is enough to calculate with.
The sum of the number of rows of the two grids returned by split_row will always be smaller than the row-size of the original.
Define
nrows : Grid α → ℕ
nrows g = let (_, r) = hbounds g in r + 1
Then
(g′, g″) := split_row g
nrows g′ + nrows g″ < nrows g
where nrows : Grid α → ℕ gives the number of rows of a grid. I’ll go further and postulate:
nrows g = nrows g′ + nrows g″ + 1
That is, split_row always divides a grid equally along its central row. This is a big simplification; maybe it only works for the example puzzle. [EDIT: Yes, it holds in general. Each crease instruction bisects a grid.]
The horizontal dimension is preserved by split_row:
ncols g′ = ncols g″ = ncols g
where
ncols g = let (c, _) = hbounds g in c + 1
Here’s the crucial property of split_row k g, which I’m thinking of here as a map T ⊆ ((ℕ × ℕ) × (ℕ × ℕ)) → Bool × Bool:
(split_row k g) ! ((i, j), (p, r))
⎧ ⊥, if j ≡ k ∨ r ≡ k -- cut out the kth row
= ⎨
⎩ (g ! (i, j), g ! (p, r + k + 1)), otherwise
This is complicated a bit by the “cutting out” of the kth row.
! denotes the index operation Grid α → (ℕ × ℕ) → α.
A similar property describes split_col:
(split_col k g) ! ((i, j), (p, r))
⎧ ⊥, if i ≡ k ∨ p ≡ k -- cut out the kth column
= ⎨
⎩ (g ! (i, j), g ! (p + k + 1, r)), otherwise
I don’t really want to define (!) on products of Grids; this is just a compact way to describe how these functions transform their arguments.
overlay is really the core of the function. What are its properties? Again, I assume for simplicity that I can only overlay grids of the same size. The crucial idea of “transparency” is captured by the following property of overlay:
(overlay (g₁, g₂)) ! (i, j) = g₁ ! (i, j) ∨ g₂ ! (i, j)
In other words, a place in the grid overlay (g₁, g₂)) is marked iff it is marked in g₁ or g₂. This is pretty much all the meaning I need to work with overlay.
The puzzle promises not to put marks on the row/column of folding, which eliminates some weird corner cases. It also explains how to overlay the two grid sections in each case: when folding vertically (on rows), I’m to fold the bottom section up, and, when folding horizontally (on columns), I’m to fold the left section over.
This is not actually a matter for overlay, but for the orient functions.
orient_v (gt, gb) = (gt, vflip gb)
orient_h (gl, gr) = (hflip gl, gr)
where vflip and hflip perform vertical and horizontal flips of a grid, respectively:
(vflip g) ! (i, j) = let rmax = π₂ (hbounds g) in
g ! (i, rmax - j)
(hflip g) ! (i, j) = let cmax = π₁ (hbounds g) in
g ! (cmax - i, j)
where row_max g and col_max g give the greatest row/column indices of g, respectively.
I have a specification for the crease functions, but it involves creating intermediate values (the two halves of the split input grid) only to compute the value I’m actually interested in. It should be possible to calculate more efficient implementations.
crease_row = split_row ; orient_v ; overlay
Thinking of grids as functions, what is the relationship between the functions g and crease_row k g? Clearly the domain of the latter is a smaller subset of ℕ × ℕ. Call it S; for (i, j) ∈ S, I can calculate:
(crease_row k g) (i, j)
= { crease_row spec. }
(overlay (orient_v (split_row k g))) (i, j)
= { overlay property }
let (g₁, g₂) = orient_v (split_row k g) in
g₁ ! (i, j) ∨ g₂ ! (i, j)
= { orient_v def. }
let (g₁, g₂) = split_row k g in
g₁ ! (i, j) ∨ (vflip g₂) ! (i, j)
= { vflip spec. }
let (g₁, g₂) = split_row k g
rmax = π₂ (hbounds g₂) in
g₁ ! (i, j) ∨ g₂ ! (i, rmax - j)
This eliminates all of the intermediate stuff except for split_row, so I’m almost at the point where I can compute crease_row k g in terms of g alone. With slight informality, I now use the defining property of split_row:
= { split_row property }
let (g₁, g₂) = split_row k g
rmax = π₂ (hbounds g₂) in
g₁ ! (i, j) ∨ g₂ ! (i, (rmax - j) + k + 1)
To eliminate split_row, I have to calculate rmax without reference to g₂. This is easy, by the transforming the postulate stated above for split_row:
nrows g₂ = nrows g - nrows g₁ - 1
≡ { nrows g₁ = k }
nrows g₂ = nrows g - k - 1
Then:
π₂ (hbounds g₂) = (nrows g₂) - 1
= (nrows g - k - 1) -1
= nrows g - k - 2
= (π₂ (hbounds g)) - k - 1
No more split_row:
(crease_row k g) (i, j) =
let rmax = (π₂ (hbounds g)) - k - 1 in
g ! (i, j) ∨ g ! (i, (rmax - j) + k + 1)
Arithmetic further simplifies this:
(crease_row k g) (i, j) = g ! (i, j) ∨ g ! (i, (π₂ (hbounds g)) - j)
In data terms, this is sufficient to compute the result of crease_row k g without building any intermediate results. Assume there’s a grid constructor (modelled on array from the Data.Array Haskell library) that takes a pair of bounds and a list of ((ℕ × ℕ) × Bool) pairs to a new grid. Then:
crease_row k g =
let (c, r) = hbounds g
rmax = r - k - 1 in
grid ((0, 0), (c, rmax))
[ ((i, j), g ! (i, j) ∨ g ! (i, r - j)) |
i ← [0..c], j ← [0..rmax] ]
This completes the calculation of a more space-efficient crease_row. An analogous calculation (left as an exercise for the reader) can be used to compute crease_col, which is similar:
crease_col k g =
let (_, r) = hbounds g
cmax = k - 1 in
grid ((0, 0), (cmax, r))
[ ((i, j), g ! (cmax - i, j) ∨ g ! (i + k + 1, j)) |
i ← [0..cmax], ← <- [0..r] ]
Assume the grid section of the puzzle input has already been parsed and converted into a Grid Bool, and let the folding instructions be described by a list:
data Inst = X ℕ | Y ℕ
[Y 7, X 5, …]
This is easy enough to construct from the puzzle input. Then it’s just a matter of folding the folds. To get the solution for part 1, I only need to count the number of marks visible after the first crease. Here’s a more general function which can be used for part 2, as well:
creases : Grid Bool → [Inst] → Grid Bool
creases = fold (λ g c →
case c of
X k → crease_col k g
Y k → crease_row k g)
solution = marked (creases init (take 1 insts))
marked : Grid Bool → ℕ
marked = count id
Here, init is the starting grid and insts is the list of fold instructions, both constructed from the puzzle input.
I have to complete the folding, now, and read the digits off the final grid. Pretty much everything is in place to do this, except for functions to print a grid in a readable form. (No, I’m not going to write an OCR function!) This isn’t very interesting, but here it is, for completeness:
print_row :: Grid -> Int -> IO ()
print_row g r = sequence_
(map putStr
(map (\c → if g ! (c, r) then "#" else ".")
[0 .. (fst (hbounds g))])
⧺ [putChar '\n'])
print_grid :: Grid -> IO ()
print_grid g = sequence_ (map (print_row g)
[0 .. (snd (hbounds g))])
These functions use the (pseudo-)monadic structure of Haskell’s
IO type. If this is unfamiliar, take a look at the built-in function
sequence_
and maybe Chapter 12 of Graham Hutton’s Programming in Haskell.