natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In combinatory logic, in the ∞-calculus?, or more generally in type theory, a looping combinator is closely akin to a fixed-point combinator, but rather than producing a true fixed point, it produces a sequence of points each of which is the image of the next.
A term is a looping combinator if for any function term to which can be applied, we have a beta reduction
where is a looping combinator.
This is a coinductive definition. Unraveled explicitly, it means that a looping combinator comes with a sequence of combinators for and reductions
A looping combinator is essentially just as good as a fixed-point combinator for implementing general recursion. See the discussion there for details.
Per Martin-Löf‘s original dependent type theory, which had the additional rule , was shown to be inconsistent by Girard's paradox. In the 1980’s, Meyer, Reinhold, and Howe (see references) showed that this paradox could be modified to construct a looping combinator.
In the short paper
it was claimed that from Girard’s paradox one could actually construct a fixed-point combinator. The proof turned out to be flawed, but it was sufficient to produce a looping combinator. Details can be found in
Mark Reinhold, “Typechecking is Undecidable When ‘Type’ is a Type”, 1989, citeseer
Douglas Howe, “The Computational Behaviour of Girard’s Paradox”, Cornell University Technical Report, 1987, link.
Further analysis is in
Last revised on January 28, 2023 at 15:44:18. See the history of this page for a list of all contributions to it.