In this paper we consider a substitution and inheritance property, which isthe necessary and sufficient condition for the uniqueness of β δ-normal formof typed λ-terms, for canonical notion of δ-reduction. Typed λ-terms usevariables of any order and constants of order ≤1, where the constants of order1 are strongly computable, monotonic functions with indeterminate values ofarguments. The canonical notion ofδ-reduction is the notion ofδ-reductionthat is used in the implementation of functional programming languages.
No institution available
Mathematics
, 2025, Issue 1, pp. 1–10
ISSN Online: 0000-0000
DOI:
10.xxxx/example-doi