# Applying a particular rule to a held (or unevaluated) function

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].

• For very good tutorials on this subject see the notebook at library.wolfram.com/infocenter/ID/377 and Chapter 7 at dropbox.com/s/j2dsyvptnxjd369/Wagner%20All%20Parts-RC.pdf Mar 26, 2021 at 22:09
• Welcome to MMA SE! You might be looking for HoldForm[nat[10]] /. DownValues[nat][[2]]. /. acts on all parts of the expression, but all of those parts are within a HoldForm, so they don't evaluate any further. (Note that HoldForm is the same as Hold, with the only difference being how it prints in the output cell.) But, this has the unpleasant effect of not evaluating anything else in the expression, e.g. 10 - 1. To only hold occurrences of nat in an expression sounds like a good exercise! There are many ways to do that, but if you're stuck I can keep trying to help. Mar 26, 2021 at 23:38

ClearAll[nat];
rule1=nat[0]:>0;
rule2=nat[n_]:>1+nat[n-1];
(* The :> will change into a single character as you type. *)


Then apply use Replace (/.) with the rule you want to use like this.

nat[10]/.rule2
(* 1+nat[9] *)


You can do the following to see what happens after applying the rule several times.

useRule2[expr_]:=expr/.rule2;
Nest[useRule2,nat[10],4]
(* 4+nat[6] *)


However, experienced used do that as follows instead.

Nest[#/.rule2&,nat[10],4]
(* 4+nat[6] *)


Inspired by Ted Ersek's answer, I figured that the following steps work for me so far without having to explicitly convert and rewrite nat's preexisting definitions (as I am working with third-party code where the function of interest is defined by literally thousands of rules).

 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]