Content deleted Content added
Line 9:
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 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., [[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 "
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]]).
| |||