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.
Keywords: main canonical notion; $ δ $-reduction; $ βδ $-reduction; normal form