Content deleted Content added
m Added 1 doi to a journal cite using AWB (10216) |
|||
Line 1:
In [[intuitionistic type theory]] (ITT), a discipline within [[mathematical logic]], '''induction-recursion''' is a feature for simultaneously declaring a type and function on that type. It allows the creation of larger types, such as universes, than [[Intuitionistic_type_theory#Inductive_types|inductive types]]. The types created still remain [[Predicativity|predicative]] inside ITT.
An [[inductive definition]] is given by rules for generating elements of a type. One can then define functions from that type by induction on the way the elements of the type are generated. Induction-recursion generalizes this situation since one can ''simultaneously'' define the type and the function, because the rules for generating elements of the type are allowed to refer to the function.<ref name=Dybjer>{{cite journal|last=Dybjer|first=Peter|title=A general formulation of simultaneous inductive-recursive definitions in type theory|journal=Journal of Symbolic Logic|volume=65|issue=2|date=June 2000|pages=525–549|url=http://www.cse.chalmers.se/~peterd/papers/Inductive_Recursive.pdf|doi=10.2307/2586554}}</ref>
Induction-recursion can be used to define large types including various universe constructions. It increases the proof-theoretic strength of type theory substantially. Nevertheless, inductive-recursive recursive definitions are still considered [[Impredicativity|predicative]].
| |||