From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4d7e59dd for ; Mon, 11 Feb 2019 13:22:22 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id q16sf11068425otf.5 for ; Mon, 11 Feb 2019 05:22:22 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=UmTrnhK6GtkNJpVqF4y+hp9qhwqq+Ui/RdrWymTw2tw=; b=MrIGjgy0QWxLfFNvpoXXI94PQg1FBhQ7omAcGGgI3FRz6iQgJ3x6l+D2o3a1SH7FvC w7IQv+vHYCpXec+PeERoEMKtg+o8+ZCweVDVXv5dWhQo7DSYFPZEEkE/pHetB8OAodwe 6rhqH5+ohUNYyViels5RChoiy2zQQFdhSFHwT1d+aPG13gNKo6hk9CIpb7pxBw3xO8ue OAt4jD5S+MgIHkMh4DUxBiMCIsdOl/x6BRS/9M9843t7S3rWT0haUp1ouZI+2HLf4uMe XRtBKpv1ongfDl7zM5QUqd+CJXfPu9u+4LyLzwXnc1i/g9jKAHrQRUwzWYUeylorcypJ RgQQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=UmTrnhK6GtkNJpVqF4y+hp9qhwqq+Ui/RdrWymTw2tw=; b=tUJOfN0aHXjgi58RRzPjPE/FkuZ7cFHgMWhd/DpXbq/sGL5YLAMUVt0HaMLw6W7+na ee2nQbX2kWZx8FZ483AAM8kOK/elfgVXlutDeATCeVzCvQtgNkRMP3w9LWL54WQwlioX oUIaHqxkYv+aymveOan08ZCH16kDKjYte3YZ4AgQrbMBHUN6FRcJmLHwLvj/cKREQJ6F NbXpuNuvazPegzLfEa/S1Oqfg8SZc6lwh7S6CJ+IHb43l50ibOtF1/lQd8KFzq6eyjZ2 oEm3PWwo7HgbJlttHmeGzCAKGJFgIavsyXN5sXrpqy8A0KjsBlDvIxjj2tExOWssRwhA cLXA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=UmTrnhK6GtkNJpVqF4y+hp9qhwqq+Ui/RdrWymTw2tw=; b=dafrxbNCXadxBV/nsf7W2r84rnInmiDKp74p1mowrVt4ZEfPEToXcXXVkNik/OkwCm M/hyg5cyn41xgzRwLriEKBUVwDYhgCHqAOjH5R1B6kI2Qsukxwf0zfsk55OCg48DT2H7 1S1ZZf5uV01Pp0ePMnnaSQZMW6hI4rQcetrptNt79d0mKMVXo2L70eV9AQMeCsKoJfYT JCyzSFXRdDWXNBh43zzgMLvIheMSnNg++KENmTDIWovG7XnhR7PX9EB3LboSti/mmq6K nPaEmXkRE9OdJDuZU3V7oPhP6PwRfK/CaBbiYS87JE84hy7vj6YTDlW3R2Zt6A45BK3z pifg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYSdpe3Oa61KZDCiL+qEFsh9JofnUHYjtA61dbLB7Q8SiGtFZBo Qx7qCuJCcPAf2oaS8zY9CWY= X-Google-Smtp-Source: AHgI3IYIUHJ+73zhAmrSE/uGN447z08KAoPcrJDZof4eDh4nqFGREU4MotUs97Elahlsinm/CMLsag== X-Received: by 2002:aca:5884:: with SMTP id m126mr5101oib.4.1549891341266; Mon, 11 Feb 2019 05:22:21 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6830:164a:: with SMTP id h10ls1884368otr.7.gmail; Mon, 11 Feb 2019 05:22:21 -0800 (PST) X-Received: by 2002:a05:6830:1212:: with SMTP id r18mr327019otp.0.1549891340861; Mon, 11 Feb 2019 05:22:20 -0800 (PST) Date: Mon, 11 Feb 2019 05:22:20 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_97_1257948308.1549891340225" X-Original-Sender: atmacen@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_97_1257948308.1549891340225 Content-Type: multipart/alternative; boundary="----=_Part_98_635159258.1549891340225" ------=_Part_98_635159258.1549891340225 Content-Type: text/plain; charset="UTF-8" I'm not convinced that I've made a mistake about Nuprl. If had mistakenly taken realizers to be the proof objects, then *all* equality would be definitional. That's not what I'm saying. The untyped beta conversion is special because beta normalization can be automatically used as necessary by all tactics invoked in the proof object. That means all proof objects (following this approach) are robust to "perturbations" that are beta conversions. Like I said, I'm not sure Nuprl folks do that. If not, you are technically correct that definitional equality is alpha. But they can and should do that. So the design of the system fully supports definitional beta conversion. (And nothing more.) Your exhortation was not pointless. I agreed with it, and attempted to explain the reason for the difference in more detail. On Monday, February 11, 2019 at 8:03:26 AM UTC-5, Jonathan Sterling wrote: > > Hi Matt, I don't have time to get sucked further into this conversation, > but let me just say that what you are saying about "untyped definitional > equality" and beta about nuprl is not accurate, or at least, it is not > accurate if you take the broad definition of 'definitional equality' that I > set in my message. > > The lack of coercions in the realizers is true, but I did (apparently > pointlessly) exhort readers to not confuse a realizer with a proof. There > are coercions in the proof objects -- we must compare apples with apples. > > On Mon, Feb 11, 2019, at 3:23 AM, Matt Oliveri wrote: > > On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling > > wrote: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 -- > > > > A discussion of the usability of propositional equality would not be > > complete without distinguishing equality that's reflective, or at least > > "subsumptive", from equality that's merely strict. Subsumptive equality > > is when the equality elimination rule rewrites in the type of a term > > without changing the term. There are no coercions. The way reflective > > equality is implemented in Nuprl is essentially a combination of > > subsumptive equality and extensionality principles. In ITT + UIP or > > Observational TT (OTT), there's a strict propositional equality, but > > you still have coercions. > > > > I see the avoidance of coercions as the main practical benefit of > > Nuprl's approach. > > > > One's approach to automation of equality checking is somewhat > > orthogonal, and I'm less opinionated about that. A number of dependent > > type systems exist based on an idea of Aaron Stump to use a combination > > of some algorithmic equality, and subsumptive (but non-extensional, > > non-reflective) equality. My impression is that Zombie is one such > > system. > > > > > usually Nuprl is characterized as using equality reflection, but this > is not totally accurate (though there is a sense in which it is true). > > > > To clarify, it depends on what you take to be judgmental equality. If > > it's the equality that determines what's well-typed, then Nuprl has > > equality reflection. Of course no useful system will implement > > reflective equality as an algorithm, since it's infeasible. So any > > algorithmic equality will be some other equality judgment. But the > > "real" judgmental equality is precisely the equality type. (As you say > > later.) > > > > > 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. > > > > Interesting. So you're counting Nuprl's proof trees and, say, Agda's > > terms as proof objects? > > > > But what about Nuprl's direct computation rules? These allow untyped > > beta reduction and expansion anywhere in a goal. This justifies > > automatic beta normalization by all tactics. I don't know if Nuprlrs > > take advantage of this, but I think they should. > > > > > 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. > > > > To clarify, the realizers in Nuprl are Nuprl's *terms*. They are what > > get normalized; they are what appear in goals. The thing in Coq > > corresponding most closely to Nuprl's proof trees are Coq's proof > > scripts, not terms. The passage from Nuprl's proofs to terms is called > > "witness extraction", and is superficially similar to Coq's program > > extraction, but its role is completely different. A distinction between > > proof objects and terms is practically necessary to avoid coercions, > > since you still need to tell the proof assistant how to use equality > > *somehow*. In other words, whereas Coq's proof scripts are an extra, > > Nuprl's proof engine is primitive. (Similarly, in Andromeda, the > > distinction between AML programs and terms is necessary.) > > > > > ...the equality type (a judgment whose derivations are crucially taken > only up to alpha, rather than up to beta/eta/xi). > > > > Although you may wish otherwise, Nuprl's judgments all respect > > computational equivalence, which includes beta conversion. (This is the > > justification of the direct computation rules.) > > > > > 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. > > > > This doesn't seem right, since Nuprl effectively has untyped beta > > conversion as definitional equality. So I would say it *is* essential > > that Nuprl is intrinsically untyped. Its untyped definitional equality > > is all about the underlying untyped computation system. > > > > > 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. > > > > This is an interesting comparison. But because I consider Nuprl as > > having untyped definitional equality, and a powerful approach to > > avoiding coercions, I have to disagree strongly. By your argument, > > Thorsten's proposal would be at least as bad as Nuprl. (For practical > > usability.) But I think it would probably be much worse, because I > > think Nuprl is pretty good. Some of that is because of beta conversion. > > But avoiding coercions using subsumptive equality is also really > > powerful. Thorsten didn't say, but I'm guessing his proposal wouldn't > > use that. > > > > (I would really like it if Nuprl could be accurately likened to some > > other proposal, since it'd probably get more people thinking about it. > > Oh well. The most similar systems to Nuprl, other than its successors, > > are Andromeda, with reflective equality, and the Stump lineage I > > mentioned, with subsumptive equality. PVS, Mizar, and F* might be > > similar too.) > > > > The main purpose of this message is not to disagree with you, Jon. I'm > > mostly trying to sing the praises of Nuprl, because I feel that you've > > badly undersold it. > > > > I don't know what the best way to deal with dependent types is. But I > > think avoiding type annotations and coercions while getting extensional > > equality is really good. I don't know about avoiding *all* type > > annotations; maybe that makes automation too hard. But I suspect the > > ideal proof assistant will be more like Nuprl than like Coq or Agda. > -- 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. ------=_Part_98_635159258.1549891340225 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I'm not convinced that I've made a mistake about N= uprl. If had mistakenly taken realizers to be the proof objects, then *all*= equality would be definitional. That's not what I'm saying. The un= typed beta conversion is special because beta normalization can be automati= cally used as necessary by all tactics invoked in the proof object. That me= ans all proof objects (following this approach) are robust to "perturb= ations" that are beta conversions. Like I said, I'm not sure Nuprl= folks do that. If not, you are technically correct that definitional equal= ity is alpha. But they can and should do that. So the design of the system = fully supports definitional beta conversion. (And nothing more.)

You= r exhortation was not pointless. I agreed with it, and attempted to explain= the reason for the difference in more detail.

On Monday, February 1= 1, 2019 at 8:03:26 AM UTC-5, Jonathan Sterling wrote:
Hi Matt, I don't have time to get sucked further= into this conversation, but let me just say that what you are saying about= "untyped definitional equality" and beta about nuprl is not accu= rate, or at least, it is not accurate if you take the broad definition of &= #39;definitional equality' that I set in my message.

The lack of coercions in the realizers is true, but I did (apparently p= ointlessly) exhort readers to not confuse a realizer with a proof. There ar= e coercions in the proof objects -- we must compare apples with apples.=20

On Mon, Feb 11, 2019, at 3:23 AM, Matt Oliveri wrote:
> On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterli= ng=20
> wrote:But this approach is not likely to yield *proof assistants* = that=20
> are more usable than existing systems which have replaced definiti= onal=20
> equality with propositional equality.=20
> > =C2=A0
> > I am referring to Nuprl --
>=20
> A discussion of the usability of propositional equality would not = be=20
> complete without distinguishing equality that's reflective, or= at least=20
> "subsumptive", from equality that's merely strict. S= ubsumptive equality=20
> is when the equality elimination rule rewrites in the type of a te= rm=20
> without changing the term. There are no coercions. The way reflect= ive=20
> equality is implemented in Nuprl is essentially a combination of= =20
> subsumptive equality and extensionality principles. In ITT + UIP o= r=20
> Observational TT (OTT), there's a strict propositional equalit= y, but=20
> you still have coercions.
>=20
> I see the avoidance of coercions as the main practical benefit of= =20
> Nuprl's approach.
>=20
> One's approach to automation of equality checking is somewhat= =20
> orthogonal, and I'm less opinionated about that. A number of d= ependent=20
> type systems exist based on an idea of Aaron Stump to use a combin= ation=20
> of some algorithmic equality, and subsumptive (but non-extensional= ,=20
> non-reflective) equality. My impression is that Zombie is one such= =20
> system.
>=20
> > usually Nuprl is characterized as using equality reflection, = but this is not totally accurate (though there is a sense in which it is tr= ue).
>=20
> To clarify, it depends on what you take to be judgmental equality.= If=20
> it's the equality that determines what's well-typed, then = Nuprl has=20
> equality reflection. Of course no useful system will implement=20
> reflective equality as an algorithm, since it's infeasible. So= any=20
> algorithmic equality will be some other equality judgment. But the= =20
> "real" judgmental equality is precisely the equality typ= e. (As you say=20
> later.)
>=20
> > 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 de= finitionally equal to J', then D is also already a proof of J'. Def= initional equality is the silent equality. In most formalisms, definitional= equality includes some combination of alpha/beta/eta/xi, but in Nuprl is i= ncluded ONLY alpha.
>=20
> Interesting. So you're counting Nuprl's proof trees and, s= ay, Agda's=20
> terms as proof objects?
>=20
> But what about Nuprl's direct computation rules? These allow u= ntyped=20
> beta reduction and expansion anywhere in a goal. This justifies=20
> automatic beta normalization by all tactics. I don't know if N= uprlrs=20
> take advantage of this, but I think they should.
>=20
> > Proof objects must NOT be confused with realizers, of course = -- just like we do not confuse Coq proofs with the OCaml code that they cou= ld be extract to.
>=20
> To clarify, the realizers in Nuprl are Nuprl's *terms*. They a= re what=20
> get normalized; they are what appear in goals. The thing in Coq=20
> corresponding most closely to Nuprl's proof trees are Coq'= s proof=20
> scripts, not terms. The passage from Nuprl's proofs to terms i= s called=20
> "witness extraction", and is superficially similar to Co= q's program=20
> extraction, but its role is completely different. A distinction be= tween=20
> proof objects and terms is practically necessary to avoid coercion= s,=20
> since you still need to tell the proof assistant how to use equali= ty=20
> *somehow*. In other words, whereas Coq's proof scripts are an = extra,=20
> Nuprl's proof engine is primitive. (Similarly, in Andromeda, t= he=20
> distinction between AML programs and terms is necessary.)
>=20
> > ...the equality type (a judgment whose derivations are crucia= lly taken only up to alpha, rather than up to beta/eta/xi).
>=20
> Although you may wish otherwise, Nuprl's judgments all respect= =20
> computational equivalence, which includes beta conversion. (This i= s the=20
> justification of the direct computation rules.)
>=20
> > Nuprl is in essence what it looks like to remove all definiti= onal equalities and replace them with internal equalities. The main differe= nce between Nuprl and Thorsten's proposal is that Nuprl's underlyin= g objects are untyped -- but that is not an essential part of the idea.
>=20
> This doesn't seem right, since Nuprl effectively has untyped b= eta=20
> conversion as definitional equality. So I would say it *is* essent= ial=20
> that Nuprl is intrinsically untyped. Its untyped definitional equa= lity=20
> is all about the underlying untyped computation system.
>=20
> > The reason I bring this up is that the question of whether su= ch an idea can be made usable, namely using a formalism with only alpha equ= ivalence regarded silently/definitionally, and all other equations mediated= through the equality type, can be essentially reduced to the question of w= hether Nuprl is practical and usable, or whether it is possible to implemen= t a version of that idea which is practical and usable.
>=20
> This is an interesting comparison. But because I consider Nuprl as= =20
> having untyped definitional equality, and a powerful approach to= =20
> avoiding coercions, I have to disagree strongly. By your argument,= =20
> Thorsten's proposal would be at least as bad as Nuprl. (For pr= actical=20
> usability.) But I think it would probably be much worse, because I= =20
> think Nuprl is pretty good. Some of that is because of beta conver= sion.=20
> But avoiding coercions using subsumptive equality is also really= =20
> powerful. Thorsten didn't say, but I'm guessing his propos= al wouldn't=20
> use that.
>=20
> (I would really like it if Nuprl could be accurately likened to so= me=20
> other proposal, since it'd probably get more people thinking a= bout it.=20
> Oh well. The most similar systems to Nuprl, other than its success= ors,=20
> are Andromeda, with reflective equality, and the Stump lineage I= =20
> mentioned, with subsumptive equality. PVS, Mizar, and F* might be= =20
> similar too.)
>=20
> The main purpose of this message is not to disagree with you, Jon.= I'm=20
> mostly trying to sing the praises of Nuprl, because I feel that yo= u've=20
> badly undersold it.
>=20
> I don't know what the best way to deal with dependent types is= . But I=20
> think avoiding type annotations and coercions while getting extens= ional=20
> equality is really good. I don't know about avoiding *all* typ= e=20
> annotations; maybe that makes automation too hard. But I suspect t= he=20
> ideal proof assistant will be more like Nuprl than like Coq or Agd= a.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_98_635159258.1549891340225-- ------=_Part_97_1257948308.1549891340225--