Suppose I've got some region of space I want to make an aesthetically pleasing outline of, call it A:
Then the first thing I can do is find the interior of that region, in the sense of doing a simple convolution filter on it so every white pixel "infects" every orthogonally adjacent pixel.
Call this □A since a pixel stays black ("true") if and only if every adjacent (accessible) pixel is black.
Now we can consider the symmetric difference of this with the original, and we do get kind of an outline:
(linear logic fans, note carefully that ⊕ is meant here as "classical exclusive or" not "linear logic or")
But it's got these ugly sharp corners:
I thought, hm, probably if I do the dual convolution (i.e. each black pixel expands into a cross of black pixels) after the original (each white pixel expands into a cross of white pixels) the result should probably be a smoothed version of the original shape:
So what actually happened is I got to this point without thinking about modal logic, and wondered if I needed to do this smoothing operation repeatedly, or if it was idempotent. But then the modal interpretation occurred to me, and I realized it reduced to asking whether
But of course this is true in any kripke model with a symmetric accessibility relation, which the pixel grid with accessibility relation being adjacency certainly is. Directly from accessibility reasoning you get B ⊦ □◇B and ◇□A ⊦ A, and by substituting □A for B and hitting the second entailment on both sides with □ you get □A ⊦ □◇□A and □◇□A ⊦ □A.
So I only need to smooth once, and smoothing and finding the boundary simplifies to:
which is a nice smooth pixelly outline with no sharp corners.