A Coalgebraic View of Bar Recursion and Bar Induction
| Autor: | Tarmo Uustalu, Venanzio Capretta |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Initial algebra
Discrete mathematics Pure mathematics Recursion Bar (music) 010102 general mathematics Bar induction 0102 computer and information sciences 01 natural sciences Constructive Mutual recursion 010201 computation theory & mathematics Computer Science::Logic in Computer Science Structural induction 0101 mathematics Axiom Mathematics |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783662496299 FoSSaCS |
| Popis: | We reformulate the bar recursion and induction principles in terms of recursive and wellfounded coalgebras. Bar induction was originally proposed by Brouwer as an axiom to recover certain classically valid theorems in a constructive setting. It is a form of induction on non-wellfounded trees satisfying certain properties. Bar recursion, introduced later by Spector, is the corresponding function definition principle. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|