A NECESSARY AND SUFFICIENT CONDITION FOR THE UNIQUENESSOFβ δ-NORMAL FORM OF TYPEDλ-TERMS FOR THE CANONICALNOTION OFδ-REDUCTION

Author(s)

A NECESSARY AND SUFFICIENT CONDITION FOR THE UNIQUENESSOFβ δ-NORMAL FORM OF TYPEDλ-TERMS FOR THE CANONICALNOTION OFδ-REDUCTION David GRIGORYAN

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.

DOI: 10.46991/PYSU:A/2019.53.1.028 Physical and Mathematical Sciences, 53(1 (248) 28-36

Download PDF

Keywords

canonical notion ofδ-reduction,β δ-reduction,β δ-normal form.

Check for updates

Share

Contact admin with any questions, comments or concerns

[email protected]