Computability became a subject of intensive research between 1930 and 1940, and led to various mathematical models, developed more or less independently, that capture in a nutshell the essence of performing computations mechanically. These models include Post’s production systems, Markov algorithms, Kleene’s recursive functions, Schoenfinkel’s and Curry’s combinators, Church’s &lgr;-calculus, and the Turing machine, all of which are equivalent with respect to provable propositions about what can and cannot be accomplished with algorithmic approaches to problem solving.

The main contribution of this paper is its attempt to introduce the concept of ρ-calculus as a generalization of a particular type of &lgr;-calculus. The authors propose two versions of the ρ-calculus, one with explicit matching and one with explicit substitutions, and a combined version of them. The content is structured into five sections.

The syntax and operational semantics of the ρ-calculus with explicit substitutions are presented in the second section of the paper. The ρ-calculus with explicit matching, extending the plain ρ-calculus with evaluation rules dealing with syntactic matching, and the combination of the proposed calculi are given a detailed treatment in the next two sections. The soundness of explicit substitutions, together with a series of such additional properties as soundness of multiplicity, preservation of multiplicity, and preservation of size are proven in the final part of the fourth section. Comments concerning the implementation of the proposed explicit ρ-calculi, conclusions, and suggestions for future research are supplied in the final section of the paper. The list of references contains some of the most outstanding published work in this field.

The computational models proposed in the paper are interesting and promising from the perspective of new developments and extensions in the area of theoretical computer science.