[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
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.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?
--
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
More information about the Types-list
mailing list