C-expressions: A variable-free calculus for equational logic programming (Q1208416)

Substitution is the basic notion used to formalize the computational model of functional (\(\beta\)-rule of \(\lambda\) calculus) and logic (resolution) languages. However, substitutions and related operations, such as instantiation and unification, are metalevel notions which are not expressed in the language. Moreover, most of the implementations of functional and logic languages do not provide explicit representation of substitutions: variable bindings are maintained using implementation structures which are not very close to language constructs. In the case of functional languages, a first proposal to fill the gap between theory and implementation was based on combinatory logic. A more recent approach is based on an extended \(\lambda\)-calculus which allows explicit manipulation of substitutions. The authors use a similar approach to deal with narrowing for equational languages and with resolution for logic programming. The basic idea is to represent explicitely in the language the notion of most general instance: this allows to avoid substitutions since all the relevant operations (such as unification) can be expressed in terms of mgi. Moving from an existing algebra of first order atomic formulas, it is proposed an abstract syntax (\(c\) expressions) for linear structures of atomic formulas which does not uses variables. Using a suitable notion of normal form the authors then show that the computation of mgi can be expressed as a \(c\)-expression normalization. A term rewriting system for the computation of the normal form is provided and it is used to define reduction machines for narrowing and unification. Finally issues concerning efficiency, both in time and space, and parallelization of the calculus based on \(c\)-expressions are discussed.