Symbolic comparison of recursive functions

I would like to test two recursive functions for equality for all arguments. So far I have this:

f[0]:=1

f[n_] := n f[n - 1]

ForAll[x,  x>=0, f[x]==f[x]]


It is clear that the result must be true. But I get this:

∀{x},x≥0 Hold[f[x]==f[x]]


Why and what would be the best way to do so?

Every tip is highly appreciated. Thanks in advance.

• For one, your f is recursive, so I recommend memoization. i.e. change the second definition to f[n_] := f[n] = n f[n - 1]. That way, values of each f[n] is saved and does not have to be re-evaluated (significantly reduces time required to compute for high n values). That being said, you get an error message with your code because the x in f[x] is not an integer. Subtracting 1 repeatedly never gets to 0. You can solve this by limiting the input to integers only. i.e. change the second line to f[n_Integer] := f[n] = n f[n - 1]. Oct 1, 2016 at 15:33
• Don't you get an error from your code? If so, what is it? It might be a clue. Oct 1, 2016 at 15:34
• What do you actually want to achieve with your last command ForAll ? Oct 1, 2016 at 15:41
• @yarchik I use Mathematica only for one day. I try to write a model checking procedure for software components and do not know how to compare two functions symbolically. So the easiest way, as for inexperienced user, was to make functions have all possible arguments to say that for the same input the components (functions) have the same output. Ideally it would be great to learn how to unfold the functions automatically. Oct 1, 2016 at 19:21

Since the recursion will only stop for positive integer values of the argument, the argument should be explicitly restricted.

Clear[f1];
f1[0] = 1;
f1[n_Integer?Positive] := f1[n] = n f1[n - 1];


A closed-form solution can be found with RSolve

Clear[f2];
f2[n_] = f2[n] /. RSolve[{f2[n] == n*f2[n - 1], f2[0] == 1}, f2[n], n][[1]]

(*  Pochhammer[1, n]  *)


The functions are identical for nonnegative integer arguments

And @@ Table[f1[n] == f2[n] == n!, {n, 0, 100}]

(*  True  *)


However, the closed-form expression is not limited to integer values of the argument.

Show[
DiscretePlot[f1[n], {n, 0, 4}, PlotStyle -> Red],
Plot[f2[n], {n, -3, 4.1}, PlotRange -> {0, (4.1)!}],
PlotRange -> {{-3, 4.1}, {0, (4.1)!}}]


EDIT: Alternatively, using FindSequenceFunction

f3[n_] = FindSequenceFunction[f1 /@ Range[10], n]

(*  n!  *)


f2 and f3 are just alternate representations and are equal for all n

f2[n] == f3[n] // FullSimplify

(*  True  *)

• Thanks very much for the answer, Bob! One question: what does this "And @@ Table[f1[n] == f2[n] == n!, {n, 0, 100}]" mean and why is it not this possible to compare the functions symbolically, by writing f1[t]==f2[t], letting Mathematica symbolically unfold these functions? Thanks for your help. Oct 1, 2016 at 18:21
• @IgorShumeiko - f1 is not defined for a symbolic argument so f1[t] cannot be evaluated unless t is given a specific nonnegative integer value. The Table does the comparison for specific numeric values and returns a list of True/False values. And@@list applies the logical And to the list and evaluates to True only if all list values are True. Oct 1, 2016 at 18:34
• Thanks for the comment. I ask this because I would like to prove something like this (very simplified example): S1[0,a_]=0 S1[t_,a_]:=S1[t-1,a]+1/; a[t-1] S1[t_,a_]:=0/; !a[t-1] S2[0,a_]=0 S2[t_,a_]:=S2[t-1,a]+2/; a[t-1] S2[t_,a_]:=0/; !a[t-1] S1[t,port]==2*S2[t,port] Since the function port[t] is unknown, I assume that it must be done symbolically. Oct 1, 2016 at 21:24
• @IgorShumeiko - I cannot make sense of your comment the way it is formatted. Recommend that you open a new question and use proper code blocks to ask your question. Oct 1, 2016 at 21:33
• Makes sense. new question link Oct 1, 2016 at 22:18

Okay so first the solution:

Clear[f]
f[0]=1;
f[n_?NumericQ]:=n f[n-1]
ForAll[x,x>=0,f[x]==f[x]]


True

So what happened here?

1. I added Clear so
your old definitions does not interfere with us.
2. I changed your f[0] to a Set instead of a SetDelayed
3. I added a ?NumericQ behind your function parameter. So why does that help? Well if we would leave the x in there, we'll get a infinite recursion because it will not reach zero. The ?NumericQ argument waits for a numeric input. If the function does not get one, it keeps unevaluated. And ForAll knows that a function (whatever it is) which equals itself, is always true.

• Thanks for very much for the answer. What if we have two functions, let us assume they are the same, and we write at the end: ForAll[x,x>=0,f[x]==g[x]]. It gives out ∀ x,x≥0 f[x]==g[x], which is not that I expected. How to get "true"? If I write g[x]==f[x], it says g[x]==f[x]. I just need to check whether they can be unfolded to the same expressions. Thanks for your help! Oct 1, 2016 at 19:25