Wolfram Cloud Document

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]]};

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,

and we can plot its distribution for the above states graph.

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.

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

We can look at the expression depth at each state node throughout the multiway states evolution graph.

Additionally, we can also examine the rule application depth for each step of the computation .

The Hausdorff dimension plot shows connected regions of varying dimension that fluctuates throughout.

The dimension histogram shows a sharp cutoff after 2.

We can easily extend these fast-growing functions to infinitary systems by adding a fixed point rule into the rewrite system, for example:

Or the Hausdorff dimension at each node.

The dimension histogram shows a much smoother distribution than the finitary case.

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

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.

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.

We note similar behaviour to that of the numerical multiway systems on Goodstein sequences.

We show the shortest path from the initial state to the final state, showing that some choices of evaluation strategy are not optimal.

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.

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.

We note the increasing depth of application of the S-rule for the above system, showing strong convergence.

Here we see the multiway states graph, each node annotated with the expression depth, reminiscent of the functions seen earlier.

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.

This can be further illustrated by fitting functions to this data and visualising the distribution of points in parameter space after dimensionality reduction.

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

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

Looking at the resulting expression tree growth we see the following pattern:

The number of nodes in the expression trees grows like this:

Plotting these shows rapidly growth.

Our fitted function is:

We might consider a thought experiment where truncated forms of such series are “compiled” into a term rewrite system using some of the functions that have been demonstrated above. This is a very unnatural thing to do – we are ignoring the reals for such a function – but we are still able to observe the behavior of such a system if we scale the function by the largest denominator value. It’s worth noting that we could choose another representation of this function; for example, a continued fraction – which is equally simple to translate into an infinitary term rewriting system.

We’ve seen how the upper layers of this system might look, so now let’s implement the functions that we left as placeholders in the above plots using the successor, predecessor, addition, subtraction, multiplication, factorial and division functions - all encoded as term rewriting rules. Evolving such a system forward we see this structure:

It is worth noting that in the study of S-combinator expressions one sees the above structures appear often, showing that we do not have to go far in the space of simple programs before we find this system and others like it.

Coloring the graph with the Hausdorff dimension shows how the dynamics of the system unfold.

Plotting the Hausdorff dimension for the single shortest path originating from our initial state and ending up at the deepest state in our multiway states graph shows an irregular pattern that is hidden by the intrinsic trend in the data.

Fitting a linear model and de-trending the data yields the following, which we could refine by averaging through all sibling states within the same foliation and by evolving the system for longer.

We now fit a model to the above data to capture a very rough approximation to the dimension fluctuations observed during the reduction steps observed.

Continuous-Time Evolution in Discrete Dynamical Systems

Given the system described in the previous section, extended with a fixed point operator, we know that periodically the system will exhibit states that correspond to the numerical quantities resulting from each successive nesting of the function in question.

The statement here is that we can reason about infinite rewrite systems by importing pre-existing mathematical techniques, in this case function evolution equations, inheriting the tools of analysis that go with them. We can make predictions about the various nodes in this lattice of rewrite rules stating, in this example, the precise quantity of successor nodes that will be present in an infinitary rewrite system with fixed point composition of an infinite set of rewrite rules.

Fractional Composition by Non-Integer Carleman Matrix Exponentiation

To illustrate the previous example we conclude with a demonstration of the derivation of the temporal fine-graining functions we require.

Continuous function iterates are usually expressed as solutions to functional evolution equations [14, 15, 16], this description corresponds to an abelian flow as exemplified by the following relation:

Taking non-integer exponents of this matrix, which can be achieved easily by diagonalization, results in the approximation of our fractionally composed function in the 2nd row.

Extracting the terms into a function yields:

Conclusion and Next Steps

We applied a somewhat contrived yet illustrative example demonstrating the complex behavior infinitary rewrite systems may possess, capturing numerical models of their limiting behaviour that have direct interpretation as physical phenomena. Extending this approach to untyped hypergraph rewrite systems, instead of combinators, would be an interesting future direction.

In the Wolfram Physics Project we must approach the question "What happens after Omega?" by considering multiway evolution on the reals and beyond; however, challenges in maintaining coherency conditions must be approached. Developing a non-termination proof procedure for hypergraph rewrite systems, like that which we have for the S-combinator, even if only applicable in restricted cases would be a highly useful next step for assisting future experimentation.

I am deeply grateful for all the help and guidance I received from my project mentors: James Boyd, Hatem Elshatlawy, Dr Stephen Wolfram, and the entire WWS 2022 team.

References

◼

[1] J. W. Klop - Term Rewriting Systems - https://www.cs.tau.ac.il/~nachum/papers/klop.pdf

◼

[2] M. Willsey - egg: Fast and Extensible Equality Saturation - https://arxiv.org/abs/2004.03082

◼

[3] V. M. Chernenkiy - Using Metagraph Approach for the Big Data Based Graph Processing - http://ceur-ws.org/Vol-2514/paper112.pdf

◼

[4] N. Dershowitz, S. Kaplan - Rewrite, rewrite, rewrite, rewrite, rewrite... - https://cdr.lib.unc.edu/downloads/1n79hd40b

◼

[5] P. Bahr - Infinitary Rewriting - Theory and Applications - https://bahr.io/pubs/entries/bahr09master.html

◼

[6] J. Ketema, J. Simonsen - Computing with Infinite Terms and Infinite Reductions - https://ketemaj.home.xs4all.nl/publ/comput_inf_fundamentals.pdf

◼

[7] J. Endrullis, et al. - Complexity of Fractran and Productivity - https://arxiv.org/abs/0903.4366

◼

[8] Wolfram Physics Project Technical Introduction - Limiting Behavior and Emergent Geometry - Geodesics https://www.wolframphysics.org/technical-introduction/limiting-behavior-and-emergent-geometry/geodesics/

◼

[9] Paris, J. and Harrington, L. - A mathematical incompleteness in Peano Arithmetic - https://www2.karlin.mff.cuni.cz/~krajicek/ph.pdf

◼

[10] R. L. Goodstein - On the Restricted Ordinal Theorem - https://fa.ewi.tudelft.nl/~hart/onderwijs/verzamelingenleer/materiaal/goodstein.pdf

◼

[11] S. Wolfram - Multicomputation with Numbers: The Case of Simple Multiway Systems - https://www.wolframphysics.org/bulletins/2021/10/multicomputation-with-numbers-the-case-of-simple-multiway-systems/

◼

[12] Hélène Touzet - Encoding the Hydra Battle as a rewrite system - http://cl-informatik.uibk.ac.at/teaching/ss15/cbr/papers/2.pdf

◼

[13] J. Endrullis, H. Zantema - Proving non-termination by finite automata - https://drops.dagstuhl.de/opus/volltexte/2015/5195/pdf/15.pdf

◼

[14] T. Curtright et al. - Approximate Solutions of Functional Equations - https://arxiv.org/abs/1105.3664

◼

[15] P. Erdös, E. Jabotinsky - On Analytic Iteration - https://old.renyi.hu/~p_erdos/1960-07.pdf

◼

[16] P. Gralewicz, K. Kowalski - Continuous time evolution from iterated maps and Carleman linearization - https://arxiv.org/abs/math-ph/0002044