Message Boards

GROUPS:

Richard Assar

[WWS22] Characterisation of infinitary rewrite systems

Richard Assar

Posted 14 days ago

365 Views

1 Reply

3 Total Likes

Follow this post

Image of numerical multiway system of the Goodstein sequence base bump operation

Characterisation of infinitary rewrite systems
by Richard Assar

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

. If a term after

steps contains redexes we can continue rewriting to sequences

ω+ω

or longer.

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

and

combinators can be symbolically represented and transformed without actually evaluating the resulting infinite cascades they would generate.

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))

. We say that the induced reduction sequence weakly converges to

f(g(g(g(...))))f(

)

. Note that the rewrite is always happening at the same depth, as is demonstrated by the following states plot and position list output. They demonstrate that the rule application is always occurring at the root of the term.

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))

, which strongly converges to

f(g(g(g(...))))f(

)

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

and

-complete [7].

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

(three factorial).

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

of a geodesic ball of radius

grows as

we can compute an effective dimension

by the following rearrangement to

d

log(V)

log(R)

. Clearly this can take on non-integer values. In a physical setting, this corresponds to the Ricci scalar curvature [8]. We can apply this method of analysis in the case of multiway function evaluation to get a sense of the “degrees of freedom” that computational observers may possess as they march forward towards the normal form (the terminal state of the system), should one exist.

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]ba[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)

where

is the

hyperoperation. Starting with

H(1,2,3)

, or

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)

, or

23

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)

, or

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)

, or the tetration of 2 and 3, written

and evaluated as

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

, the set of decision problems solvable by a Turing machine or the set of decidable languages.

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)

. For a closer look we may examine the expression depth at every state node.

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-

representation. To do this, we first write out our number as a sum of powers of

. We then write each power in terms of powers of

and so on, and continue until we can no longer do so. As a concrete example let’s take the number 246, which in hereditary base-2 representation looks like this:

Out[]=

1+2+

We call this

(246)

. In order to compute the next number in the Goodstein sequence all we need to do is replace all of the twos in the above expression with threes (the so-called “base bump” operation) and then subtract one. The next number in the sequence is...

(246)

Out[]=

854066918318573

Okay, that blew up pretty fast! Perhaps we should start smaller. Let’s try looking at the Goodstein sequence

(1)

Out[]=

{1,0}

That died out in one step – so far so good. Let’s look at

(2)

Out[]=

{2,2,1,0}

This time it took three steps before we reached zero. Let’s take a look at

(3)

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,

(4)

, right... ?

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,

(4)

takes

3

402653211

-3

steps to reach zero! Just to put this into perspective, there are an estimated

3.2

particles in the observable universe - you would need

2

121210614

universes, and that’s assuming you make the best move at every step!

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{

(n),n+1}

with initial conditions including the numbers from 1 to 20.

In[]:=

ResourceFunction["NestGraphTagged"][n|->{nextGoodstein[n,3],n+1},Range[20],7,"StateLabeling"->False]

Out[]=

Similarly, we show

n{

(n),n+1}

, which begins to reveal a very interesting topological structure.

Out[]=

Let’s go on a few more steps. This is what

n{

(n),n+1}

looks like.

Out[]=

Finally, we remain on

(5)

but look at initial conditions ranging from 101 to 121.

Out[]=

If we look at

(n,b){(

(n),b+1),(

n+1

(n),b+1),

n+3

(n),b+1)}

, we observe more of this divergent behaviour.

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)

and expand it to the Taylor series representation using the Mathematica function Series[...]

Out[]=

120

5040

O[x]

We see the familiar alternating sum with odd-valued exponents and factorial quantities in the denominators. These arise from another infinite series,

, which defines a unit circle in the complex plane. Factoring into real and imaginary parts, we obtain infinite series definitions for the harmonic functions

Sin(x)

and

Cos(x)

Out[]//TableForm=

120

5040

120

5040

362880

If we nest progressively truncated version of this series we get:

Out[]//TableForm=

120

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

yields the following parameters.

Out[]=

{a0.00826208,b2.86501}

Our fitted function is:

Out[]=

0.00826208

2.86501x



Note the exponent i