Approaching substructural term calculi via the resource control calculus

Abstract

In this talk, we propose a new way to obtain a computational interpretation of some substructural logics, starting from an intuitionistic term calculus with explicit control of resources. Substructural logics [1] are a wide family of logics obtained by restricting or rejecting some of Gentzen’s structural rules, such as thinning, contraction and exchange.The most well known substructural logic is the linear logic of Girard [3], in which, due to the absence of contraction and weakening, each formula appears exactly once in the theorem. The other well known substructural logics are the relevant logic (the one without thinning), the affine logic (without contraction) and the Lambek calculus(without all three mentioned structural rules). From the computational point of view, structural rules of thinning and contractionare closely related to the control of available resources (i.e. term variables). More precisely, contraction corresponds to the duplication of the variable that is supposed to be used twice in a term, whereas weakening corresponds to the erasure of an useless variable. These concepts were implemented into several extensions of the lambda calculus [2, 4, 5, 6]. Here, we use the resource control lambda calculus λr, proposed in [2], as a starting point for obtaining computational interpretations of implicative fragments of some substructural logics, namely relevant and affine logic. The corresponding formal calculi are obtained by syntactic restrictions, along with modifications of the reduction rules and the type assignment system. The pre-terms of λr are given by the following abstract syntax: Pre-termsf: =x|λx.f|ff|xf|x <x1x2f where x ranges over a denumerable set of term variables, λx.f is an abstraction,ff is an application, xf is a thinning and x <x1x2f is a contraction. λr-terms are derived from the set of pre-terms by inference rules, that informally specify that bound variables must actually appear in a term and that each variable occurs at most once. Operational semantics of λr-calculus is defined by four groups of reduction rules and some equivalencies. The main computational step is the standard β reduction, executed by substitution defined as meta-operator. The group of(γ) reductions performs propagation of contraction into the term. Similarly, (ω) reductions extract thinning out of the terms. This discipline allows us to optimize the computation by delaying duplication of variables on the one hand, and by performing erasure of variables as soon as possible on the other. Finally, the rules in (γω) group explain the interaction between explicit resource operators that are of different nature. The simple types are introduced to the λr-calculus in the following figure. In the obtained system λr→, thinning is explicitly controlled by the choice of the axiom, while the control of the contraction is managed by implementing context-splitting style (i.e. requiring thatΓ,∆represents disjoint union of the two bases). Modifications of the λr→ system can provide the computational interpretation of some substructural logics, different from the usual approach via linear logic. For instance, if one excludes the (Thin) rule but preserves the axiom that controls the introduction of variables, the resulting system would correspond to the logic without thinning and with explicit control of contraction i.e. to the variant of implicative fragment of relevance logic. Similarly, if one excludes the( Cont)rule, but preserves context-splitting style of the rest of the system, correspondence with the variant of the logic without contraction and with explicit control of thinning i.e. implicative fragment of affine logic is obtained. Naturally, these modifications also require certain restrictions on the syntactic level, changes in the definition of terms and modifications of operational semantics as well. We also proposed intersection type assignment systems for both the λr-calculusand its substructural restrictions, that enable the specification of the role of a variable in a term and therefore can be naturally connected with the resource control term calculi. Although the proposed systems may be considered naive due to the fact that they only correspond to implicative fragments of relevant and affine logics and therefore are not able to treat characteristic split conjunction and disjunction connectives, they could be useful as a simple and neat logical foundation for the specific relevant and affine programming languages.