ON TYPED AND UNTYPED LAMBDA-TERMS

T.V. Khondkaryan

doi:10.46991/PSYU:A/2015.49.2.045

ON TYPED AND UNTYPED LAMBDA-TERMS

Authors

T.V. Khondkaryan Chair of Programming and Information Technologies, YSU, Armenia

DOI:

https://doi.org/10.46991/PSYU:A/2015.49.2.045

Keywords:

typed $\lambda$-terms, untyped $\lambda$-terms, translation, $\beta$-reduction, $\delta$-reduction

Abstract

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