## 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 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
- computer sience
Note that ex-directory lists are not shown. |
## Other listsCond. Mat. seminar SoCS PhD Research Training Sessions Medical Imaging Research Seminars## Other talksTitle tbc Stabilisation of a periodically driven classical spin-chain The increasing complexity of Dark Matter searches in ATLAS Title tbc Symmetry Protected Topological Order in Open Quantum Systems Replica Analysis of the Linear Model with Markov or Hidden Markov Signal Priors |