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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vk1-xa3c.google.com (mail-vk1-xa3c.google.com [IPv6:2607:f8b0:4864:20::a3c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 08d75f6a for ; Mon, 11 Feb 2019 13:38:00 +0000 (UTC) Received: by mail-vk1-xa3c.google.com with SMTP id b189sf5169726vke.21 for ; Mon, 11 Feb 2019 05:38:00 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549892279; cv=pass; d=google.com; s=arc-20160816; b=Z8Wnwz2WqZireL8KYs0f5pOIshutNSOi8n7Q7mI8P3B/7bl5DqJPZ3AO1rBmpqAVKl hrfkzjETPZ8UPT9XLxRXUlGISpqTm/l1NCsgguPjNZwKdK+DXuggGEHic2XlIJBkM3lP s5w0EZ65W6cVcNXLERJFKVGk3Jtru2L+w+xQTl3OgbPjorNSkt9na92+wc8O6jfj6ed4 bHki34Tjrcw2mQLvwliT4iLynHodiPw0y9OjSXSF4bw7TCyqIy1oX4Go1Lx5cBP4KcWM k6/uPtPEAUyMvGv10n65cgqwzZScWxgUMP2tSDfaFpI0z9z2JnXsHCk53cIDiDFoz+v0 uYNw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:subject:to:from :date:references:in-reply-to:message-id:user-agent:mime-version :sender:dkim-signature; bh=VDqdnOabGTWBa+X8s0W9rNvsxja1AA9/DiYkP6mDzfw=; b=CK5UZmpjjfOISmb8aE+AoHGH43Og/kwgzL8rskdQrlpesec5imnshL8fNoNjP+v+0g JvtBi+BVx7wMXrzV+QLQ4WbA9pmf2UN6YB2UerAYOc1l6/OSVCQ5ZkhLP8PsK5hfeOPt BSPXmpn11OW6WFGDoEB7uG+pM/FtNsz0Hui/88ocWhMLcOe6QAZvnqDcUERk0lsXFFSB uCSZf1mrd9l+9rgskXFvYegpRbg29cLJfg5dO+3igaADNnydp0r0IQ8gEB2ZIP374j1L 7bwogqmK4WbS4rMVV8j9AtjyHywVtMGtdV604RMrep9jHmDK38MHSMAJUuyUbOCloUpC 253A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=GAeZoiy7; spf=neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:user-agent:message-id:in-reply-to:references :date:from:to:subject:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=VDqdnOabGTWBa+X8s0W9rNvsxja1AA9/DiYkP6mDzfw=; b=FkYOjrzB4CUM41RIdWvv2QIHud0zj9uv2Ft3HK55wAF4eJNB5B2AFl4ZnEO3xmszKK n4Vbv6OdPLOpnYpFo5K1UIYv57WKKkl10Kb0Go2ym74OeqI7YSwfoKP3VqcnAuNaVA3k LFMB+rCtM/Eg7GMS6ZE6ESLAc4STm8zILJ868QjTW2Rr3+Zaedkhw6b5tsHTX+ZYYf5r Bf42LHVZbfdOSDCW5pbmQBX10IFvc3h8/HMPDgHOhXlZdjJy+PgrS16dotX9E5nhNUwn w314oNQzqoNcd6Kk9uPYN1iqpgKy6vAXCV5UPhTMqrGdQmA+dDdzvL0aQT9xXXts+QNQ suyQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:user-agent:message-id :in-reply-to:references:date:from:to:subject :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=VDqdnOabGTWBa+X8s0W9rNvsxja1AA9/DiYkP6mDzfw=; b=JcCmldcdAQ5RtrzLsyAvdLdDnbN6rFZ3p8SQaQb7qXca6TZLH31H1P4HCvSYZlF9ud fmo/Hva5NkLpBapk+enrVXysn9RqBTno+Mqjex/CGp8/abhoBDjv67C/TC1g4Aciy9vY Q/p1rVSWEiK84n7EYfS0qyUP7x1vWOjjtCmYBXuSDVvigX3r6kdd69yLHFbVU3wNzIqy Jui2EB9m9vwOh3criIwDjOA2fBZLR/Gus9cq4k40DYuG6+KnCU1Wo9dz47OFBbPsaU6j FGZWgnT87BGhDKVIV3KbkHFBrzvrI2I8xb0WF7GSr6t8T6jU6pKuayV22wq+RWx5a9Tx 8C7g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubjqFmt/7bBQ9c0Fp4pH5gS8WDd8oefw7ksPYW5nDQSTcbGHg+s uGVI/SA5ABShzZDo4N1dTkM= X-Google-Smtp-Source: AHgI3Ib9fVCd0HKf0Jgqj7RGpDcNm+BRVg6cJucPfLRyXA/G0zCRoR2uQXwDuMfzOtoS0wT2vW4CUw== X-Received: by 2002:a67:7e8c:: with SMTP id z134mr93403vsc.6.1549892279679; Mon, 11 Feb 2019 05:37:59 -0800 (PST) MIME-Version: 1.0 X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:7d04:: with SMTP id y4ls2751730vsc.2.gmail; Mon, 11 Feb 2019 05:37:59 -0800 (PST) X-Received: by 2002:a67:4502:: with SMTP id s2mr25143922vsa.11.1549892279306; Mon, 11 Feb 2019 05:37:59 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549892279; cv=none; d=google.com; s=arc-20160816; b=sbONlPmLnwJGs7hu2rgC+05WYMVu/wg0dUOgOMcHXDb1S58Jd//1tmmnmRyK/bbyLI mcNOsHHIvNADeyNSLRKfGygzTuDlc2VI295FRK2vPTMnklpM3ydIIx0q59vJiHpVTuna 2dPBrmovRsmRzGGDe6gbpZDwHyeYtYnN0jmzvKUXB/2F9/zVTsXcnq1Y+FJosrKKNjbz IS2w0DwbeiOVq6BM0ABCYK+hB1Zp0WhLUKpFZZfDNPf7Mp7m788NuvbTXP+GY6UjH0Gx pT61UERPoVcodPGLUUimWf2RLcOcT/KG2gC4M8YFmpRYcQYJfaWXQX71fY2XP3eyHPBK t0jg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:to:from:date:references :in-reply-to:message-id:user-agent:dkim-signature; bh=a5X0QALuuB71CKODI+YsxOs3+hLl4iYrVy9OAy2//so=; b=tI6YpzLVIW3AfMHRiUFW4CTeO8R6JJVTNLrmiw6vY5lB3XadrOBkIL7ax+cl74z5zh pDbcEODKRawMBja5lMp14XSm0o58BJjvzaVlE0NbrsjmEZ/8uhn5iLO6S+iuRuTjMlnO tjY+c7+dXHMzYzFlcDQnTXh5gQmKa2eJh9+xjHmqmrzp2R5RlLjQ+sclNeg3Gnv01U5H rLDwJdSnhegY2xgThbnnNAaAj5ouPZXh6nzqwacf3tqBMlCI2PD7u5KUcAWo6eOlXQyH kKUpmntvPSv66TZz9SokbOj17QyHjjrquXOz9TiQ4sRtWvpWS8hs747SsppkYJFBvVM4 yCuA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=GAeZoiy7; spf=neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from wout2-smtp.messagingengine.com (wout2-smtp.messagingengine.com. [64.147.123.25]) by gmr-mx.google.com with ESMTPS id z24si686940uar.0.2019.02.11.05.37.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 05:37:59 -0800 (PST) Received-SPF: neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=64.147.123.25; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.west.internal (Postfix) with ESMTP id F3A3330B5 for ; Mon, 11 Feb 2019 08:37:57 -0500 (EST) Received: from imap3 ([10.202.2.53]) by compute2.internal (MEProxy); Mon, 11 Feb 2019 08:37:58 -0500 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedtledrleelgdefjecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfhuthenuceurghilhhouhhtmecufedt tdenucesvcftvggtihhpihgvnhhtshculddquddttddmnegoufhushhpvggtthffohhmrg hinhculdegledmnecujfgurhepofgfkfgjfhffhffvufgtgfesthhqredtreertdenucfh rhhomhepfdflohhnucfuthgvrhhlihhnghdfuceojhhonhesjhhonhhmshhtvghrlhhinh hgrdgtohhmqeenucffohhmrghinhepghhoohhglhgvrdgtohhmnecurfgrrhgrmhepmhgr ihhlfhhrohhmpehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomhenucevlhhushhtvg hrufhiiigvpedt X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 4D7917C173; Mon, 11 Feb 2019 08:37:57 -0500 (EST) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.1.5-832-gba113d7-fmstable-20190201v1 X-Me-Personality: 19972253 Message-Id: In-Reply-To: References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> Date: Mon, 11 Feb 2019 08:37:56 -0500 From: "Jon Sterling" To: "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Re: Why do we need judgmental equality? Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=GAeZoiy7; spf=neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.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: , Hi Matt, my final comment is just to clarify that even if you take the tact= ic trees as the proof objects (which is a position that I think is fine to = argue), it is not acceptable to say that they are robust to "beta perturbat= ions", because if your tactics run beta rules automatically, it is trivial = for me to cook up an example where a beta-perturbation would make your tact= ic script fail to terminate (even if the theorem is true). This is because = in Nuprl, you are often working with fixed points (a very cool feature!), a= nd must be circumspect in the computation rules that you apply to them -- f= or instance, consider proving something about an infinite stream of binary = digits. The "substitutive" or "perturbative equality" in Nuprl is indeed al= pha, I can confirm, regardless of whether you are thinking of tactic script= s or finished proofs as the proof objects. I just want to re-emphasize what Mike was saying about "ideas" being so fuz= zy that they can be characterized using multiple, conflicting explanations = -- definitional equality is one of these things, and is a scientific or phi= losophical concept rather than a technical concept (as Martin-Lof convincin= gly argued in the 1970s in his famous paper on definitional equality). You= may have your own way to understand what is happening in Nuprl, and that's= ok --- but the way that I am propounding in this thread is an analogy that= allows us to compare apples with apples, a very difficult thing to do in t= his context. If there is anything mathematical to be said about these thing= s, we need a common technical basis, and it seems like the simplest way to = do that is to analyze what function definitional equality plays in practice= -- it is the thing which (1) doesn't require proof, and (2) doesn't add an= y coercions to the thing that counts as proof. That is the "universal prope= rty" of definitional equality. I'm too busy to respond further (paper deadline!), so I would request that = people wait a few days to contact me about it :) On Mon, Feb 11, 2019, at 8:22 AM, Matt Oliveri wrote: > I'm not convinced that I've made a mistake about Nuprl. If had=20 > mistakenly taken realizers to be the proof objects, then *all* equality= =20 > would be definitional. That's not what I'm saying. The untyped beta=20 > conversion is special because beta normalization can be automatically=20 > used as necessary by all tactics invoked in the proof object. That=20 > means all proof objects (following this approach) are robust to=20 > "perturbations" that are beta conversions. Like I said, I'm not sure=20 > Nuprl folks do that. If not, you are technically correct that=20 > definitional equality is alpha. But they can and should do that. So the= =20 > design of the system fully supports definitional beta conversion. (And=20 > nothing more.) >=20 > Your exhortation was not pointless. I agreed with it, and attempted to=20 > explain the reason for the difference in more detail. >=20 > On Monday, February 11, 2019 at 8:03:26 AM UTC-5, Jonathan Sterling=20 > wrote:Hi Matt, I don't have time to get sucked further into this=20 > conversation, but let me just say that what you are saying about=20 > "untyped definitional equality" and beta about nuprl is not accurate,=20 > or at least, it is not accurate if you take the broad definition of=20 > 'definitional equality' that I set in my message.=20 > > =20 > > 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 > > =20 > > On Mon, Feb 11, 2019, at 3:23 AM, Matt Oliveri wrote:=20 > > > On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling= =20 > > > wrote:But this approach is not likely to yield *proof assistants* tha= t=20 > > > are more usable than existing systems which have replaced definitiona= l=20 > > > equality with propositional equality.=20 > > > >=20 > > > > I am referring to Nuprl --=20 > > >=20 > > > A discussion of the usability of propositional equality would not be= =20 > > > complete without distinguishing equality that's reflective, or at lea= st=20 > > > "subsumptive", from equality that's merely strict. Subsumptive equali= ty=20 > > > is when the equality elimination rule rewrites in the type of a term= =20 > > > without changing the term. There are no coercions. The way reflective= =20 > > > equality is implemented in Nuprl is essentially a combination of=20 > > > subsumptive equality and extensionality principles. In ITT + UIP or= =20 > > > Observational TT (OTT), there's a strict propositional equality, but= =20 > > > you still have coercions.=20 > > >=20 > > > I see the avoidance of coercions as the main practical benefit of=20 > > > Nuprl's approach.=20 > > >=20 > > > One's approach to automation of equality checking is somewhat=20 > > > orthogonal, and I'm less opinionated about that. A number of dependen= t=20 > > > type systems exist based on an idea of Aaron Stump to use a combinati= on=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 > > >=20 > > > > usually Nuprl is characterized as using equality reflection, but th= is is not totally accurate (though there is a sense in which it is true).= =20 > > >=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 type. (As you sa= y=20 > > > later.)=20 > > >=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 definitionally equ= al to J', then D is also already a proof of J'. Definitional equality is th= e silent equality. In most formalisms, definitional equality includes some = combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha.=20 > > >=20 > > > Interesting. So you're counting Nuprl's proof trees and, say, Agda's= =20 > > > terms as proof objects?=20 > > >=20 > > > But what about Nuprl's direct computation rules? These allow untyped= =20 > > > beta reduction and expansion anywhere in a goal. This justifies=20 > > > automatic beta normalization by all tactics. I don't know if Nuprlrs= =20 > > > take advantage of this, but I think they should.=20 > > >=20 > > > > Proof objects must NOT be confused with realizers, of course -- jus= t like we do not confuse Coq proofs with the OCaml code that they could be = extract to.=20 > > >=20 > > > To clarify, the realizers in Nuprl are Nuprl's *terms*. They are 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 is calle= d=20 > > > "witness extraction", and is superficially similar to Coq's program= =20 > > > extraction, but its role is completely different. A distinction betwe= en=20 > > > proof objects and terms is practically necessary to avoid coercions,= =20 > > > since you still need to tell the proof assistant how to use equality= =20 > > > *somehow*. In other words, whereas Coq's proof scripts are an extra,= =20 > > > Nuprl's proof engine is primitive. (Similarly, in Andromeda, the=20 > > > distinction between AML programs and terms is necessary.)=20 > > >=20 > > > > ...the equality type (a judgment whose derivations are crucially ta= ken only up to alpha, rather than up to beta/eta/xi).=20 > > >=20 > > > Although you may wish otherwise, Nuprl's judgments all respect=20 > > > computational equivalence, which includes beta conversion. (This is t= he=20 > > > justification of the direct computation rules.)=20 > > >=20 > > > > Nuprl is in essence what it looks like to remove all definitional e= qualities and replace them with internal equalities. The main difference be= tween Nuprl and Thorsten's proposal is that Nuprl's underlying objects are = untyped -- but that is not an essential part of the idea.=20 > > >=20 > > > This doesn't seem right, since Nuprl effectively has untyped beta=20 > > > conversion as definitional equality. So I would say it *is* essential= =20 > > > that Nuprl is intrinsically untyped. Its untyped definitional equalit= y=20 > > > is all about the underlying untyped computation system.=20 > > >=20 > > > > 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 equivalen= ce regarded silently/definitionally, and all other equations mediated throu= gh 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 ve= rsion of that idea which is practical and usable.=20 > > >=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 practical= =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 conversio= n.=20 > > > But avoiding coercions using subsumptive equality is also really=20 > > > powerful. Thorsten didn't say, but I'm guessing his proposal wouldn't= =20 > > > use that.=20 > > >=20 > > > (I would really like it if Nuprl could be accurately likened to some= =20 > > > other proposal, since it'd probably get more people thinking about it= .=20 > > > Oh well. The most similar systems to Nuprl, other than its successors= ,=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 > > >=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 you'v= e=20 > > > badly undersold it.=20 > > >=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 extension= al=20 > > > equality is really good. I don't know about avoiding *all* type=20 > > > annotations; maybe that makes automation too hard. But I suspect the= =20 > > > ideal proof assistant will be more like Nuprl than like Coq or Agda. > =20 >=20 >=20 > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.