## Induction for CyclesAdd 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 Dr 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 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
Note that ex-directory lists are not shown. |
## Other listsTheoretical Physics Journal Club Type the title of a new list here Dinner Table Terrorism - Achieving Food Security## Other talksTitle tbc TBA Title tbc Title tbc Open Problem Workshop Title tbc |