## 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 listsArtificial Intelligence and Natural Computation seminars Astrophysics Seminars Condensed Matter Group Meetings## Other talksModelling nanoplasmonic hot carrier generation Medical Image Analysis with Data-efficient Learning Rigidity of symmetry-forced frameworks Uniqueness of the phase transition in many-dipole cavity QED systems Haptic human-robot communication Non-stationary quantum many-body dynamics |