Journal of Logic and Computation, Volume 10, Issue 3, pp. 349-380: Abstract.
Relating the [lgr][sgr]- and [lgr]s-styles of explicit substitutions
F Kamareddine1 and A Rìos2
1Department of Computing and Electrical Engineering, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, UK, E-mail: firstname.lastname@example.org, 2Department of Computer Science, University of Buenos Aires, Pabellón I - Ciudad Universitaria (1428) Buenos Aires, Argentina, E-mail: email@example.com
The aim of this article is to compare two styles of Explicit Substitutions: the [lgr][sgr]- and [lgr]s-styles. We start by introducing a criterion of adequacy to simulate [bgr]-reduction in calculi of explicit substitutions and we apply it to several calculi: [lgr][sgr], [lgr][sgr][uArr], [lgr]v, [lgr]s, [lgr]t, and [lgr]u. The latter is presented here for the first time and may be considered as an adequate variant of [lgr]s. By doing so, we establish that calculi à la [lgr]s are usually more adequate at simulating [bgr]-reduction than calculi in the [lgr][sgr]-style. In fact, we prove that [lgr]t is more adequate than [lgr]v and that [lgr]u is more adequate than [lgr]v, [lgr][sgr][uArr] and [lgr]s. We also give counterexamples to show that all other comparisons are impossible according to our criterion.
Our next step consists in presenting the [lgr][ohgr] and [lgr][ohgr]e calculi, the two-sorted (term and substitution) versions of the [lgr]s and [lgr]se calculi, respectively. We establish an isomorphism between the [lgr]se and the term restriction of [lgr][ohgr]e. Since the [lgr][ohgr] and [lgr][ohgr]e calculi are given in the style of the [lgr][sgr]-calculus they are bridge calculi between [lgr]s and [lgr][sgr] and between [lgr]se and [lgr][sgr] and thus we are able to better understand one calculus in terms of the other. Finally, we present typed versions of all the calculi and check that the above mentioned isomorphism preserves types.
As a consequence, the [lgr][ohgr]-calculus is a calculus in the [lgr][sgr]-style that has the following properties: (a) [lgr][ohgr] simulates one step [bgr]-reduction, (b) [lgr][ohgr] is confluent (on closed terms), [lgr][ohgr] preserves strong normalization, (d) [lgr][ohgr]'s associated calculus of substitutions is SN, (e) the simply typed [lgr][ohgr] calculus is SN, (f) the [lgr][ohgr]-calculus possesses and extension [lgr][ohgr]e that is confluent on open terms (terms with eventual metavariables of sort term only), and (g) the simply typed [lgr][ohgr]e calculus is weakly normalizing (on open term). As far as we know, the [lgr][ohgr]-calculus is the first calculus in the [lgr][sgr]-style that has all the properties (a)-(g). However, the open problem of the SN of the associated calculus of substitution of [lgr][ohgr]e remains unsolved and like in the case of [lgr][sgr], [lgr]v and [lgr]se, lgr;[ohgr]e does not have PSN.
Keywords: [lgr]-calculus, explicit substitutions, [lgr][sgr], [lgr]s.