![]() |
![]() |
Induction for CyclesAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Anupam Das. (Joint work with Jakob von Raumer.) Consider paths in a given graph. If we want to prove a certain property for all paths, the obvious approach is to try induction on [the length of] paths. If we want to prove a certain property for all closed paths a.k.a. cycles (first vertex = last vertex), this does not work since closed paths are not inductively generated (if we remove an edge from a closed path, it is not closed any more). We have studied this situation because certain coherence conditions in homotopy type theory can be formulated in terms of cycles. The problem discussed above then makes it difficult to verify these conditions in the case of natural applications. We build on the observation that, at least in all those cases we are interested in, the graph is given by the symmetric closure of a locally confluent and Noetherian (co-well-founded) proof-relevant relation. Under these assumptions, we construct a new Noetherian relation on cycles which allows co-well-founded induction. As a consequence, whenever we have to prove a property for all cycles, it suffices to prove the property for the empty cycle and for those given by local confluence. An application in homotopy type theory is the statement that the fundamental groups of the free higher group over a set are trivial. This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsType the title of a new list here Condensed Matter Physics Seminars School of Chemistry SeminarsOther talksUltrafast Spectroscopy and Microscopy as probes of Energy Materials Life : it’s out there, but what and why ? Counting cycles in planar graphs TBA Hunt for an Earth-twin Control variates for computing transport coefficients |