Re: [HoTT] Re: Why do we need judgmental equality?

["Jon Sterling" <jon@jonmsterling.com>]

Hi all,

I think there's two different issues being conflated -- there is the question of whether definitional equalities can be removed, in order to obtain more direct interpretation into weaker models, and then there is the question of whether definitional equalities can be removed as a way to make a proof assistant more modular, exploiting conservativity results locally to add defintional equalities.

The first seems more interesting to me, and is indeed the topic of Curien's famous paper. Many interesting coherence theorems lurk underneath the definitional equalities that we take for granted, and we can only see them if we treat definitional equalities as defeasible.

The issue about proof assistants seems quite different to me -- the approach that seems to be proposed by some of the people in the room, to replace judgmental equality with a good enough equality *type* seems perfectly good for studying algebra and models (for instance, the discipline of QIITs in the presence of [semantically] extensional equality types seems like a good tool for dependently-sorted algebraic theories). But this approach is not likely to yield *proof assistants* that are more usable than existing systems which have replaced definitional equality with propositional equality.

I am referring to Nuprl -- usually Nuprl is characterized as using equality reflection, but this is not totally accurate (though there is a sense in which it is true). When I say "definitional equality" for a formalism, what I mean is that if I have a proof object D of a judgment J, if J is definitionally equal to J', then D is also already a proof of J'. Definitional equality is the silent equality. In most formalisms, definitional equality includes some combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha. What I mean is that in a proof object for Nuprl, the biggest relation by which you can "purturb" a judgment without needing to update the proof object is alpha equivalence. Proof objects must NOT be confused with realizers, of course -- just like we do not confuse Coq proofs with the OCaml code that they could be extract to.

So how does Nuprl work? "Real" equality is captured purely using the equality type, and not using any judgment except membership in the equality type (a judgment whose derivations are crucially taken only up to alpha, rather than up to beta/eta/xi). When you want to reason using beta/eta/xi (and the much richer equations that are also available), you use the equality type and its elimination rules directly, essentially in the same way that Thorsten has advocated.

Nuprl is in essence what it looks like to remove all definitional equalities and replace them with internal equalities. The main difference between Nuprl and Thorsten's proposal is that Nuprl's underlying objects are untyped -- but that is not an essential part of the idea.

The reason I bring this up is that the question of whether such an idea can be made usable, namely using a formalism with only alpha equivalence regarded silently/definitionally, and all other equations mediated through the equality type, can be essentially reduced to the question of whether Nuprl is practical and usable, or whether it is possible to implement a version of that idea which is practical and usable.

As many of the people on this list are aware, in the years past I was very bullish on this idea, but now after having implemented two separate proof assistants based on this idea, I am not as optimistic about it as I was (but I don't rule it out). Today, I have changed my methodology and embraced strong definitional equality, in order to achieve my actual goals during the very finite historical period of my PhD -- to build usable proof assistants for formalizing mathematics.

Best,
Jon




On Sat, Feb 9, 2019, at 9:05 AM, Nicolai Kraus wrote:
> On Sat, Feb 9, 2019 at 11:53 AM Felix Rech <s9ferech@gmail.com> wrote:
> > One of the motivations for my question was that I actually expect usability benefits if one worked in a dependent type theory without judgmental equality that has good support by a proof assistant.
> 
> Yes, me too (but I think *a lot* of work needs to be done before we can 
> have a proof assistant based on this idea which provides better 
> usability than the current ones).
> I agree with your points. But I think "x + 0 = x versus 0 + x = x" is 
> an example where I'd expect that one should be able to produce a 
> conservativity proof and use both at the same time instead of choosing 
> one. I think it's not necessary that we restrict ourselves to 
> computation rules that come from actual definitions; anything that is 
> "constructively conservative" over a weak theory should be allowed. In 
> Agda, one can have additional computation rules, but it's not a safe 
> feature.
> Nicolai
> 
> 
> >  1. Judgmental equality cannot be taken as assumptions. If one wants to use judgmental equalities then one has to give concrete definitions that satisfy those equalities and cannot hide the definition details. This makes it impossible to change definitions later on without breaking constructions that depend on them.
> >  2. In nontrivial definitions, judgmental equalities seem more arbitrary than natural. If we define addition of natural numbers for example then we can choose between x + 0 = x and 0 + x = x as judgmental equality but we cannot have both. This makes it hard to find the right definitions and to predict their behavior.
> > Another motivation was of course that it would simplify the implementation of proof checkers and parts of the metatheory.
> > 
> > I would appreciate any comments on this.
> >  
> 
> 
> > -- 
> > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> > For more options, visit https://groups.google.com/d/optout.
> >  
>  
> 
> 
>  -- 
>  You received this message because you are subscribed to the Google 
> Groups "Homotopy Type Theory" group.
>  To unsubscribe from this group and stop receiving emails from it, send 
> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>  For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.