On procedural semantics of strong typed functional programs

The paper is devoted to procedural semantics of strong typed functional programs that are based on interpretation algorithms. These algorithms use three operations: substitution, one-step $\beta$-reduction and one-step $\delta$-reduction. It is proved that the procedural semantics, based on any of such algorithms are consistent. It is also proved that procedural semantics, based on sevеral interpretation algorithms are incomparable.