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-x33f.google.com (mail-ot1-x33f.google.com [IPv6:2607:f8b0:4864:20::33f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 61e1d3e2 for ; Mon, 11 Feb 2019 08:23:04 +0000 (UTC) Received: by mail-ot1-x33f.google.com with SMTP id q11sf10207398otl.23 for ; Mon, 11 Feb 2019 00:23:04 -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=5a2bLHrzpuW1eAIm61f0h9VpqhRoeQqPXQKbhoEQMTo=; b=XzgNKXrsqaGYq68e9fG8l6yaaGboi/IamPMco6xdymODpDmny1Yw7FwrkTpCIsAsTb GvpNoHHupDaZFsx6EQpbX/8PB4fsLTg3qJ9PNNPWORmJNjmzqTmSAlcIS1y35dtSxbMb /e5ctwCJy+J0fum/YJ9TNN3HgbdPGlwVEKkZHQ1PLCeU6rM/HW3c0IpFaePDYKlTjqP+ rvoyzOc7a5PqMDFqnu+a4ppEapMODG5VWKPxgyPS1OnViEc/nGxsA5hw6YBcz+0Emfbw /F9+alibV+VM3Rx6zuhge68m3q+e+2nXGqQnyLUns/1BbWxK5EEfO7L+eHXGSfN13ZqA BD3Q== 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=5a2bLHrzpuW1eAIm61f0h9VpqhRoeQqPXQKbhoEQMTo=; b=NG9Lt7yKmevMFWw4a+xVUzllWLRempwPqYMW2OanMVP816DNvAJ6YbB0HZK6HxN0tl xcLY8IdhPKRZxPymp5g8DT8SrTcfm0H9ElRtuF0Ka8erVtUZUh2S5agbWcgLj06HauAu 3UePWyi6gzn6vr0uTFCA3BR9oOmD8EWg52VK0Z0mwU8F8qcaceq3E3h+fHkYtSgrYSDE lZfDG0cOoLnd5A+lLll2wGQ3Tek7m6g3NS5IcT2bVzvf5BTMPniUkQ9mFvJltfaCt6Qi a1THOt9UK4IuDq3IgFNF7cajHBHzeo1gF8miSFZ92FGz2PLtti61KiAnf8wuaGuoqjrJ 5QaQ== 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=5a2bLHrzpuW1eAIm61f0h9VpqhRoeQqPXQKbhoEQMTo=; b=CyO3BC5sm77a35+zvAMK1EejCE4YKEN4g9C4sx+AfKkzDaPpGBl6sbBEkMC5+9N0/Z /MNQrM/XoCfHvtcKvHulpilNwbc8hAcBDf5/AoG9n8fToyCR1xSroX6o94Xr5cqrS0r/ +o8wRU8bUMR41KbgPpzNh8zKuUU6Dlct5iw1xvgvqtQ3nOjaSX1QZ+66IRH1bo3zb4i9 0tc7+olIAvqS4i8RB/E9eWVLV2cHYLSHXqjgoEPhYnKnTXP1B5+ePzX340i5MV5HYPtp xc/rGMC5lD7raf63b5aW8f9L4qdpaHHQLW/0GJHkwXslnn7WM1DPnrL13Wr8H/FMpkQn wabQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAub+JemJtUnpDk5KTjdG6b/fKr7YnkNfhSa9Un+CabB/lvv0EDo/ m8tcYiEliYfTE7lp+Sspx64= X-Google-Smtp-Source: AHgI3IaKQFPJzQ9RruYD87wiIu+H7cVwFsPg+0SVf8cRtkUtWwJWWW0KoLklmup9+hv7jsGpE+5s1w== X-Received: by 2002:aca:4b89:: with SMTP id y131mr3642oia.3.1549873383472; Mon, 11 Feb 2019 00:23:03 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:5412:: with SMTP id i18ls5041325oib.5.gmail; Mon, 11 Feb 2019 00:23:03 -0800 (PST) X-Received: by 2002:a54:4d86:: with SMTP id y6mr78988oix.0.1549873382881; Mon, 11 Feb 2019 00:23:02 -0800 (PST) Date: Mon, 11 Feb 2019 00:23:02 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> 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_1085_587238284.1549873382297" 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_1085_587238284.1549873382297 Content-Type: multipart/alternative; boundary="----=_Part_1086_1251501753.1549873382297" ------=_Part_1086_1251501753.1549873382297 Content-Type: text/plain; charset="UTF-8" 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_1086_1251501753.1549873382297 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonatha= n Sterling wrote:
But this appr= oach is not likely to yield *proof assistants* that are more usable than ex= isting systems which have replaced definitional equality with propositional= equality.

I am referring to Nuprl --

A discussion of the usa= bility of propositional equality would not be complete without distinguishi= ng equality that's reflective, or at least "subsumptive", fro= m equality that's merely strict. Subsumptive equality is when the equal= ity elimination rule rewrites in the type of a term without changing the te= rm. There are no coercions. The way reflective equality is implemented in N= uprl is essentially a combination of subsumptive equality and extensionalit= y principles. In ITT + UIP or Observational TT (OTT), there's a strict = propositional equality, but you still have coercions.

I see the avoi= dance of coercions as the main practical benefit of Nuprl's approach.
One's approach to automation of equality checking is somewhat ort= hogonal, and I'm less opinionated about that. A number of dependent typ= e systems exist based on an idea of Aaron Stump to use a combination of som= e algorithmic equality, and subsumptive (but non-extensional, non-reflectiv= e) 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 the= re is a sense in which it is true).

To clarify, it dep= ends on what you take to be judgmental equality. If it's the equality t= hat determines what's well-typed, then Nuprl has equality reflection. O= f course no useful system will implement reflective equality as an algorith= m, since it's infeasible. So any algorithmic equality will be some othe= r equality judgment. But the "real" judgmental equality is precis= ely the equality type. (As you say later.)

When I say "definitional equality" fo= r 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&= #39;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 justif= ies automatic beta normalization by all tactics. I don't know if Nuprlr= s take advantage of this, but I think they should.

Proof objects must NOT be confused with r= ealizers, of course -- just like we do not confuse Coq proofs with the OCam= l code that they could be extract to.

To clarify, = the realizers in Nuprl are Nuprl's *terms*. They are what get normalize= d; they are what appear in goals. The thing in Coq corresponding most close= ly to Nuprl's proof trees are Coq's proof scripts, not terms. The p= assage from Nuprl's proofs to terms is called "witness extraction&= quot;, and is superficially similar to Coq's program extraction, but it= s role is completely different. A distinction between proof objects and ter= ms is practically necessary=20 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 Androm= eda, the distinction between AML programs and terms is necessary.)

<= /div>
...the equality type (a j= udgment whose derivations are crucially taken only up to alpha, rather than= up to beta/eta/xi).

Although you may wish otherwi= se, Nuprl's judgments all respect computational equivalence, which incl= udes 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 rep= lace them with internal equalities. The main difference between Nuprl and T= horsten's proposal is that Nuprl's underlying objects are untyped -= - but that is not an essential part of the idea.

T= his doesn't seem right, since Nuprl effectively has untyped beta conver= sion as definitional equality. So I would say it *is* essential that Nuprl = is intrinsically untyped. Its untyped definitional equality is all about th= e 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 equation= s mediated through the equality type, can be essentially reduced to the que= stion of whether Nuprl is practical and usable, or whether it is possible t= o implement a version of that idea which is practical and usable.

This is an interesting comparison. But because I consider N= uprl as having untyped definitional equality, and a powerful approach to av= oiding coercions, I have to disagree strongly. By your argument, Thorsten&#= 39;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 pret= ty good. Some of that is because of beta conversion. But avoiding coercions= using subsumptive equality is also really powerful. Thorsten didn't sa= y, 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 m= ost similar systems to Nuprl, other than its successors, are Andromeda, wit= h 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 exten= sional 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 &= 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_1086_1251501753.1549873382297-- ------=_Part_1085_587238284.1549873382297--