[TYPES] decidability of BCCCs?

[Ryan Wisnesky]

Hi Arbob,

I would very much like to know more about this work.  If you handle the full calculus, including the eliminator for 0, it would answer my question in the affirmative.  Unfortunately, I was unable to tell if this was the case just by looking at the publicly available material.

Thanks,
Ryan

On Sep 21, 2013, at 5:26 AM, Arbob Ahmad <adahmad+ at cs.cmu.edu> wrote:

> Hello Ryan,
> 
> Dan Licata, Bob Harper, and I designed an algorithm for deciding beta-eta equality for the simply typed lambda calculus with 0, 1, +, and * but without unspecified base types. The basic idea is that all of these types are finitely inhabited so we can enumerate their inhabitants to uniquely identify a member of each type. As you mention, finding a unique canonical form is the tricky part. We essentially used a form of multi-focusing that focused on everything in the context it possibly could simultaneously and then performed all necessary inversions simultaneously as well. This means if there is a variable of type bool -> bool in the context, a canonical form in this context must apply this function to both true and false simultaneously to uniquely determine which of the four possible functions of this type the variable represents. We haven't published this result, but I can send you more information if you're interested.
> 
> I would also point you to the work of Lindley in Typed Lambda Calculus and Applications 2007. This gives a decision procedure based on extensional rewriting for the simply typed lambda calculus with + and *. It does not include 0 and 1 but suggests these wouldn't be too hard to add.
> 
> Arbob Ahmad
> 
> Tadeusz Litak wrote:
>> [ 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
>>