A coalgebraic view of bar recursion and bar induction
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 tr...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Springer
2016
|
| Online Access: | https://eprints.nottingham.ac.uk/33872/ |
| _version_ | 1848794725041045504 |
|---|---|
| author | Capretta, Venanzio Uustalu, Tarmo |
| author_facet | Capretta, Venanzio Uustalu, Tarmo |
| author_sort | Capretta, Venanzio |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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 defnition principle.
We give a generalization of these principles, by introducing the notion of barred coalgebra: a process with a branching behaviour given by a functor, such that all possible computations terminate.
Coalgebraic bar recursion is the statement that every barred coalgebra is recursive; a recursive coalgebra is one that allows defnition of functions by a coalgebra-to-algebra morphism. It is a framework to characterize valid forms of recursion for terminating functional programs. One application of the principle is the tabulation of continuous functions: Ghani, Hancock and Pattinson defned a type of wellfounded trees that represent continuous functions on streams. Bar recursion allows us to prove that every stably continuous function can be tabulated to such a tree where by stability we mean that the modulus of continuity is also continuous.
Coalgebraic bar induction states that every barred coalgebra is well-founded; a wellfounded coalgebra is one that admits proof by induction. |
| first_indexed | 2025-11-14T19:20:45Z |
| format | Article |
| id | nottingham-33872 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T19:20:45Z |
| publishDate | 2016 |
| publisher | Springer |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-338722020-05-08T12:30:18Z https://eprints.nottingham.ac.uk/33872/ A coalgebraic view of bar recursion and bar induction Capretta, Venanzio Uustalu, Tarmo 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 defnition principle. We give a generalization of these principles, by introducing the notion of barred coalgebra: a process with a branching behaviour given by a functor, such that all possible computations terminate. Coalgebraic bar recursion is the statement that every barred coalgebra is recursive; a recursive coalgebra is one that allows defnition of functions by a coalgebra-to-algebra morphism. It is a framework to characterize valid forms of recursion for terminating functional programs. One application of the principle is the tabulation of continuous functions: Ghani, Hancock and Pattinson defned a type of wellfounded trees that represent continuous functions on streams. Bar recursion allows us to prove that every stably continuous function can be tabulated to such a tree where by stability we mean that the modulus of continuity is also continuous. Coalgebraic bar induction states that every barred coalgebra is well-founded; a wellfounded coalgebra is one that admits proof by induction. Springer 2016-03-22 Article PeerReviewed application/pdf en https://eprints.nottingham.ac.uk/33872/1/Barred_Coalgebras_FOSSACS2016.pdf Capretta, Venanzio and Uustalu, Tarmo (2016) A coalgebraic view of bar recursion and bar induction. Lecture Notes in Computer Science, 9634 . pp. 91-106. ISSN 0302-9743 http://link.springer.com/chapter/10.1007/978-3-662-49630-5_6 doi:10.1007/978-3-662-49630-5_6 doi:10.1007/978-3-662-49630-5_6 |
| spellingShingle | Capretta, Venanzio Uustalu, Tarmo A coalgebraic view of bar recursion and bar induction |
| title | A coalgebraic view of bar recursion and bar induction |
| title_full | A coalgebraic view of bar recursion and bar induction |
| title_fullStr | A coalgebraic view of bar recursion and bar induction |
| title_full_unstemmed | A coalgebraic view of bar recursion and bar induction |
| title_short | A coalgebraic view of bar recursion and bar induction |
| title_sort | coalgebraic view of bar recursion and bar induction |
| url | https://eprints.nottingham.ac.uk/33872/ https://eprints.nottingham.ac.uk/33872/ https://eprints.nottingham.ac.uk/33872/ |