Stream: new members

Topic: Is induction-recursion and induction-induction limitation?

Chris M (Aug 25 2020 at 08:01):

The lean prover manual says "In the type theory literature, there are further generalizations of inductive definitions, for example, the principles of induction-recursion and induction-induction. These are not supported by Lean." I read a bit about induction-recursion (wikipedia). This is just a curiosity: Is this something that would ever be useful in formalizing math?

Mario Carneiro (Aug 25 2020 at 08:08):

You see it used mostly by the type theory fanatics that already see inductive types as a hammer and everything as a nail

Mario Carneiro (Aug 25 2020 at 08:09):

An example is that you can use an inductive-recursive type to very naturally capture the type of well typed terms mutual with the type of contexts, and so prove the consistency of DTT

Mario Carneiro (Aug 25 2020 at 08:30):

I forget all the details, but it's something like this:

mutual inductive context, type, term
with context : Type
| nil : context
| cons (Γ : context) (A : type Γ) : context
with type : context → Type
| univ {Γ} : type Γ
| pi {Γ} (A : type Γ) (B : type (context.cons Γ A)) : type Γ
| T {Γ} : term Γ type.univ → type Γ
with term : context → type → Type
| var {Γ A} : term (context.cons Γ A) A
| lift {Γ A B} : term Γ B → term (context.cons Γ A) B
| lam {Γ A B} : term (context.cons Γ A) B → term Γ (type.pi A B)


Mario Carneiro (Aug 25 2020 at 08:33):

I recall a talk by Peter LeFanu Lumsdaine (I think) about how to represent buildings (some homotopy theory thing like CW complexes) using inductive-recursive types

Mario Carneiro (Aug 25 2020 at 08:38):

Misremembered the author, but the slides here look familiar

Kevin Buzzard (Aug 25 2020 at 08:50):

@Bhavik Mehta and I had an interesting discussion about this on the discord a few weeks back. The question came up about higher inductive types and whether they were useful for mathematics, and I said "well I formalised perfectoid spaces and schemes and I didn't need anything apart from structures so clearly they're not important" and then Bhavik linked to a parody article about someone who knows a programming language which is not too high-level and not too low-level and then looks at what the lower-level programming languages do and says "golly I'm glad my language has got these features so you don't have to struggle like they do" and then he looks at what higher-level programming languages are doing and says "they're using all these crazy features and I don't understand their code but it's clearly not necessary because I can do everything I want to do in my language"

Kevin Buzzard (Aug 25 2020 at 08:51):

the point being that perhaps higher inductive types are useful even though I don't need them

Kevin Buzzard (Aug 25 2020 at 08:51):

Bhavik will I'm sure remember the link to the parody

Kyle Miller (Aug 25 2020 at 08:52):

That's known as the blub paradox. Maybe it was Paul Graham's essay that introduced them?

Kyle Miller (Aug 25 2020 at 08:53):

I guess you said a parody, so probably not. But here's his essay: http://paulgraham.com/avg.html

Mario Carneiro (Aug 25 2020 at 08:56):

someone needs to write a language called blub

Kevin Buzzard (Aug 25 2020 at 08:59):

Yeah this is it, perhaps it was someone else's take on Blub but I think it was called Blub

Kevin Buzzard (Aug 25 2020 at 08:59):

in fact I can now search for it on the discord

Kevin Buzzard (Aug 25 2020 at 08:59):

oh except I am live streaming at 10

Reid Barton (Aug 25 2020 at 10:24):

regarding higher inductive types, Lean doesn't have "higher types" in the first place, but you probably used quotients, which you can see as a particular hard-coded baby higher inductive type.

Reid Barton (Aug 25 2020 at 10:31):

About induction-recursion, I would say: yes, there are definitions in math that can naturally be viewed as examples of induction-recursion; but they aren't of this "model of type theory" sort, and (usually?) can be encoded in other ways. So for the purposes of math, not supporting induction-recursion is sort of like (hypothetically) not supporting mutual inductive types.

Reid Barton (Aug 25 2020 at 10:33):

Whether it would be useful to have direct support for induction-recursion is hard to say, given that it's not so easy to try using them.

Bhavik Mehta (Aug 25 2020 at 10:33):

Kyle Miller said:

I guess you said a parody, so probably not. But here's his essay: http://paulgraham.com/avg.html

Yeah this was exactly what I'd linked

Scott Morrison (Aug 25 2020 at 12:01):

I remember trying to formalise some definition of Jamie Vicary's about higher categories at some point, and realised I was trying to write something than needed induction-recursion. I can't find this now.

Scott Morrison (Aug 25 2020 at 12:02):

A student at some point claimed that they wanted to use induction-recursion to formalise CW complexes, but I never got to the bottom of their difficulty. I'm pretty confident in that case it was not necessary.

Devon Tuma (Aug 25 2020 at 12:16):

They may have been trying to do a HoTT style of cell complex, where the type associated to most cell complexes will be a higher inductive type? (e.g. the CW complex for a circle would translate to a type with two constructors: A base point, and a non-trivial path from the base point to itself, a torus would be a type with 4 constructors, etc.) Although this is more a way to look at particular complexes than a generic formalization of them.

Reid Barton (Aug 25 2020 at 12:16):

If you want to build the type "CW complexes of dimension at most n" as an inductive family indexed on n, then you need induction-recursion in order to say what it means to give attaching maps for the n-cells. But you can also define that type by recursion on n, and this would be supported by Lean.

Reid Barton (Aug 25 2020 at 12:20):

When I realized this (and that it would also solve another problem of mine) I stopped accumulating a list of examples of induction-recursion in math. :upside_down:

Reid Barton (Aug 25 2020 at 12:21):

The CW complex example is a bit flawed in that it's not clear how you would describe infinite-dimensional ones.

Last updated: May 06 2021 at 22:13 UTC