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

[James Cheney <james....@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4726 bytes --]

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.
>

[-- Attachment #2: Type: text/html, Size: 6180 bytes --]