×

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
PDFBibTeX XMLCite
Full Text: DOI