Type system for λσ-calculus with all de Bruijn indices


  • Kaliana dos Santos Dias de Freitas




λσ-calculus, calculus of explicit substitutions, de Brujin indices, simple types


The λ-calculus was developed in the 30s as a mechanism of computing numerical functions. Its main operation is the β-conversion that performs the process of substitutions implicitly. In 1990 [1], Abadi, Cardelli, Curien, and Lèvy introduced an extension of λ-calculus, called λσ-calculus, using De Bruijn notation. The λσ-calculus is a calculus with explicit substitutions and its syntax contains just the natural number 1 and all the other natural numbers are encoded from the index 1 using closures with compositions of the shift operator (denoted by ↑). They showed that the λσ-calculus simulates the one-step β-reduction and it is confluent over its ground terms. In this work, we propose a variant of λσ-calculus with all De Bruin indices in its syntax, which we call λσdB-calculus and we adapt the proof of confluence of ground terms of λσ to the λσdB. We prove that λσdB enjoys the main properties of λσ: a) the subcalculus of substitutions is terminating and confluent, b) the full calculus simulates the β-reduction and c) it is confluent over ground terms, which are those without metavariables. Beside that, we define a system type for λσdB and we prove that the system is type checking decidable, soundness, equivalent with the the S1-system and with L1-system on σdB-nf.


Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.: Explicit substitutions. Journal of functional programming 1(4), 375–416 (1991)

Curien, P.L., Hardin, T., Lévy, J.J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM (JACM) 43(2), 362–397 (1996)

Curien, P.: Categorical combinators, sequential algorithms, and functional programming. Springer Science & Business Media (2012)

De Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In: Indagationes Mathematicae (Proceedings). vol. 75, pp. 381–392. Elsevier (1972

Hardin, T.: Confluence results for the pure strong categorical logic ccl. λ-calculi as subsystems of CCL. Theoretical computer science 65(3), 291–342 (1989)

Hindley, J.R.: Basic simple type theory, Cambridge Tracts in Theoretical Computer Science, vol. 42. Cambridge University Press (1997)

Kamareddine, F., Ríos, A.: A λ-calculus à la de bruijn with explicit substitutions. In: International Symposium on Programming Language Implementation and Logic Programming. pp. 45–62. Springer (1995)

Kamareddine, F., Ríos, A.: Efficiency of lambda-calculi with explicit substitutions. Technical Report TR-1996-3 (1996)

Kamareddine, F., Ríos, A.: Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms. Journal of Functional Programming 7(4), 395–420 (1997)

Kamareddine, F., Ríos, A.: Bridging de bruijn indices and variable names in explicit substitutions calculi. Logic Journal of the IGPL 6(6), 843–874 (1998)

Kamareddine, F., Ríos, A.: Relating the λσ-and λ s-styles of explicit substitutions. Journal of Logic and Computation 10(3), 349–380 (2000)

Melliès, P.A.: Typed λ-calculi with explicit substitutions may not terminate. In: International Conference on Typed Lambda Calculi and Applications. TLCA, vol. 902, pp. 328–334. Springer, Berlin, Heidelberg (1995)

Munõz, C.: Confluence and preservation of strong normalisation in an explicit substitutions calculus. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. pp. 440–447. IEEE (1996)

Munõz, C.: A left-linear variant of λσ. In: Algebraic and Logic Programming. vol. 1298, pp. 224–239. Springer (1997)




How to Cite

de Freitas, K. dos S. D. (2023). Type system for λσ-calculus with all de Bruijn indices. OBSERVATÓRIO DE LA ECONOMÍA LATINOAMERICANA, 21(10), 15260–15286. https://doi.org/10.55905/oelv21n10-041