Wolfram Cloud Document

This project explores preliminary work in creating a homoiconic foundation of mathematics in the Wolfram Language Framework. A homoiconic foundation is one where the connection between the syntax and semantics of a formal theory is established from the beginning. The basis for this work is inspired by the general methodology of mathematical logic, where systems of derivation rules (proof theory) and systems of models (model theory) are developed independently and then connected via an interpretation. A homoiconic foundation is one where the connection between the syntax and semantics of a formal theory is established from the beginning. The basis for this work is inspired by the general methodology of mathematical logic, where systems of derivation rules (proof theory) and systems of models (model theory) are developed independently and then connected via an interpretation. Constructing this interpretation is not always a straightforward process. A homoiconic foundation would put the effort of constructing the interpretation into the building blocks of the theory. This project presents a syntactic formal theory for two small groups in terms of WL rewrite rules and data structures. It then expresses the categorical structure of the theory in terms of the Categorica tools from the WL. The resulting functor is a component of a larger interpretation. There is a great deal of possible future work to perform. The functions and techniques used in this project are exploratory and preliminary, and refinement is called for in many places. Beyond that, the methodology of the project needs to be generalized to other formal theories, so that it can legitimately serve as a foundation.

The Methodology of Formal Logic

Understanding the goals of this project requires some general background in how investigations in formal logic typically proceed.

Syntax

The syntax of a mathematical theory refers to its purely symbolic representation.
Wolfram Language has a Theorem Proving tool that operates directly on syntactically defined theories.
It uses First Order Logic, and a basic set theory proof will serve as an illustration of both syntax and semantics.
Consider the set theory equation;

a⋃(b⋂c)(a⋃b)⋂(a⋃c)

Each symbol, (⋃,⋂,==) has a corresponding definition in terms of the connectives of First Order Logic (simplified here).

ProofObject

Logic: Predicate/EquationalLogic	Steps: 4
Theorem: (a\|\|(b&&c))((a\|\|b)&&(a\|\|c))

["ProofDataset"][All,"Statement"]proof=FindEquationalProof[Or[a,And[b,c]]==And[Or[a,b],Or[a,c]],{}]

Out[]=

ProofObject

Logic: Predicate/EquationalLogic	Steps: 4
Theorem: (a\|\|(b&&c))((a\|\|b)&&(a\|\|c))



FindEquationalProof will construct a sequence of statements that follow from each other by rewrite rules corresponding to axioms of First Order Logic. In this way, the derivation of theorems in a formal system can be thought of as purely symbolic. The statements of the theory and the rewrite rules relating them form a mathematical structure in their own right. They can be studied independently of the models/space the theory describes.

Semantics

Formal theories should describe something. The semantics of a theory are a different, usually more familiar or well-known mathematical object. This model provides an interpretation of the purely symbolic derivations done by the formal theory.
We can interpret a set as a region on the 2-dimensional plane, and then interpret ‘⋂’ as ‘only the overlap’ and ‘⋃’ as ‘connecting’ the regions.

Then a ⋃ (b ⋂ c) corresponds to subregions a = {1,2,3,7} and (b ⋂ c) = {5,3}, which combine into {1,2,3,5,7}

And (a ⋃ b) ⋂ (a ⋃ c) corresponds to the overlap of (a ⋃ b) = {1,2,3,4,5,7} and (a ⋃ c) = {1,2,3,5,6,7}, which overlap at {1,2,3,5,7}

So semantically, the two constructions correspond to the same region.

Out[]=

Interpretations

It is reassuring to see that the equation

a ⋃ (b ⋂ c)  (a ⋃ b) ⋂ (a ⋃ c)

Can be verified in more than one way; as (i) a statement that holds true in a model, and (ii) the result of a valid symbolic derivation.
Even better the two ways of seeing agree! Each perspective can provide insight. The very surprising thing that formal logic lets us do is go beyond and particular equation and establish in principle that any derivation corresponds to a valid model (this is called soundness), and conversely, that any fact describing a model can be formally expressed and derived (completeness). Soundness and completeness results allow us to:
First Order Logic and Set Theory are only the most elementary examples to illustrate this idea. Although the remainder of the project launches into the abstract wilderness of category theory, bear in mind that the methodology is essentially the same! We have a syntactic theory, and we construct from it an interpretation into a familiar mathematical space; in this case, the Category of Sets.

A Syntactic Theory of Groups

A group is an abstract mathematical structure, often thought to describe the possible ways a concrete object can be symmetrical. One common way to build and describe groups is via a group presentation; a list of generators and relations. Every group element is constructed by successive composition of generators, reduced by the relations. From this perspective a group consists of a list of generators and a list of relations.

K4=AbstractGroup[(*TheKlein4Group*){a,b},(*Generators*){CircleDot[a,a]==e,CircleDot[b,b]==e,CircleDot[CircleDot[a,b],CircleDot[a,b]]==e,(*Relations*)CircleDot[a,b]==CircleDot[b,a]}]C4=AbstractGroup[(*TheCyclicGroupofOrder4*){x},{CircleDot[CircleDot[x,x],CircleDot[x,x]]==e}]

To build the categorical structure around these group presentations, we also need a notion of a map between groups; a group homomorphism. An advantage of the generator-relation presentation is that a group homomorphism can be described completely in terms of a map from generators to generators, and by adding the relations of the domain group to those of the codomain group.

K4toC4=AbstractGroupHomomorphism[K4,(*Domain*){a->x,b->x},(*Mappingsofgenerators*){x},(*Newgenerators*){CircleDot[CircleDot[x,x],CircleDot[x,x]]==e}(*NewrelationstoimposeontheimageofK4*)]

Now, while this data does characterize a homomorphism between group presentations, another feature of these groups we need access to is the notion of equality between two groups. Some relations may be redundant, especially after generator mappings. However homomorphisms as defined above can only add generators and relations. However, two presentations might encode the same group structure. That is, two instances like K4 and C4 defined above might not be extensionally equal; though they will be different in terms of their expression, they may be representations of isomorphic groups. We want to consider groups up to isomorphism, so we want to be able to know that we are not conflating two isomorphic groups simply because they are not extensionally equal.

For this we use a function that creates canonical representations of groups in terms of their elements and Cayley Table. We will use C4 as an example. First we generate all words (up to length 4, since the group is of order 4) on the generators. This list is reduced to a canonical form of left-associated parentheses.

{a,a⊙a,(a⊙a)⊙a,((a⊙a)⊙a)⊙a}

Then construct all equations between any two such words.

Out[]=

{aa⊙a,a(a⊙a)⊙a,a((a⊙a)⊙a)⊙a,a⊙aa,a⊙a(a⊙a)⊙a,a⊙a((a⊙a)⊙a)⊙a,(a⊙a)⊙aa,(a⊙a)⊙aa⊙a,(a⊙a)⊙a((a⊙a)⊙a)⊙a,((a⊙a)⊙a)⊙aa,((a⊙a)⊙a)⊙aa⊙a,((a⊙a)⊙a)⊙a(a⊙a)⊙a}

Next we use FindEquationalProof, plus rewrite rule versions of the Group Axioms, and relations for C4 to further reduce any duplicate elements that can be equated via the relations. In the case of a cyclic group, this process is not very interesting. Finally we generate the Cayley, or multiplication table on this set of elements to encode the overall group structure.

x⊙x	(x⊙x)⊙x	e	x
(x⊙x)⊙x	e	x	x⊙x
e	x	x⊙x	(x⊙x)⊙x
x	x⊙x	(x⊙x)⊙x	e

Categorical Interpretations

The syntactic theory of groups detailed in the previous section gives rise to a category.The objects are the groups themselves; K4 and C4, and:A central result in Category Theory is that any category C has a Yoneda Embedding into another category, the category of functors from C* into the category of Sets. Essentially this means that any category has a standard kind of representation in one of the most familiar categories. The Yoneda Embedding makes use of a specific type of functor, a hom-functor, which maps objects to the set of morphisms into** that object, and morphisms to compositions of morphisms. Since the images of objects under these functors are sets, the images of morphisms are functions. A pair of such functions can produce a morphism between functors known as a natural transformation. The Yoneda Embedding makes use of the fact that every morphism in a category gives rise to a natural transformation between hom-functors, and that this correspondence respects the structure of the original category. Here is the categorical structure of the groups we defined.

*technically the dual category to C.
**or out of.

Concluding remarks

As the title suggests, this project is only a first step toward the broader goal of developing a homoiconic foundation.
A constant tension throughout the project was to decide when it was prudent to take a categorical approach, looking only at structural properties, and when to focus on the fine details of each data type.
Methodologically, the categorical perspective is designed to allow us not to worry about details of our objects. However, many of the results prove to be of minimal interest when expressed only in categorical terms.
Of course, when focused on the exact structure of each group and their morphisms, a great deal of tedious work was necessary to ensure correctness.

Many details of the code presented here are ad-hoc to ensure that the specific example will work;
We know the order of each group, which helps to reduce the number of possible terms to consider when constructing a Cayley table.
The Wolfram Language Categorica Tools already provide a great deal of the categorical structure needed to express functors.
The image of the hom-functors and the Yoneda embedding are essentially equivalent to their images -there is no ambient category of Sets from which to draw the required morphisms.

Steps to take to continue to project include;
Generalizing many functions to take any group presentation and produce a Cayley table.
Generalizing Categorica tools to allow for the construction of hom-functors, and the Yoneda embedding for any category. (this latter may require building a bit of Set)
Outlining a procedure for creating such a categorical representation of any formal theory.
Constructing some ‘common’ categorical structures to be the images of newly built AbstractFunctor expressions.

Keywords

◼

Homoiconic

◼

Syntax

◼

Semantics

◼

Interpretation

◼

Group

◼

Acknowledgment

I would not be able to have completed this project without the guidance of my mentor, Jonathan Gorard.
Jonathan’s previous work in Category Theory tools in Wolfram Language helped pave the way for not only for the categorical side of my project, but as a template for the Group Theory part.

Other mentors in the Wolfram Summer School who helped support me, in no particular order;
Mano Namuduri
Nikola Bukowiecka
Eric Parfitt
Hatem Elshatlawy
Yi Yin
Mark Greenberg

And my classmates/fellow Jonathan mentees;
Frederico Semenzato
Rob Giometti
Michael Ostroff
Srishti Nautiyal
Ananya Mukherjee
Jacabo Uggeri