[TYPES] decidability of BCCCs?

[Altenkirch Thorsten]

The issue with empty types is that you have to decide propositional
consistency, that is
	
	G |- true = false

if and only if G is propositionally inconsistent (I.e. you can derive an
inhabitant of the empty type).

I believe that using this you get decidability of all coproducts including
the empty one.

This also strongly suggests that the calculus with dependent types and
empty coproducts is undecidable because you would need to decide the
consistency of a context in predicate logic.

Cheers,
Thorsten


On 20/09/2013 21:36, "Ryan Wisnesky" <ryan at cs.harvard.edu> 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

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.