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