[TYPES] decidability of BCCCs?
tadeusz.litak at gmail.com
Fri Sep 20 19:55:44 EDT 2013
it's not exactly my area, but the LiCS'01 reference that you quote mentions earlier work of Neil Ghani:
>>A decision procedure for cartesian closed categories with binary coproducts has been presented in Ghani's the- sis
[Gh95a] (see [Gh95b] for a summary) <<
[Gh95b] comments on the addition of empty type at the beginning of Section 3.
And [Gh95a], i.e., Neil's PhD Thesis available at this link:
discusses the subject in conclusions on p. 145. Also see "Initial objects" subsection on p. 104.
Although I cannot find the reference "Inconsistency and extensionality" anywhere: not sure if it materialized.
Anyway, HTH ...
On 9/20/13 1:36 PM, Ryan Wisnesky wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 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.
More information about the Types-list