[TYPES] decidability of BCCCs?

Roberto Di Cosmo roberto at dicosmo.org
Sat Sep 21 09:34:48 EDT 2013

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

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

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


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
MIME accepted, Word deprecated
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

More information about the Types-list mailing list