On Church-Rosser Property of Notion of βδ-Reduction for Canonical Notion of δ-Reduction
Keywords:Canonical notion of δ-reduction, Church-Rosser property, βδ-reduction
In this paper the canonical notions of δ-reduction for typed λ-terms are considered. Typed λ-terms use variables of any order and constants of order ≤ 1, where constants of order 1 are strongly computable, monotonic functions with indeterminate values of arguments. The canonical notions of δ-reduction are the notions of δ-reduction that are used in the implementations of functional programming languages. It is shown that for the main canonical notion of δ-reduction the notion of βδ-reduction has the Church-Rosser property. It is also shown that there exists a canonical notion of δ-reduction such that the notion of βδ-reduction does not have Church-Rosser property.
S.A.NigiyanandT.V.Khondkaryan,Oncanonicalnotionof±-reductionandontrans-lationoftyped ̧-termsintountyped ̧-terms,ProceedingsoftheYSU,PhysicalandMathematicalSciences,no.1,pp.46-52,2017.
How to Cite
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.