ON FORMALIZATION OF NOTION OF $\delta$-REDUCTION IN MONOTONIC MODELS OF TYPED $\lambda$-CALCULUS

Abstract

In this paper monotonic models of typed $\lambda$-calculus are examined. Formal definition of concept of a $\delta$-reduction is given. Strong $\delta$-normalization and strong $\beta\delta$-normalization of terms are proved. The concept of a natural $\delta$-reduction is defined and the necessary and sufficient condition for uniqueness of a $\beta\delta$-normal form for such concept of a $\delta$-reduction is resulted.