[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
