My understanding is that recursive definitions are considered second-order since they require the fixpoint operator in order to be formulated as "true" definitions. This is even though they contain no higher order quantifiers eg.

times(x,s(y)) = plus(x,times(x,y))
times(x,0) = 0

needs to be written as times = \mu x. F(x) for some F, and the fixpoint operator is second order. I believe the same is true for recursive Horn clauses. But then why is a Prolog program considered first order, since it typically contains many recursive rules?


1 Answer 1


Horn clauses in prolog are not recursive definitions. They are logical formulas. For example,

times(_, 0, 0).
times(x, S(y), w) :- times(x,y,z), plus(x,z,w).

is not the definition of a recursive function, but just two logical formulas, written fully as \begin{gather*} \forall x .\, \mathtt{times}(x, 0, 0), \\ \forall x, y, w, z .\, \mathtt{times}(x,y,z) \land \mathtt{plus}(x,z,w) \Rightarrow \mathtt{times}(x,S(y),w). \end{gather*} Here $\mathtt{times}$ and $\mathtt{plus}$ are ternary relation symbols, $0$ is a constant, and $\mathtt{S}$ is a unary function symbol.

It is the case that the above formulas tell prolog how to search for solution to queries using a strategy (depth-first search) that resembles computation of functions given by recursive definitions, but the formulas themselves are just first-order logic statement.

As for the necessity of using the fixpoint $\mu$ operator for recursive definitions, there is no such necessity. We can directly define first-order functions using a schema that allows self reference. Such a schema may be translated to an application of $\mu$, but it does not have to be. One can explain it directly. For instance, primitive recursive functions are defined such a schema, without any fixed point operator.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.