Haeusler, Edward Hermann; Ayala-Rincón, Mauricio On the computability of relations on \(\lambda \)-terms and Rice’s theorem – the case of the expansion problem for explicit substitutions. (English) Zbl 1406.03040 Pardo, Alberto (ed.) et al., LATIN 2014: theoretical informatics. 11th Latin American symposium, Montevideo, Uruguay, March 31 – April 4, 2014. Proceedings. Berlin: Springer (ISBN 978-3-642-54422-4/pbk). Lecture Notes in Computer Science 8392, 202-213 (2014). Summary: Explicit substitutions calculi are versions of the \(\lambda \)-calculus having a concretely defined operation of substitution. An Explicit substitutions calculus, \(\lambda _{\xi }\), extends the language \(\Lambda \), of the \(\lambda \)-calculus including operations and rewriting rules that explicitly implement the implicit substitution involved in \(\beta \)-reduction in \(\Lambda \). \(\Lambda _{\xi }\), that is the language of \(\lambda _{\xi }\), might have terms without any computational meaning, i.e., that do not arise from pure lambda terms in \(\Lambda \). Thus, it is relevant to answer whether for a given \(t \in \Lambda _{\xi }\), there exists \(s \in \Lambda \) such that \(s\rightarrow^*_{\lambda_\xi} t\), i.e., whether there exists a pure \(\lambda \)-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 \(\lambda \sigma \)-calculus by using a version of Rice’s theorem. This method is more straightforward and general than the one based on Scott’s theorem.For the entire collection see [Zbl 1284.68026]. MSC: 03B40 Combinatory logic and lambda calculus Keywords:explicit substitution; \(\lambda\)-calculus; Rice’s theorem; Scott’s theorem PDFBibTeX XMLCite \textit{E. H. Haeusler} and \textit{M. Ayala-Rincón}, Lect. Notes Comput. Sci. 8392, 202--213 (2014; Zbl 1406.03040) Full Text: DOI