[TYPES] decidability of BCCCs?

[Arbob Ahmad]

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
>