Applying a particular rule to a held (or unevaluated) function in Mathematica

user_6553853 0
Viewed 113

I am a very novice Mathematica user and still can't get my head around its evaluation control, all possible constructs related to it (e.g. Hold, Unevaluated, etc.) and how they work, despite the thorough documentation and the numerous StackExchange and StackOverflow questions discussing this topic. So, apologies for any possible duplicates.

My use case is the following: I have a function (say f) defined by thousands of rules and patterns (DownValues). I want to start from an unrolled representation of f[expr] (for some expr) and get the result of applying a single, particular rule to f[expr]. I want the result to stay unrolled as well.

As a particular example, suppose we have the following:

 In[1]: nat[0] := 0
 In[2]: nat[n_] := 1 + nat[n - 1]
 In[3]: DownValues[nat]
Out[3]: {HoldPattern[nat[0]] :> 0, HoldPattern[nat[n_]] :> 1 + nat[n - 1]}
 In[4]: nat[10]
Out[4]: 10

Now, I want to start from an expression represented as nat[10] (unevaluated!) and want to specifically apply the second rule (HoldPattern[nat[n_]] :> 1 + nat[n - 1]) to obtain the expression in the form of 1 + nat[9]. Analogously, shall I wish to apply the first rule (HoldPattern[nat[0]] :> 0), I would expect the result to stay unchanged in its original form, i.e. nat[10].

Thank you for your help!

wolfram-mathematica
2 Answers

This should help with your understanding of Mathematica's method of operation.

Wolfram reference : The Ordering of Definitions

I.e. Mathematica "looks for the value of an expression of the form f[n], it tries the special case f[1] first, and only if this does not apply, it tries the general case f[n_]."

So with the functions below nat[0] is always tried first, but of course it only evaluates if the argument is 0. Then nat[n_] is tried.

nat[0] := 0
nat[n_] := 1 + nat[n - 1]

For your question as to obtaining 1 + nat[9] here is one way

Clear[nat]

nat[0] := 0
nat[n_] := HoldForm[1 + nat[o]] /. o -> n - 1

ans = nat[10]

1 + nat[9]

Do[ans = ReleaseHold[ans], 10]

ans

10

Alternatively (and better)

Clear[nat]

nat[0] := 0
nat[n_] := With[{m = n - 1}, HoldForm[1 + nat[m]]]

ans = nat[10]

1 + nat[9]

Do[ans = ReleaseHold[ans], 9]

ans

9 + (1 + nat[0])

Note this is the result after 10 iterations. The final ReleaseHold results in nat[0] evaluating to 0.

ReleaseHold[ans]

10

You might find it easier to see what is happening if you use Hold instead of HoldForm in the above demonstration.

user_8796010

As posted as a reply in a parallel discussion in Mathematica's StackExchange, I found a relatively more direct and straightforward way of dealing with the problem:

 In[6] rules = DownValues[nat]                                                 
Out[6] {HoldPattern[nat[0]] :> 0, HoldPattern[nat[n_]] :> 1 + nat[n - 1]}

 In[7] DownValues[nat] = {}                                                    
Out[7] {}

 In[8] nat[10]                                                                 
Out[8] nat[10]

 In[9] nat[10] /. rules[[1]]                                                   
Out[9] nat[10]

 In[10] nat[10] /. rules[[2]]                                                  
Out[10] 1 + nat[9]
user_65538530
Related