Unification

In this note we present the basic theory of substitutions and a unification algorithm expressed in an applicative side-effect free programming language. 1 INTRODUCTION 1 1 Introduction Unification was first introduced in theorem proving by Robinson [9], and the problem is well known in the literature (see for example Siekmann [10]). Unification is ubiquitous in Computer Science; several applications are presented in [2]. The theory of unification is well established and it is briefly recalled here. Specifically, we introduce the representation of expressions, the theory of substitution and then the definition of most general unifier. Finally, we present a unification algorithm expressed in an applicative side-effect free programming language. Such a formulation has been formally synthesized by a logical specification using the deductive tableau method [7]. 2 Basic theories and conventions Before introducing the basic theories, a few remarks about the notation. We use lower case let..