[TYPES] decidability of BCCCs?

[Tadeusz Litak]

Hello Ryan,

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:
http://hdl.handle.net/1842/404
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 ...
Best,
t.

On 9/20/13 1:36 PM, Ryan Wisnesky wrote:
> [ 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