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 →* λξ 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. © 2014 Springer-Verlag Berlin Heidelberg.