= Bar recursion
{wiki=Bar_recursion}
Bar recursion is a form of recursion used primarily in the context of constructive mathematics and type theory. It generalizes the notion of recursion, allowing for the definition of functions that are not necessarily computable in the traditional sense, but are still well-defined in a constructive framework. The concept of bar recursion was introduced by the mathematician and logician Per Martin-Löf. It can be seen as a method to define functions by using infinite sequences (or "bars") that represent computations.
Back to article page