Induction-recursion: Difference between revisions

Revision as of 03:08, 4 January 2023

Revision as of 14:54, 22 August 2023

Line 11:

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 Induction-Recursion definitions to be made inside the type theory.<ref name=DybjerSetzer>{{cite book|last=Dybjer|first=Peter|title=Typed Lambda Calculi and Applications |chapter=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|citeseerx=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==

Line 57:

==Usage==

Induction-Recursion is implemented in [[Agda (programming language)|Agda]] and [[Idris (programming language)|Idris]].<ref>{{Cite journalbook|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|title=A Brief Overview of Agda – A Functional Language with Dependent Types|chapter-url=https://link.springer.com/chapter/10.1007%2F978-3-642-03359-9_6|journal=Theorem Proving in Higher Order Logics|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>

==See also==