Induction for Cycles

Add to your list(s) Download to your calendar using vCal

• Nicolai Kraus (University of Birmingham)
• Friday 31 January 2020, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

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:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.