ON THE UNIQUENESS OF β δ-NORMAL FORM OF TYPEDλ-TERMSFOR THE CANONICAL NOTION OF δ-REDUCTION
prev
next
prev
next
Author(s)
Author(s)
ON THE UNIQUENESS OF β δ-NORMAL FORM OF TYPEDλ-TERMSFOR THE CANONICAL NOTION OF δ-REDUCTION David Grigoryan
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.
DOI: 10.46991/PYSU:A/2019.53.1.037 Physical and Mathematical Sciences, 53(1 (248) 37-46