Induction-recursion: Difference between revisions

Revision as of 16:42, 1 August 2013

Latest revision as of 16:02, 10 June 2025

(31 intermediate revisions by 19 users not shown)

Line 1:

{{Short description|Concept in mathematical logic}}

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, suchthan as[[Intuitionistic universestype theory#Inductive types|inductive types]], thansuch as [[Intuitionistic_type_theoryIntuitionistic type theory#Inductive_types|inductiveUniverse types|universes]]. 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|monthdate=June|year= 2000|pages=525–549|url=http://www.cse.chalmers.se/~peterd/papers/Inductive_Recursive.pdf|doi=10.2307/2586554|jstor=2586554|citeseerx=10.1.1.6.4575|s2cid=18271311 }}</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]].

===Background===

Induction-Recursion came out of investigations to the rules of Martin-Löf's [[intuitionistic type theory]]. The type theory has a number of "type formers" and 4 kinds rules for each one. Martin-Löf had hinted that the rules for each type former followed a pattern, which preserved the properties of the type theory (e.g., [[Normalization property (abstract rewriting)|strong normalization]], [[Impredicativity|predicativity]]). Researchers started looking for the most general description of the pattern, since that would tell what kinds of type formers could be added (or not added!) to extend the type theory.

Induction-Recursionrecursion came out of investigations tointo the rules of Martin-Löf's [[intuitionistic type theory]]. The type theory has a number of "type formers" and 4four kinds of rules for each one. Martin-Löf had hinted that the rules for each type former followed a pattern, which preserved the properties of the type theory (e.g., [[Normalization property (abstract rewriting)|strong normalization]], [[Impredicativity|predicativity]]). Researchers started looking for the most general description of the pattern, since that would tell what kinds of type formers could be added (or not added!) to extend the type theory.

The "universe" type former was the most interesting, because when the rules were written "ala Tarski", they simultaneously defined the "universe type" ''and ''a function that operated on it. This eventually lead Dybjer to Induction-Recursion.

The "universe" type former was the most interesting, because when the rules were written "alaà la Tarski", they simultaneously defined the "universe type" ''and '' a function that operated on it. This eventually lead Dybjer to Inductioninduction-Recursionrecursion.

Dybjer's initial papers called Induction-Recursion a "schema" for rules. It stated what type formers could be added to the type theory. Later, he and Setzer would write a new type former with rules that allowed new Induction-Recursion definitions to be made inside the type theory.<ref name=DybjerSetzer>{{cite journal|last=Dybjer|first=Peter|title=A finite axiomatization of inductive-recursive definitions|journal=Lecture Notes in Computer Science|volume=1581|year=1999|url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.219.2442}}</ref> This was added to the Half proof assistant (a variant of [[ALF (proof assistant)|Alf]]).

Dybjer's initial papers called Inductioninduction-Recursionrecursion a "schema" for rules. It stated what type formers could be added to the type theory. Later, he and Setzer would write a new type former with rules that allowed new Inductioninductive-Recursionrecursive definitions to be made inside the type theory.<ref name=DybjerSetzer>{{cite journalbook|last=Dybjer|first=Peter|titlechapter=A finiteFinite axiomatizationAxiomatization of inductiveInductive-recursiveRecursive Definitions definitions|journalseries=Lecture Notes in Computer Science |title=Typed Lambda Calculi and Applications |volume=1581|pages=129–146|year=1999|url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.219.2442|doi=10.1007/3-540-48959-2_11|isbn=978-3-540-65763-7}}</ref> This was added to the Half [[proof assistant]] (a variant of [[ALF (proof assistant)|Alf]]).

===The Idea===

Before covering Inductive-Recursive types, the simpler case is Inductive Types. Constructors for Inductive types can be self-referential, but in a limited way. The constructor's parameters must be "positive":

===The Idea=idea==

Before covering Inductiveinductive-Recursiverecursive types, the simpler case is Inductiveinductive Typestypes. Constructors for Inductiveinductive types can be self-referential, but in a limited way. The constructor's parameters must be "positive":

* not refer to the type being defined

* be exactly the type being defined, or

* be a function that returns the type being defined.

With Inductiveinductive types, a parameter's type can depend on earlier parameters, but they cannot refer to ones of the type being defined. Inductive-Recursiverecursive types go further: anda parameter's types ''can'' refer to earlier parameters that use the type being defined. These must be "half-positive":

* be a function depending on an earlier parameter '''if''' that parameter is wrapped in the function being defined.

Line 24 ⟶ 27:

* <math>a:A</math>

* <math>d:D</math>

* <math>g:A \to \mathsf{Type}</math>

* <math>h:A \to D</math>

* <math>i:A \to B \to D</math>

Line 37 ⟶ 40:

* <math>m: z\ d</math> (Depends on <math>d</math> of type <math>D</math>, but not through the function <math>f</math>.)

=== Universe Exampleexample ===

A simple common example is the Universetype alaformer Tarskifor typea former.universe à la Tarski. It createsconsists of a type <math>U</math> and a function <math>T : U \to \mathsf{Type}</math>. such that Therethere is an element of <math>U</math> for every type in the type theory (except <math>U</math> itself!)., and Thethe function <math>T</math> maps the elements of <math>U</math> to the associated type.

The type <math>U</math> has a constructor (or introduction rule) for each type former in the type theory. The one for dependent functions would be:

=== Universe Example ===

A simple common example is the Universe ala Tarski type former. It creates a type <math>U</math> and a function <math>T</math>. There is an element of <math>U</math> for every type in the type theory (except <math>U</math> itself!). The function <math>T</math> maps the elements of <math>U</math> to the associated type.

<math>constructor_\mathsf{constructor}_\Pi (u:U) (u' : (x: T(u)) \to U) : U</math>

The type <math>U</math> has a constructor (or introduction rule) for each type former in the type theory. The one for dependent functions would be:

That is, it takes an element <math>u</math> of type <math>U</math> that will map to the type of the parameter, and ana elementfunction <math>u'</math> such that willfor mapall values <math>x:T(u)</math>, <math>u'(x)</math> maps to the return type of the function (which is dependent on the value of the parameter, <math>x</math>). (The final <math>:U</math> says that the result of the constructor is an element of type <math>U</math>.)

<math>constructor_\Pi (u:U) (u' : (x: T(u)) U) : U</math>

The reduction (or computation rule) says that <math>T(\mathsf{constructor}_\Pi(u, u'))</math> reduces to <math>\prod_{x:T(u)} T(u'(x))</math>.

That is, it takes an element <math>u</math> of type <math>U</math> that will map to the type of the parameter and an element <math>u'</math> that will map to the return type of the function (which is dependent on the value of the parameter). (The final <math>:U</math> says that the result of the constructor is an element of type <math>U</math>.)

After reduction, the function <math>T</math> is operating on a smaller part of the input. If that holds when <math>T</math> is applied to any constructor, then <math>T</math> will always terminate. Without going into the details, Induction-Recursion states what kinds of definitions (or rules) can be added to the theory such that the function calls will always terminate.

The reduction (or computation rule) says that

==Usage==

<math>T(constructor_\Pi(u, u'))</math> becomes <math>\Pi( T(u), (x) T(u'(x)) )</math>

Induction-recursion is implemented in [[Agda (programming language)|Agda]] and [[Idris (programming language)|Idris]].<ref>{{Cite book|last1=Bove|first1=Ana|last2=Dybjer|first2=Peter|last3=Norell|first3=Ulf|title=Theorem Proving in Higher Order Logics |chapter=A Brief Overview of Agda – A Functional Language with Dependent Types |date=2009|editor-last=Berghofer|editor-first=Stefan|editor2-last=Nipkow|editor2-first=Tobias|editor3-last=Urban|editor3-first=Christian|editor4-last=Wenzel|editor4-first=Makarius|chapter-url=https://link.springer.com/chapter/10.1007%2F978-3-642-03359-9_6|series=Lecture Notes in Computer Science|volume=5674 |language=en|___location=Berlin, Heidelberg|publisher=Springer|pages=73–78|doi=10.1007/978-3-642-03359-9_6|isbn=978-3-642-03359-9}}</ref>

After reduction, the function <math>T</math> is operating on a smaller part of the input. If that holds when <math>T</math> is applied to any constructor, then <math>T</math> will always terminate. Without going into the details, Induction-Recursion states what kinds of definitions (or rules) can be added to the theory such that the function calls will always terminate.

===Usage=See also==

* [[Induction-Induction_(type_theory) | Induction-Inductioninduction]] - Furtherfurther work that defines a type and a family- of- types at the same time.

Induction-Recursion is implemented in [[Agda (programming language)|Agda]].

==References{{reflist}}==

{{reflist}}

===See Also===

* [[Induction-Induction_(type_theory) | Induction-Induction]] Further work that defines a type and family-of-types at the same time.

References{{reflist}}

== External links ==

*[http://www.cse.chalmers.se/~peterd/papers/inductive.html A list of Peter Dybjer's publications on induction and induction-recursion]

*[http://www.cs.swan.ac.uk/~csetzer/slides/dybjer60thBirthdayGothenburgJune2013/dybjer60thBirthdayGothenburgJune2013.pdf Slides covering Induction-Recursion and its derivatives]

*[http://www.cs.swan.ac.uk/~csetzer/slides/dybjer60thBirthdayGothenburgJune2013/dybjer60thBirthdayGothenburgJune2013.pdf Slides covering Induction-Recursion and its derivatives]

[[Category:Type theory]]