Induction-recursion: Difference between revisions

Revision as of 15:56, 1 August 2013

Revision as of 16:42, 1 August 2013

Line 12:

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]]).

===ExampleThe 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":

Induction-Recursion is when a type is defined simultaneously with a function that operates on that type. The important concept, like with recursion, is that when the function is called on an instance of the type, the function will eventually terminate.

* not refer to the type being defined

* be exactly the type being defined, or

* be a function that returns the type being defined.

With Inductive types, a parameter's type can depend on earlier parameters, but they cannot refer to ones of the type being defined. Inductive-Recursive types go further and 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.

So, if <math>D</math> is the type being defined and <math>f</math> is the function being (simultaneously) defined, these parameter declarations are positive:

* <math>a:A</math>

* <math>d:D</math>

* <math>g:A \to Type</math>

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

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

* <math>j: g\ a</math> (Depends on earlier parameters, none of which are type <math>D</math>.)

This is half-positive:

* <math>k : (f\ d) \to D </math> (Depends on parameter <math>d</math> of type <math>D</math> but only through call to <math>f</math>.)

These are '''not''' positive nor half-positive:

* <math>k: D \to A</math> (<math>D</math> is a parameter to the function.)

* <math>l: (A \to D) \to A</math> (The parameter takes a function that returns <math>D</math>, but returns <math>A</math> itself.)

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

=== 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.

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 <math>constructor_\Pi (u:U) (u' : (x: T(u)) U) : U</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>.)

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

The reduction (or computation rule) says that <math>T(constructor_\Pi(u, u'))</math> becomes <math>\Pi( T(u), (x) T(u'(x)) )</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.

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>.)

The reduction (or computation rule) says that

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

The reduction (or computation rule) says that <math>T(constructor_\Pi(u, u'))</math> becomes <math>\Pi( T(u), (x) T(u'(x)) )</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.

===Usage===

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

===See Also===

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