Induction on lattices

Stream: Is there code for X?

[Alena Gusakov]

Is there some kind of general-purpose induction API for lattices? Is such a thing feasible?

[Mario Carneiro]

what would that mean?

[Alena Gusakov]

Well, I'm only really thinking of this in terms of graph theory right now - maybe if something is true for all subgraphs of a graph, you can use the hypothetical induction on lattices to prove that it must be true for the original graph

[Alena Gusakov]

So I guess it would be sublattices defined by a certain property or something like that

[Mario Carneiro]

Well the generalization of induction is a well founded relation

[Mario Carneiro]

so you need your order to be well founded

[Mario Carneiro]

in the case of subgraphs this is usually easy because the size (is finite and) decreases

[Mario Carneiro]

but in such cases you can usually rephrase it as an induction on the size of the graph instead of a well founded recursion on the lattice of subgraphs

[Bhavik Mehta]

Sometimes you want to induct on the number of edges, and other times on the number of vertices (and sometimes on some combination) but in any case it's still just induction on some natural

[Alena Gusakov]

Right, I guess that makes sense