Breaking up large mutual inductives

Stream: lean4

[Mario Carneiro]

Are there any techniques for dealing with inductive types which contain a large recursion? The issue is that I have an almost acyclic collection of types A ... Z that all build on one another, but A needs to refer to Z, and this causes all the types in between to end up in one giant mutual inductive block, which causes problems for the kernel. I'm considering using unsafe to avoid all the theorem generation because I don't need anything to be verified, I just want long distance mutual recursion like one would find in C / haskell / etc. Lean 4 core has a couple file-spanning mutual recursions, but they generally seem to go via builtin_initialize which isn't available to user code.

[Daniel Fabian]

oftentimes, what the F# folks do is being parametric in the type you would have to be recursive on otherwise. Maybe that could work for you?

[Mario Carneiro]

You still have to close the loop at the end, though. Is lean able to handle nested inductives like that?

[Mac]

I think @Daniel Fabian means something like this:

inductive BaseFoo a
| foo (foobar : a)

inductive BaseBar a
| bar (foobar : a)

inductive Foobar
| foo (foo : BaseFoo Foobar)
| bar (bar : BaseBar Foobar)

abbrev Foo := BaseFoo Foobar
abbrev Bar := BaseBar Foobar

which works like the following mutual block:

mutual

inductive Foo
| foo (foobar : Foobar)

inductive Bar
| bar (foobar : Foobar)

inductive Foobar
| foo (foo : Foo)
| bar (bar : Bar)

end

I've used this pattern myself in the past. For example, I used it to model LLVM's type hierarchy, which you can see here if you want.

[Mario Carneiro]

doesn't this incur just as much complexity internally as the mutual block? In order to prove that the nested inductive is okay it has to work out all the intermediate inductives

[Mario Carneiro]

it's not so bad here but imagine there are 6 more defs and structures between BaseFoo and the thing that shows up in Foobar

[Mac]

Mario Carneiro said:

In order to prove that the nested inductive is okay it has to work out all the intermediate inductives

What do you mean by okay? I don't think any special checking is going on in the non-mutual example. I know that, at the very least, some of the checking that goes on in a mutual block does not occur, since you can mix structures and inductives with this pattern but you can't do so in mutual blocks.

[Mario Carneiro]

I think that's just mutual being stingy

[Mario Carneiro]

structure is just an inductive under the hood

[Mario Carneiro]

there are lots of other things that could be supported in mutual but aren't like variable, set_option, and especially def and structure

[Mac]

Mario Carneiro said:

structure is just an inductive under the hood

You've mentioned this before and it has always struck me as odd. As, at the very least, structures support extends which behaves specially in many cases. So, I would not say they are all that identical.

[Mario Carneiro]

structures have lots of elaborator magic layered on top but from the kernel's perspective they are just inductives

[Mario Carneiro]

they generate all the usual inductive gizmos like noConfusion, plus some more things specific to structures like projections and parent instances

[Mac]

Ah, that's it. I tend to think at the Lean level, not the kernel level. For me, that's what matters.

[Mario Carneiro]

when asking whether a nested inductive is okay the check is in terms of kernel concepts

[Mac]

I am confused though about what part of this you would expect to error. In the non-mutual pattern there isn't really any nested inductives (in the sense that they are mutually referring to one another).

[Mario Carneiro]

mutual blocks are part of the elaborator layered on top, which is why it's possible for mutual to reject something that would be perfectly fine if it made it to the kernel

[Mario Carneiro]

Foobar is a nested inductive

[Mario Carneiro]

in order to validate a nested inductive that has a constructor like mk : Foo T -> T, you have to inspect and unfold Foo down to basic parts, because not every type operator Foo is sound in that position

[Mario Carneiro]

specifically, Foo := \lam X, X -> False would cause a contradiction

[Mario Carneiro]

The check that has to be done is that Foo unfolds to a nested combination of inductive type operators

[Mario Carneiro]

and this process entails essentially building that whole mutual inductive block under the hood

[Mario Carneiro]

It might be a bit faster since this construction is happening at a lower level where the elaborator doesn't have to get involved, but from a pure complexity standpoint they should be about the same

[Mac]

Ah. Makes sense. Sadly, I don't know much about how the kernel works.

[Mario Carneiro]

Plus, the recursor for a nested inductive explicitly references all those intermediates, and lean also wants to prove a bunch of injectivity lemmas about the inductive, and I think this is what costs most of the processing time

[Mario Carneiro]

I'm sure you have noticed that if you put unsafe on a large mutual or nested inductive it runs a lot faster

[Mac]

That's weird, because I said, I used this pattern to represent LLVM type hierarchy (i.e. here) which had a decent number of different nested inductives and I didn't really notice any overhead. But maybe that wasn't enough nesting?

[Mario Carneiro]

you should try playing with the nested inductive here. I gave up trying to fold Command into the big mutual inductive and instead I'm storing the backreferences in an external data structure and storing CommandId in the inductive instead

[Mario Carneiro]

It's already enough to exceed maxHeartbeats if you add a few more of those inductives into the mutual block

[Mac]

Do you think you could try the parameterized pattern there and see if this might be an elaborator issue with mutual blocks rather than a kernel issue with nested inductives?

[Mac]

Because while I haven't experienced slowdowns with the parametrized pattern, I definitely have encountered many a problem with using mutual blocks (including processing time).

[Mac]

Though I guess it might be wise to probe the Lean developers further to see if that could really be a solution before engaging in such a large refactor.

[Mac]

I do suspect though that the problem may be that mutual blocks have to do a lot more checking because they don't know a priori if the inductives are merely nested or if they are fully mutually recursive.

[Mario Carneiro]

Just for fun, here's a plot of the dependency graph between all the inductives (only counting the ones in the SCC) lean3-mutual.png

[Daniel Fabian]

Mario Carneiro said:

It might be a bit faster since this construction is happening at a lower level where the elaborator doesn't have to get involved, but from a pure complexity standpoint they should be about the same

have you verified this? I'd expect that you can do the check locally for each parametrized inductive as opposed to having to do it for the whole SCC. The fact that you are parametric breaks the loop after all.

[Mario Carneiro]

I actually don't know that much about what it's doing; my paper on the lean kernel was pre-nested inductives and I haven't looked at it since beyond observational testing like this

[Daniel Fabian]

as in does adding the type parameter fix your perf problem or not?

[Mario Carneiro]

I haven't tried it yet; one type parameter wouldn't be enough to untangle that graph, maybe 3 would get it into a collection of reasonably small mutual inductives but there are little cycles all over

[Sebastian Ullrich]

Now I'm glad that Syntax is stringly-typed... it does avoid this whole bunch of issues

[Sebastian Ullrich]

Mario Carneiro said:

Plus, the recursor for a nested inductive explicitly references all those intermediates, and lean also wants to prove a bunch of injectivity lemmas about the inductive, and I think this is what costs most of the processing time

You could try set_option genInjectivity false for that

[Sebastian Ullrich]

Mario Carneiro said:

but they generally seem to go via builtin_initialize which isn't available to user code.

I think initialize should work there instead

[Chris B]

That graph is nicely formatted btw, how'd you make it?

[Mario Carneiro]

mathematica, no special settings, just Graph[data, VertexLabels -> All]. I was originally hoping that one of the embeddings would help find good cut points in the graph, but it's pretty interconnected

[Mario Carneiro]

I don't suppose anyone knows whether there is an algorithm for finding a permutation of vertices of a directed graph that minimizes the number of backward edges (like topological sort, but for non-dags)

[Kyle Miller]

Mario Carneiro said:

I don't suppose anyone knows whether there is an algorithm for finding a permutation of vertices of a directed graph that minimizes the number of backward edges (like topological sort, but for non-dags)

According to section 9.4 of di Battista et al., "Graph Drawing: Algorithms for the Visualization of Graphs," this is an NP-complete problem. They give a greedy linear time algorithm, and they claim it works relatively well for sparse digraphs. (The formulation of the problem is to find the subset of edges to reverse to form a DAG.)

[Kyle Miller]

The greedy algorithm calculates a permutation of the vertices (as a list) that tries to minimize the set of leftward edges. Pseudocode:

let L and R be initialized as empty lists.
while there are still vertices:
  remove all sinks, prepending them to the list R
  remove all sources, appending them to the list L
  if G is nonempty,
    choose and remove a vertex maximizing outdeg - indeg, and append it to the list L
the result is L concatenated with R.

[Mario Carneiro]

is the vertex chosen in the last step also removed from the graph?

[Kyle Miller]

Oh, I made a big mistake translating it. Hold on.

[Kyle Miller]

Ok, fixed. I was reading the notation too quickly, sorry.

[Marcus Rossel]

Mario Carneiro said:

my paper on the lean kernel

What paper is that?