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-it1-x137.google.com (mail-it1-x137.google.com [IPv6:2607:f8b0:4864:20::137]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d31f1cb7 for ; Mon, 11 Feb 2019 13:03:27 +0000 (UTC) Received: by mail-it1-x137.google.com with SMTP id m1sf4938232ita.9 for ; Mon, 11 Feb 2019 05:03:27 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549890206; cv=pass; d=google.com; s=arc-20160816; b=qkJnx4xst88ZNGf6wKCFsAL364W/G8DFk5znKN1Fz7xCSWIpGMT01f4w+NlpxLZl8x m+dgQhCYZBLEldEw1W1D9xvQprO6CQUFp34v4rFzeQWyc3ckJr5fGQteYfl1KJn7ify0 FnGsAGhABaaUc7qm8C7fOswL5AOIsMCcncu8B3z1w3Xe8CtSBzdwmilNvtMYCrDWS/wM lIhY44JsMdka3Lkez7kGGLKoJAlKhvmXpmodg34PvI7ABSfDp0upVn/4BGYXCvF+gJeG cw7SWCsFDv+gtjIB3SgP92AqiglbN+QXIbW0qhizqQ6wX1U1fCYtzwjQVmvWTwF8H8hS fAKQ== 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=oIcI1KRuPNfyFqzv6RzIa/+2uIM7q7nQhmTaFxL5HTg=; b=gF76MK77RXwXY4cVaOZJviRFLDE5lhPEHfjoA2mfDhpSVL38zRw3uOaoKBApcOLZTw 8T9yddc5bgbxai2f/vmF3m2vWOq/qbPBQvSlL6PRrTKv/YLhVs6cdutL+wKa6DHQQFxL u/H0/qXnI2TuIjLE9ZdbteDIH3PsQdUaJD5O91upzAE5AyuMoRKjELXerJrAfpJts6cF hFQQlBfsaW9E2VxqYFytfesodawOCl1KsIIvccmza4rjAn1b33pRXG97iKZd1MwtphR2 G58ObOl2jtGEYzQRrejO8J7NutUqyDwc6LYtJC56zcUlu/zDHlsOgH88kxP8mfXc5GCJ 3KIA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=wmGZvFhN; 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:x-original-sender :x-original-authentication-results:content-transfer-encoding :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=oIcI1KRuPNfyFqzv6RzIa/+2uIM7q7nQhmTaFxL5HTg=; b=cTX3GhdLHyXY1NiUK4SNPQ7hV/TCx2325ufaxrYztdvIoe6TiodzZ/HPA6KJB1hGfJ PKxrQnVl0O9+6zd6knO52tY8TJi1Yz/ldsd4+kxUpK9aBnvM2MNjs31urFcVZgo7Z/ij JC3oRwq93sp302Flsrypb7F4HUwNWtOgvBPfru8EUEg/vqsZ+EDHZAz06Ppi3hlkU1wx FUNvpsz+PcY8s8qY+pBrQdVMhf6ARdBBBRfaUUqvOVjHNaMEIwqe9OeWaHJonSwN3BH/ Xuo7qfw4bRC9U581vB+IzTEqex1pHJ1e+9dshkwZkDV6yW8rJ0m5lgq4SvypdVJkmq1a sy8A== 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:x-original-sender :x-original-authentication-results:content-transfer-encoding :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-unsubscribe; bh=oIcI1KRuPNfyFqzv6RzIa/+2uIM7q7nQhmTaFxL5HTg=; b=XH5828SULEP56II6jOXsMFdtcUnhIfvOgRHsZ9ysvgrfEamptktXo0Hp8+WosTcvPK jkgQH7fdYv4z/XRVnrCUHszeVPEIlmHSUGRJ+X8tamLEefL1jAvtnjyQ1W5G7T9+gW3i C/Gf490yCloCbEZ4dJRJ+dMieSgFRXi0w2mbUcx7zRPShuSxNOLsthzwJwgmGKkVqDNV nCLEPtZvhRrjqbr1RVa3FrzxZSVVrtcWINcUC/BoWOwvDelmBv7ofT2KFfVhWsu04WDo UutIGQaDReY+wqviJqpablvCvo2+9UUi4JEM3dUU7+k1dhVlIY41CptJlsQbx38KAQOn oc/A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZLRuebQsVEl1ZIJIKNtDF+dTKM9fQ5vE4ZEyQMee84kzJFhlrm /y9yw4aDSpPaQZQhBsRnsXc= X-Google-Smtp-Source: AHgI3IbZhVoPeQaT4sBJpUU/IU7n5G41Elo8Kk4l//pkN/qSAYzB2tXZ+b1hbiaXLaqzLWqtMDvK1w== X-Received: by 2002:a24:4353:: with SMTP id s80mr31918itb.1.1549890206443; Mon, 11 Feb 2019 05:03:26 -0800 (PST) MIME-Version: 1.0 X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:ed02:: with SMTP id n2ls345953iog.2.gmail; Mon, 11 Feb 2019 05:03:26 -0800 (PST) X-Received: by 2002:a5d:8794:: with SMTP id f20mr960295ion.32.1549890206096; Mon, 11 Feb 2019 05:03:26 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549890206; cv=none; d=google.com; s=arc-20160816; b=Gmpptb9ywYxpgWPW7EWKZVIn83sGPJC4dmM1zsCGqsSF/1gOfGs7WmRYCwv5ZF8HK6 65ufOweIGNKr783mrtdw/m2Me4e9OqUvPv6KLf1pnfkSAgCjV+Bt8WglV/edmXekjKaA aNkkb0YZ+j/c5GUq/h4mHPiwz8eaaUOcTnPd7/YN0S+nbk91aRwGQc4lcF56dURoiEol SLb+0c4n65y4NgAD1cLn5OVdHyXbwhjzvgs/l0lcSAVNkGxXgnG+2EhLk3JAI1pAFKTl 9UsWMdG2urTkVXdsyMt9lzTjijIFRP+lEP5y1i4lAgV+w5k+F4iuQ+Z1qxNnf5aQOGQG UvCA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=subject:to:from:date:references:in-reply-to:message-id:user-agent :dkim-signature; bh=LYL2/IA/L3mWYHjJyPqu9c/we18EPTTMuo4wvkPpfzA=; b=ewajfFFs0id7LEZCLRW4OfjPnV9zsxPL92jZ46n74s/bRdmvdav9YQf2FS6YS5TW6F qTbxgpVNHUU6tbHdbIUrhbETwWS8C/fuXjZtRoH2JqjBdIruA1gUTULKKRz1oBOnfgLl w/NSIuWxYj04PnA3o9uMZ6z3CbEhd01pevowCNZKb3sIjHAl633/nhLHj19hBFmfcfwi EC6HGWKuRaeY4ZIYjl+xszLcvsnLLOBkccbvCOu0t2tYAAJ+yJ6CkZhvrzQVR2ICAW/p 0P3OZZz5FZVSd/CjqVy1eZ4e9fQWPuCezPM6VhhU97JV9aGY8LcFxhNa5hVpKuMB6o3W j8+g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=wmGZvFhN; 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 204si457866itw.2.2019.02.11.05.03.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 05:03:25 -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 54B7730A8 for ; Mon, 11 Feb 2019 08:03:24 -0500 (EST) Received: from imap3 ([10.202.2.53]) by compute2.internal (MEProxy); Mon, 11 Feb 2019 08:03:24 -0500 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedtledrleelgdeftdcutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfhuthenuceurghilhhouhhtmecufedt tdenucesvcftvggtihhpihgvnhhtshculddquddttddmnegoufhushhpvggtthffohhmrg hinhculdegledmnecujfgurhepofgfkfgjfhffhffvufgtsehttdertderredtnecuhfhr ohhmpedflfhonhcuufhtvghrlhhinhhgfdcuoehjohhnsehjohhnmhhsthgvrhhlihhngh drtghomheqnecuffhomhgrihhnpehgohhoghhlvgdrtghomhenucfrrghrrghmpehmrghi lhhfrhhomhepjhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhmnecuvehluhhsthgvrh fuihiivgeptd X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 983F57C355; Mon, 11 Feb 2019 08:03:23 -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:03:22 -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" 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=wmGZvFhN; 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 Content-Transfer-Encoding: quoted-printable 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, I don't have time to get sucked further into this conversation, bu= t let me just say that what you are saying about "untyped definitional equa= lity" 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 point= lessly) exhort readers to not confuse a realizer with a proof. There are co= ercions 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 Sterling=20 > wrote:But this approach is not likely to yield *proof assistants* that=20 > are more usable than existing systems which have replaced definitional=20 > equality with propositional equality.=20 > > =20 > > 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. Subsumptive equality= =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 > 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 dependent=20 > type systems exist based on an idea of Aaron Stump to use a combination= =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 i= s not totally accurate (though there is a sense in which it is true). >=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 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 definitionally equal t= o J', then D is also already a proof of J'. Definitional equality is the si= lent equality. In most formalisms, definitional equality includes some comb= ination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha. >=20 > Interesting. So you're counting Nuprl's proof trees and, say, Agda's=20 > terms as proof objects? >=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 > > Proof objects must NOT be confused with realizers, of course -- just li= ke we do not confuse Coq proofs with the OCaml code that they could be extr= act to. >=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 called=20 > "witness extraction", and is superficially similar to Coq's program=20 > extraction, but its role is completely different. A distinction between= =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 > > ...the equality type (a judgment whose derivations are crucially 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 is the= =20 > justification of the direct computation rules.) >=20 > > Nuprl is in essence what it looks like to remove all definitional equal= ities and replace them with internal equalities. The main difference betwee= n Nuprl and Thorsten's proposal is that Nuprl's underlying objects are unty= ped -- but that is not an essential part of the idea. >=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 equality=20 > is all about the underlying untyped computation system. >=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 equivalence r= egarded silently/definitionally, and all other equations mediated through t= he equality type, can be essentially reduced to the question of whether Nup= rl is practical and usable, or whether it is possible to implement a versio= n 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 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 conversion.= =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 > (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 > 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'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 extensional= =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.