1
$\begingroup$

Unfortunately copy/paste doesn't work for this paper Inductive Definitions and Type Theory, but here is a snippet.

enter image description here

The paper begins by stating:

enter image description here

The first sentence of the second paragraph says type theory as a theory of inductive definitions. I have never really paid much attention to how central induction is to type theory, but it seems to be one of the main requirements, hence this question.

Is induction a requirement for type theory? That is, can you have a modern robust type theory or typed programming language without induction? If not, why not? If so, what would it look like generally speaking (just looking for pointers for the right research to look into). Why is induction central to type theory? What does type theory as a theory of inductive definitions mean?

Sorry if this is a really basic question. I am just trying to get a solid grasp of the foundations, and asking anything that is unclear to me in the process without having a full picture and being an expert yet.

$\endgroup$
1
  • $\begingroup$ Don't use images as main content of your post. This makes your question impossible to search and inaccessible to the visually impaired; we don't like that. Please transcribe text and mathematics. You can use LaTeX. $\endgroup$
    – D.W.
    Feb 6, 2022 at 20:36

1 Answer 1

1
$\begingroup$

Induction is not a requirement. You can take inductive definitions out of Martin-Löf type theory, and you still get a consistent theory. It's just not an interesting theory.

Without induction, you can only make finitary, non-self-referential descriptions of data and proofs. If you interpret types as sets of terms, without induction, types are just certain finite subsets of certain finite sets. You don't need such theoretical machinery to reason about finite sets. Reasoning about finite sets opens different problems, mostly about keeping the descriptions down to a reasonable size.

Type theory aims to reason about infinite classes of objects. For example, there's a type containing all lists of integers, not just some finite collections of integers. And you can make functions that work over arbitrary lists, regardless of their length: without induction, a function could only act on a limited number of objects for a given length of the function's source code.

Type theory lets you reason about interesting properties of objects even when those objects are inductively defined.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.