Zulip Chat Archive

Stream: Is there code for X?

Topic: Induction on lattices


view this post on Zulip Alena Gusakov (Dec 12 2020 at 22:03):

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

view this post on Zulip Mario Carneiro (Dec 12 2020 at 22:03):

what would that mean?

view this post on Zulip Alena Gusakov (Dec 12 2020 at 22:04):

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

view this post on Zulip Alena Gusakov (Dec 12 2020 at 22:05):

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

view this post on Zulip Mario Carneiro (Dec 12 2020 at 22:05):

Well the generalization of induction is a well founded relation

view this post on Zulip Mario Carneiro (Dec 12 2020 at 22:06):

so you need your order to be well founded

view this post on Zulip Mario Carneiro (Dec 12 2020 at 22:06):

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

view this post on Zulip Mario Carneiro (Dec 12 2020 at 22:07):

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

view this post on Zulip Bhavik Mehta (Dec 12 2020 at 22:17):

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

view this post on Zulip Alena Gusakov (Dec 12 2020 at 22:19):

Right, I guess that makes sense


Last updated: May 16 2021 at 05:21 UTC