Natural Sciences, Mathematics, 2026
A NECESSARY AND SUFFICIENT CONDITION FOR THE UNIQUENESSOFβ δ-NORMAL FORM OF TYPEDλ-TERMS FOR THE CANONICALNOTION OFδ-REDUCTION
This is an open access article distributed under the
Creative Commons Attribution License, which permits unrestricted use, distribution,
and reproduction in any medium, provided the original work is properly cited.
Submitted: 2025-01-30
© 2026 by author(s) and The Gufo Inc.
This work is licensed under Creative Commons Attribution–NonCommercial International License
(CC BY-NC 4.0).
Abstract
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.