[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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 <[email protected]> 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 <[email protected]> > >> [ 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: [email protected] > >> 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 : [email protected] 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
