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