# Message Boards

Answer
(Unmark)

GROUPS:

3

# [WWS22] Characterisation of infinitary rewrite systems

Posted 14 days ago

Can we say something finite about non-terminating rewrite systems beyond just stating the fact that they do not terminate? We examine multiple classes of rewrite systems: terminating, slowly terminating and non-terminating, and develop methods of analysis that enable us to reason about their behaviour. The main outcome of this work is an exemplified connection between continuous dynamical systems and the Wolfram Physics Project. As next steps we outline some potential future directions in the study of functional evolution equations and multiway systems over continuous domains.
Motivation Many computations in practice do not actually halt without user interruption; for example computing the transcendental number π, running physical simulations or training a neural network. Non-halting computations are of interest for two reasons. On the one hand, we want efficient, high-level programming languages that permit us to express infinite objects, infinite sets and infinite series - programs that yield progressive precision, where intermediate results are generated with ever-increasing detail over time. On the other hand, infinite rewriting is of importance to the efforts ongoing within the Wolfram Physics Project, in which continuum-limiting properties of rewrite systems inevitably arise. We give a brief description of rewrite systems, both finitary and infinitary, highlighting the properties and categorisations of such systems and touching on the topics of non-termination proof and undecidability. We then conduct some simple experiments on multiway systems of recursive functions, building up to an illustrative example that shows how continuous-time dynamics arise out of the resulting abelian flows.
Introduction and Definitions
Historical Background Almost a century ago, the mathematician Alonzo Church developed the λ-calculus, likely the most famous term rewriting system in existence, which played a key role in mathematical logic and the formalization of computability. Given that λ-calculus terms operate on other λ-calculus terms, and even on themselves, questions arose around the topic of semantics. Later, the work of Dana Scott and Gordon Plokin introduced the concept of denotational semantics of programming languages: a formalization of the meaning of programs through the construction of mathematical objects, and operational semantics - a formal treatment of program properties and behaviour. Their work also showed that total functions can model the untyped λ-calculus.
Term Rewriting Rewriting is the repeated transformation of a discrete structured symbolic object according to a set of rules and is the computational formalism underpinning functional programming, logic programming and the Wolfram Model of Fundamental Physics. Term rewriting is a concrete instance of rewriting where the objects operated upon are tree-like expressions consisting of variables and function symbols. One source of interest in term rewriting systems is their dual interpretation, rules are both syntactic transformations and can also be interpreted as equations. Term rewriting systems are favourable due to their simplicity. They enable rigorous mathematical analysis and provide a natural means for effective computation whilst also supporting abstract data types and theorem proving. A more complete and formal description can be found in [1]. In discussing term rewriting systems the following properties are often discussed, this is by no means a complete list. ◼ Termination (or the Noetherian property) - the existence of at least one normal form ◼ Weak normalization - every term is eventually reducible to a normal form ◼ Strong normalization - every sequence of rewrites on at least one term eventually terminates with a normal form ◼ Confluence - the restriction to exactly one normal form, implying convergence of critical pairs ◼ Canonicity - that every term rewrites to a unique canonical form ◼ Church-Rosser property - a permutation invariance on the ordering of rewrite rule application ◼ Orthogonality - reduction rules are left-linear, where each variable occurs only once on the left-hand side This is by no means a complete list. Understanding of the above properties is not assumed in the rest of this article, and it is worth highlighting that these definitions do not always hold for infinitary term rewriting.
Infinitary Term Rewriting Before giving a description of infinitary term rewriting let us look at an example demonstration in the Mathematica language. x //. x -> {x, x} For clarity this expression in full form is: ReplaceRepeated[x, Rule[x, List[x, x]]] Note that if you do run this you will need to press [Alt+.] to stop the computation. Congratulations! You’ve just solved the halting problem. Of course this is not actually the case; however, you have done something very interesting - you have ran an infinitary term rewriting system. Infinitary rewriting generalizes ordinary finitary rewriting to infinite terms with a notion of convergence, including reductions of ordinal lengths larger than ω ω ω+ω 2 ω An interesting point to note is that term graph rewriting, that is, graph rewriting on term graphs, subsumes infinitary term rewriting by representing potentially infinite reductions with cycles in the term graph. As an example, the infinite Böhm trees of the meaningless terms produced by the Ω Y In the context of equational reasoning one may make use of e-graphs [2], data structures that capture congruence relations of terms through the process of equality saturation. E-graphs make use of edge-edge relations, a concept that appears in the meta-graph [3] representation. The set of all cyclic paths in a given e-graph represents all possible infinitary reductions of the underlying term rewriting system. With techniques such as this we could identify the currently problematic line above and return something like, Infinitary[x //. x -> {x, x}] instead off hitting the recursion limit. One might ask if higher representations always possess this infinity-subsumption property, do term hypergraphs subsume term graphs? Do simplicial complices, CW-complices and so on always subsume the infinitary behavior of the representation beneath? If there always exists a more powerful representation then this suggests the existence of a "representational" space in addition to our spatial, causal, branchial and rulial spaces.
Strong and Weak Convergence A very simple categorisation of infinitary rewrite systems we can make is strong vs. weak convergence. The notion of convergence was first substantially studied by Dershowitz in [4]. An illustrative example is given in [5], which we shall examine here. Let's take the term-rewriting system with a single rule: f(g(x))f(g(g(x)) f(g(g(g(...))))f( ω g In[]:= wcrules={f[g[x_]]->f[g[g[x]]]};ResourceFunction["MultiwayCombinator"][wcrules,f[g[x]],3,"StatesGraph"] Out[]= In[]:= wcstates=ResourceFunction["MultiwayCombinator"][wcrules,f[g[x]],3,"AllStatesList"]; In[]:= Map[(Position[ToExpression[#[[1]]],wcrules[[1,1]]]//Map[Length[#]&]//Max)&,wcstates] Out[]= {0,0,0,0} Now let’s examine the rule: g(x)g(g(c)) f(g(g(g(...))))f( ω g In[]:= scrules={g[c_]->g[g[c]]}; In[]:= ResourceFunction["MultiwayCombinator"][scrules,f[g[x]],3,"StatesGraph"] Out[]= In[]:= scstates=ResourceFunction["MultiwayCombinator"][scrules,f[g[x]],3,"AllStatesList"]; In[]:= Map[(Position[ToExpression[#[[1]]],scrules[[1,1]]]//Map[Length[#]&]//Max)&,scstates] Out[]= {1,2,3,4} Note that the depth at which rewriting takes place increases without bound allowing larger prefixes of the term to remain stable. This is a crucial property that enables us to relate the structure of the limiting term to that of the terms of the reduction sequence. Once we have the notion of a reduction that converges to a limit, we can continue to rewrite to sequences of transfinite length. Worthy of note is the fact that a given infinitary term-rewriting system may have a computable modulus of convergence; that is to say, there exists a computable function that expresses the growth of rule application depth as the infinitary process unfolds over time [6]. Of course, this is not always the case; there exist infinitary rewrite systems whose behaviour is not computable, thus escaping our attempts to make formal statements and constructive proofs concerning their properties. Rice’s Theorem states that all such non-trivial properties of programs are in the general case undecidable just as there are undecidable languages such as that of the Post Correspondence Problem. As a concrete example, the determination of productivity, the property that infinite computations will actually produce values indefinitely, is of analytical complexity 1 Π 1 1 Σ 1
Multiway Systems on Recursive Functions "The foundations of elementary arithmetic established by the recursive mode of thought, without the use of apparent variables ranging over infinite domains." – Thoralf Skolem We begin by looking at some terminating systems that exhibit interesting properties whilst having practical utility for illustrating the central idea of this project.
The Factorial Function In discussing the proof complexity intrinsic to statements about a given rewrite system and the topics of derivational and computational complexity, we now examine the simple case of primitive recursive functions. We can always know how many steps these computations will require to complete given the input. The factorial function is a perfect example of this and will also be useful later in our discussion. Here is its multiway states graph as it computes the value of 3! ResourceFunction["MultiwayCombinator"][{fac[0]->s[0],fac[s[x_]]->mul[s[x],fac[x]],mul[x_,0]->0,mul[x_,s[y_]]->add[mul[x,y],x],add[x_,0]->x,add[x_,s[y_]]->s[add[x,y]]},fac[s[s[s[0]]]],50,"StatesGraphStructure"] Out[]= Every node in this graph represents a unique state the system may occupy. The directed edges reveal the flow of state evolution within the system. One metric used within the Physics Project is the computation of the Hausdorff-Besicovitch dimension. Observing the fact that the volume V R d R d d log(V) log(R) Out[]= The connectivity structure of the multiway states graph for the factorial function interesting despite its simplicity. Note that this is a rare instance in which all paths from the initial state to the final state have exactly the same length, representing no opportunity for computational reducibility. We’ll soon see a progression to more complicated structures where this isn’t the case as we explore higher computational complexity classes.
The Hyperoperation Function The hyperoperation sequence is an infinite sequence of arithmetic operations that begins with the successor operation and continues with addition, multiplication, exponentiation, tetration, pentation, hexation and beyond to functions better-described by Knuth’s up-arrow notation. Each hyperoperation may be viewed as a recursive application of the previous one: a[n]ba[n-1](a[n](b-1)), n≥1 This function is recursive but not primitive recursive. We now observe the multiway states graph for H(n,2,3) n th n H(1,2,3) 2+3 In[]:= hrules={h[0,a_,b_]->s[b],h[s[0],a_,0]->a,h[s[s[0]],a_,0]->0,h[s[s[s[n_]]],a_,0]->s[0],h[s[n_],a_,s[b_]]->h[n,a,h[s[n],a,b]]}; In[]:= hc=ResourceFunction["MultiwayCombinator"][hrules,h[s[0],s[s[0]],s[s[s[0]]]],50,"StatesGraphStructure"] Out[]= extending to H(2,2,3) 23 In[]:= hc=ResourceFunction["MultiwayCombinator"][hrules,h[s[s[0]],s[s[0]],s[s[s[0]]]],50,"StatesGraphStructure"] Out[]= and finally H(3,2,3) 3 2 In[]:= hc=ResourceFunction["MultiwayCombinator"][hrules,h[s[s[s[0]]],s[s[0]],s[s[s[0]]]],50,"StatesGraphStructure"] Out[]= As we can see, the behaviour of the function, implemented here as a term rewriting system, grows rapidly even for small inputs. Let’s look at the partial evaluation of H(4,2,3) 3 2 2 2 In[]:= hc=ResourceFunction["MultiwayCombinator"][hrules,h[s[s[s[s[0]]]],s[s[0]],s[s[s[0]]]],110,"StatesGraphStructure"] Out[]= We see many interesting phases of state evolution as the system evolves, beginning with a thread of states that branch in two small bulbs before a section that lasts longer but then dies off back to a single linear thread again, after which there’s another explosion of state space. The Hausdorff dimension fluctuates wildly, Out[]= and we can plot its distribution for the above states graph. Out[]= We can also look at how the dimension fluctuates down a single path; for example, the shortest path from the initial state to our most recently computed state. Out[]=
General Recursive Functions "Indeed, if general recursive function is the formal equivalent of effective calculability, its formulation may play a role in the history of combinatory mathematics second only to that of the formulation of natural number." — Emil Post (1944) The general recursive functions are exactly the set of functions computable by a Turing machine. Studying their multiway behaviour takes us up to the computational complexity class R
The Ackermann Function The Ackermann function is one of the earliest examples of a total recursive function which is not primitive recursive, often used as a measure of a compiler’s ability to optimize recursion. The inverse function often appears in the time complexity analysis of some algorithms. An interesting relation noted in [6] states that a term rewriting system terminating from the Knuth-Benedix order (KBO) has a maximal number of rewrite steps bounded by the Ackermann function. Here is the multiway states graph for a system computing A(2,3) arules={a[0,n_]->s[n],a[s[m_],0]->a[m,s[0]],a[s[m_],s[n_]]->a[m,a[s[m],n]]}; In[]:= ac=ResourceFunction["MultiwayCombinator"][arules,a[s[s[0]],s[s[s[0]]]],60,"StatesGraphStructure"] Out[]= We can look at the expression depth at each state node throughout the multiway states evolution graph. Out[]= Additionally, we can also examine the rule application depth for each step of the computation . Out[]= The Hausdorff dimension plot shows connected regions of varying dimension that fluctuates throughout. Out[]= The dimension histogram shows a sharp cutoff after 2. Out[]= We can easily extend these fast-growing functions to infinitary systems by adding a fixed point rule into the rewrite system, for example: arules={a[0,n_]->s[n],a[s[m_],0]->a[m,s[0]],a[s[m_],s[n_]]->a[m,a[s[m],n]],a[m_,n_]->a[m,s[n]],a[m_,n_]->a[s[m],n]}; In[]:= ac=ResourceFunction["MultiwayCombinator"][arules,(*s[s[s[s[s[s[s[0]]]]]]]*)a[s[s[0]],s[s[s[0]]]],14,"StatesGraphStructure"] Out[]= This interesting structure results from the fact we are constantly instantiating new computations during the intermediate computations of A(a,b) In[]:= depths=Map[Depth[ToExpression[#]]&,VertexList[ac]];minDepth=Min[depths];maxDepth=Max[depths]; In[]:= Show[GraphPlot3D[ac,VertexRenderingFunction->({Hue[(Depth[ToExpression[#2]]-minDepth)/(maxDepth-minDepth)/2,1,1],EdgeForm[Black],Sphere[#,.09],Black}&)],Epilog->Inset[BarLegend[{Hue[(#-minDepth)/(maxDepth-minDepth)/2,1,1]&,{minDepth,maxDepth}}],{Right,Center},{Right,Center}]] Out[]= Or the Hausdorff dimension at each node. In[]:= mindims=Min[dims];maxdims=Max[dims]; In[]:= Show[GraphPlot3D[ac,VertexRenderingFunction->({Hue[0.5-((dims[[#2]]-mindims)/(maxdims-mindims)/2),1,1],EdgeForm[Opacity[0.1,Black]],Sphere[#,.05],Opacity[0.1,Black]}&)],Epilog->Inset[BarLegend[{Hue[(#-mindims)/(maxdims-mindims)/2,1,1]&,{mindims,maxdims}}],{Right,Center},{Right,Center}]] Out[]= The dimension histogram shows a much smoother distribution than the finitary case. Out[]=
Slowly Terminating Systems On our path to infinity we now consider slowly terminating systems as these will equip us with the conceptual tools that we will need later on .
Goodstein's Theorem and The Hydra Battle Since the construction of Gödel’s incompleteness theorems, it has been known that true statements expressible within a system may not be provable within the system itself. The first unprovable mathematical statements regarding the natural numbers, that were more “natural”, were discovered by Paris and Harrington [9]. This led to another independence result, Goodstein’s Theorem. Goodstein’s Theorem [10] is an example of a true theorem of the natural numbers that is independent of the Peano axioms. Unlike prior independence statements, which were combinatorial, Goodstein’s Theorem is entirely number-theoretic. One can view the Goodstein sequence as a game on a tree structure where the player, Hercules, cuts the heads off of the hydra, causing more heads to grow. One can assign ordinals to the nodes of the tree and consider the player’s moves as decreasing these ordinals. Due to the fact that there are no infinite strictly decreasing sequences of ordinals, the hydra will eventually die!
Goodstein Sequences Goodstein’s theorem states that all Goodstein sequences, each corresponding to a unique hydra game, will terminate at zero for all possible initial conditions. Let’s start by representing numbers by their hereditary base- n n n Out[]= 2+ 2 2 2 2 2 1+ 2 2 2 2+ 2 2 2 1+2+ 2 2 2 We call this G 0 G 1 Out[]= 854066918318573 Okay, that blew up pretty fast! Perhaps we should start smaller. Let’s try looking at the Goodstein sequence G n Out[]= {1,0} That died out in one step – so far so good. Let’s look at G n Out[]= {2,2,1,0} This time it took three steps before we reached zero. Let’s take a look at G n Out[]= {3,3,3,2,1,0} Five steps – that wasn’t so bad either. So we should see similar behaviour with the next number, G n Out[]= {4,26,41,60,83,109,139,173,211,253,299,348,401,458,519,584,653,726,803,884,969} Okay – it’s not terminating yet but we could be forgiven for assuming that it terminates soon. Well actually, amazingly, G n 3 402653211 2 3.2 80 10 2 121210614 10
Visualising the Goodstein Numerical Multiway System We can get a little insight into the behaviour of the base bump operation by looking at numerical multiway systems [11]. These allow us to look at the structure and behaviour of a given system of functions by transforming an initial numerical state and connecting edges to vertices representing unique numerical quantities produced by the system after each function application. Here we show the system n{ G 3 In[]:= ResourceFunction["NestGraphTagged"][n|->{nextGoodstein[n,3],n+1},Range[20],7,"StateLabeling"->False] Out[]= Similarly, we show n{ G 4 Out[]= Let’s go on a few more steps. This is what n{ G 5 Out[]= Finally, we remain on G n Out[]= If we look at (n,b){( G n G n+1 G n+3 ResourceFunction["MultiwaySystem"][<|"StateEvolutionFunction"->({Tuple[nextGoodstein[#1〚1〛,#1〚2〛],#1〚2〛+1],Tuple[nextGoodstein[#1〚1〛+1,#1〚2〛],#1〚2〛+1],Tuple[nextGoodstein[#1〚1〛+2,#1〚2〛],#1〚2〛+1],Tuple[nextGoodstein[#1〚1〛+3,#1〚2〛],#1〚2〛+1]}&),"StateEquivalenceFunction"->SameQ,"StateEventFunction"->Identity,"EventDecompositionFunction"->Identity,"EventApplicationFunction"->Identity,"SystemType"->"Function","EventSelectionFunction"->Identity|>,{Tuple[2,2]},24,"StatesGraphStructure","StateRenderingFunction"functionStateRenderingFunction,"EventRenderingFunction"functionEventRenderingFunction]//GraphPlot3D Out[]=
Translating the Hydra Game to a Term Rewriting System Now we translate the hydra game to a term rewriting system so that we can view it under our microscope. The termination of this rewriting system implies Goodstein’s theorem, but a proof of this requires the use of transfinite induction. Given the rules in [12] shown here, we observe the following progression of the multiway states graph. In[]:= HydraRules={Dott[x_]->FilledDot[Rect[x]],(*1*)FilledDot[Rect[x_]]->Rect[FilledDot[FilledDot[x]]],(*2*)H[0,x_]->Dott[x],(*3*)FilledDot[H[H[0,y_],z_]]->c1[y,z],(*4*)FilledDot[H[H[H[0,x_],y_],z_]]->c2[x,y,z],(*5*)FilledDot[c1[x_,y_]]->c1[x,H[x,y]],(*6*)FilledDot[c2[x_,y_,z_]]->c2[x,H[x,y],z],(*7*)c1[y_,z_]->Dott[z],(*7*)c2[x_,y_,z_]->Dott[H[y,z]],(*8*)Rect[Dott[x_]]->Dott[Rect[x]],(*10*)FilledDott[x_]->x(*11*)}; In[]:= initialStateCase1[n_]:=Dott[Nest[Rect[#]&,H[0,t],n]]; In[]:= Table[ResourceFunction["MultiwayCombinator"][HydraRules,initialStateCase1[a],25,"StatesGraphStructure"],{a,0,3}] Out[]= We note similar behaviour to that of the numerical multiway systems on Goodstein sequences. In[]:= mwc=ResourceFunction["MultiwayCombinator"][HydraRules,initialStateCase1[2],60,"StatesGraphStructure"] Out[]= We show the shortest path from the initial state to the final state, showing that some choices of evaluation strategy are not optimal. In[]:= sp=FindShortestPath[mwc,First[VertexList[mwc]],Last[VertexList[mwc]]];HighlightGraph[mwc,Subgraph[mwc,PathGraph[sp]]] Out[]= The disconnected components present in the branchial graph suggest distinct reduction strategies which do not share a common ancestor during evaluation of the term. An observer of this system therefore has to possess a very high branching factor to efficiently combat the time-complexity of this function. ResourceFunction["MultiwayCombinator"][HydraRules,initialStateCase1[15],20,"BranchialGraphStructure"]
Infinitary Behaviour
Combinators The invention of combinators in 1924 by Moses Schönfinkel paved the way for the development of formalisms in mathematical logic possessing expressive power exceeding that of first-order logic. More recently, due to their rediscovery by Haskell Curry, they have been applied as models of computation. Using only the S and K combinators is extensionally equivalent to the λ-calculus and therefore, by Church’s thesis, is capable of universal computation. As above we can examine their behaviour in terms of convergence. In[]:= skrules={s[x_][y_][z_]:>x[z][y[z]],k[x_][y_]:>x}; In[]:= mwc2=ResourceFunction["MultiwayCombinator"][skrules,s[s][s][s[s]][s][s],17,"StatesGraphStructure"] In[]:= sp2=FindShortestPath[mwc2,First[VertexList[mwc2]],Last[VertexList[mwc2]]];HighlightGraph[mwc2,Subgraph[mwc2,PathGraph[sp2]]] Out[]= We note the increasing depth of application of the S-rule for the above system, showing strong convergence. Out[]= Here we see the multiway states graph, each node annotated with the expression depth, reminiscent of the functions seen earlier. In[]:= g=ResourceFunction["MultiwayCombinator"][{s[x_][y_][z_]->x[z][y[z]],k[x_][y_]->x},plus[integer[1]][integer[1]][s][k],40,"StatesGraphStructure"]; In[]:= depths=Map[Depth[ToExpression[#]]&,VertexList[g]]; In[]:= min=Min[depths];max=Max[depths]; In[]:= Show[GraphPlot3D[g,VertexRenderingFunction->({Hue[(Depth[ToExpression[#2]]-min)/(max-min)/2,1,1],EdgeForm[Black],Sphere[#,.075],Black}&)],Epilog->Inset[BarLegend[{Hue[(#-min)/(max-min)/2,1,1]&,{min,max}}],{Right,Center},{Right,Center}]] Out[]=
Non-Termination There are many examples of non-terminating combinator expressions. Here, we restrict ourselves to the S-combinator. If we enumerate all S-combinator expressions having up to 10 symbols, this results in a set of 6918 terms. A matrix plot showing the vertex count of the multiway states graphs of all of these expressions shows a diversity in growth rate. In[]:= inits=Flatten[Table[ResourceFunction["EnumerateCombinators"][n,{s}],{n,1,8}]]; In[]:= srule=s[x_][y_][z_]->x[z][y[z]] In[]:= growth=Table[ParallelMap[Function[init,ResourceFunction["MultiwayCombinator"][{srule},init,n,"StatesGraphStructure"]],inits],{n,1,5}]; In[]:= Map[Function[grow,Map[VertexCount[#]&,grow]],growth]//MatrixPlot[#,Frame->False]& Out[]= This can be further illustrated by fitting functions to this data and visualising the distribution of points in parameter space after dimensionality reduction. In[]:= growths=Map[Function[grow,Map[VertexCount[#]&,grow]],growth]//Transpose; In[]:= fits=Map[FindFit[#,a+b*x+c*x^2+d*x^3,{a,b,c,d},x]&,growths]; In[]:= fitsVec=Map[Function[fit,{fit[[1]][[2]],fit[[2]][[2]],fit[[3]][[2]],fit[[4]][[2]]}],fits]; In[]:= dr=DimensionReduction[fitsVec] In[]:= ListPlot[dr[fitsVec],PlotRange->Full] We observe an interesting bimodal distribution with plenty of outliers. Despite this analysis, we can’t know whether any of these S-combinator expression will evolve indefinitely; however, there exists a technique using SAT-solver generated tree automata [13] which can solve the decision problem of S-combinator non-termination. It is important to emphasise that this procedure only works for S-combinator expressions and non-termination for rewrite systems remains undecidable.
Infinite Series and Their Relation to Infinitary Rewriting A mathematical series is the addition of infinitely many terms and is fundamental to the topics of calculus and analysis, they are used to define continuity, derivatives, integrals and much more. For most of history the concept that an infinite sum could produce a finite result was considered paradoxical, as illustrated by Zeno’s paradox, but this was resolved by the introduction of limits. We can view the computation of an infinite series as a fixed point term subject to infinite reduction creating an endless cascade of redexes that generate the full series in the limit term. This process of symbolising an infinite form having limiting behavior is a concrete example of computational reducibility. We would like to find similar instances of these pockets of reducibility in the infinitary rewrite systems that we encounter in the Physics Project.
Compiling Infinite Series Representations to Term Rewriting Systems As an example, let’s take the function Sin(x) Out[]= x- 3 x 6 5 x 120 7 x 5040 8 O[x] We see the familiar alternating sum with odd-valued exponents and factorial quantities in the denominators. These arise from another infinite series, ix e Sin(x) Cos(x) Out[]//TableForm=
If we nest progressively truncated version of this series we get: Out[]//TableForm=
Looking at the resulting expression tree growth we see the following pattern: In[]:= Table[Nest[Normal[Series[Sin[x],{x,0,2n+1}]]/.x->#&,x,n+1]//ExpressionGraph,{n,0,3}] Out[]= The number of nodes in the expression trees grows like this: Out[]= {1,18,140,1340,16246} Plotting these shows rapidly growth. Out[]= Fitting a function of the form a bx e Out[]= {a0.00826208,b2.86501} Our fitted function is: Out[]= 0.00826208 2.86501x Note the exponent i |