Partial Greedy Theorem

The partial greedy theorem can help derive greedy algorithms whose input is constrained in some way. The theorem is actually quite restricted since the feasible solutions must be lists of the same type. Generalisation is possible, but the original purpose of its development has disappeared. Now this post exists only for historical reasons.

First we need to extend the usual monotonicity to a weaker one (which is why one would need a different greedy theorem). (The inclusion is not a proper one; somehow the line denoting equality is truncated.)

For our purpose, C is taken to be coreflexive. We need another concept that ensures the restriction on the input is propagated through the folding process.

The inclusion becomes equality if C is coreflexive. Now we have our theorem:

The proof consists of two parts. The first part establishes that cata (min R . ΛS . C) ⊆ min R . Λ(cata S), which in essence is the proof of the original greedy theorem.

The second part refines cata (min R . ΛS . C) to cata (min R . ΛS) . cata (α . C) (i.e., the former includes the latter) by fold fusion. The fusion condition is:

Oops, my first proof of the claim is not right. But it looks good pointwisely. Of course, we need to prove the claim in order to establish the theorem's validity.

--
But I won't continue unless the theorem looks useful again...