About: Induction-recursion

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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, such as universes, than inductive types. The types created still remain predicative inside ITT. 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 predicative.

Property Value
dbo:abstract
  • 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, such as universes, than inductive types. The types created still remain 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. 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 predicative. (en)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 38365576 (xsd:integer)
dbo:wikiPageLength
  • 7416 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 982093953 (xsd:integer)
dbo:wikiPageWikiLink
dbp:wikiPageUsesTemplate
dcterms:subject
rdfs:comment
  • 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, such as universes, than inductive types. The types created still remain predicative inside ITT. 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 predicative. (en)
rdfs:label
  • Induction-recursion (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License