Give an example of a program in Simply Typed Lambda that produces Bottom.

Question

I'm not sure how bottom applies to simply typed lambda calculus.

not A is a common abbreviation for A -> ⊥

But I see no way to construct a function of that signature within the theory.

Edit: A more precise way of phrasing my original question is "Is it impossible to prove a negation (A -> ⊥) unless another negation is specified?"

Since if you are given a constant t1:A->⊥ and if you are given the constant t2:B->A then it is trivial to construct a function to Bottom (t1 t2):B->⊥.

If no constant that returns bottom is provided, bottom can never be can never be proven in Simply Typed Lambda Calculus?

Thanks

Answer 1

Simply typed lambda calculus is strongly normalizing (Intensional Interpretations of Functionals of Finite Type I, W.W. Tait, JSL 32(2), 1967).

Given a base type $A \ne \bot$, if there was a term of type $\neg A$, then its normal form (which exists as we've just seen) would be of the form $\lambda x:A. M$, with $x:A \vdash M : \bot$. Since $M$ is a normal form, it must be either of the form $x N$ (impossible because $x$ does not have a function type) or $\lambda y:B. N'$ (impossible because $M$ does not have a function type). So there is no such term.

There can of course be functions whose return type is $\bot$, if the argument lets $\bot$ in. For example there is an obvious function of type $\bot\rightarrow\bot$.

This is a general phenomenon: in a typed lambda calculus which is strongly normalizing, there is no way to construct a term of type $\bot$, short of introducing ad hoc constants. In the Curry-Howard correspondence, $\bot$ is the type of false propositions. Strongly normalizing calculi do not allow proving false propositions, so they have no closed term of type $\bot$.

Lambda calculus with intersection types is an interesting extension. This calculus defines all terms to have the type $\top$, and has the properties that a term can be typed without using $\top$ if and only if it has a normal form. This gives a simple type-theoretic characterization of terminating computations (of course, typing is not decidable). See Does there exist a Turing complete typed lambda calculus?