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

摘要

Explicit substitutions calculi are versions of the λ-calculus having a concretely defined operation of substitution. An Explicit substitutions calculus, λ_ε, extends the language A, of the A-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 un-decidable 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 them the one based on Scott's theorem.