ON TYPED AND UNTYPED LAMBDA-TERMS
DOI:
https://doi.org/10.46991/PSYU:A/2015.49.2.045Keywords:
typed $\lambda$-terms, untyped $\lambda$-terms, translation, $\beta$-reduction, $\delta$-reductionAbstract
Typed $\lambda$-terms that use variables of any order and don't use constants of order $>1$ are studied in the paper. An algorithm of translation of typed $\lambda$-terms to untyped $\lambda$-terms is presented. According to that algorithm, each typed term $t$ is mapped to an untyped term $t'$. We study in which case typed terms $t_1$, $t_2$ such that $t_1 \to \to_{\beta\delta} t_2$ correspond to untyped terms ${t_1}',{t_2}'$ such that ${t_1}' \to\to_\beta {t_2}'.$
Downloads
Published
2015-06-12
How to Cite
Khondkaryan, T. (2015). ON TYPED AND UNTYPED LAMBDA-TERMS. Proceedings of the YSU A: Physical and Mathematical Sciences, 49(2 (237), 45–52. https://doi.org/10.46991/PSYU:A/2015.49.2.045
Issue
Section
Informatics
License
Copyright (c) 2015 Proceedings of the YSU
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.