This work is licensed under Creative Commons Attribution–NonCommercial International License
(CC BY-NC 4.0).
n this paper the canonical notion ofδ-reduction is considered. Typedλ-terms use variables of any order and constants of order≤1, where theconstants of order 1 are strongly computable, monotonic functions with indeter-minate values of arguments. The canonical notion ofδ-reduction is the notionofδ-reduction that is used in the implementation of functional programminglanguages. It is shown that for canonical notion ofδ-reduction SI-property isthe necessary and sufficient condition for the uniqueness ofβ δ-normal form oftypedλ-terms.