A small exercise on the floor (function)
I’m about to resubmit my functional pearl paper Programming metamorphic algorithms in Agda to the Journal of Functional Programming.
(Edit: I end up publishing the paper in the Art, Science, and Engineering of Programming journal.)
A metamorphism is a fold followed by an unfold, and a typical example is base conversion (for fractions): consuming a list of digits to compute the value it represents by a fold, and then producing a colist of digits that represents the same value in a different base by an unfold.
For instance, to convert $0.625$ in base $10$ to $0.101$ in base $2$, we can use a three-element State type that records the current accumulated value and the weights of the next input and output digits; consuming the decimal digits $6$, $2$, and $5$ updates the states like
$$ (0, 0.1, 0.5) ~\stackrel{6}{\mapsto}~ (0.6, 0.01, 0.5) ~\stackrel{2}{\mapsto}~ (0.62, 0.001, 0.5) ~\stackrel{5}{\mapsto}~ (0.625, 0.0001, 0.5) $$
and then from the last state the binary digits $1$, $0$, and $1$ are produced like
$$ (0.625, 0.0001, 0.5) ~\stackrel{1}{\mapsto}~ (0.125, 0.0001, 0.25) ~\stackrel{0}{\mapsto}~ (0.125, 0.0001, 0.125) ~\stackrel{1}{\mapsto}~ (0, 0.0001, 0.0625) $$
The algebra and coalgebra used above are
alg : State -> Digit -> State
alg (v , wi , wo) d = (v + d × wi , wi / bi , wo)
coalg : State -> Maybe (Digit × State)
coalg (v , wi , wo) = if v > 0 then let e = ⌊ v / wo ⌋; r = v - e × wo
in Just (e , (r , wi , wo / bo))
else Nothing
where bi and bo are the input and output bases ($10$ and $2$ above).
The example is included in the paper to provide some intuition about metamorphisms (but the paper’s focus is on constructing generic metamorphic algorithms in a type-driven development environment).
At the end of Section 5 on the streaming algorithm (where output digits may be produced before all input digits are consumed), there is a claim that by changing the coalgebra to a more conservative one (that has a stronger condition for producing a digit)
coalg' : State -> Maybe (Digit × State)
coalg' (v , wi , wo) = let e = ⌊ v / wo ⌋; r = v - e × wo
in if v > 0 ∧ r + bi × wi ≤ wo
then Just (e , (r , wi , wo / bo))
else Nothing
we can prove that alg and coalg' satisfy a ‘streaming condition’ (that guarantees the correctness of the algorithm).
The proof is omitted from the paper (because it’s beside the point); the key trick is to use the (contrapositive) universal property of the floor function.
The proof is not hard, but not entirely straightforward either, so it seems worthwhile to write up the proof.
(I must have done it casually while the paper was written up but cannot find it anymore.)
This post will be about the proof only, rather than the whole story about metamorphisms, base conversion, streaming etc, which can be found in the paper.
The streaming condition is
$$ \mathsf{coalg'}\ s = \mathsf{Just}\ (e, t) \quad\Rightarrow\quad \mathsf{coalg'}\ (\mathsf{alg}\ s\ d) = \mathsf{Just}\ (e, \mathsf{alg}\ t\ d)$$
Substituting $(v, w_i, w_o)$ for $s$ and expanding the definition of $\mathsf{coalg'}$, we see that the antecedent allows us to assume
\begin{align} & v > 0 \label{eq:assumption-1} \\ & v - \left\lfloor \frac{v}{w_o} \right\rfloor \times w_o + b_i \times w_i \leq w_o \label{eq:assumption-2} \end{align}
and substitute $\lfloor v / w_o \rfloor$ for $e$ and $(v - \lfloor v/w_o \rfloor \times w_o, w_i, w_o/b_o)$ for $t$.
To establish the consequent, first we need to prove that $\mathsf{coalg'}\ (\mathsf{alg}\ s\ d) = \mathsf{coalg'}\ (v + d \times w_i, w_i / b_i, w_o)$ produces a $\mathsf{Just}$-value by checking that the condition of the if expression evaluates to true:
\begin{align} & v + d \times w_i > 0 \label{eq:obligation-3} \\ & v + d \times w_i - \left\lfloor \frac{v + d \times w_i}{w_o} \right\rfloor \times w_o + b_i \times \frac{w_i}{b_i} \leq w_o \label{eq:obligation-4} \end{align}
And then we should check that the digit and state produced are indeed the right-hand side of the equation; the weights obviously match, and the remaining two obligations are
\begin{align} & \left\lfloor \frac{v + d \times w_i}{w_o} \right\rfloor = \left\lfloor \frac{v}{w_o} \right\rfloor \label{eq:obligation-5} \\ & v + d \times w_i - \left\lfloor \frac{v + d \times w_i}{w_o} \right\rfloor \times w_o = v - \left\lfloor \frac{v}{w_o} \right\rfloor \times w_o + d \times w_i \label{eq:obligation-6} \end{align}
Obligation \ref{eq:obligation-3} easily follows from Assumption \ref{eq:assumption-1} since both $d$ and $w_i$ are nonnegative. Among the remaining three obligations, we see that Obligation \ref{eq:obligation-5} is the key: if it holds, then Obligation \ref{eq:obligation-6} obviously holds, and Obligation \ref{eq:obligation-4} is also easily discharged:
\begin{align*} & v + d \times w_i - \left\lfloor \frac{v + d \times w_i}{w_o} \right\rfloor \times w_o + b_i \times \frac{w_i}{b_i} \\ =& \reason{Obligation \ref{eq:obligation-5}; arithmetic} \\ & v - \left\lfloor \frac{v}{w_o} \right\rfloor \times w_o + (d + 1) \times w_i \\ \leq& \reason{$d + 1 \leq b_i$; $w_i$ nonnegative} \\ & v - \left\lfloor \frac{v}{w_o} \right\rfloor \times w_o + b_i \times w_i \\ \leq& \reason{Assumption \ref{eq:assumption-2}} \\ & w_o \end{align*}
So our main task is to establish Obligation \ref{eq:obligation-5}, which is an equation involving the floor function, which computes the greatest integer no larger than its input, and hence satisfies the universal property
$$ z \leq \lfloor q \rfloor \quad\Leftrightarrow\quad z \leq q \qquad\forall z \in \mathbb{Z}, q \in \mathbb{Q} $$
(which, like all other universal properties, actually uniquely defines the floor function). For Obligation \ref{eq:obligation-5}, what we’ll need is the contrapositive version:
$$ z > \lfloor q \rfloor \quad\Leftrightarrow\quad z > q \qquad\forall z \in \mathbb{Z}, q \in \mathbb{Q} $$
Note that the domain restriction on $z$ is very important: we are allowed to add or remove the floor function on one side of an inequation only when the other side is an integer. Since $d \times w_i$ is nonnegative and the floor function is monotonic, we only need to prove
$$ \left\lfloor \frac{v + d \times w_i}{w_o} \right\rfloor \leq \left\lfloor \frac{v}{w_o} \right\rfloor $$
And this can be derived from Assumption \ref{eq:assumption-2}: Moving the middle term on the left-hand side to the right and using the fact $d < b_i$ again, we get
$$ v + d \times w_i < v + b_i \times w_i \leq \left(\left\lfloor \frac{v}{w_o} \right\rfloor + 1\right) \times w_o $$
Dividing both sides by $w_o$ (which is nonnegative and hence the direction of the inequation does not change), we get
$$ \frac{v + d \times w_i}{w_o} < \left\lfloor \frac{v}{w_o} \right\rfloor + 1 $$
The right-hand side is obviously an integer, so we’re entitled to put in the floor function:
$$ \left\lfloor \frac{v + d \times w_i}{w_o} \right\rfloor < \left\lfloor \frac{v}{w_o} \right\rfloor + 1 $$
This is an inequation on integers, and hence equivalent to what we need to prove.
One question I’d love to ask is whether we can explain this proof intuitively (in particular, why we should use the universal property in this way), but I’ll leave the pondering to another time and get back to working on the paper.
