The Basic Semantics of Untyped Functional Programs and Reduction Strategies

Abstract

The paper is devoted to untyped functional programs, which are defined as equation systems with separating variables in the untyped λ-calculus. The semantics of such programs is usually defined by means of the fix-point combinator Y . Previously, it was proved that the semantics of such programs is invariant with respect to the fix-point combinator. However, in this paper, we prove that this invariance is no longer valid when the reduction strategy is fixed.