Abstract

The ρ-calculus integrates in a uniform and simple setting first-order rewriting, λ-calculus and non-deterministic computations. Its abstraction mechanism is based on the rewrite rule formation and its main evaluation rule is based on matching modulo a theory T.In this first part, the calculus is motivated and its syntax and evaluation rules for any theory T are presented. In the syntactic case, i.e. when T is the empty theory, we study its basic properties for the untyped case. We first show how it uniformly encodes λ-calculus as well as first-order rewriting derivation. Then we provide sufficient conditions for ensuring confluence of the calculus