A necessary and sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms
Proceedings of the Yerevan State University. Physical and mathematical sciences, Tome 53 (2019) no. 1, pp. 28-36.

Voir la notice de l'article provenant de la source Math-Net.Ru

In this paper the canonical notion of $\delta$-reduction is considered. Typed $\lambda$-terms use variables of any order and constants of order $\leq 1$, where the constants of order $1$ are strongly computable, monotonic functions with indeterminate values of arguments. The canonical notion of $\beta\delta$-reduction is the notion of $\delta$-reduction that is used in the implementation of functional programming languages. It is shown that for canonical notion of $\delta$-reduction SI-property is the necessary and sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms.
Keywords: Canonical notion of $\delta$-reduction, $\beta\delta$-reduction, $\beta\delta$-normal form.
@article{UZERU_2019_53_1_a4,
     author = {L. Budaghyan and D. A. Grigoryan and L. H. Torosyan},
     title = {A necessary and  sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms},
     journal = {Proceedings of the Yerevan State University. Physical and mathematical sciences},
     pages = {28--36},
     publisher = {mathdoc},
     volume = {53},
     number = {1},
     year = {2019},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/UZERU_2019_53_1_a4/}
}
TY  - JOUR
AU  - L. Budaghyan
AU  - D. A. Grigoryan
AU  - L. H. Torosyan
TI  - A necessary and  sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms
JO  - Proceedings of the Yerevan State University. Physical and mathematical sciences
PY  - 2019
SP  - 28
EP  - 36
VL  - 53
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/UZERU_2019_53_1_a4/
LA  - en
ID  - UZERU_2019_53_1_a4
ER  - 
%0 Journal Article
%A L. Budaghyan
%A D. A. Grigoryan
%A L. H. Torosyan
%T A necessary and  sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms
%J Proceedings of the Yerevan State University. Physical and mathematical sciences
%D 2019
%P 28-36
%V 53
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/UZERU_2019_53_1_a4/
%G en
%F UZERU_2019_53_1_a4
L. Budaghyan; D. A. Grigoryan; L. H. Torosyan. A necessary and  sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms. Proceedings of the Yerevan State University. Physical and mathematical sciences, Tome 53 (2019) no. 1, pp. 28-36. http://geodesic.mathdoc.fr/item/UZERU_2019_53_1_a4/

[1] S. A. Nigiyan, “On Non-classical Theory of Computability”, Proceedings of the YSU. Physical and Mathematical Sciences, 2015, no. 1, 52–60 | Zbl

[2] S. A. Nigiyan, T. V. Khondkaryan, “On Canonical Notion of $\delta$-Reduction and on Translation of Typed $\lambda$-Terms into Untyped $\lambda$-Terms”, Proceedings of the YSU. Physical and Mathematical Sciences, 51:1 (2017), 46–52 | Zbl

[3] L. E. Budaghyan, “Formalizing the Notion of $\delta$-Reduction in Monotonic Models of Typed $\lambda$-Calculus”, Algebra, Geometry $\$ Their Applications, 1 (2002), 48–57 | MR | Zbl

[4] H. Barendregt, The Lambda Calculus. Its Syntax and Semantics, North-Holland Publishing Company, Amsterdam–New York–Oxford, 1981, 654 pp. | MR | Zbl