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-x338.google.com (mail-ot1-x338.google.com [IPv6:2607:f8b0:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2c6be04e for ; Tue, 12 Feb 2019 09:01:36 +0000 (UTC) Received: by mail-ot1-x338.google.com with SMTP id 4sf2027185otg.3 for ; Tue, 12 Feb 2019 01:01:36 -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=DgzDyIQikltINzMWY1LpuEAgN6eLuNG9UrftNOajtlo=; b=YcyWFCUQsxaBTJ+i5S3gKu5kwY9IGA7pLnvRolfXIwGYtyLZ77OqlokM+wi266pS+G cUglv9auWnjKZDSs+DrJvh1OBsMEgVoQS8DSgDq3eqVltoiU3j7+ygkAn+nupljor46j ImmSbYjwTW74K1tn97szgPwtObh0dA2xaInemhfY0V6K82IchE50qdTDGyy93wQxYZVW WP51/Xrhldo+GaEx6Cb02+nViy2B5Zf7ajkXZWT7/qmUkYDqGDh/XznBbsLR8EjNR0SM XAErYyS1xaNfIpDS0/9F8NryWmlUm1tDve5nqHbI4ZoX8XQa8yceTwCFzXpHDIQFkA6m r9Eg== 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=DgzDyIQikltINzMWY1LpuEAgN6eLuNG9UrftNOajtlo=; b=WiLpwANSQ7IMyMqefMfywqzSN1jcoiMeyhdpQV0M/5VzxWUx9lYjC8UifLCCZAX258 edrkflzbNDUBEgaQloyTivVU+4977B0yaI2ombwZTKoLGF/a63nfVxnD2TQ6YyEo7Nuu x71Y8odlXQk9GtCRqwygB2YLH/DnezOt9nluKlykJLZEFUr4jRtMgfuJQhhfZVfQAY8A QFJ8++GLlCiUOdGovjwWHjK2qSvZpgOmLiQ7fUfC5u79qHpTGJ4PElbfCNxEIe9DF6CU NlzsxPFu7qPOvPCC5A3NOHzSz6YZMsP3PAn5y9/RRkOq2+CUQ1AzWWMprOa/NUQfvGft UDRA== 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=DgzDyIQikltINzMWY1LpuEAgN6eLuNG9UrftNOajtlo=; b=SBD9EdTUoXJJooiKBVIxaCgNlYEfPPf5AOCpMMu0ELPuwYids2oFOquhXz6EZIw2nE YDONoMfStVwCwQTrH+ZG8sWdf8vhMMqM6oKfjiINTwzX8OvkkJ48kmIPbkZBvLucl8I8 BgQ15ybHvyq7xOcGn3/Sa6pihtI2MfvsVms1Egsy3SAwax3bg3JseGTVbUqV6i9JzQ3n cBp2S6slXidcfCNn6lDdDk+qj5sXvMHZJNghWaaFLVuhlRHso/mtY/SqQFJGNOjowHGo 1Ion09zrJ4y5kHaYYkFe6diRXxw7IXCRQgm+hrktxdlbujhbAkzTAFF0K2Tny0K6YAtk eF+g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZBQt3QUX5PXZOCwpUenbm8vkIYeAYR2T94O3RkMc0P1sgYrPh9 bmW5dzHS15C/NdvctB0uk1c= X-Google-Smtp-Source: AHgI3IbZ2CbpJoh7KT1Qe5mYupq7r/Tc5iIaJD6F1RjTbYwM3CxTro7wVATmAsJ2/SmdNqzjezCsRA== X-Received: by 2002:a9d:5e01:: with SMTP id d1mr62893oti.1.1549962094862; Tue, 12 Feb 2019 01:01:34 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:32c8:: with SMTP id u66ls10087331otb.0.gmail; Tue, 12 Feb 2019 01:01:34 -0800 (PST) X-Received: by 2002:a9d:2c22:: with SMTP id f31mr64159otb.4.1549962094470; Tue, 12 Feb 2019 01:01:34 -0800 (PST) Date: Tue, 12 Feb 2019 01:01:33 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <58de3e94-fee9-405c-ab18-5a35cb90eb68@googlegroups.com> In-Reply-To: References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> <7b35e7cb-3021-44cd-8c97-a7cc1159f999@googlegroups.com> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1741_1007127888.1549962093528" 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_1741_1007127888.1549962093528 Content-Type: multipart/alternative; boundary="----=_Part_1742_1743569968.1549962093528" ------=_Part_1742_1743569968.1549962093528 Content-Type: text/plain; charset="UTF-8" On Monday, February 11, 2019 at 4:50:19 PM UTC-5, Michael Shulman wrote: > > Well, I can't tell exactly what Jon meant by "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'.". If he meant that an entire typing judgment > "M:A" is only "definitionally equal" to a typing judgment "N:B" if > *the very same derivation tree* of M:A counts also as a derivation of > N:B, then in the ordinary presentations of *any* ordinary type theory > I don't think any two judgments that differ by anything more than > alpha-equivalence would be considered "definitionally equal". > Right. So I assumed he didn't mean that. I'm pretty sure that for ITT, the terms are the proof objects. But it's not clear what should count as proof objects otherwise. This is a weakness of the definition. I guessed at what the proof objects were for Nuprl, but it looks like Jon had something else in mind. If the proof objects are taken to be whatever notion of formal proof the formalizer needs to produce, then definitional equality is an important consideration for proof engineering. That's what I was thinking about. Crucially, proof automation changes the notion of proof, in practice. But this makes things fuzzy. AML programs do not denote something in a model, > and I can't think of any sense in which two of them could be "equal by > definition". You seem confused. Definitional equality is not a relation on proof objects, it's a relation on expressions appearing in the judgments they prove. AML programs don't appear in judgments. (Well, not any semantically relevant judgments.) For instance, (\lambda x. x^2)(3) is equal by definition > to 3^2, because \lambda x. x^2 denotes by definition the function that > takes its argument and squares it. This sure seems completely different from what Jon was getting at. But anyway, what's the difference between "denoting by definition" and regular denoting? An important aspect of Jon's definition of "definitional equality", which I think is right, is that it doesn't have to do with models. Definitional equality is an intentional issue. An issue tied to implementation. ITT pins definitional equality to judgmental equality, which *does* have to do with models, and I think that's *bad*. I suspect that the discomfort or lack of understanding many mathematicians supposedly have with definitional equality stems from the fact that it is, in fact, an implementation issue. So I would say that Andromeda with its reflection rule does not > include a "definitional equality" as a distinguished notion of the > core language. Agree. However, when using Andromeda as a logical framework > to implement some object language, one might assert a particular class > of substitutional equalities in the object language that are all > definitional. > How would you tell when a class of equalities is definitional? On Mon, Feb 11, 2019 at 11:27 AM Matt Oliveri > wrote: > > > > Jon's definitional equality is based on proof objects. The Andromeda > terms aren't proof objects, since you can't check just a term. So the fact > that Andromeda terms don't have coercions for strict equality doesn't do > anything for definitional equality. I would guess AML programs should be > considered the relevant proof objects. I'd say definitional equality in > Andromeda is pretty interesting, since algebraic effect handlers let you > locally add new automation for equality. But it can't be as rich as strict > equality (if you have e.g. induction on nats). And globally, it sounds like > it's just alpha conversion. > -- 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_1742_1743569968.1549962093528 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Monday, February 11, 2019 at 4:50:19 PM UTC-5, Michael = Shulman wrote:
Well, I can'= t tell exactly what Jon meant by "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'.". =C2=A0If he meant that an entire typi= ng judgment
"M:A" is only "definitionally equal" to a typing ju= dgment "N:B" if
*the very same derivation tree* of M:A counts also as a derivation of
N:B, then in the ordinary presentations of *any* ordinary type theory
I don't think any two judgments that differ by anything more than
alpha-equivalence would be considered "definitionally equal".=

Right. So I assumed he didn't mean that. I= 9;m pretty sure that for ITT, the terms are the proof objects. But it's= not clear what should count as proof objects otherwise. This is a weakness= of the definition. I guessed at what the proof objects were for Nuprl, but= it looks like Jon had something else in mind.

If the proof objects = are taken to be whatever notion of formal proof the formalizer needs to pro= duce, then definitional equality is an important consideration for proof en= gineering. That's what I was thinking about. Crucially, proof automatio= n changes the notion of proof, in practice. But this makes things fuzzy.
AML programs do not= denote something in a model,
and I can't think of any sense in which two of them could be "= equal by
definition".

You seem confused. Definitional = equality is not a relation on proof objects, it's a relation on express= ions appearing in the judgments they prove. AML programs don't appear i= n judgments. (Well, not any semantically relevant judgments.)

=
For instance, (\lambda x. x^2)= (3) is equal by definition
to 3^2, because \lambda x. x^2 denotes by definition the function that
takes its argument and squares it.

This sure seems= completely different from what Jon was getting at. But anyway, what's = the difference between "denoting by definition" and regular denot= ing?

An important aspect of Jon's definition of "definition= al equality", which I think is right, is that it doesn't have to d= o with models. Definitional equality is an intentional issue. An issue tied= to implementation. ITT pins definitional equality to judgmental equality, = which *does* have to do with models, and I think that's *bad*. I suspec= t that the discomfort or lack of understanding many mathematicians supposed= ly have with definitional equality stems from the fact that it is, in fact,= an implementation issue.

So I would say that Andromeda with its reflection rule does not
include a "definitional equality" as a distinguished notion o= f the
core language.

Agree.

However, when using Andromeda as a logical fr= amework
to implement some object language, one might assert a particular class
of substitutional equalities in the object language that are all
definitional.

How would you tell when a class = of equalities is definitional?

On Mon, Feb 11, 2019 at 11:27 AM Matt Oliveri <atm...@gmail.c= om> wrote:
>
> Jon's definitional equality is based on proof objects. The And= romeda terms aren't proof objects, since you can't check just a ter= m. So the fact that Andromeda terms don't have coercions for strict equ= ality doesn't do anything for definitional equality. I would guess AML = programs should be considered the relevant proof objects. I'd say defin= itional equality in Andromeda is pretty interesting, since algebraic effect= handlers let you locally add new automation for equality. But it can't= be as rich as strict equality (if you have e.g. induction on nats). And gl= obally, it sounds like it's just alpha conversion.

--
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_1742_1743569968.1549962093528-- ------=_Part_1741_1007127888.1549962093528--