[TYPES] decidability of BCCCs?
adahmad at cs.cmu.edu
Sat Sep 21 06:05:00 EDT 2013
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.
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:
> 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
>> - 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