ON FORMALIZATION OF NOTION OF δ-REDUCTION IN MONOTONIC MODELS OF TYPED λ-CALCULUS - Budaghyan, L. E. (Proceedings of the YSU A: Physical and Mathematical Sciences, 2003)
In this paper monotonic models of typed λ-calculus are examined. Formal definition of concept of a δ-reduction is given. Strong δ-normalization and strong βδ-normalization of terms are proved. The concept of a natural δ-reduction is defined and the necessary and sufficient condition for uniqueness of a βδ-normal form for such concept of a δ-reduction is resulted.