[TYPES] decidability of BCCCs?
Roberto Di Cosmo
roberto at dicosmo.org
Thu Oct 6 15:32:30 EDT 2016
That's great news: thanks for sharing, Gabriel, and congratulations for
this nice step forward!
--
Roberto
On Thu, Oct 06, 2016 at 02:58:39PM -0400, Gabriel Scherer wrote:
> Hi all,
>
> I'm coming back to this old types-list thread to announce the article
>
> Deciding equivalence with sums and the empty type
> Gabriel Scherer, 2016
> https://arxiv.org/abs/1610.01213
>
> which proposes a proof of decidability of contextual equivalence for
> the simply-typed lambda-calculus with sums and empty types, which
> corresponds to decidability in the free bicartesian category. Any
> feedback is of course warmly welcome.
>
>
> # Context of the work
>
> The proof builds on an extension of the proof-theoretic technique of
> focusing. Focusing is a technique to make the proofs of a logic more
> canonical by reasoning on the invertibility of proof rules, and
> imposing an ordering between invertible phases (automatic) and
> non-invertible phases (interesting). In previous work with Didier
> Rémy, we proposed a refinement of focused intuitionistic logic that is
> "saturated" (non-invertible phases have to perform all possible
> non-invertible deductions at once, modulo some restrictions to
> preserve termination), and give quasi-normal forms that are quite
> close to the normal forms in previous work on equivalence in presence
> of sums. The goal was to answer the question, in a type system with
> sums but no empty types (we knew empty types are hard, in large part
> due to the discussion in this very types-list thread): "which types
> have a unique inhabitant?", which requires a type system with as
> little redundant (equivalent) terms as possible.
>
> While experimenting with the implementation of an algorithm that
> computes an answer the following question (given a type, explore its
> saturated derivation to check whether there is a unique one), we
> noticed that adding the empty type seemed to work perfectly, although
> our theory did not account for it. While wrapping up my PhD manuscript
> ( https://hal.inria.fr/tel-01309712/ ; it contains a detailed
> introduction to focusing and saturation), I tried to provide
> a rigorous canonicity proof for the system extended with the empty
> type, but could not provide a rigorous one in time for submission. The
> above article now proposes an answer to this question.
>
> Many thanks to the participants to this types-list thread, which got
> me interested in trying to extend the system with empty types. Without
> it I also wouldn't have found about Arbob Ahmad's work, an
> (unfortunately unpublished) independent use of focusing for program
> equivalence which I find very interesting.
>
>
> # Related work
>
> I don't yet have a good understanding of the relation between this
> approach and existing works on Normalization by Evaluation (NbE). NbE
> requires a good understanding of how to combine/compose fragment of
> normal forms together while evaluating the original source terms; our
> normal forms have a very non-local structure that make it difficult
> (In particular, I think that it's possible to present an equivalence
> algorithm that compares two focused terms, computing a saturated form
> on the fly; but starting from un-focused terms and doing focusing on
> the fly looks rather difficult). Saturated normal forms are related to
> the notion of "maximally multi-focused proof" (multi-focusing is an
> extension of focusing that has been studied in the last decade), and
> this corresponds to the known difficulty of formulating
> cut-elimination processes that preserves maximal
> multi-focusing. Giving a normalization-by-evaluation presentation of
> saturation would thus be very interesting.
>
> It is easier to relate to the rewriting-based approaches of Neil Ghani
> and Sam Lindley; the normalization of focused terms into saturated
> terms is very close to the rewriting they propose. In rewriting-based
> approaches, one try to extrude matches of the form (match n with ...)
> (where n is a neutral term; if n started with a constructor, this
> would be beta-reducible) to move them closer to the root of the term,
> and then merge redundant matches. When rewriting a focused term into
> a saturated term, the syntax has let-bindings for neutrals of positive
> type (let x = n in ...), and those get extruded up in the term. Then
> the focusing structure imposes that the corresponding match happen as
> soon as possible after that (so the "merge" of redundant matches is
> implied by focusing). (The use of control operators in Balat, Di
> Cosmo, Fiore also serves the same purpose of finding the earliest
> possible place to introduce a neutral). On the other hand, saturation
> will do forward-based proof search to synthesize all definable
> neutrals, instead of just permuting fragments of the two terms to
> compare, and this is the key ingredient that makes it gracefully
> extend to the empty type: one has to go out in the wild looking for
> proofs of 0.
>
>
> On Sat, Sep 21, 2013 at 10:25 AM, Ryan Wisnesky <ryan at cs.harvard.edu> wrote:
> > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> >
> > Hi Roberto,
> >
> > BCCCs seem to come up a lot at the intersection between database theory and programming language theory. For example, if you say that a database schema is a finitely presented category, then the category of schemas and mappings between them is a BCCC. For this particular BCCC, I believe that equality is semi-decidable, so I would like to say that its semi-decidability comes from its particular nature, and is not inherited from the free BCCC. BCCCs also come up when you try to connect higher-order logic to the nested relational calculus via their categorical (topos) semantics. I'd be happy to talk more about it offline.
> >
> > Thanks,
> > Ryan
> >
> > On Sep 21, 2013, at 9:34 AM, Roberto Di Cosmo <roberto at dicosmo.org> wrote:
> >
> >> Dear Ryan,
> >> beta-eta equality in the presence of strong sums is a tricky subject that has been object of some attention for more than 20 years, both "per se" in the rewriting community, that looked for an elegant confluent rewriting system, and as a "tool" for researchers interested in type theory and semantics, that wanted to know for example whether one can characterise object isomorphism in a BiCCC, problem that one can try to attack by studying invertible terms in the corresponding lambda calculus with strong types.
> >>
> >> If one stays in the 1,*,-> fragment, all is wonderful: you get a nice confluent and normalising rewriting system for the lambda calculs based on eta expansion (see a blazingly short proof in http://www.dicosmo.org/Articles/POD.ps), the type isomorphisms are finitely axiomatizable
> >> and exactly correspond to the equations one knows from high schools for natural numbers equipped with product, unit and exponentiation, related to Tarski's High School algebra problem
> >> (a nice proof through Finite Sets is due to Sergei Soloviev in 1988, I gave one based on invertible terms in my PhD thesis back in 1992).
> >>
> >> You may add weak sums to the calculus, and still get a nice confluent and normalising rewriting system, that can also accomodate bounded recursion (http://www.pps.univ-paris-diderot.fr/~kesner/papers/icalp93.ps.gz).
> >>
> >> As soon as you add strong sums, though, things get very hairy: Neil Ghani proposed in his PhD thesis back in 1995 a decision procedure for lambda terms with strong 1,+,*,-> (no zero, see
> >> https://personal.cis.strath.ac.uk/neil.ghani/papers/yellowthesis.ps.gz): a rewriting system is used to bring terms in this calculus to a normal form which is not unique, and then it is shown that all such normal forms are equivalent modulo a sort of commuting conversions, so to decide equality of two terms, you first normalise them, and then check whether they are equivalent w.r.t. conversion (the equivalence classes being finite, this is decidable). The NBE appoach of Thorsten Altenkirch (et al.) of your LICS01 reference seems to provide a more straightforward way to decide equality, even if somebody coming from the rewriting world might like a more intuitive description of what the normal form actually look like.
> >>
> >> If you add the zero, you are in for more surpises: looking at the special BiCCC formed by the natural numbers equipped with 0,1,+,* and exponentiation, you discover that equality is no longer finitely axiomatisable, and yet a decision procedure does exist (see http://www.dicosmo.org/Papers/zeroisnfa.pdf),
> >> which solves in the negative, but with a positive note, Tarski's problem for this system.
> >>
> >> But then, in BiCCCs, the connection between numerical equalities and type isomorphisms breaks down and the nice result above says nothing about what happens for the general case. In http://www.dicosmo.org/Papers/lics02.pdf we proved that isos are non finitely axiomatisable in BiCCC, but we know nothing on decidability.
> >>
> >> As for deciding beta-eta equality, the work of Marcelo Fiore and Vincent Balat http://www.cl.cam.ac.uk/~mpf23/papers/Types/tdpe.pdf shows how to compute normal forms in full BiCCCs, and I kind of remember that we were convinced at some point that these normal forms must be unique up to some sort of commuting conversions (you can see this in the examples of the paper), but we did not prove it at that moment, and it is true that one would like to see this last step done (or a proof that it cannot be done).
> >>
> >> I wonder whether Marcelo, Neil and Thorsten might shed some light on this (Vincent and I started working on quite different areas a while ago)
> >>
> >> By the way, out of curiosity, would you mind telling us how this result would be useful your research?
> >>
> >> --
> >> Roberto
> >>
> >> P.S.: for those interested in type isomorphism, http://www.dicosmo.org/Paper/mscs-survey.pdf provides a concise overview, even if no longer up to date.
> >>
> >>
> >>
> >> 2013/9/20 Ryan Wisnesky <ryan at cs.harvard.edu>
> >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> >>
> >> Hello,
> >>
> >> I am trying to find a reference that states whether or not the free bi-cartesian closed category is decidable. That is, I am wondering if beta-eta equality of the simply typed lambda calculus extended with strong 0,1,+,* types is decidable. (In particular, I am interested in the full calculus, including the eliminator for 0, introduction for 1, and eta for all types).
> >>
> >> So far, my search through the literature says that the answer to this question is "almost" or "maybe" :
> >>
> >> - the STLC with strong 1,+,* types is decidable (omits 0, the empty type): http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf
> >>
> >> - the STLC with strong 0,1,+,* types has normal forms, but equivalent terms may have different such normal forms:http://www.cl.cam.ac.uk/~mpf23/papers/Types/tdpe.pdf
> >>
> >> - work on mechanized proofs of correctness for deciding co-product equality may or may not include the "absurd" eliminator for the empty type: http://www.cis.upenn.edu/~sweirich/wmm/wmm07/programme/licata.pdf
> >>
> >> I feel like the answer to this question is probably well-known, but I can't seem to find it in the literature. Any help would be appreciated.
> >>
> >> Thanks,
> >> Ryan
> >>
> >>
> >>
> >> --
> >> Roberto Di Cosmo
> >>
> >> ------------------------------------------------------------------
> >> Professeur En delegation a l'INRIA
> >> PPS E-mail: roberto at dicosmo.org
> >> Universite Paris Diderot WWW : http://www.dicosmo.org
> >> Case 7014 Tel : ++33-(0)1-57 27 92 20
> >> 5, Rue Thomas Mann
> >> F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo
> >> FRANCE. Twitter: http://twitter.com/rdicosmo
> >> ------------------------------------------------------------------
> >> Attachments:
> >> MIME accepted, Word deprecated
> >> http://www.gnu.org/philosophy/no-word-attachments.html
> >> ------------------------------------------------------------------
> >> Office location:
> >>
> >> Bureau 320 (3rd floor)
> >> Batiment Sophie Germain
> >> Avenue de France
> >> Metro Bibliotheque Francois Mitterrand, ligne 14/RER C
> >> -----------------------------------------------------------------
> >> GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3
> >
--
Roberto Di Cosmo
------------------------------------------------------------------
Professeur (on leave at/detache a INRIA Roquencourt)
IRIF E-mail : roberto at dicosmo.org
Universite Paris Diderot Web : http://www.dicosmo.org
Case 7014 Twitter : http://twitter.com/rdicosmo
5, Rue Thomas Mann
F-75205 Paris Cedex 13 France
------------------------------------------------------------------
Office location:
Paris Diderot INRIA
Bureau 3020 (3rd floor) Bureau C123
Batiment Sophie Germain Batiment C
8 place Aurélie Nemours 2, Rue Simone Iff
Tel: +33 1 57 27 92 20 Tel: +33 1 80 49 44 42
Metro
Bibliotheque F. Mitterrand Ligne 6: Dugommier
ligne 14/RER C Ligne 14/RER A: Gare de Lyon
------------------------------------------------------------------
GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3
More information about the Types-list
mailing list