How to Think of Intersection Types as Cartesian Products

In their paper “Intersection types and lambda definability” [Bucciarelli, A., Piperno, A., Salvo I., Intersection types and lambda definability, MSCS03, 13 (1), pp. 15-53, (2003)] Bucciarelli, Piperno, and Salvo give a mapping of the strongly normalizable untyped terms into the simply typed terms via the assignment of intersection types. Here we shall both generalize their result and provide a converse. We shall do this by retracting untyped terms with surjective pairing onto untyped terms without pairing by using a special variant of Stovring's notion [Støvring, K., Extending the extensional lambda calculus with surjective pairing is conservative, LMCS 2, pp. 1-14] of a symmetric term. The symmetric ones which have simple types with Cartesian products are precisely the ones which retract onto (eta expansions of) strongly normalizable untyped terms. The intersection types of the strongly normalizable terms are related to the simple types with products in that we just replace ∧ by Cartesian product and vice versa.