univalence normalization

[stelleg]

Hey Guys,

I've enjoyed playing around with building proofs using funExt, all of which have normalized successfully. When I went to play around with univalence, however, I noticed that none of the proofs of univalence normalize. I let each of the three proofs from examples/univalence.ctt run to about 12GB of memory usage, and none of them terminated.

I haven't carefully read all of the cubicaltt papers, nor carefully reasoned about the proofs of univalence, so I'm wondering if this is a known property of the type theory? It seems worrying from a standard Curry-Howard perspective.

Cheers, George

[mortberg]

This is a known issue, I experimented with a more efficient approach to composition in the universe on the branch compU recently. I managed to get some examples involving univalence to normalize, but I'm not sure if the computation of normal forms of the terms in univalence.ctt ever terminated. Maybe you can try?

I made a list of things on the wiki which I plan to implement as soon as I have time, and some of these should make things much more efficient. There might also be some simplifications to the algorithm for composition for glueing which might make things more efficient.

[stelleg]

So far no luck with compU. It does seem to grow in memory footprint slower though. The first proof of univalence got up to about an hour and 80GB of memory.

Looking at the normalized proof terms, as you are probably aware, the proof terms seem to be blowing up exponentially. For example, normalized equivLemma works out to be half a megabyte of printed proof, and proofs that use it are significantly larger, if they terminate at all.

[stelleg]

idToId did finish, with the normalized proof weighing in at ~186MB in printed form.

[coquand]

Thanks for looking at this example. We spent the last months working on the presentation of the underlying type system, and not on the implementation. We really have to understand why the normal form of equivLemma is so big; if it is a bug in the program or where the exponential behavior comes from!

On Dec 18, 2015, at 7:18 AM, George Stelle wrote:

idToId did finish, with the normalized proof weighing in at ~186 megabytes in printed form.

— Reply to this email directly or view it on GitHub.

[coquand]

Here is a file with a simpler proof of equivLemma (but I changed the definition of fiber and equivalence)

On Dec 18, 2015, at 7:18 AM, George Stelle wrote:

idToId did finish, with the normalized proof weighing in at ~186 megabytes in printed form.

— Reply to this email directly or view it on GitHub.

[coquand]

And here is a file with a simpler proof of the Lemma about family of propositions. The normal form of equivLemma is still quite long and one should understand where the exponential behavior comes from.

On Dec 18, 2015, at 7:18 AM, George Stelle wrote:

idToId did finish, with the normalized proof weighing in at ~186 megabytes in printed form.

— Reply to this email directly or view it on GitHub.

[mortberg]

stelleg: Thanks for experimenting! How long did it take for idToId to terminate?

coquand: Could you please send the files to my email instead? I don't think one can send attachments to the github comment threads...

[stelleg]

The thanks belongs to both of you for such interesting work!

mortberg: Not sure exactly how long, but I would guess on the order of 10-30 minutes and tens of gigabytes of memory.

Do either of you have a sense of whether the exponential behavior could be inherent to the type theory or an implementation issue?

[coquand]

I put a file testEquiv.ctt with maybe a simpler version of idToId

Thierry

On Dec 18, 2015, at 6:25 PM, George Stelle wrote:

The thanks belongs to both of you for such interesting work!

mortberg: Not sure exactly how long, but I would guess on the order of 10-30 minutes and tens of gigabytes of memory.

Do either of you have a sense of whether the exponential behavior could be inherent to the type theory or an implementation issue?

— Reply to this email directly or view it on GitHub.

[coquand]

Do either of you have a sense of whether the exponential behavior could be inherent to the type theory or an implementation issue?

The size is inherent to the type system. We tried before to compute the result of programs of a concrete type (like nat) and the computation of normal form is something new.

[coquand]

The computation of idToId should be lighter now in the file testEquiv. Can you try transEquivIsEquiv in this file?

On Dec 18, 2015, at 7:18 AM, George Stelle wrote:

idToId did finish, with the normalized proof weighing in at ~186 megabytes in printed form.

— Reply to this email directly or view it on GitHub.

[stelleg]

coquand: idToId is much faster/smaller: it only takes ~1 minute. Very nice!

Unfortunately transEquivIsEquiv got up to about 80GB of memory usage and a couple hours and didn't terminate.

[martinescardo]

I am interested in knowing the reason for this computational blow-up. Is this something intrinsic to the cubical model? Or is this a computational property of univalence? Or is this just an artifact of the experimental implementation of the cubical model, which could perhaps/probably be improved with more thought?

[coquand]

Good questions!

Here is a summary of some examples in the file testEquiv.

We have two maps

f = transEquiv : Path U A B -> equiv A B g = transEquivToId : equiv A B -> Path U A B

The proof eqToEq that g f is the identity has a small normal form

The proof idToId that fg is the identity has a normal form which is quite big

The two facts together show that f has an inverse, which is one way to state univalence.

Already the proof of equivLemma is surprisingly relatively big. And this proof is only a proof that

Path (equiv A B) f g holds

if we have

Path (A->B) f.1 g.1

On Dec 21, 2015, at 10:04 PM, Martin Escardo wrote:

I am interested in knowing the reason for this computational blow-up. Is this something intrinsic to the cubical model? Or is this a computational property of univalence? Or is this just an artifact of the experimental implementation of the cubical model, which could perhaps/probably be improved with more thought?

— Reply to this email directly or view it on GitHub.

[mortberg]

We have now formalized another proof of univalence whose normal form can be computed in reasonable time on a normal computer (it takes about 1m20s on my laptop), see the univalence.ctt file on the master branch for details. The proof is the one from section 7.2 of our cubicaltt paper where we prove a more general formulation of univalence using the unglue operation. Corollary 10 (lem1 in the formalization) was formalized by Fabian Ruch.

We still haven't been able to compute the normal form of the other proof of univalence (appendix 2 of the paper). As Thierry writes above even the lemma about equality of equivalences (ie maps with contractible fibers) takes a lot of time to normalize. I formalized this lemma in Coq using the UniMath library and found out that Coq takes up all the memory on my computer while trying to normalize it. I then minimized the example and figured out that the main culprit seems to be the grad lemma (ie the lemma showing that an isomorphism is an equivalence).

More precisely I noticed an interesting complexity increase when normalizing the term isweqinvmap from the UniMath library which gives the inverse of an equivalence:

https://github.com/UniMath/UniMath/blob/master/UniMath/Foundations/Basics/PartA.v#L1331

This lemma relies on four different things which all normalize in no time:

Time Eval compute in gradth.
(* Finished transaction in 0.141 secs (0.116u,0.s) (successful) *)
Time Eval compute in invmap.
(* Finished transaction in 0.004 secs (0.u,0.s) (successful) *)
Time Eval compute in homotweqinvweq.
(* Finished transaction in 0.003 secs (0.u,0.s) (successful) *)
Eval compute in homotinvweqweq.
(* Finished transaction in 0.01 secs (0.u,0.s) (successful) *)

but when one combines all of these in isweqinvmap things get much slower:

Time Eval compute in isweqinvmap.
(* Finished transaction in 19.739 secs (18.499u,0.266s) (successful) *)

Here gradth is the Coq proof of the grad lemma, and isweqinvmap is proved by applying it to the other terms whose normal forms are all small. The proof we have in cubicaltt of the grad lemma is different (it is done by computing a composition in a complicated cube), but regardless I have noticed similar increases in computation time when computing the normal form of terms involving it. In particular the proof of univalence which we never managed compute the normal form of relies on this lemma in multiple places (in particular the last step of the proof is a call to it with complicated input) which might explain why we never manage to compute its normal form.

This suggests that the grad lemma should be avoided if one wants to be able to compute normal forms of terms, and that the computational blow-up is not intrinsic to cubicaltt or the implementation but to the first proof of univalence.

[martinescardo]

Interesting!

[coquand]

In particular, the proof of your formulation of univalence (lem1) is almost already in normal form. The proof becomes much bigger however when proving from this the usual statement of univalence, but the normal form of each component of the argument is itself relatively small...

On Jan 4, 2016, at 10:26 PM, Martin Escardo wrote:

Interesting!

— Reply to this email directly or view it on GitHub.

[stelleg]

Very interesting! I can't say run-time efficiency is ever something I've taken into consideration when writing a proof.

Do you expect that it's possible for this kind of exponential blowup to occur during type checking? In simpler dependent type systems that I've come across normalization is used to check convertibility of types, but here it looks as though a weaker evaluation function is used, halting evaluation on neutral applications. It seems possible to me that the weaker eval could blow up in a similar way, though maybe much less likely. I apologize if this is an obvious question, I'm still fairly new to the area.

[martinescardo]

Mortberg and Thierry: your experiments and replies address my questions very much to the point.

In particular, I see that the blow-up is not to be attributed to the "cubicality" of your type theory.

But I am still mystified by the question of what is going on with the very large normal forms you get for some formulations of univalence (either in ctt or in coq), because although it is easy to come up with short terms with arbitrarily large normal forms, in principle there is nothing to imply a priori that (some natural formulations of) univalence would give us such examples. What is going on? I would expect, in my naive intuition, univalence not to do much other than cleverly chasing equivalences. Of course, this is not a claim, but rather an intuition raising the question.

[mortberg]

martin: I have no good answer to your question yet, but we have now managed to typecheck the normal form of univalence!

More precisely we have computed and typechecked the normal form of:

thmUniv (t : (A X : U) -> Id U X A -> equiv X A) (A : U) :
  (X : U) -> isEquiv (Id U X A) (equiv X A) (t A X) =
    equivFunFib U (\(X : U) -> Id U X A) (\(X : U) -> equiv X A)
      (t A) (lemSinglContr' U A) (lem1 A)

In the process of doing this we found multiple bugs in the implementation, but luckily nothing serious. The fixes of these bugs makes the computation take longer than before, more precisely it takes about 10 min on my computer now. The output is 11.6MB and you can find it at:

https://github.com/mortberg/cubicaltt/blob/master/examples/nthmUniv.ctt

This is the file that we finally managed to typecheck and as it is pretty huge this took a lot of time (about 51.5 hours on my computer). I think the fact that we manage to compute this huge normal form and then check that it is correct gives us quite good empirical evidence that what we are doing is correct.

I also formalized some more tests to see if the huge normal form poses some problems for actually computing something. I have formalized various results about Voevodsky's impredicative set quotients in:

https://github.com/mortberg/cubicaltt/blob/master/examples/setquot.ctt

using this I have defined Z as the quotient of nat * nat by the relation

(x1,x2) ~ (y1,y2) := (x1 + y2 = x2 + y1)

Finally I use a general result on set quotients to get an equality test on Z from the one on nat and with this I can check that 0 is not equal to 1 and that 1 is equal to 1 by computation. This example uses univalence (for propositions, but proved using the general statement) in multiple places and the computations are very fast (about 0.5s on my computer).

[martinescardo]

This is very interesting. I am mystified why univalence in normal form should be so long! The quotient example is also interesting on its own.