[ 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
