DEFINITE CLAUSE PROGRAMS are CANONICAL
Howard A. Blair, Allen L. Brown · 1990
For each first-order language L with a nonempty Herbrand universe, we construct an algebra ~r interpreting the function symbols of L that is a model of the Clark equality theory with language L and is canonical in the sense that for every definite clause program P in the language L, Te ~ ~ o~ is the greatest fixed point of T~. The universe of individuals in r is a quotient of the set of terms of L and is, a fortiori, countable if L is countable. If s162 contains at least one function symbol of arity at least 2, then the graphs of partial recursive functions on ~, suitably defined, are representable in a natural way as individuals in cg.