WolframAlpha.com
WolframCloud.com
All Sites & Public Resources...
Products & Services
Wolfram|One
Mathematica
Wolfram|Alpha Notebook Edition
Programming Lab
Finance Platform
SystemModeler
Wolfram Player
Wolfram Engine
WolframScript
Enterprise Private Cloud
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:
Wolfram Science
Mathematics
Physics
Wolfram Language
Wolfram Summer School
6
Xerxes Arsiwalla
[WSS20] Homotopic Foundations of Wolfram Models
Xerxes Arsiwalla, Pompeu Fabra University
Posted
10 months ago
3578 Views
|
0 Replies
|
6 Total Likes
Follow this post
|
Xerxes D. Arsiwalla
Pompeu Fabra University, Barcelona, Spain
Project Goals: The main objective of this project is to contextualize the Wolfram physics models within the foundations of Homotopic Type Theory. This mathematical foundation helps formalize the notion of space and seeks to address the subset of rules that lead to physically plausible universes. Homotopy Type Theory (HoTT) provide the mathematical grounding for a synthetic theory of structure. Logic, topology and geometry are then formulated upon those structures. A natural question would be to ask what the physical counterparts of these mathematical objects may manifest themselves as within the Wolfram models? Moreover HoTT also characterizes inductive and higher inductive rules for transforming between rules. This parallels the rules and rules of rules in the Wolfram model. The significance of expressing physical models in this language of HoTT is that it makes precise the links between proofs and geodesics, thereby demonstrating a realization of the Einstein equations for higher types (and a corresponding Wheeler-DeWitt equation at each level). This exploration also provides a mathematical interpretation of the Knuth-Bendix completion within Wolfram models as an application of the Univalence Axiom in HoTT.
At its crux, the Wolfram physics project seeks to explore the most fundamental structures in the universe that admit the laws of physics as we know it. In order to achieve this, models in the project seek to understand how simple rules compose together leading to complex structures in possible physical universes. The quest for understanding fundamental structures has parallels in the foundations of physics as well as mathematics. The purpose of this article is to explore the mathematical foundations of multiway hypergraphs, branchial spaces and rulial spaces appearing in Wolfram models of the universe.
In recent years, Homotopic Type Theory (HoTT) has been developed as a framework for formalizing the foundations of mathematics. HoTT combines Martin-Lof Type theory from Intuitionistic Logic along with Voevodsky’s univalence axiom to provide the formal foundations for all mathematical structures. This program subsumes traditional set theory and generalizes to higher types that eventually provide a precise notion of spatial structures via Grothendieck’s hypothesis. In what follows, we illustrate how the formalism of HoTT relates to Wolfram models of physics. We begin with a discussion of multiway models of generic mathematical structures from the point of view of HoTT and how these objects can be identified as a free topos of space. This construction when interpreted as a section of the rulial space presents a multiverse of multiway systems. We discuss potential structures necessary to admit the laws of physics on these spaces. Finally, we discuss a further generalization of the full rulial multiverse as an
∞
-topos and a potential classification of these universes as cellular automata.
M
u
l
t
i
w
a
y
M
o
d
e
l
s
o
f
M
a
t
h
e
m
a
t
i
c
a
l
S
t
r
u
c
t
u
r
e
s
Rules in Wolfram models formally correspond to Type Constructors equipped with universal properties. In type theory, these constructors correspond to mathematical operations or objects, repeated application of which, generates the corresponding structure. For example, with type constructors corresponding to a binary product, a generator, an identity and an inverse (along with conditions of associativity) one generates a group structure. In the Wolfram model, these rules generate a multiway system, which is in fact the Cayley graph of the group. With the addition of co-products, the multiway system yields a co-algebra. In this way, the multiway models are capable of representing several mathematical structures.
Comparing type theoretic constructions of multiway models to HoTT, one can identify the multiway system to an
∞
-Groupoid (this is a quasi-category where inverse morphisms exist and equalities of identity and associativity are replaced by isomorphisms up to homotopy of infinitely higher types). As per Grothendieck’s hypothesis,
∞
-Groupoids are formal homotopic spaces, where terms of given types correspond to points and paths to type-theoretic proofs. Paths between terms can be isomorphic up to higher homotopies (when isomorphisms are strict equalities, we simply obtain a 1-category, in that sense, an
∞
-Groupoid is a natural structure with fewer restrictions). When interpreted in type-theoretic terms, this is exactly the underlying construction of multiway systems. Additionally, if one includes a subobject classifier
Ω
(which is the categorical generalization of a subset identifier) among the type constructors and ensures that finite limits exist, one get an elementary topos
T
(sometimes referred to as a logical topos). Such a construction comes equipped with a functor
Γ
to the topos of sets along with two adjoint functors
Δ
and
∇
which respectively admit the discrete and indiscrete topology upon
T.
A free topos with these string of adjoint functors formalizes the notion of a homotopic space. The multiway systems of the Wolfram models precisely present the respective graphs of such homotopic spaces. Foliations in the multiway correspond to a sub-category, referred to as a branchial space. Completions in the multiway models are precisely identifications of propositional extensionality in Type theory (subsequently generalized to identification of types using the Univalence Axiom). These spaces are more general than those obtained from ZFC based set-theoretic constructions, in that they may may not always admit the law of the excluded middle or the axiom of choice. Rather, these topoi of spaces come equipped with Voevodsky’s Univalence Axiom.
[
◼
]
M
u
l
t
i
w
a
y
S
y
s
t
e
m
[
{
"
A
"
"
A
B
"
}
,
"
A
A
"
,
5
,
"
S
t
a
t
e
s
G
r
a
p
h
"
]
O
u
t
[
]
=
Figure: A single rule multiway system as a prototype of mathematical structures.
M
u
l
t
i
v
e
r
s
e
M
o
d
e
l
s
o
f
P
h
y
s
i
c
a
l
S
t
r
u
c
t
u
r
e
s
Given the above identification of multiway systems as formal spaces, the question we address here is what type of multiway models realize physically relevant spaces? The key mathematical question is: what type of topoi admit geometric structures relevant for physics? Not all multiways in HoTT admit smooth topological spaces with Riemannian or pseudo-Riemannian metrics. This is where very recent developments in Cohesive HoTT come into play [Shulman]. These authors have shown that topoi whose objects themselves are R^n (as a type, not necessarily a set) for all n
∈
N, admit smooth structures giving Riemannian geometries. Though it is not precisely known what collection of type constructors will specifically lead to such topoi, one can infer that the constructors needed have to at least include function types, natural number objects and identity types, among others. Additionally, for getting the category of quantum mechanics, a tensor product type constructor would be required. In the Wolfram models, hypergraphs with multiple rules corresponding to the abovementioned constructor types would potentially yield a realization of a geometric topos. Of course, here all quotients of R^n and their automorphisms are allowed. This is in fact, a multiverse of multiway models (each multiway corresponding to a single rule). Proof completions in the multiverse are now elegantly captures by the univalence axiom which generalizes propositional extensionality to type extensionality. Moreover, the sub-category obtained from a foliation of this multiverse precisely yields the categorical quantum mechanics of [Abramsky, Coecke] provided we have included the tensor product constructor. In other words, the branchial space of the multiverse is simply a categorical tensor product of finite dimensional vector spaces admitting an inner product. The geometric structure at the level of the rulial space is that the multiverse of physics is obtained as a fiber bundle, where a section of the rulial space forms a base and multiways corresponding to individual rules form fibers.
O
u
t
[
]
=
Figure: Schema of a multiverse generated from multiple rules
C
l
a
s
s
i
f
i
c
a
t
i
o
n
o
f
t
h
e
R
u
l
i
a
l
T
o
p
o
s
a
s
C
e
l
l
u
l
a
r
A
u
t
o
m
a
t
a
?
One can now go beyond the section of the rulial space generating a multiverse and ask what the full rulial space and its fibers correspond to? In fact, the most general rulial space will correspond not just to rules, but also to rules of rules. In HoTT, such objects are known as Higher Inductive Types (HITs). With HITs, the rulial space by itself acquires the structure of an
∞
-Groupoid. Given that a multiverse without HITs was a topos, what we now obtain is in fact an
∞
-topos (where the fibers collectively form all possible multiverses). However, one may ask whether the full
∞
-topos may even be relevant for physics? One way to think about this issue is to classify multiverse fibers in a way analogous to the classification of one dimensional cellular automata. Having a universe built from every possible rule will inevitably include rules similar to rule 30 leading to multiverses that are computationally irreducible (class 3 cellular automata). This may not lead to computationally reducible universes. Physics itself may result from only those subsections of rulial space that allow for a certain degree of computational reducibility, corresponding to the class of computational automata (class 4). On the other hand, sectors of rulial space corresponding to computationally irreducible multiverses may potentially be relevant for describing potentially non-computational structures (for instance, mental attributes - which might be modelled as an observer-dependent projection of a computationally irreducible fiber to a reducible one, creating an illusion of "understanding").
{
A
r
r
a
y
P
l
o
t
[
C
e
l
l
u
l
a
r
A
u
t
o
m
a
t
o
n
[
1
1
0
,
{
{
1
}
,
0
}
,
5
0
]
]
,
A
r
r
a
y
P
l
o
t
[
C
e
l
l
u
l
a
r
A
u
t
o
m
a
t
o
n
[
3
0
,
{
{
1
}
,
0
}
,
5
0
]
]
}
I
n
[
]
:
=
,
O
u
t
[
]
=
Figure: Are the multiverses of physics akin to cellular automata as rule 110 or rule 30?
Keywords
Homotopy Type Theory
◼
∞
-Groupoids
◼
Univalence Axiom
◼
Grothendieck’s Homotopy Hypothesis
◼
Acknowledgments
Mentor
: Jonathan Gorard
The author profusely thanks Jonathan and Stephan for many inspiring and informative discussions. Thanks also to the entire organizing team of the WSS 2020!
References
M. Shulman, Homotopy Type Theory: The Logic of Space, New Spaces for Mathematics and Physics, 2017
◼
S. Abramsky, B. Coecke, Categorical Quantum Mechanics, Handbook of Quantum Logic and Quantum Structures, 2009
◼
POSTED BY:
Xerxes Arsiwalla
Answer
Mark as an Answer
Reply
|
Flag
Reply to this discussion
in reply to
Add Notebook
Community posts can be styled and formatted using the
Markdown syntax
.
Tag limit exceeded
Note: Only the first five people you tag will receive an email notification; the other tagged names will appear as links to their profiles.
Publish anyway
Cancel
Reply Preview
Attachments
Remove
Add a file to this post
Follow this discussion
or
Discard
Group Abstract
Be respectful. Review our
Community Guidelines
to understand your role and responsibilities.
Community Terms of Use
Feedback
Enable JavaScript to interact with content and submit forms on Wolfram websites.
Learn how »