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) qquadqquad 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) qquadqquad 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)quaddfrac{Γ, 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:Squad Γ, x:T_2 vdash M:S}{Γ, x:T_1 ∨ T_2 vdash M:S}(∨E)quaddfrac{}{Γ, 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
