Geodesic
On typed and untyped lambda-terms
Proceedings of the Yerevan State University. Physical and mathematical sciences, no. 2 (2015), pp. 45-52 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

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}$.
Keywords: typed $\lambda$-terms, untyped $\lambda$-terms, translation, $\beta$-reduction, $\delta$-reduction. 
@article{UZERU_2015_2_a7,
     author = {T. V. Khondkaryan},
     title = {On typed and untyped lambda-terms},
     journal = {Proceedings of the Yerevan State University. Physical and mathematical sciences},
     pages = {45--52},
     year = {2015},
     number = {2},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/UZERU_2015_2_a7/}
}
TY  - JOUR
AU  - T. V. Khondkaryan
TI  - On typed and untyped lambda-terms
JO  - Proceedings of the Yerevan State University. Physical and mathematical sciences
PY  - 2015
SP  - 45
EP  - 52
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/UZERU_2015_2_a7/
LA  - en
ID  - UZERU_2015_2_a7
ER  - 
%0 Journal Article
%A T. V. Khondkaryan
%T On typed and untyped lambda-terms
%J Proceedings of the Yerevan State University. Physical and mathematical sciences
%D 2015
%P 45-52
%N 2
%U http://geodesic.mathdoc.fr/item/UZERU_2015_2_a7/
%G en
%F UZERU_2015_2_a7
T. V. Khondkaryan. On typed and untyped lambda-terms. Proceedings of the Yerevan State University. Physical and mathematical sciences, no. 2 (2015), pp. 45-52. http://geodesic.mathdoc.fr/item/UZERU_2015_2_a7/

[1] S.A. Nigiyan, “Functional Languages”, Programming and Computer Software, 1991, no. 5, 77–86 | Zbl

[2] L.E. Budaghyan, “Formalizing the Notion of $\delta$-Reduction in Monotonic Models of Typed $\lambda$-Calculus”, Algebra, Geometry $\$ Their Applications, v. 1, YSU Press, Yer., 2002, 48–57 | MR

[3] H. Barendregt, The Lambda Calculus Its Syntax and Semantics, North-Holland Pub. Comp., 1981 | MR | Zbl

[4] S. A. Nigiyan, “On non-classical theory of computability”, Proceedings of the YSU, Physics Mathematics, 2015, no. 1, 52–60 | Zbl