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.
No institution available
Mathematics
, 2025, Issue 1, pp. 1–10
ISSN Online: 0000-0000
DOI:
10.xxxx/example-doi