philosophy of induction and recursion in type theory

Stream: new members

[Chris M]

I'm reading on induction and recursion in Lean now (the "theorem proving in lean" tutorial). If I understand correctly, induction and recursion have a somewhat different role in Lean's type theory than they have in mainstream mathematics: a they seem to be more of a part of the foundations of the system, compared to set-theoretic foundations. Is there a good article that talks about the philosophy and motivation behind the role of recursion and induction in type theories? (maybe in comparison to set theoretic foundations?)

[Jeremy Avigad]

You do understand correctly. From a foundational perspective, if you want to talk about inductively characterized structures, you have two choices: (1) make sure your axioms give you enough to sets/types to work with and use them define your inductive structures (typically as an intersection of all subsets of some suitable universe of things satisfying some closure conditions), or (2) include them axiomatically.

The set-theoretic constructions are well understood, so in set theory they are generally constructed. (In fact, the only inductive structure mathematicians really use all that often is the natural numbers. It's really computer scientists who care about induction on terms and expressions.) The same is generally true even in systems based on simple type theory, which usually use classical logic freely. For example, Isabelle has an elaborate datatype package; you describe want you want, and, underneath the hood, the system proves the existence of everything you need. (http://isabelle.in.tum.de/dist/doc/datatypes.pdf)

With constructive dependent type theory, however, the tradition is to include inductive types axiomatically. There are two reasons for that. The first is pragmatic: if you care about computation, it is better to present inductively defined datatypes in such a way that the computational principles and behavior are manifest. In particular, type checking in systems like Lean depends on computational reductions of the recursors, and you want that to be specified by the logic. (If you did it with an ad-hoc construction, you would have to later somehow tell the system how to implement the computational behavior in a sound way.)

The second reason is more philosophical: from a constructive, intuitionistic standpoint, it is more natural to assert that some construction can be carried out than to assert that some big infinite set exists. In other words, constructivists may assert that inductive types are the natural foundation. In Brouwerian intuitionistism, choice sequences (and the fan theorem and the bar theorem) are basically theorems about well-founded trees and their inductive characterizations. In more recent history, Martin-Löf added W-types as the fundamental inductive definition, and there are senses in which arbitrary inductive definitions can be reduced to those. (Wikipedia is a good place to start learning the history: https://en.wikipedia.org/wiki/Intuitionistic_type_theory)

[Pedro Minicz]

There is a historical/pragmatical reason for the inclusion of inductive types in type theories. As you may have noticed, inductive types are quite distinct and more complex and then anything else in type theory. To be more precise, you can specify the rules for typing dependent functions and function application in less than a page, but you would need way more than a page to specify everything that make dependent types work (the same can be said about recursion, but recursion may be defined as syntax sugar for type recursors).

Type theories emerged from the study of set theory and, particularly, lambda calculi. Untyped calculus can express recursion and recursively defined datatypes (algebraic datatypes), however it is not consistent. Many typed lambda calculus - such as simply typed lambda calculus or the calculus of constructions - are logically consistent, but lack the power to express recursion or to encode most datatypes. Lean is based on the calculus of inductive constructions, which extends the calculus of constructions with inductive types and expands its definition from half a page to many.

There are ways of expanding on the calculus of constructions such that inductive types can be defined instead of
axiomized. Cedille is a proof assistant based on the calculus of dependent lambda eliminations, which can be defined in about a page and allows one to use lambda encoded inductive types. Sadly, work in this area seem sparse in favor for the more heavy handed primitive inductive types. Also, I've seen someone argue on Stackoverflow that a lambda encoding for an inductive type cannot allow for complex pattern matching (that is, see what is inside the type without destructing it) and efficient induction/recursion, although I am not sure that is necessarily true.

So, inductive types may be more of a historical accident/pragmatical necessity than a philosophical decision from type theorists.