From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.160.197 with SMTP id j188mr11885786vke.10.1501580071079; Tue, 01 Aug 2017 02:34:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.182.213 with SMTP id g204ls10197550iof.29.gmail; Tue, 01 Aug 2017 02:34:30 -0700 (PDT) X-Received: by 10.129.85.141 with SMTP id j135mr13740151ywb.209.1501580070240; Tue, 01 Aug 2017 02:34:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1501580070; cv=none; d=google.com; s=arc-20160816; b=IB1uWod7TXsSOCVawAfi6HIbO+Y64Iyp1JdfJm3gGNxFXE2nskkVB9c0NsKC6LiA+r /Pfc96ty+tyyrcRbrVsfyhf7iVAp0NJm5R4gJ9t3YYnkYDClERLkOFV99JV4s34dY87u zrk4JrQtxsj57bf0CXUt0xm6FMefI2nziRmvHd1eDMQLBNIZ8HPqSt/IVOGS+GiV9dz7 TAXlQrVL97pZ1hEUI+8ZkJpH2pq1RBLsfXoxKA/WmmNTSKy+CqVeh5dOMF+PvMcEzUpw nRMWZRFvIY9wU4zl1ulIYbZh54pzNP7jTMZCVdGJwF73Rn65FDGmFpvJtr7wo1uQjnMT z/nw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=3yob/C+zgerPuiGsmW7MZXtWYIjAZ9nIFn7v6GHFQl4=; b=iMPySft2HV4nbjSAZONwara4D0VM7hNjqV7Rlz9yDREbkqWGEPKgT/WZKTsgKfGumb zCvoMwC3II+0JbuGe3FfoQOblYt3xJDn05KxlQzasz6XngcG5GMpW3WCL3eMwB8MYckU AoxjRpAUeDWNP5tvU+Ie/0BgB5WPtxIGEXH1bUw8nvNKZWaziNkUIW+I5OJV9SBhd/oa XpsWdMwpe2ma43MJdcrTqi9gp2gYbYLlh6VO85gQOCJ7dNepo7K6jjzJZFnWz1n+27E2 SaEUgsHXF2Pt9kBmgj5Q/B3j/K22sfy42K1tRW+d/dLeqgy3OZ/QnMQvEurWCIi/ri3N fA7g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=hWgPzNc5; spf=pass (google.com: domain of james....@gmail.com designates 2607:f8b0:4001:c0b::229 as permitted sender) smtp.mailfrom=james....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-it0-x229.google.com (mail-it0-x229.google.com. [2607:f8b0:4001:c0b::229]) by gmr-mx.google.com with ESMTPS id c133si60237itb.7.2017.08.01.02.34.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 01 Aug 2017 02:34:30 -0700 (PDT) Received-SPF: pass (google.com: domain of james....@gmail.com designates 2607:f8b0:4001:c0b::229 as permitted sender) client-ip=2607:f8b0:4001:c0b::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=hWgPzNc5; spf=pass (google.com: domain of james....@gmail.com designates 2607:f8b0:4001:c0b::229 as permitted sender) smtp.mailfrom=james....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x229.google.com with SMTP id 77so4996338itj.1 for ; Tue, 01 Aug 2017 02:34:30 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=3yob/C+zgerPuiGsmW7MZXtWYIjAZ9nIFn7v6GHFQl4=; b=hWgPzNc5QyaINY8/tHYzKXHzxoseGVHvn/pilbVyFIxgBho/vUjJeeuF6SYWde6EoS m+UHZ5tyKhEKmaD34HJghLFnYIK+UyBvOmMJaRuFxRWYH+M9K6LO9xfBU+YaF83VaKq0 mqSaeaD7r9cqdWqBDuNZGa8BuHvYrS2+oLctwmKX35YNOgoI6zp8TtWHaPBz+RxUhBSJ 4r8g8sbyvvERdB7If9Qr0mc6zwc2bkX1qZz6pFZkbOE2GJl7os/LCA1uLbh55iAhDm4C bB05Nj7AIUNenGGibtQADQKfhlEetL9CeF1zV/5oWwJOQpWLJEetonb7Xd3e7qyifCgZ dsuA== X-Gm-Message-State: AIVw110ZeRHJkOhi6pzf053aTBnnPcLBM213Sfat/5/kNNzEA+LqsUYj up8rA6yQ6n0JTuGje1wurBk6IZYzRw== X-Received: by 10.36.210.133 with SMTP id z127mr1082034itf.120.1501580070011; Tue, 01 Aug 2017 02:34:30 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.168.144 with HTTP; Tue, 1 Aug 2017 02:34:29 -0700 (PDT) In-Reply-To: References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> <38162a12-c8b2-401d-b272-07d1db7c1be8@googlegroups.com> From: James Cheney Date: Tue, 1 Aug 2017 10:34:29 +0100 Message-ID: Subject: Re: [HoTT] Re: cubical type theory with UIP To: Michael Shulman Cc: Neelakantan Krishnaswami , Homotopy Type Theory Content-Type: multipart/alternative; boundary="94eb2c05f816acd08b0555adda6a" --94eb2c05f816acd08b0555adda6a Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Not sure if it's what you're looking for or if it is an example of a "not fully satisfactory" system, but Negri and von Plato's book "Structural Proof Theory" (esp. ch. 6) talks about axiomatic extensions to sequent calculi that preserve cut elimination. The main idea is to turn axioms of the form P1 & ... & Pn =3D> Q1 | ... | Qm into right-rules of the form Q1,Gamma =3D> Delta, ... Qm, Gamma =3D> Delta --------------------------------------------------------------- P1,...,Pn, Gamma =3D> Delta so that no new principal cuts are introduced. This can handle equality or other FOL axioms of the form forall X. /\_i Pi =3D=3D> \/_i Q_i where P_i a= nd Q_i are atomic. --James On Tue, Aug 1, 2017 at 10:20 AM, Michael Shulman wrote: > Yes, I think I've seen something like this before. It may give a good > programming language, but from a semantic category-theoretic > perspective I don't think it's any good. Two syntactically distinct > terms might still turn out to be semantically equal, so you need a > left rule for equality that does more than just syntactically analyze > the terms being equated. > > On Tue, Aug 1, 2017 at 2:14 AM, Neelakantan Krishnaswami > wrote: > > On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote: > >> > >> Another motivation is that as far as I know, there is not a really > >> satisfactory version of sequent calculus for first-order logic with > >> equality (e.g. not having a fully satisfactory cut-elimination > >> theorem). If cubical methods are a good way to treat equality > >> "computationally", I wonder whether a "cubical sequent calculus" would > >> be able to deal with equality better. > > > > > > Actually, there *are* good versions of sequent calculus with > > equality. Jean-Yves Girard and Peter Schroeder-Heister have both given > > the appropriate rules. So, given a language of terms with some > > equational theory, the right and left rules are: > > > > > > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94 =3DR > > =CE=93 =E2=8A=A2 t =3D t > > > > > > =E2=88=80=CE=B8 =E2=88=88 csu(s,t). =CE=B8(=CE=93) =E2=8A=A2 =CE=98= (C) > > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94 =3DL > > =CE=93, s =3D t =E2=8A=A2 C > > > > The premise of the left rule quantifies over a *complete set of > > unifiers* for s and t. For terms freely generated by some signature, > > there is a single most general unifier (if one exists), and so the > > left rule has at most one premise. Once you add equations then > > there can be more than one most general unifier -- possibly even > > infinite (eg, if terms are lambda-terms modulo beta/eta, as in > > higher-order unification). > > > > The Girard/Schroeder-Heister equality is not the same as the Martin-Lof > > identity type, but it gives rise to a nicer programming language than > raw J > > does, since the left rule is invertible. Invertible left rules are what > give > > rise to > > pattern matching syntax, and so languages like Agda choose a fragment > > where the G/SH rule and J coincide to implement pattern matching. > > > > Agda restricts pattern matching so that an identity type > > argument can only have a refl pattern when the two terms being equated > > are generated from variables and constructors. So an identity proof > > p : (cons x y) =3D (cons a b)) can be matched as refl, but an identity > > proof q : (append x y) =3D (append a b)) can't be. > > > > This restriction ensures that first-order unification suffices for the > > G/SH elim, and therefore to implement pattern matching. > > > > If you are very interested in this topic, Joshua Dunfield and I have a > draft > > paper where we work out the Curry-Howard story for pattern matching > > with the G/SH equality (what are called GADTs by PL theorists) in gory > > detail: > > > > Sound and Complete Bidirectional Typechecking for Higher-Rank > Polymorphism > > and Indexed Types > > > > > > -- > > Neel Krishnaswami > > nk...@cl.cam.ac.uk > > > > -- > > You received this message because you are subscribed to the Google Grou= ps > > "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send = an > > email to HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --94eb2c05f816acd08b0555adda6a Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Not sure if it's what you're l= ooking for or if it is an example of a "not fully satisfactory" s= ystem, but Negri and von Plato's book "Structural=20 Proof Theory" (esp. ch. 6) talks about axiomatic extensions to sequent= =20 calculi that preserve cut elimination.=C2=A0 The main idea is to turn axiom= s=20 of the form

P1 & ... & Pn =3D> Q1 | ...=C2=A0 | Qm<= br>
into right-rules of the form

Q1,Gamma =3D>= ; Delta, ... Qm, Gamma =3D> Delta
------------------------= ---------------------------------------
P1,...,Pn, Gamma =3D&= gt; Delta

so that no new principal cuts are introduced.=C2=A0 = This can handle equality or other FOL axioms of the form forall X. /\_i Pi = =3D=3D> \/_i Q_i where P_i and Q_i are atomic.

--James
<= br>

On Tue, = Aug 1, 2017 at 10:20 AM, Michael Shulman <shu...@sandiego.edu> wrote:
Yes, I think I've seen so= mething like this before.=C2=A0 It may give a good
programming language, but from a semantic category-theoretic
perspective I don't think it's any good.=C2=A0 Two syntactically di= stinct
terms might still turn out to be semantically equal, so you need a
left rule for equality that does more than just syntactically analyze
the terms being equated.

On Tue, Aug 1, 2017 at 2:14 AM, Neelakantan Krishnaswami
<n.krish...@cs.bham.ac.uk> wrote:
> On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote: >>
>> Another motivation is that as far as I know, there is not a really=
>> satisfactory version of sequent calculus for first-order logic wit= h
>> equality (e.g. not having a fully satisfactory cut-elimination
>> theorem).=C2=A0 If cubical methods are a good way to treat equalit= y
>> "computationally", I wonder whether a "cubical sequ= ent calculus" would
>> be able to deal with equality better.
>
>
> Actually, there *are* good versions of sequent calculus with
> equality. Jean-Yves Girard and Peter Schroeder-Heister have both given=
> the appropriate rules. So, given a language of terms with some
> equational theory, the right and left rules are:
>
>
>=C2=A0 =C2=A0 =C2=A0=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =3DR
>=C2=A0 =C2=A0 =C2=A0=CE=93 =E2=8A=A2 t =3D t
>
>
>=C2=A0 =C2=A0 =C2=A0=E2=88=80=CE=B8 =E2=88=88 csu(s,t). =CE=B8(=CE=93) = =E2=8A=A2 =CE=98(C)
>=C2=A0 =C2=A0 =C2=A0=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94 =3DL
>=C2=A0 =C2=A0 =C2=A0=CE=93, s =3D t =E2=8A=A2 C
>
> The premise of the left rule quantifies over a *complete set of
> unifiers* for s and t. For terms freely generated by some signature, > there is a single most general unifier (if one exists), and so the
> left rule has at most one premise. Once you add equations then
> there can be more than one most general unifier -- possibly=C2=A0 even=
> infinite (eg, if terms are lambda-terms modulo beta/eta, as in
> higher-order unification).
>
> The Girard/Schroeder-Heister equality is not the same as the Martin-Lo= f
> identity type, but it gives rise to a nicer programming language than = raw J
> does, since the left rule is invertible. Invertible left rules are wha= t give
> rise to
> pattern matching syntax, and so languages like Agda choose a fragment<= br> > where the G/SH rule and J coincide to implement pattern matching.
>
> Agda restricts pattern matching so that an identity type
> argument can only have a refl pattern when the two terms being equated=
> are generated from variables and constructors. So an identity proof > p : (cons x y) =3D (cons a b)) can be matched as refl, but an identity=
> proof q : (append x y) =3D (append a b)) can't be.
>
> This restriction ensures that first-order unification suffices for the=
> G/SH elim, and therefore to implement pattern matching.
>
> If you are very interested in this topic, Joshua Dunfield and I have a= draft
> paper where we work out the Curry-Howard story for pattern matching > with the G/SH equality (what are called GADTs by PL theorists) in gory=
> detail:
>
>=C2=A0 =C2=A0Sound and Complete Bidirectional Typechecking for Higher-R= ank Polymorphism
> and Indexed Types
>=C2=A0 =C2=A0<http://www.cl.cam.ac.uk/~nk480/gadt= .pdf>
>
> --
> Neel Krishnaswami
> nk...@cl.cam.ac.uk
>
> --
> You received this message because you are subscribed to the Google Gro= ups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send= an
> email to Homot= opyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.google.com/d/opto= ut.

--
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 HomotopyTyp= eTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--94eb2c05f816acd08b0555adda6a--