WolframAlpha.com
WolframCloud.com
All Sites & Public Resources...
Products & Services
Wolfram|One
Mathematica
Wolfram|Alpha Notebook Edition
Finance Platform
System Modeler
Wolfram Player
Wolfram Engine
WolframScript
Enterprise Private Cloud
Application Server
Enterprise Mathematica
Wolfram|Alpha Appliance
Enterprise Solutions
Corporate Consulting
Technical Consulting
Wolfram|Alpha Business Solutions
Resource System
Data Repository
Neural Net Repository
Function Repository
Wolfram|Alpha
Wolfram|Alpha Pro
Problem Generator
API
Data Drop
Products for Education
Mobile Apps
Wolfram Player
Wolfram Cloud App
Wolfram|Alpha for Mobile
Wolfram|Alpha-Powered Apps
Services
Paid Project Support
Wolfram U
Summer Programs
All Products & Services »
Technologies
Wolfram Language
Revolutionary knowledge-based programming language.
Wolfram Cloud
Central infrastructure for Wolfram's cloud products & services.
Wolfram Science
Technology-enabling science of the computational universe.
Wolfram Notebooks
The preeminent environment for any technical workflows.
Wolfram Engine
Software engine implementing the Wolfram Language.
Wolfram Natural Language Understanding System
Knowledge-based broadly deployed natural language.
Wolfram Data Framework
Semantic framework for real-world data.
Wolfram Universal Deployment System
Instant deployment across cloud, desktop, mobile, and more.
Wolfram Knowledgebase
Curated computable knowledge powering Wolfram|Alpha.
All Technologies »
Solutions
Engineering, R&D
Aerospace & Defense
Chemical Engineering
Control Systems
Electrical Engineering
Image Processing
Industrial Engineering
Mechanical Engineering
Operations Research
More...
Finance, Statistics & Business Analysis
Actuarial Sciences
Bioinformatics
Data Science
Econometrics
Financial Risk Management
Statistics
More...
Education
All Solutions for Education
Trends
Machine Learning
Multiparadigm Data Science
Internet of Things
High-Performance Computing
Hackathons
Software & Web
Software Development
Authoring & Publishing
Interface Development
Web Development
Sciences
Astronomy
Biology
Chemistry
More...
All Solutions »
Learning & Support
Learning
Wolfram Language Documentation
Fast Introduction for Programmers
Wolfram U
Videos & Screencasts
Wolfram Language Introductory Book
Webinars & Training
Summer Programs
Books
Need Help?
Support FAQ
Wolfram Community
Contact Support
Premium Support
Paid Project Support
Technical Consulting
All Learning & Support »
Company
About
Company Background
Wolfram Blog
Events
Contact Us
Work with Us
Careers at Wolfram
Internships
Other Wolfram Language Jobs
Initiatives
Wolfram Foundation
MathWorld
Computer-Based Math
A New Kind of Science
Wolfram Technology for Hackathons
Student Ambassador Program
Wolfram for Startups
Demonstrations Project
Wolfram Innovator Awards
Wolfram + Raspberry Pi
Summer Programs
More...
All Company »
Search
WOLFRAM COMMUNITY
Connect with users of Wolfram technologies to learn, solve problems and share ideas
Join
Sign In
Dashboard
Groups
People
Message Boards
Answer
(
Unmark
)
Mark as an Answer
GROUPS:
Staff Picks
Wolfram Science
Computer Science
Mathematics
Physics
Graphics and Visualization
Graphs and Networks
Wolfram Language
Wolfram Summer School
Wolfram Fundamental Physics Project
6
Richard Assar
[WWS22] Characterisation of infinitary rewrite systems
Richard Assar
Posted
5 months ago
1941 Views
|
2 Replies
|
6 Total Likes
Follow this post
|
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:
R
e
p
l
a
c
e
R
e
p
e
a
t
e
d
[
x
,
R
u
l
e
[
x
,
L
i
s
t
[
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
ω
+
ω
,
2
ω
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
Y
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,
I
n
f
i
n
i
t
a
r
y
[
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.
L
e
t
'
s
t
a
k
e
t
h
e
t
e
r
m
-
r
e
w
r
i
t
i
n
g
s
y
s
t
e
m
w
i
t
h
a
s
i
n
g
l
e
r
u
l
e
:
f
(
g
(
x
)
)
f
(
g
(
g
(
x
)
)
.
W
e
s
a
y
t
h
a
t
t
h
e
i
n
d
u
c
e
d
r
e
d
u
c
t
i
o
n
s
e
q
u
e
n
c
e
w
e
a
k
l
y
c
o
n
v
e
r
g
e
s
t
o
f
(
g
(
g
(
g
(
.
.
.
)
)
)
)
f
(
ω
g
)
.
N
o
t
e
t
h
a
t
t
h
e
r
e
w
r
i
t
e
i
s
a
l
w
a
y
s
h
a
p
p
e
n
i
n
g
a
t
t
h
e
s
a
m
e
d
e
p
t
h
,
a
s
i
s
d
e
m
o
n
s
t
r
a
t
e
d
b
y
t
h
e
f
o
l
l
o
w
i
n
g
s
t
a
t
e
s
p
l
o
t
a
n
d
p
o
s
i
t
i
o
n
l
i
s
t
o
u
t
p
u
t
.
T
h
e
y
d
e
m
o
n
s
t
r
a
t
e
t
h
a
t
t
h
e
r
u
l
e
a
p
p
l
i
c
a
t
i
o
n
i
s
a
l
w
a
y
s
o
c
c
u
r
r
i
n
g
a
t
t
h
e
r
o
o
t
o
f
t
h
e
t
e
r
m
.
I
n
[
]
:
=
w
c
r
u
l
e
s
=
{
f
[
g
[
x
_
]
]
-
>
f
[
g
[
g
[
x
]
]
]
}
;
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
w
c
r
u
l
e
s
,
f
[
g
[
x
]
]
,
3
,
"
S
t
a
t
e
s
G
r
a
p
h
"
]
O
u
t
[
]
=
I
n
[
]
:
=
w
c
s
t
a
t
e
s
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
w
c
r
u
l
e
s
,
f
[
g
[
x
]
]
,
3
,
"
A
l
l
S
t
a
t
e
s
L
i
s
t
"
]
;
I
n
[
]
:
=
M
a
p
[
(
P
o
s
i
t
i
o
n
[
T
o
E
x
p
r
e
s
s
i
o
n
[
#
[
[
1
]
]
]
,
w
c
r
u
l
e
s
[
[
1
,
1
]
]
]
/
/
M
a
p
[
L
e
n
g
t
h
[
#
]
&
]
/
/
M
a
x
)
&
,
w
c
s
t
a
t
e
s
]
O
u
t
[
]
=
{
0
,
0
,
0
,
0
}
N
o
w
l
e
t
’
s
e
x
a
m
i
n
e
t
h
e
r
u
l
e
:
g
(
x
)
g
(
g
(
c
)
)
,
w
h
i
c
h
s
t
r
o
n
g
l
y
c
o
n
v
e
r
g
e
s
t
o
f
(
g
(
g
(
g
(
.
.
.
)
)
)
)
f
(
ω
g
)
.
I
n
[
]
:
=
s
c
r
u
l
e
s
=
{
g
[
c
_
]
-
>
g
[
g
[
c
]
]
}
;
I
n
[
]
:
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
s
c
r
u
l
e
s
,
f
[
g
[
x
]
]
,
3
,
"
S
t
a
t
e
s
G
r
a
p
h
"
]
O
u
t
[
]
=
I
n
[
]
:
=
s
c
s
t
a
t
e
s
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
s
c
r
u
l
e
s
,
f
[
g
[
x
]
]
,
3
,
"
A
l
l
S
t
a
t
e
s
L
i
s
t
"
]
;
I
n
[
]
:
=
M
a
p
[
(
P
o
s
i
t
i
o
n
[
T
o
E
x
p
r
e
s
s
i
o
n
[
#
[
[
1
]
]
]
,
s
c
r
u
l
e
s
[
[
1
,
1
]
]
]
/
/
M
a
p
[
L
e
n
g
t
h
[
#
]
&
]
/
/
M
a
x
)
&
,
s
c
s
t
a
t
e
s
]
O
u
t
[
]
=
{
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
and
1
Σ
1
-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
3
!
(three factorial).
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
{
f
a
c
[
0
]
-
>
s
[
0
]
,
f
a
c
[
s
[
x
_
]
]
-
>
m
u
l
[
s
[
x
]
,
f
a
c
[
x
]
]
,
m
u
l
[
x
_
,
0
]
-
>
0
,
m
u
l
[
x
_
,
s
[
y
_
]
]
-
>
a
d
d
[
m
u
l
[
x
,
y
]
,
x
]
,
a
d
d
[
x
_
,
0
]
-
>
x
,
a
d
d
[
x
_
,
s
[
y
_
]
]
-
>
s
[
a
d
d
[
x
,
y
]
]
}
,
f
a
c
[
s
[
s
[
s
[
0
]
]
]
]
,
5
0
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
O
u
t
[
]
=
E
v
e
r
y
n
o
d
e
i
n
t
h
i
s
g
r
a
p
h
r
e
p
r
e
s
e
n
t
s
a
u
n
i
q
u
e
s
t
a
t
e
t
h
e
s
y
s
t
e
m
m
a
y
o
c
c
u
p
y
.
T
h
e
d
i
r
e
c
t
e
d
e
d
g
e
s
r
e
v
e
a
l
t
h
e
f
l
o
w
o
f
s
t
a
t
e
e
v
o
l
u
t
i
o
n
w
i
t
h
i
n
t
h
e
s
y
s
t
e
m
.
O
n
e
m
e
t
r
i
c
u
s
e
d
w
i
t
h
i
n
t
h
e
P
h
y
s
i
c
s
P
r
o
j
e
c
t
i
s
t
h
e
c
o
m
p
u
t
a
t
i
o
n
o
f
t
h
e
H
a
u
s
d
o
r
f
f
-
B
e
s
i
c
o
v
i
t
c
h
d
i
m
e
n
s
i
o
n
.
O
b
s
e
r
v
i
n
g
t
h
e
f
a
c
t
t
h
a
t
t
h
e
v
o
l
u
m
e
V
o
f
a
g
e
o
d
e
s
i
c
b
a
l
l
o
f
r
a
d
i
u
s
R
g
r
o
w
s
a
s
d
R
w
e
c
a
n
c
o
m
p
u
t
e
a
n
e
f
f
e
c
t
i
v
e
d
i
m
e
n
s
i
o
n
d
b
y
t
h
e
f
o
l
l
o
w
i
n
g
r
e
a
r
r
a
n
g
e
m
e
n
t
t
o
d
l
o
g
(
V
)
l
o
g
(
R
)
.
C
l
e
a
r
l
y
t
h
i
s
c
a
n
t
a
k
e
o
n
n
o
n
-
i
n
t
e
g
e
r
v
a
l
u
e
s
.
I
n
a
p
h
y
s
i
c
a
l
s
e
t
t
i
n
g
,
t
h
i
s
c
o
r
r
e
s
p
o
n
d
s
t
o
t
h
e
R
i
c
c
i
s
c
a
l
a
r
c
u
r
v
a
t
u
r
e
[
8
]
.
W
e
c
a
n
a
p
p
l
y
t
h
i
s
m
e
t
h
o
d
o
f
a
n
a
l
y
s
i
s
i
n
t
h
e
c
a
s
e
o
f
m
u
l
t
i
w
a
y
f
u
n
c
t
i
o
n
e
v
a
l
u
a
t
i
o
n
t
o
g
e
t
a
s
e
n
s
e
o
f
t
h
e
“
d
e
g
r
e
e
s
o
f
f
r
e
e
d
o
m
”
t
h
a
t
c
o
m
p
u
t
a
t
i
o
n
a
l
o
b
s
e
r
v
e
r
s
m
a
y
p
o
s
s
e
s
s
a
s
t
h
e
y
m
a
r
c
h
f
o
r
w
a
r
d
t
o
w
a
r
d
s
t
h
e
n
o
r
m
a
l
f
o
r
m
(
t
h
e
t
e
r
m
i
n
a
l
s
t
a
t
e
o
f
t
h
e
s
y
s
t
e
m
)
,
s
h
o
u
l
d
o
n
e
e
x
i
s
t
.
O
u
t
[
]
=
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
n
is the
t
h
n
hyperoperation. Starting with
H
(
1
,
2
,
3
)
, or
2
+
3
:
I
n
[
]
:
=
h
r
u
l
e
s
=
{
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
]
]
}
;
I
n
[
]
:
=
h
c
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
h
r
u
l
e
s
,
h
[
s
[
0
]
,
s
[
s
[
0
]
]
,
s
[
s
[
s
[
0
]
]
]
]
,
5
0
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
O
u
t
[
]
=
extending to
H
(
2
,
2
,
3
)
, or
2
3
:
I
n
[
]
:
=
h
c
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
h
r
u
l
e
s
,
h
[
s
[
s
[
0
]
]
,
s
[
s
[
0
]
]
,
s
[
s
[
s
[
0
]
]
]
]
,
5
0
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
O
u
t
[
]
=
and finally
H
(
3
,
2
,
3
)
, or
3
2
:
I
n
[
]
:
=
h
c
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
h
r
u
l
e
s
,
h
[
s
[
s
[
s
[
0
]
]
]
,
s
[
s
[
0
]
]
,
s
[
s
[
s
[
0
]
]
]
]
,
5
0
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
O
u
t
[
]
=
A
s
w
e
c
a
n
s
e
e
,
t
h
e
b
e
h
a
v
i
o
u
r
o
f
t
h
e
f
u
n
c
t
i
o
n
,
i
m
p
l
e
m
e
n
t
e
d
h
e
r
e
a
s
a
t
e
r
m
r
e
w
r
i
t
i
n
g
s
y
s
t
e
m
,
g
r
o
w
s
r
a
p
i
d
l
y
e
v
e
n
f
o
r
s
m
a
l
l
i
n
p
u
t
s
.
L
e
t
’
s
l
o
o
k
a
t
t
h
e
p
a
r
t
i
a
l
e
v
a
l
u
a
t
i
o
n
o
f
H
(
4
,
2
,
3
)
,
o
r
t
h
e
t
e
t
r
a
t
i
o
n
o
f
2
a
n
d
3
,
w
r
i
t
t
e
n
3
2
a
n
d
e
v
a
l
u
a
t
e
d
a
s
2
2
2
.
I
n
[
]
:
=
h
c
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
h
r
u
l
e
s
,
h
[
s
[
s
[
s
[
s
[
0
]
]
]
]
,
s
[
s
[
0
]
]
,
s
[
s
[
s
[
0
]
]
]
]
,
1
1
0
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
O
u
t
[
]
=
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,
O
u
t
[
]
=
and we can plot its distribution for the above states graph.
O
u
t
[
]
=
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.
O
u
t
[
]
=
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 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
)
.
a
r
u
l
e
s
=
{
a
[
0
,
n
_
]
-
>
s
[
n
]
,
a
[
s
[
m
_
]
,
0
]
-
>
a
[
m
,
s
[
0
]
]
,
a
[
s
[
m
_
]
,
s
[
n
_
]
]
-
>
a
[
m
,
a
[
s
[
m
]
,
n
]
]
}
;
I
n
[
]
:
=
a
c
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
a
r
u
l
e
s
,
a
[
s
[
s
[
0
]
]
,
s
[
s
[
s
[
0
]
]
]
]
,
6
0
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
O
u
t
[
]
=
We can look at the expression depth at each state node throughout the multiway states evolution graph.
O
u
t
[
]
=
Additionally, we can also examine the rule application depth for each step of the computation .
O
u
t
[
]
=
The Hausdorff dimension plot shows connected regions of varying dimension that fluctuates throughout.
O
u
t
[
]
=
The dimension histogram shows a sharp cutoff after 2.
O
u
t
[
]
=
We can easily extend these fast-growing functions to infinitary systems by adding a fixed point rule into the rewrite system, for example:
a
r
u
l
e
s
=
{
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
]
}
;
I
n
[
]
:
=
a
c
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
a
r
u
l
e
s
,
(
*
s
[
s
[
s
[
s
[
s
[
s
[
s
[
0
]
]
]
]
]
]
]
*
)
a
[
s
[
s
[
0
]
]
,
s
[
s
[
s
[
0
]
]
]
]
,
1
4
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
O
u
t
[
]
=
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.
I
n
[
]
:
=
d
e
p
t
h
s
=
M
a
p
[
D
e
p
t
h
[
T
o
E
x
p
r
e
s
s
i
o
n
[
#
]
]
&
,
V
e
r
t
e
x
L
i
s
t
[
a
c
]
]
;
m
i
n
D
e
p
t
h
=
M
i
n
[
d
e
p
t
h
s
]
;
m
a
x
D
e
p
t
h
=
M
a
x
[
d
e
p
t
h
s
]
;
I
n
[
]
:
=
S
h
o
w
[
G
r
a
p
h
P
l
o
t
3
D
[
a
c
,
V
e
r
t
e
x
R
e
n
d
e
r
i
n
g
F
u
n
c
t
i
o
n
-
>
(
{
H
u
e
[
(
D
e
p
t
h
[
T
o
E
x
p
r
e
s
s
i
o
n
[
#
2
]
]
-
m
i
n
D
e
p
t
h
)
/
(
m
a
x
D
e
p
t
h
-
m
i
n
D
e
p
t
h
)
/
2
,
1
,
1
]
,
E
d
g
e
F
o
r
m
[
B
l
a
c
k
]
,
S
p
h
e
r
e
[
#
,
.
0
9
]
,
B
l
a
c
k
}
&
)
]
,
E
p
i
l
o
g
-
>
I
n
s
e
t
[
B
a
r
L
e
g
e
n
d
[
{
H
u
e
[
(
#
-
m
i
n
D
e
p
t
h
)
/
(
m
a
x
D
e
p
t
h
-
m
i
n
D
e
p
t
h
)
/
2
,
1
,
1
]
&
,
{
m
i
n
D
e
p
t
h
,
m
a
x
D
e
p
t
h
}
}
]
,
{
R
i
g
h
t
,
C
e
n
t
e
r
}
,
{
R
i
g
h
t
,
C
e
n
t
e
r
}
]
]
O
u
t
[
]
=
Or the Hausdorff dimension at each node.
I
n
[
]
:
=
m
i
n
d
i
m
s
=
M
i
n
[
d
i
m
s
]
;
m
a
x
d
i
m
s
=
M
a
x
[
d
i
m
s
]
;
I
n
[
]
:
=
S
h
o
w
[
G
r
a
p
h
P
l
o
t
3
D
[
a
c
,
V
e
r
t
e
x
R
e
n
d
e
r
i
n
g
F
u
n
c
t
i
o
n
-
>
(
{
H
u
e
[
0
.
5
-
(
(
d
i
m
s
[
[
#
2
]
]
-
m
i
n
d
i
m
s
)
/
(
m
a
x
d
i
m
s
-
m
i
n
d
i
m
s
)
/
2
)
,
1
,
1
]
,
E
d
g
e
F
o
r
m
[
O
p
a
c
i
t
y
[
0
.
1
,
B
l
a
c
k
]
]
,
S
p
h
e
r
e
[
#
,
.
0
5
]
,
O
p
a
c
i
t
y
[
0
.
1
,
B
l
a
c
k
]
}
&
)
]
,
E
p
i
l
o
g
-
>
I
n
s
e
t
[
B
a
r
L
e
g
e
n
d
[
{
H
u
e
[
(
#
-
m
i
n
d
i
m
s
)
/
(
m
a
x
d
i
m
s
-
m
i
n
d
i
m
s
)
/
2
,
1
,
1
]
&
,
{
m
i
n
d
i
m
s
,
m
a
x
d
i
m
s
}
}
]
,
{
R
i
g
h
t
,
C
e
n
t
e
r
}
,
{
R
i
g
h
t
,
C
e
n
t
e
r
}
]
]
O
u
t
[
]
=
The dimension histogram shows a much smoother distribution than the finitary case.
O
u
t
[
]
=
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
representation. To do this, we first write out our number as a sum of powers of
n
. We then write each power in terms of powers of
n
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:
O
u
t
[
]
=
2
+
2
2
+
2
2
2
+
1
+
2
2
2
+
2
+
2
2
2
+
1
+
2
+
2
2
2
We call this
G
0
(
2
4
6
)
. 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...
G
1
(
2
4
6
)
:
O
u
t
[
]
=
8
5
4
0
6
6
9
1
8
3
1
8
5
7
3
Okay, that blew up pretty fast! Perhaps we should start smaller. Let’s try looking at the Goodstein sequence
G
n
(
1
)
:
O
u
t
[
]
=
{
1
,
0
}
That died out in one step – so far so good. Let’s look at
G
n
(
2
)
:
O
u
t
[
]
=
{
2
,
2
,
1
,
0
}
This time it took three steps before we reached zero. Let’s take a look at
G
n
(
3
)
:
O
u
t
[
]
=
{
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
(
4
)
, right... ?
O
u
t
[
]
=
{
4
,
2
6
,
4
1
,
6
0
,
8
3
,
1
0
9
,
1
3
9
,
1
7
3
,
2
1
1
,
2
5
3
,
2
9
9
,
3
4
8
,
4
0
1
,
4
5
8
,
5
1
9
,
5
8
4
,
6
5
3
,
7
2
6
,
8
0
3
,
8
8
4
,
9
6
9
}
Okay – it’s not terminating yet but we could be forgiven for assuming that it terminates soon. Well actually, amazingly,
G
n
(
4
)
takes
3
4
0
2
6
5
3
2
1
1
2
-
3
steps to reach zero! Just to put this into perspective, there are an estimated
3
.
2
8
0
1
0
particles in the observable universe - you would need
2
1
2
1
2
1
0
6
1
4
1
0
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
{
G
3
(
n
)
,
n
+
1
}
with initial conditions including the numbers from 1 to 20.
I
n
[
]
:
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
N
e
s
t
G
r
a
p
h
T
a
g
g
e
d
"
]
[
n
|
-
>
{
n
e
x
t
G
o
o
d
s
t
e
i
n
[
n
,
3
]
,
n
+
1
}
,
R
a
n
g
e
[
2
0
]
,
7
,
"
S
t
a
t
e
L
a
b
e
l
i
n
g
"
-
>
F
a
l
s
e
]
O
u
t
[
]
=
Similarly, we show
n
{
G
4
(
n
)
,
n
+
1
}
, which begins to reveal a very interesting topological structure.
O
u
t
[
]
=
Let’s go on a few more steps. This is what
n
{
G
5
(
n
)
,
n
+
1
}
looks like.
O
u
t
[
]
=
Finally, we remain on
G
n
(
5
)
but look at initial conditions ranging from 101 to 121.
O
u
t
[
]
=
If we look at
(
n
,
b
)
{
(
G
n
(
n
)
,
b
+
1
)
,
(
G
n
+
1
(
n
)
,
b
+
1
)
,
G
n
+
3
(
n
)
,
b
+
1
)
}
, we observe more of this divergent behaviour.
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
S
y
s
t
e
m
"
]
[
<
|
"
S
t
a
t
e
E
v
o
l
u
t
i
o
n
F
u
n
c
t
i
o
n
"
-
>
(
{
T
u
p
l
e
[
n
e
x
t
G
o
o
d
s
t
e
i
n
[
#
1
〚
1
〛
,
#
1
〚
2
〛
]
,
#
1
〚
2
〛
+
1
]
,
T
u
p
l
e
[
n
e
x
t
G
o
o
d
s
t
e
i
n
[
#
1
〚
1
〛
+
1
,
#
1
〚
2
〛
]
,
#
1
〚
2
〛
+
1
]
,
T
u
p
l
e
[
n
e
x
t
G
o
o
d
s
t
e
i
n
[
#
1
〚
1
〛
+
2
,
#
1
〚
2
〛
]
,
#
1
〚
2
〛
+
1
]
,
T
u
p
l
e
[
n
e
x
t
G
o
o
d
s
t
e
i
n
[
#
1
〚
1
〛
+
3
,
#
1
〚
2
〛
]
,
#
1
〚
2
〛
+
1
]
}
&
)
,
"
S
t
a
t
e
E
q
u
i
v
a
l
e
n
c
e
F
u
n
c
t
i
o
n
"
-
>
S
a
m
e
Q
,
"
S
t
a
t
e
E
v
e
n
t
F
u
n
c
t
i
o
n
"
-
>
I
d
e
n
t
i
t
y
,
"
E
v
e
n
t
D
e
c
o
m
p
o
s
i
t
i
o
n
F
u
n
c
t
i
o
n
"
-
>
I
d
e
n
t
i
t
y
,
"
E
v
e
n
t
A
p
p
l
i
c
a
t
i
o
n
F
u
n
c
t
i
o
n
"
-
>
I
d
e
n
t
i
t
y
,
"
S
y
s
t
e
m
T
y
p
e
"
-
>
"
F
u
n
c
t
i
o
n
"
,
"
E
v
e
n
t
S
e
l
e
c
t
i
o
n
F
u
n
c
t
i
o
n
"
-
>
I
d
e
n
t
i
t
y
|
>
,
{
T
u
p
l
e
[
2
,
2
]
}
,
2
4
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
,
"
S
t
a
t
e
R
e
n
d
e
r
i
n
g
F
u
n
c
t
i
o
n
"
f
u
n
c
t
i
o
n
S
t
a
t
e
R
e
n
d
e
r
i
n
g
F
u
n
c
t
i
o
n
,
"
E
v
e
n
t
R
e
n
d
e
r
i
n
g
F
u
n
c
t
i
o
n
"
f
u
n
c
t
i
o
n
E
v
e
n
t
R
e
n
d
e
r
i
n
g
F
u
n
c
t
i
o
n
]
/
/
G
r
a
p
h
P
l
o
t
3
D
O
u
t
[
]
=
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.
I
n
[
]
:
=
H
y
d
r
a
R
u
l
e
s
=
{
D
o
t
t
[
x
_
]
-
>
F
i
l
l
e
d
D
o
t
[
R
e
c
t
[
x
]
]
,
(
*
1
*
)
F
i
l
l
e
d
D
o
t
[
R
e
c
t
[
x
_
]
]
-
>
R
e
c
t
[
F
i
l
l
e
d
D
o
t
[
F
i
l
l
e
d
D
o
t
[
x
]
]
]
,
(
*
2
*
)
H
[
0
,
x
_
]
-
>
D
o
t
t
[
x
]
,
(
*
3
*
)
F
i
l
l
e
d
D
o
t
[
H
[
H
[
0
,
y
_
]
,
z
_
]
]
-
>
c
1
[
y
,
z
]
,
(
*
4
*
)
F
i
l
l
e
d
D
o
t
[
H
[
H
[
H
[
0
,
x
_
]
,
y
_
]
,
z
_
]
]
-
>
c
2
[
x
,
y
,
z
]
,
(
*
5
*
)
F
i
l
l
e
d
D
o
t
[
c
1
[
x
_
,
y
_
]
]
-
>
c
1
[
x
,
H
[
x
,
y
]
]
,
(
*
6
*
)
F
i
l
l
e
d
D
o
t
[
c
2
[
x
_
,
y
_
,
z
_
]
]
-
>
c
2
[
x
,
H
[
x
,
y
]
,
z
]
,
(
*
7
*
)
c
1
[
y
_
,
z
_
]
-
>
D
o
t
t
[
z
]
,
(
*
7
*
)
c
2
[
x
_
,
y
_
,
z
_
]
-
>
D
o
t
t
[
H
[
y
,
z
]
]
,
(
*
8
*
)
R
e
c
t
[
D
o
t
t
[
x
_
]
]
-
>
D
o
t
t
[
R
e
c
t
[
x
]
]
,
(
*
1
0
*
)
F
i
l
l
e
d
D
o
t
t
[
x
_
]
-
>
x
(
*
1
1
*
)
}
;
I
n
[
]
:
=
i
n
i
t
i
a
l
S
t
a
t
e
C
a
s
e
1
[
n
_
]
:
=
D
o
t
t
[
N
e
s
t
[
R
e
c
t
[
#
]
&
,
H
[
0
,
t
]
,
n
]
]
;
I
n
[
]
:
=
T
a
b
l
e
[
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
H
y
d
r
a
R
u
l
e
s
,
i
n
i
t
i
a
l
S
t
a
t
e
C
a
s
e
1
[
a
]
,
2
5
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
,
{
a
,
0
,
3
}
]
O
u
t
[
]
=
We note similar behaviour to that of the numerical multiway systems on Goodstein sequences.
I
n
[
]
:
=
m
w
c
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
H
y
d
r
a
R
u
l
e
s
,
i
n
i
t
i
a
l
S
t
a
t
e
C
a
s
e
1
[
2
]
,
6
0
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
O
u
t
[
]
=
We show the shortest path from the initial state to the final state, showing that some choices of evaluation strategy are not optimal.
I
n
[
]
:
=
s
p
=
F
i
n
d
S
h
o
r
t
e
s
t
P
a
t
h
[
m
w
c
,
F
i
r
s
t
[
V
e
r
t
e
x
L
i
s
t
[
m
w
c
]
]
,
L
a
s
t
[
V
e
r
t
e
x
L
i
s
t
[
m
w
c
]
]
]
;
H
i
g
h
l
i
g
h
t
G
r
a
p
h
[
m
w
c
,
S
u
b
g
r
a
p
h
[
m
w
c
,
P
a
t
h
G
r
a
p
h
[
s
p
]
]
]
O
u
t
[
]
=
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.
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
H
y
d
r
a
R
u
l
e
s
,
i
n
i
t
i
a
l
S
t
a
t
e
C
a
s
e
1
[
1
5
]
,
2
0
,
"
B
r
a
n
c
h
i
a
l
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
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.
I
n
[
]
:
=
s
k
r
u
l
e
s
=
{
s
[
x
_
]
[
y
_
]
[
z
_
]
:
>
x
[
z
]
[
y
[
z
]
]
,
k
[
x
_
]
[
y
_
]
:
>
x
}
;
I
n
[
]
:
=
m
w
c
2
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
s
k
r
u
l
e
s
,
s
[
s
]
[
s
]
[
s
[
s
]
]
[
s
]
[
s
]
,
1
7
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
I
n
[
]
:
=
s
p
2
=
F
i
n
d
S
h
o
r
t
e
s
t
P
a
t
h
[
m
w
c
2
,
F
i
r
s
t
[
V
e
r
t
e
x
L
i
s
t
[
m
w
c
2
]
]
,
L
a
s
t
[
V
e
r
t
e
x
L
i
s
t
[
m
w
c
2
]
]
]
;
H
i
g
h
l
i
g
h
t
G
r
a
p
h
[
m
w
c
2
,
S
u
b
g
r
a
p
h
[
m
w
c
2
,
P
a
t
h
G
r
a
p
h
[
s
p
2
]
]
]
O
u
t
[
]
=
We note the increasing depth of application of the S-rule for the above system, showing strong convergence.
O
u
t
[
]
=
Here we see the multiway states graph, each node annotated with the expression depth, reminiscent of the functions seen earlier.
I
n
[
]
:
=
g
=
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
{
s
[
x
_
]
[
y
_
]
[
z
_
]
-
>
x
[
z
]
[
y
[
z
]
]
,
k
[
x
_
]
[
y
_
]
-
>
x
}
,
p
l
u
s
[
i
n
t
e
g
e
r
[
1
]
]
[
i
n
t
e
g
e
r
[
1
]
]
[
s
]
[
k
]
,
4
0
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
;
I
n
[
]
:
=
d
e
p
t
h
s
=
M
a
p
[
D
e
p
t
h
[
T
o
E
x
p
r
e
s
s
i
o
n
[
#
]
]
&
,
V
e
r
t
e
x
L
i
s
t
[
g
]
]
;
I
n
[
]
:
=
m
i
n
=
M
i
n
[
d
e
p
t
h
s
]
;
m
a
x
=
M
a
x
[
d
e
p
t
h
s
]
;
I
n
[
]
:
=
S
h
o
w
[
G
r
a
p
h
P
l
o
t
3
D
[
g
,
V
e
r
t
e
x
R
e
n
d
e
r
i
n
g
F
u
n
c
t
i
o
n
-
>
(
{
H
u
e
[
(
D
e
p
t
h
[
T
o
E
x
p
r
e
s
s
i
o
n
[
#
2
]
]
-
m
i
n
)
/
(
m
a
x
-
m
i
n
)
/
2
,
1
,
1
]
,
E
d
g
e
F
o
r
m
[
B
l
a
c
k
]
,
S
p
h
e
r
e
[
#
,
.
0
7
5
]
,
B
l
a
c
k
}
&
)
]
,
E
p
i
l
o
g
-
>
I
n
s
e
t
[
B
a
r
L
e
g
e
n
d
[
{
H
u
e
[
(
#
-
m
i
n
)
/
(
m
a
x
-
m
i
n
)
/
2
,
1
,
1
]
&
,
{
m
i
n
,
m
a
x
}
}
]
,
{
R
i
g
h
t
,
C
e
n
t
e
r
}
,
{
R
i
g
h
t
,
C
e
n
t
e
r
}
]
]
O
u
t
[
]
=
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.
I
n
[
]
:
=
i
n
i
t
s
=
F
l
a
t
t
e
n
[
T
a
b
l
e
[
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
E
n
u
m
e
r
a
t
e
C
o
m
b
i
n
a
t
o
r
s
"
]
[
n
,
{
s
}
]
,
{
n
,
1
,
8
}
]
]
;
I
n
[
]
:
=
s
r
u
l
e
=
s
[
x
_
]
[
y
_
]
[
z
_
]
-
>
x
[
z
]
[
y
[
z
]
]
I
n
[
]
:
=
g
r
o
w
t
h
=
T
a
b
l
e
[
P
a
r
a
l
l
e
l
M
a
p
[
F
u
n
c
t
i
o
n
[
i
n
i
t
,
R
e
s
o
u
r
c
e
F
u
n
c
t
i
o
n
[
"
M
u
l
t
i
w
a
y
C
o
m
b
i
n
a
t
o
r
"
]
[
{
s
r
u
l
e
}
,
i
n
i
t
,
n
,
"
S
t
a
t
e
s
G
r
a
p
h
S
t
r
u
c
t
u
r
e
"
]
]
,
i
n
i
t
s
]
,
{
n
,
1
,
5
}
]
;
I
n
[
]
:
=
M
a
p
[
F
u
n
c
t
i
o
n
[
g
r
o
w
,
M
a
p
[
V
e
r
t
e
x
C
o
u
n
t
[
#
]
&
,
g
r
o
w
]
]
,
g
r
o
w
t
h
]
/
/
M
a
t
r
i
x
P
l
o
t
[
#
,
F
r
a
m
e
-
>
F
a
l
s
e
]
&
O
u
t
[
]
=
This can be further illustrated by fitting functions to this data and visualising the distribution of points in parameter space after dimensionality reduction.
I
n
[
]
:
=
g
r
o
w
t
h
s
=
M
a
p
[
F
u
n
c
t
i
o
n
[
g
r
o
w
,
M
a
p
[
V
e
r
t
e
x
C
o
u
n
t
[
#
]
&
,
g
r
o
w
]
]
,
g
r
o
w
t
h
]
/
/
T
r
a
n
s
p
o
s
e
;
I
n
[
]
:
=
f
i
t
s
=
M
a
p
[
F
i
n
d
F
i
t
[
#
,
a
+
b
*
x
+
c
*
x
^
2
+
d
*
x
^
3
,
{
a
,
b
,
c
,
d
}
,
x
]
&
,
g
r
o
w
t
h
s
]
;
I
n
[
]
:
=
f
i
t
s
V
e
c
=
M
a
p
[
F
u
n
c
t
i
o
n
[
f
i
t
,
{
f
i
t
[
[
1
]
]
[
[
2
]
]
,
f
i
t
[
[
2
]
]
[
[
2
]
]
,
f
i
t
[
[
3
]
]
[
[
2
]
]
,
f
i
t
[
[
4
]
]
[
[
2
]
]
}
]
,
f
i
t
s
]
;
I
n
[
]
:
=
d
r
=
D
i
m
e
n
s
i
o
n
R
e
d
u
c
t
i
o
n
[
f
i
t
s
V
e
c
]
I
n
[
]
:
=
L
i
s
t
P
l
o
t
[
d
r
[
f
i
t
s
V
e
c
]
,
P
l
o
t
R
a
n
g
e
-
>
F
u
l
l
]
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
S
i
n
(
x
)
and expand it to the Taylor series representation using the Mathematica function
Series[...]
O
u
t
[
]
=
x
-
3
x
6
+
5
x
1
2
0
-
7
x
5
0
4
0
+
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,
i
x
e
, which defines a unit circle in the complex plane. Factoring into real and imaginary parts, we obtain infinite series definitions for the harmonic functions
S
i
n
(
x
)
and
C
o
s
(
x
)
.
O
u
t
[
]
/
/
T
a
b
l
e
F
o
r
m
=
x
x
-
3
x
6
x
-
3
x
6
+
5
x
1
2
0
x
-
3
x
6
+
5
x
1
2
0
-
7
x
5
0
4
0
x
-
3
x
6
+
5
x
1
2
0
-
7
x
5
0
4
0
+
9
x
3
6
2
8
8
0
If we nest progressively truncated version of this series we get:
O
u
t
[
]
/
/
T
a
b
l
e
F
o
r
m
=
x
x
-
3
x
6
-
1
6
3
x
-
3
x
6
x
-
3
x
6
+
5
x
1
2
0
-
1
6
3
x
-
3
x
6
+
5
x
1
2
0
+
1
1
2
0
5
x
-
3
x
6
+
5
x
1
2
0
-
1
6
3
x
-
3
x
6
+
5
x
1
2
0
-
1
6
3
x
-
3
x
6
+
5
x
1
2
0
+
1
1
2
0
5
x
-
3
x
6
+
5
x
1
2
0
+
1
1
2
0
5
x
-
3
x
6
+
5
x
1
2
0
-
1
6
3
x
-
3
x
6
+
5
x
1
2
0
+
1
1
2
0
5
x
-
3
x
6
+
5
x
1
2
0
Looking at the resulting expression tree growth we see the following pattern:
I
n
[
]
:
=
T
a
b
l
e
[
N
e
s
t
[
N
o
r
m
a
l
[
S
e
r
i
e
s
[
S
i
n
[
x
]
,
{
x
,
0
,
2
n
+
1
}
]
]
/
.
x
-
>
#
&
,
x
,
n
+
1
]
/
/
E
x
p
r
e
s
s
i
o
n
G
r
a
p
h
,
{
n
,
0
,
3
}
]
O
u
t
[
]
=
The number of nodes in the expression trees grows like this:
O
u
t
[
]
=
{
1
,
1
8
,
1
4
0
,
1
3
4
0
,
1
6
2
4
6
}
Plotting these shows rapidly growth.
O
u
t
[
]
=
Fitting a function of the form
a
b
x
e
yields the following parameters.
O
u
t
[
]
=
{
a
0
.
0
0
8
2
6
2
0
8
,
b
2
.
8
6
5
0
1
}
Our fitted function is:
O
u
t
[
]
=
0
.
0
0
8
2
6
2
0
8
2
.
8
6
5
0
1
x
N
o
t
e
t
h
e
e
x
p
o
n
e
n
t
i