greedy constructions

Stream: Is there code for X?

[Mario Carneiro]

I've been thinking about this pattern of "greedy constructions" that show up in the Equational Theories project, and it seems like something where mathlib will have a general version but I'm coming up empty. Here's my characterization of the pattern:

• You have a partial order of states
• There are some tasks you want to accomplish. For every task and every state, there exists some later state which solves the task, and every state thereafter will have solved that particular task
• If $\kappa$ is the number of tasks, then every chain of length less than $\kappa$ has an upper bound.

Then, there exists a chain of length $\kappa$ on which every task has been solved.

This looks very much like Zorn's lemma as stated, but I'm not sure how to get the cardinality bounds. Example uses:

• $\kappa=\omega$ and we are constructing a function while avoiding countably many obstructions. At each stage we have a finite approximation and so we can avoid any particular obstruction, and by resolving each obstruction in a fair manner (even if solving obstructions creates new obstructions), eventually we will have pointwise solved every obstruction.
• The proof that every countable dense linear order $D$ without endpoints is order-isomorphic to $\mathbb{Q}$ has this structure (again with $\kappa=\omega$). You build up a partial bijection point by point and the "tasks" are to make sure each element of $\mathbb{Q}$ and each element of $D$ is covered.
• There are also examples with uncountable $\kappa$, but these are less common. I think you can do the well ordering principle and some kind of forcing constructions using this method.

[Mario Carneiro]

It also looks a lot like Kőnig's lemma, but Kőnig's lemma lacks the "fairness" element that is required by this kind of construction, it just lets you take any infinite path, meaning that you may have solved infinitely many tasks without solving all of them.

[Yaël Dillies]

It feels a lot like a back and forth argument, in the sense that you assign a "deadline " to each task after which you will have solved it

[Shreyas Srinivas]

Something stronger than filters?

[Shreyas Srinivas]

Are you looking for a general tactic or a math concept or an algorithm?

[Shreyas Srinivas]

Or maybe coussot's abstract interpretation?

[Yaël Dillies]

@Sky Wilshaw might have ideas

[Mario Carneiro]

Shreyas Srinivas said:

Are you looking for a general tactic or a math concept or an algorithm?

This is a theorem

[Mario Carneiro]

but if it exists in the literature that will make it easier to find in mathlib if it exists and name if it doesn't

[Kyle Miller]

This is something the too-general docs#nonempty_sections_of_finite_cofiltered_system can be useful for. More specific is docs#nonempty_sections_of_finite_inverse_system, which is used by Hall's theorem (docs#Finset.all_card_le_biUnion_card_iff_exists_injective) and a graph homomorphism extension theorem (docs#nonempty_hom_of_forall_finite_subgraph_hom) to turn finite extensibility into a solution on the full type.

The second one is easier to explain in terms of colorings. Suppose we've proved the 4-color theorem for finite planar graphs. Then, for a particular (infinite) planar graph G, we create an inverse system indexed by finite subgraphs of G, where the type for a given finite subgraph consist of the all the 4-colorings of it. This is an inverse system because we can always restrict colorings to smaller subgraphs. Each of the types are finite and nonempty, so nonempty_hom_of_forall_finite_subgraph_hom applies. From this section, we can read off a global solution.

Choosing a color for a vertex is a kind of task, and what I think is interesting about this example is that we don't require every coloring to be able to make forward progress — you might make a tragic choice of vertex color at some point that leads to contradiction only thousands of choices later — an interpretation of the nonemptiness hypotheses is that you could have made a good choice. If you do have a forward progress result that makes nonemptiness of each type in the inverse system all the easier.

[Kyle Miller]

(These are category-theoretic formulations of the compactness theorem by the way.)

[Mario Carneiro]

Kyle Miller said:

Choosing a color for a vertex is a kind of task, and what I think is interesting about this example is that we don't require every coloring to be able to make forward progress — you might make a tragic choice of vertex color at some point that leads to contradiction only thousands of choices later — an interpretation of the nonemptiness hypotheses is that you could have made a good choice. If you do have a forward progress result that makes nonemptiness of each type in the inverse system all the easier.

How would you express this requirement in the partial order language I used? I agree that something like this might be important, in particular in many of the examples the set of tasks isn't really fixed but depend on the current approximation - but you can at least upper bound the set of tasks by $\kappa$ so it should still work, where if a task is not applicable then we just skip it on that step.

[Kyle Miller]

(One more note: these are proved with docs#TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system, which is formulated using nonempty compact T2 spaces, which I think is kind of nice since 'compactness' shows up more directly in this compactness theorem.)

[Mario Carneiro]

I'm also interested in using this as a "workhorse theorem" so it should be relatively straightforward to apply in areas which don't have any of the above floating around. You quite often need to custom build a partial order or what have you on the spot to apply these theorems because they are really tuned for the application and are not general structure

[Mario Carneiro]

I'm guessing that an explicitly category theoretic statement will not meet these requirements because constructing a category on the spot is a chore

[Kyle Miller]

Mario Carneiro said:

How would you express this requirement in the partial order language I used?

To use the Konig-like theorems I mentioned, it seems important that the type of states can be indexed by a partial order I, and for any given term of I the collection of states with that index are finite. There are counterexamples when you relax this finiteness

[Mario Carneiro]

exactly, that's what caused me issues when applying Zorn's lemma because it wants to talk about a maximal element but the thing I'm going for isn't going to be finite even if it is a limit of finite approximations

[Kyle Miller]

And yeah, using these theorems, even nonempty_sections_of_finite_inverse_system, is a chore. You can look at the couple applications I linked to to see. There's universe level juggling, but also the final assembly of the global solution, not to mention creating the functor for the inverse system.

[Mario Carneiro]

constructing a partial order is also a chore, I would like to have a version specialized for the case where the partial order is the set of partial functions satisfying a property (and the maximal element is a total function), because almost all examples fit in that form

[Mario Carneiro]

the way I framed it above has the finiteness baked in to the type of "states", so the final result is not actually a state but more of a coherent diagram on the states for which you might be able to take a limit in a larger space

[Edward van de Meent]

Mario Carneiro said:

I would like to have a version specialized for the case where the partial order is the set of partial functions satisfying a property

i think i wrote something along these lines some time ago... let me see if i can find it...

[Edward van de Meent]

here

[Edward van de Meent]

this is code for proving that for any property P of a sequence a->b that you can check at some index a (i.e. P:(a->b) -> a -> Prop), if a is wellfounded, you can use that wellfoundedness as a framework to define a sequence which will have said property for all a

[Edward van de Meent]

in this case, i guess the property would be "all tasks <= n have been completed at step n"

[Terence Tao]

Perhaps the correct abstract framework is a state space Ω and a task space T: Set ( Set Ω ), and to have the following two (easy) results:

1. Compactness theorem: if the state space is a compact space, the tasks are all closed, and every finite set F: Finset T of tasks is satisfiable by at least one state, then the entire set of tasks is satisfiable by a single state.
2. Greedy algorithm: if the state space is partially ordered and non-empty, and the tasks are all downwardly closed and cofinal, then every finite set of tasks is satisfiable by at least one state.

Of course, these combine to give

Infinite Greedy algorithm: If the state space is compact, partially ordered and non-empty, and the tasks are all topologically closed, downwardly closed, and cofinal, then there is a state that satisfies all the tasks.

[Mario Carneiro]

Is your state space including the infinite solutions? In (1) it seems like it has to be, but in (2) we need to know we are not already in an infinite state in order to argue that there is a way to solve a given task

[Terence Tao]

Ah, good point. In applications one needs to apply the greedy algorithm to a subset of the full state space. So, um, the corollary looks more like this:

Infinite Greedy algorithm (revised): If the state space is compact, there is a subset of the state space which is partially ordered and non-empty, the tasks are all topologically closed in the full state space and downwardly closed and cofinal in the subset of the state space, then there is a state (in the full state space) that satisfies all the tasks.

[Shreyas Srinivas]

Are these structures that are being described something like infinite variants of greedoids or matroids? (Every time I read your initial statement, I get a different structure in my mind, so I am trying to understand what your structure would mean in an algorithmic sense)

[Terence Tao]

I retract my proposal. In many contexts (particularly ones where there are an infinite number of available choices at each step), one does not in fact have compactness, and this approach is not suitable. I now think one should not use any topological notions and only proceed through order theory. Something like:

Infinite Greedy algorithm (third proposal): If one has a partially ordered state space, with every chain having an upper bound, all tasks upwardly closed, and within a non-empty subset of the state space, all tasks are cofinal, then there is a state that obeys all the tasks.

[One may need to strengthen "every chain has an upper bound" to "every directed set has an upper bound". I thought Zorn's lemma meant the two were equivalent, but actually I can't see this right now. EDIT: They are equivalent, though nontrivially so, see https://mathoverflow.net/questions/378004/suprema-of-directed-sets]

As an example, states might be partial functions obeying some rules, and each task verifies that some functional equation is well defined and satisfied for such a partial function. The greedy part is in verifying the cofinality, that every task can be achieved by extending the partial function suitably, if the partial function is "small" (e.g., only defined on a finite set).