[TYPES] decidability of BCCCs?

[Ryan Wisnesky]

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