0
$\begingroup$

It seems to me that recursive equations can always be presented as inference rules. For the forward direction, an example is addition over Peono numerals (built from $O$ and $S(\_)$)

$$ \begin{align} add(O, m) & = m \\ add(S(n), m) & = S(add(n, m)) \end{align} $$

which can be also presented as

$$ \frac{ }{add(O, m) = m} \qquad \frac{add(n, m) = a}{add(S(n), m) = S(a)} $$

Is the backward conversion (from inference rules to recursive equations) always possible? If not, it seems inference rules more general, right? Except the superficial difference between the presentations, is there any other deeper difference between the two?

$\endgroup$
  • 1
    $\begingroup$ One obvious rematk is that equality is itself based on the use of (implicit) inference rules that include reflexivity, symmetry and substitution of equals for equals in any context (which implies transitivity). Your second example is only an instance of that substitution rule for equality. $\endgroup$ – babou Aug 7 '14 at 13:46
3
$\begingroup$

Inference rules are "more general". A recursive equation, actually any equation $E_1 = E_2$ is like an inference rule without premisses: $$\frac{}{E_1 = E_2}$$ A general inference rule may have premisses, and so it is like a conditional equation. Only very special kinds of inference rules may be equivalently expressed as equations. For instance, it seems difficult to express $$\frac{a \bullet c = b \bullet c}{a = b}$$ and $$\frac{add(x,add(y,z)) = add(x,z)}{add(y,z) = z}$$ as equations.

$\endgroup$
  • $\begingroup$ But isn't the resulting set defined as (smallest) fixpoint of a recursive function built from the inference rules? $\endgroup$ – Raphael Aug 7 '14 at 12:31
  • $\begingroup$ @Raphael: I remember I have seen inference rules being used to present corecursion. $\endgroup$ – day Aug 7 '14 at 12:55
  • $\begingroup$ @AndrejBauer: According to the first sentence of your answer, the second rule in my example may be presented simply as $add(S(n), m) = S(add(n, m))$ with an empty set of premises. Is there any difference between the two presentations? $\endgroup$ – day Aug 7 '14 at 13:01
  • $\begingroup$ Looking at your two examples, the second is an instance of the first with $a=add(y,z)$, $b=z$ and $\bullet=\lambda x y.add(y,x)$. This said, I tend to agree with you, but I do not know why, and you only say: "it seems difficult", which is hardly a proof. - - Suppose I postulate the unary operator $-$, and the nullary operator $0$, and the equalities $c\bullet-c=0$ and $(a\bullet b)\bullet c= a\bullet(b\bullet c)$ and $a\bullet 0=a$. Then I no longer need the inference rule (that is pretty much how $\mathbb{Z}$ is actually constructed). Well, I use the equality inference rules, always implicit. $\endgroup$ – babou Aug 7 '14 at 13:33
  • $\begingroup$ @Raphael: what "resulting set" are you referring to? The set of derivable statements? You can define it either as a least point, or expicitly ("those statements for which there exists a finite derivation tree"). $\endgroup$ – Andrej Bauer Aug 7 '14 at 14:07
0
$\begingroup$

I think recursion is more fundamental than inference rules. Note that I mentioned recursion and not recursive equation.

Recursion can be defined as a property of definition of some concept where the definition uses/include/refer to the concept itself that was being described. Now this concept can be anything or can have any particular representation. It could be inference rules, equations, relations, functions etc. From this point of view recursions is more fundamental than inference rules or any other notations of concepts.

UPDATE

To be more precise as par the question, yes it is possible to convert a inference rule to recursive equation if the inference rule is recursive.

$\endgroup$
  • $\begingroup$ Thanks for your input but you are not answering my question. $\endgroup$ – day Aug 7 '14 at 11:24
  • $\begingroup$ @day: If you mean "Is the backward conversion (from inference rules to recursive equations) always possible". Then answer is - Yes it is possible to do so if the inference rule is recursive. $\endgroup$ – Ankur Aug 7 '14 at 11:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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