[Solved]: Characterization of lambda-terms that have union types

Problem Detail: 

Many textbooks cover intersection types in the lambda-calculus. The typing rules for intersection can be defined as follows (on top of the simply typed lambda-calculus with subtyping):

$$ \dfrac{\Gamma \vdash M : T_1 \quad \Gamma \vdash M : T_2} {\Gamma \vdash M : T_1 \wedge T_2} (\wedge I) \qquad\qquad \dfrac{} {\Gamma \vdash M : \top} (\top I) $$

Intersection types have interesting properties with respect to normalization:

• A lambda-term can be typed without using the $\top I$ rule iff it is strongly normalizing.
• A lambda-term admits a type not containing $\top$ iff it has a normal form.

What if instead of adding intersections, we add unions?

$$ \dfrac{\Gamma \vdash M : T_1} {\Gamma \vdash M : T_1 \vee T_2} (\vee I_1) \qquad\qquad \dfrac{\Gamma \vdash M : T_2} {\Gamma \vdash M : T_1 \vee T_2} (\vee I_2) $$

Does the lambda-calculus with simple types, subtyping and unions have any interesting similar property? How can the terms typable with union be characterized?

Asked By : Gilles

Answered By : Stéphane Gimenez

In the first system what you call subtyping are these two rules:

$$\dfrac{Γ, x:T_1 \vdash M:S}{Γ, x:T_1 ∧ T_2 \vdash M:S}(∧E_1)\quad\dfrac{Γ, x:T_2 \vdash M:S}{Γ, x:T_1 ∧ T_2 \vdash M:S}(∧E_2)$$

They correspond to elimination rules for $∧$; without them the connective $∧$ is more or less useless.

In the second system (with connectives $∨$ and $→$, to which we could also add a $⊥$), the above subtyping rules are irrelevant, and I think the accompanying rules you had in mind are the following:

$$\dfrac{Γ, x: T_1 \vdash M:S\quad Γ, x:T_2 \vdash M:S}{Γ, x:T_1 ∨ T_2 \vdash M:S}(∨E)\quad\dfrac{}{Γ, x: {⊥} \vdash M:S}({⊥}E)$$

For what it's worth, this system allows to type $(λx. I)Ω:A→A$ (using the ${⊥}E$ rule), which cannot be typed with just simple types, which has a normal form, but is not strongly normalizing.

---

Random thoughts: (maybe this is worth asking on TCS)

This leads me to conjecture that the related properties are something like:

• a λ-term $M$ admits a type not containing $⊥$ iff $MN$ has a normal form for all $N$ which has a normal form. ($δ$ fails both tests, but the above λ-term pass them)
• a λ-term $M$ can be typed without using the ${⊥}E$ rule iff $MN$ is strongly normalizing for all strongly normalizing $N$.

Exercise: prove me wrong.

Also it seems to be a degenerated case, maybe we should consider adding this guy into the picture. As far as I remember, it would allow to obtain $A ∨ (A → {⊥})$?

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/62