[TYPES] decidability of BCCCs?
Roberto Di Cosmo
roberto at dicosmo.org
Sat Sep 21 11:54:58 EDT 2013
The link to the survey on isomorphisms does not work; there was a missing
"s", I apologize for the mistyping, here is the correct one
http://www.dicosmo.org/Papers/mscs-survey.pdf
By the way, all mentioned works are actually published, and the official
versions can be found by looking for example at the DBLP listings for
Altenkirch, Dezani, Di Cosmo, Fiore, Ghani, Kesner, etc.
2013/9/21 Roberto Di Cosmo <roberto at dicosmo.org>
> 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
>
--
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