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

Abstract

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.