On the Computability of Relations on λ-Terms and Rice’s Theorem - The Case of the Expansion Problem for Explicit Substitutions

  • Edward Hermann Haeusler
  • Mauricio Ayala-Rincón
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8392)


Explicit substitutions calculi are versions of the λ-calculus having a concretely defined operation of substitution. An Explicit substitutions calculus, λ ξ , extends the language Λ, of the λ-calculus including operations and rewriting rules that explicitly implement the implicit substitution involved in β-reduction in Λ. Λ ξ , that is the language of λ ξ , might have terms without any computational meaning, i.e., that do not arise from pure lambda terms in Λ. Thus, it is relevant to answer whether for a given t ∈ Λ ξ , there exists s ∈ Λ such that \(s\rightarrow^*_{\lambda_\xi} t\), i.e., whether there exists a pure λ-term reducing in the extended calculus to the given term. This is known as the expansion problem and was proved to be undecidable for a few explicit substitutions calculi by using Scott’s theorem. In this note we prove the undecidability of the expansion problem for the λσ calculus by using a version of Rice’s theorem. This method is more straightforward and general than the one based on Scott’s theorem.


Explicit Substitution Lambda-Calculus Rice’s and Scott’s Theorem 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit Substitutions. J. of Functional Programming 1(4), 375–416 (1991)CrossRefzbMATHGoogle Scholar
  2. 2.
    Arbiser, A.: The Expansion Problem in Lambda Calculi with Explicit Substitution. J. Log. Comput. 18(6), 849–883 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Benaissa, Z.-E.-A., Briaud, D., Lescanne, P., Rouyer-Degli, J.: λυ, a Calculus of Explicit Substitutions which Preserves Strong Normalization. J. of Functional Programming 6(5), 699–722 (1996)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Bloo, R., Rose, K.H.: Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection. In: CSN-95: Computer Science in the Netherlands, pp. 62–72 (1995)Google Scholar
  5. 5.
    da Silva, F.H.: Expansibilidade em Cálculos de Substituições Explícitas. Master’s thesis, Graduate Program in Informatics, Universidade de Brasília (December 2012) (in Portuguese)Google Scholar
  6. 6.
    de Bruijn, N.G.: Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indag. Mat. 34(5), 381–392 (1972)CrossRefGoogle Scholar
  7. 7.
    de Moura, F.L.C., Ayala-Rincón, M., Kamareddine, F.: Higher-Order Unification: A structural relation between Huet’s method and the one based on explicit substitutions. J. Applied Logic 6(1), 72–108 (2008)CrossRefzbMATHGoogle Scholar
  8. 8.
    Dowek, G., Hardin, T., Kirchner, C.: Higher-order Unification via Explicit Substitutions. Information and Computation 157(1/2), 183–235 (2000)CrossRefzbMATHMathSciNetGoogle Scholar
  9. 9.
    Kamareddine, F., Ríos, A.: A λ-calculus à la de Bruijn with Explicit Substitutions. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol. 982, pp. 45–62. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  10. 10.
    Kesner, D.: The Theory of Calculi with Explicit Substitutions Revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 238–252. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. 11.
    Machtey, M., Young, P.: An introduction to the general theory of algorithms. Theory of computation series. Elsevier North-Holland, New York (1978)Google Scholar
  12. 12.
    Rice, H.G.: Classes of Recursively Enumerable Sets and Their Decision Problems. Trans. Amer. Math. Soc. 74, 358–366 (1953)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Rogers Jr., H.: Theory of recursive functions and effective computability. MIT Press, Cambridge (1987)Google Scholar
  14. 14.
    Rose, K.H.: Explicit Cyclic Substitutions. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 36–50. Springer, Heidelberg (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Edward Hermann Haeusler
    • 1
  • Mauricio Ayala-Rincón
    • 2
  1. 1.Departamento de InformáticaPUC-RioBrasil
  2. 2.Departamentos de Computação e MatemáticaUniversidade de BrasíliaBrasil

Personalised recommendations