On typed and untyped lambda-terms

T. V. Khondkaryan

Proceedings of the Yerevan State University. Physical and mathematical sciences, no. 2 (2015), pp. 45-52

Résumé

Typed $\lambda$-terms that use variables of any order and don’t use constants of order $> 1$ are studied in the paper. Used constants of order $1$ are strong computable functions and each of them has an untyped $\lambda$-term, which $\lambda$-defines it. Besides, for the set of built-in functions there exists such a notion of $\delta$-reduction, that every typed term has a single normal form. 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^{\prime}$. 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^{\prime},\, t_2^{\prime}$ such that $t_1^{\prime}\to\to_{\beta} t_2^{\prime}$.

Détail

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