ON MAIN CANONICAL NOTION OF δ -REDUCTION - Grigoryan, D.A. (Proceedings of the YSU A: Physical and Mathematical Sciences, 2018)
In this paper the main canonical notion of δ -reduction is 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 notion of δ -reduction is the notion of δ -reduction that is used in the implementation of functional programming languages. For main canonical notion of d-reduction the uniqueness of βδ -normal form of typed λ -terms is shown.