Reducibility method and resource control

Abstract

The basic relationship between logic and computation is given by the Curry-Howard correspondence [4] between simply typed λ-calculus and intuitionistic natural deduction. This connection can be extended to other calculi and logical systems. There source control lambda calculus, λr[2], is an extension of the λ-calculus with explicit operators for erasure and duplication, which brings the same correspondence to intuitionistic natural deduction with explicit structural rules of weakening and contraction on the logical side [1]. It corresponds to theλcwlcw-calculus of Kesner and Renaud [5]. Inλrin every subterm every free variable occurs exactly once, and every binder binds (exactly one occurrence of)a free variable.The main computational step isβreduction. But there are also reductions which perform propagation of contraction into the expression and reductions which extract weakening out of expressions. This discipline allows to optimize the computation by delaying duplication of terms and by performing erasure of terms as soon as possible.Our intersection type assignment systemλr∩integrates intersection into logical rules, thus preserving syntax-directedness of the system. We assign restricted form of intersection types to terms, namely strict types, therefore minimizing the need for pre-order on types. By using this intersection type assignment system we prove that terms in the calculus enjoy strong normalisation if and only if they are typeable. We prove that terms typeable in λr-calculus are strongly normalising by adapting the reducibility method for explicit resource control operators.The reducibility method is a well known framework for proving reduction properties ofλ-terms typeable in different type systems [3]. It was introduced by Tait [6] for proving the strong normalization property for the simply typed lambda calculus. Its main idea is to relate terms typeable in a certain typeassignment system and terms satisfying certain realizability properties (e.g.,strong normalisation, confluence). To this aim we interpret types by suitable sets ofλ-terms called saturated sets, based on the sets of strongly normalizing terms. Then we obtain the soundness of type assignment with respect to these interpretations. As a consequence of soundness we have that every term161 typeable in the type system belongs to the interpretation of its type. This is an intermediate step between the terms typeable in a type system and strongly normalizing terms. Hence, the necessary notions for the reducibility method are:type interpretation, variable, reduction, expansion, weakening and contraction properties (which lead to the definition of saturated sets), term valuation, and soundness of the type assignment. Suitable modified reducibility method leads to uniform proofs of other reduction properties ofλr-terms, such as confluence or standardization.