HOME

TheInfoList



OR:

In
intuitionistic type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory (MLTT)) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematicia ...
(ITT), a discipline within
mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, induction-recursion is a feature for simultaneously declaring a type and function on that type. It allows the creation of larger types than inductive types, such as universes. The types created still remain predicative inside ITT. An
inductive definition In mathematics and computer science, a recursive definition, or inductive definition, is used to define the elements in a set in terms of other elements in the set ( Aczel 1977:740ff). Some examples of recursively definable objects include fact ...
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. 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 definitions are still considered predicative.


Background

Induction-recursion came out of investigations into the rules of Martin-Löf's
intuitionistic type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory (MLTT)) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematicia ...
. The type theory has a number of "type formers" and four 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., strong normalization, 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 "à la Tarski", they simultaneously defined the "universe type" ''and'' a function that operated on it. This eventually lead Dybjer to induction-recursion. 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 inductive-recursive definitions to be made inside the type theory. This was added to the Half
proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof edi ...
(a variant of 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": * 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: a 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 D is the type being defined and f is the function being (simultaneously) defined, these parameter declarations are positive: * a:A * d:D * g:A \to \mathsf * h:A \to D * i:A \to B \to D * j: g\ a (Depends on earlier parameters, none of which are type D.) This is half-positive: * k : (f\ d) \to D (Depends on parameter d of type D but only through call to f.) These are not positive nor half-positive: * k: D \to A (D is a parameter to the function.) * l: (A \to D) \to A (The parameter takes a function that returns D, but returns A itself.) * m: z\ d (Depends on d of type D, but not through the function f.)


Universe example

A simple common example is the type former for a universe à la Tarski. It consists of a type U and a function T : U \to \mathsf such that there is an element of U for every type in the type theory (except U itself!), and the function T maps the elements of U to the associated type. The type U has a constructor (or introduction rule) for each type former in the type theory. The one for dependent functions would be: \mathsf_\Pi (u:U) (u' : T(u) \to U) : U That is, it takes an element u of type U that will map to the type of the parameter, and a function u' such that for all values x:T(u), u'(x) maps to the return type of the function (which is dependent on the value of the parameter, x). (The final :U says that the result of the constructor is an element of type U.) The reduction (or computation rule) says that T(\mathsf_\Pi(u, u')) reduces to \prod_ T(u'(x)). After reduction, the function T is operating on a smaller part of the input. If that holds when T is applied to any constructor, then T will always terminate.


Usage

Induction-recursion is implemented in Agda and
Idris Idris may refer to: People * Idris (name), a list of people and fictional characters with the given name or surname * Idris (prophet), Islamic prophet in the Qur'an, traditionally identified with Enoch, an ancestor of Noah in the Bible * Idris ...
.


See also

*
Induction-induction In intuitionistic type theory (ITT), a discipline within mathematical logic, induction-induction is for simultaneously declaring some inductive type and some inductive predicate over this type. An inductive definition In mathematics and comput ...
- further work that defines a type and a family of types at the same time


References

{{reflist


External links


A list of Peter Dybjer's publications on induction and induction-recursionSlides covering Induction-Recursion and its derivatives
Type theory