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 nonwellfounded trees satisfying certain properties. Bar recursion, introduced later by Spector, is the corresponding function definition 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 definition 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 Patti...

• Type: Journal
• Year: 2016
• Where: FOSSACS
• Authors: Venanzio Capretta, Tarmo Uustalu
• Keywords: FOSSACS 2016, Software Engineering