TY - JOUR
AU - Grigoryan, Davit A.
PY - 2021/12/10
Y2 - 2024/04/21
TI - On Church-Rosser Property of Notion of βδ-Reduction for Canonical Notion of δ-Reduction
JF - Mathematical Problems of Computer Science
JA - MPCS
VL - 50
IS -
SE - Articles
DO - 10.51408/1963-0024
UR - http://mpcs.sci.am/index.php/mpcs/article/view/62
SP - 81-87
AB - <p>In this paper the canonical notions of δ-reduction for typed λ-terms are considered. Typed λ-terms use variables of any order and constants of order ≤ 1, where constants of order 1 are strongly computable, monotonic functions with indeterminate values of arguments. The canonical notions of δ-reduction are the notions of δ-reduction that are used in the implementations of functional programming languages. It is shown that for the main canonical notion of δ-reduction the notion of βδ-reduction has the Church-Rosser property. It is also shown that there exists a canonical notion of δ-reduction such that the notion of βδ-reduction does not have Church-Rosser property.</p>
ER -