Inductive families Export

@article{dybjer94inductive, abstract = {A general formulation of inductive and recursive definitions in Martin-Lof\&\#039;s type theory is presented. It extends Backhouse\&\#039;s `Do-It-Yourself Type Theory \&\#039; to include inductive definitions of families of sets and definitions of functions by recursion on the way elements of such sets are generated. The formulation is in natural deduction and is intended to be a natural generalization to type theory of Martin-Lof\&\#039;s theory of iterated inductive definitions in predicate logic. Formal criteria are given for correct formation and introduction rules of a new set former capturing definition by strictly positive, iterated, generalized induction. Moreover, there is an inversion principle for deriving elimination and equality rules from the formation and introduction rules. Finally, there is an alternative schematic presentation of definition by recursion. The resulting theory is a flexible and powerful language for programming and constructive mathematics. We hint at the wealth of possible applications by showing several basic examples: predicate logic, generalized induction, and a formalization of the untyped lambda calculus.}, author = {Dybjer, Peter}, citeulike-article-id = {3391259}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.74}, journal = {Formal Aspects of Computing}, keywords = {dependent, inductive, recursion, types}, pages = {440--465}, posted-at = {2008-10-09 18:59:29}, priority = {3}, title = {Inductive families}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.74}, volume = {6}, year = {1994} }

TY - JOUR ID - dybjer94inductive L3 - citeulike-article-id:3391259 N2 - A general formulation of inductive and recursive definitions in Martin-Lof's type theory is presented. It extends Backhouse's `Do-It-Yourself Type Theory ' to include inductive definitions of families of sets and definitions of functions by recursion on the way elements of such sets are generated. The formulation is in natural deduction and is intended to be a natural generalization to type theory of Martin-Lof's theory of iterated inductive definitions in predicate logic. Formal criteria are given for correct formation and introduction rules of a new set former capturing definition by strictly positive, iterated, generalized induction. Moreover, there is an inversion principle for deriving elimination and equality rules from the formation and introduction rules. Finally, there is an alternative schematic presentation of definition by recursion. The resulting theory is a flexible and powerful language for programming and constructive mathematics. We hint at the wealth of possible applications by showing several basic examples: predicate logic, generalized induction, and a formalization of the untyped lambda calculus. JF - Formal Aspects of Computing EP - 465 TI - Inductive families VL - 6 SP - 440 KW - dependent KW - inductive KW - recursion KW - types AU - Dybjer, Peter PY - 1994/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.74 ER -