Re: [HoTT] Re: cubical type theory with UIP

[Michael Shulman <shu...@sandiego.edu>]

I think I've seen something like that too; it seems to be basically
giving up on eliminating cuts involving equalities by building them
into the primitive rules.  I would expect equality to be one of the
*logical* operations, so that we can eliminate its cuts, rather than
being described by axioms as if it were part of the "theory".

On Tue, Aug 1, 2017 at 2:34 AM, James Cheney <james....@gmail.com> wrote:
> 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 => Q1 | ...  | Qm
>
> into right-rules of the form
>
> Q1,Gamma => Delta, ... Qm, Gamma => Delta
> ---------------------------------------------------------------
> P1,...,Pn, Gamma => Delta
>
> so that no new principal cuts are introduced.  This can handle equality or
> other FOL axioms of the form forall X. /\_i Pi ==> \/_i Q_i where P_i and
> Q_i are atomic.
>
> --James
>
>
> On Tue, Aug 1, 2017 at 10:20 AM, Michael Shulman <shu...@sandiego.edu>
> 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
>> <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 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:
>> >
>> >
>> >     —————————— =R
>> >     Γ ⊢ t = t
>> >
>> >
>> >     ∀θ ∈ csu(s,t). θ(Γ) ⊢ Θ(C)
>> >     —————————————————————————— =L
>> >     Γ, s = t ⊢ 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) = (cons a b)) can be matched as refl, but an identity
>> > proof q : (append x y) = (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
>> >   <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
>> > 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.
>>
>> --
>> 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.
>
>