CITE THIS NOTEBOOK: Sub-axiomatic foundations of group theory in SK combinators by Wolfram Emerging Leaders Program. Wolfram Community JAN 27 2023.
The Wolfram Emerging Leaders Program is a 4-month long, project-based program designed for gifted high school students to take a deep dive into a topic of their choice. Students work remotely in small groups to take their project from ideation to completion, with the guidance of Wolfram experts. Wolfram Emerging Leaders Program participants are selected from the Wolfram High School Summer Camp, which is open to talented, STEM-oriented students age 17 and under. This essay was written by:
◼
  • Henry Gustafson
    • ◼
  • Joseph Stoke
    • SK combinators form a system of Turing-complete, universal computation which only uses function application. Recently, Stephen Wolfram used the combinator model to construct the complete set of binary (dyadic) Boolean operators. The goal of our project was to extend this work to magmas and groups, and to find representations for the group axioms in combinators. We successfully created functions to generate combinator expressions for the elements of any group, its binary operation, other operations including the equality operation and the inverse operation, and representations of the group axioms in combinators.

    Background Information

    Combinators

    The two very simple combinators S and K create a system of universal computation. Any symbolic structure can be created by applying some sequence of S's and K's. The two combinators follow the very simple following replacement rules:
    Definition of S and K combinators
    In[]:=
    s[x_][y_][z_]->x[z][y[z]]​​k[x_][y_]->x
    Out[]=
    s[x_][y_][z_]x[z][y[z]]
    Out[]=
    k[x_][y_]x
    For example, if we wanted to construct c[a[b][c]] from a, b, and c, which could be any symbolic objects, we can pass them as inputs into the combinator expression S[S[K[S]][S[K]]]. Following the replacement rule for the S combinator, the leftmost S is applied to S[K[S]][S[K]], a, and b, so that part of the expression is replaced with S[K[S]][S[K]][b][a[b]], as shown below.
    One step of the evolution of the combinator expression
    In[]:=
    s[s[k[s]][s[k]]][a][b][c]/.{s[x_][y_][z_]->x[z][y[z]],k[x_][y_]->x}
    Out[]=
    s[k[s]][s[k]][b][a[b]][c]
    Repeatedly applying these rules, we eventually get to a point where no rules can be applied to change the expression, known as the fixed point of the expression, which is in this case the desired result.
    Fixed point of the combinator expression
    In[]:=
    s[s[k[s]][s[k]]][a][b][c]//.{s[x_][y_][z_]->x[z][y[z]],k[x_][y_]->x}
    Out[]=
    c[a[b][c]]
    In the Wolfram Language, there is a resource function that shows each step of the combinator expression's evolution to its fixed point.
    Full evolution from the original expression to its fixed point
    In[]:=
    ResourceFunction["CombinatorFixedPointList"][s[s[k[s]][s[k]]][a][b][c],"SKGlyphs"->{s,k}]//Column
    Out[]=
    s[s[k[s]][s[k]]][a][b][c]
    s[k[s]][s[k]][b][a[b]][c]
    k[s][b][s[k][b]][a[b]][c]
    s[s[k][b]][a[b]][c]
    s[k][b][c][a[b][c]]
    k[c][b[c]][a[b][c]]
    c[a[b][c]]
    By following the replacement rules, the expression eventually collapsed to the c[a[b][c]] object we wanted to construct. Because the S and K combinators are together computationally universal, there exists a combinator expression that could return any possible symbolic object. This means any computation can be done with combinators by representing objects as combinator expressions themselves.

    Previous Work

    SK combinators can be used for basic computation with integers. For example, every integer can be represented by starting with S[K] as zero and repeatedly applying S[S[K[S]][K]] n times to represent an integer n.
    Represent every positive integer as a combinator expression
    In[]:=
    CombinatorInteger[n_Integer]:=Nest[s[s[k[s]][k]],s[k],n]
    There also exist combinators for arithmetic operations. These combinators can be applied like functions to the expressions that represent integers.
    Arithmetic operations as combinators
    In[]:=
    plus=s[k[s]][s[k[s[k[s]]]][s[k[k]]]]​​times=s[k[s]][k]​​power=s[k[s[s[k][k]]]][k]
    Out[]=
    s[k[s]][s[k[s[k[s]]]][s[k[k]]]]
    Out[]=
    s[k[s]][k]
    Out[]=
    s[k[s[s[k][k]]]][k]
    As an example, applying the plus combinator to the expressions for 1 and 2 should become the expression for 3 when the replacement rules are applied.
    1+2 in combinator form
    In[]:=
    ResourceFunction["CombinatorFixedPointList"][plus[CombinatorInteger[1]][CombinatorInteger[2]][s][k],"SKGlyphs"->{s,k}]//Column
    Out[]=
    The result applies the S combinator 3 times, representing the integer 3. The same thing can be done with the times and power operations, using the CombinatorFixedPoint resource function to show only the result.
    3*2 in combinator form
    In[]:=
    ResourceFunction["CombinatorFixedPoint"][times[CombinatorInteger[3]][CombinatorInteger[2]][s][k],"SKGlyphs"->{s,k}]
    Out[]=
    s[s[s[s[s[s[k]]]]]]
    2^3 in combinator form
    In[]:=
    ResourceFunction["CombinatorFixedPoint"][power[CombinatorInteger[2]][CombinatorInteger[3]][s][k],"SKGlyphs"->{s,k}]
    Out[]=
    s[s[s[s[s[s[s[s[k]]]]]]]]
    Recently, Stephen Wolfram created a search to find the following combinator expressions for 2-input Boolean functions.
    In[]:=
    Grid[Table[{i,ArrayPlot[{IntegerDigits[i,2,4]},ColorRules->{1->GrayLevel[.35],0->White},Mesh->True,ImageSize->50],{False,Nor,"",Not,"",Not,Xor,Nand,And,Equal,Last,Implies,First,"",Or,True}[[i+1]],Extract[ttresults,Position[ttresults,i][[1,;;2]]][[1]]/.{s->Style[s,Black,FontWeight->"SemiBold"],k->Style[k,Black,FontWeight->"SemiBold"]},ResourceFunction["CombinatorTraditionalForm"][Extract[ttresults,Position[ttresults,i][[1,;;2]]][[1]]]},{i,15,0,-1}],Frame->All]
    Out[]=
    15
    True
    k[k[k]]
    K(KK)
    14
    Or
    s[s[s]][s][s[k]]
    S(SS)S(SK)
    13
    s[k[s[s[s][k[k[k]]]]]][k]
    S(K(S(SS(K(KK)))))K
    12
    First
    k
    K
    11
    Implies
    s[s][k[k[k]]]
    SS(K(KK))
    10
    Last
    s[k]
    SK
    9
    Equal
    s[s][k[s[s[s][k[k[k]]]][s]]]
    SS(K(S(SS(K(KK)))S))
    8
    And
    s[s][k]
    SSK
    7
    Nand
    s[s[k[s[s[s][k[k[k]]]]]]][s]
    S(S(K(S(SS(K(KK))))))S
    6
    Xor
    s[s[s[s[s]][s[s[s[k]]]][s]]][k]
    S(S(S(SS)(S(S(SK)))S))K
    5
    Not
    k[s[s[s][k[k[k]]]][s]]
    K(S(SS(K(KK)))S)
    4
    s[k[s[s[s[s[k]]][s]]]][k]
    S(K(S(S(S(SK))S)))K
    3
    Not
    s[s][s[s[s[s[k]]][s]]][k[k]]
    SS(S(S(S(SK))S))(KK)
    2
    s[s[s[k]]][s]
    S(S(SK))S
    1
    Nor
    s[s[s[s[s][k[k[k[k]]]]]][k[s]]]
    S(S(S(SS(K(K(KK)))))(KS))
    0
    False
    k[k[s[k]]]
    K(K(SK))
    These combinators can be combined to create any Boolean function. As an example of a computation, we can apply the Xor function to True and False and we should expect the result to be True (the value not the function), which is represented by the K combinator.
    Xor[True, False] in combinators
    In[]:=
    true=k;​​false=s[k];​​XorCombinator=s[s[s[s[s]][s[s[s[k]]]][s]]][k];​​ResourceFunction["CombinatorFixedPoint"][XorCombinator[true][false],"SKGlyphs"->{s,k}]
    Out[]=
    k
    As another example, applying And to the same inputs should return False, which is represented by the combinator S[K].
    And[True,False] in combinators
    In[]:=
    AndCombinator=s[s][k];​​ResourceFunction["CombinatorFixedPoint"][AndCombinator[true][false],"SKGlyphs"->{s,k}]
    Out[]=
    s[k]

    Group Theory

    The goal of our project was to extend the area of math that can be represented computationally in combinators to group theory. A group is a set of elements and a group operation that combines any two elements to produce another element in the set. Groups must follow the following axioms:
    Axioms of group theory
    In[]:=
    AxiomaticTheory["GroupAxioms"]
    Out[]=
    
    ∀
    a.,b.,c.
    a.⊗b.⊗c.a.⊗b.⊗c.,
    ∀
    a.
    a.⊗
    
    1
    a.,
    ∀
    a.
    a.⊗
    a.
    
    
    1
    
    ◼
  • The first axiom is associativity; this is the idea that parentheses can be rearranged without changing the result.
    • ◼
  • The next axiom is identity; there must be one element in the group that, when composed with any other element in the set, leaves the other element unchanged.
    • ◼
  • The third axiom is inverse; for every element in the group, that element can be composed with its inverse to produce the identity element.
    • Our goal was to find a combinator expression for the group operation and every element of any group. Because the axioms also contain ForAll and equality, they both need to be represented in combinator form as well. For example, take the cyclic group with three elements,
    C
    3
    .
    In[]:=
    GroupElements[CyclicGroup[3]]
    Out[]=
    {Cycles[{}],Cycles[{{1,2,3}}],Cycles[{{1,3,2}}]}
    Composing the first element, the identity element, with either of the other two will return the other element. Composing the second element with either of the other two will shift that element one to the right. The third element similarly shifts one element to the left. If the elements were said to represent the rotational symmetries of an equilateral triangle, the first element would represent no rotation, the second a rotation 120 degrees clockwise, and the third a 120 degree counterclockwise rotation. The group operator that takes two of these three elements as inputs needs to be represented as a combinator.
    Cayley graph of
    C
    3
    In[]:=
    CayleyGraph[CyclicGroup[3]]
    Out[]=
    Every combinator of length 4 or less applied to [1][2][3]
    It turns out that there is a combinator that provided the correct output.
    Finding combinator that returned 1
    Following a similar process for the other two, we get the following three combinators:
    This represents all three elements in the set computationally, but the group operation still needs to be written as a combinator expression. To search for the correct expression, we created a function to test a group operator by using it to compose every pair of two elements in the group with each other.
    Composing every pair of elements
    For example, if we used simply K as our group operator, the result should always be the first of the two inputs.
    Testing K as the group operator
    As we predicted, when the first element is composed with any of the three elements, the first element is returned and the same is true for each of the others. Composing every pair of elements in the group with each other shows what we should expect SKGroup3Table to return.
    Compose every pair of elements (not in combinator form)
    Now, all combinator expressions can be searched to find one that returns the expected multiplication table output from SKGroup3Table.
    Checking all combinators up to length 4 for the desired output
    We were not able to find any combinator that returned the correct list until we reached combinator expressions with 76 S's and K's.

    Generalizing to magmas

    A magma (or groupoid) is a basic algebraic structure consisting of a set of elements, and a binary operator with closure over those elements. Magmas are a more fundamental structure than groups; when the group axioms of identity, inverse, and associativity are imposed on top of this structure, groups are created.

    Combinator expressions for set elements

    Given this structure of magmas, we thought it would be sensible to model the elements of an arbitrarily large, finite magma in a similar way. For a magma of n elements, unique combinators corresponding to these elements with indices 1...n can be constructed as combinators which take n inputs and return the ith input.
    The SKCombinatorCompile resource function constructed our group elements much more efficiently than our manual method. However, because of the way the combinator expressions are constructed, we do miss the minimal length representation. For example, using our brute force search we found a shorter expression for the third element.
    Combinator constructed to represent the third element
    Shorter combinator found through brute force
    Now it is trivial to generalize our function to construct combinator expressions for the elements of any magma.
    We can test our function on magmas of order greater than 3 to confirm that it works.
    Generate elements for a magma of order 5
    Confirm that each combinator returns the corresponding index
    Generating elements for magmas of greater order begins to reveal the pattern in how the combinator construction works as well.
    Generate elements for a magma of order 8
    The identity element always repeatedly applied the S[K[K]] combinator, which is often abbreviated as the I combinator in SKI combinator calculus. Then, replacing one of these S[K[K]]’s in the expression with a K has the effect of applying the rest of the expression to the inputs, with the first one removed.
    First step of the second element applied to five inputs' evolution to its fixed point

    Combinator representation of binary operation

    Now, given a unique set of elements, the next step is to find a binary combinator with closure over this set of elements. We identified a method to construct said binary operators via multiplication tables. This began with the observation that given our choice of element structure, the magma elements themselves encoded indices which could be used to lookup corresponding values as we have shown several times.
    Each element selects the corresponding input
    By chaining two levels of index lookup together, a binary operator can be constructed. For example, to select the middle column of the table, the second element's combinator can be applied to all three rows. Then to select the item that is also in the first row, the first element's combinator can be applied to this column.
    Select second element from each row, then the first of these
    Since the interior index is repeated, the combinator can be compiled to leftmost form.
    Compile combinator to do above
    We can now see what this combinator does by treating it as a function as applying it to two elements of the group. To see what exactly the combinator does, we simply pass in 1 and 2 as these inputs.
    Apply above combinator to two inputs
    Given this method of constructing binary operators, it is now straightforward to compile a group operator to a combinator. Take for example, the cyclic group of order 3. As before, we generate the expected multiplication table.
    Replace element numbers with their respective combinator expressions
    Next, we write this multiplication table in the format we used before so that the group operation combinator can be compiled. We will apply some combinator we are calling "y" for now to each row and then some combinator "x" to the three elements that result. This will enable us to any two combination of elements to what the multiplication table says their "product" should be.
    Replace numbers with corresponding element as a combinator
    Compile binary operation combinator
    We can verify that this is indeed the operator on the cyclic group with three elements by reconstructing the multiplication table.
    Display each combinator's corresponding element number
    This entire process can then be condensed to a single function:

    Applying to group axioms

    Equality and inverse

    Given our focus on the axiomatic systems, we also found it important to reconstruct some additional operators required for the statement of said axioms.

    Equality operator as a combinator

    Firstly, we found it necessary to construct an equality operator on magmas to distinguish unique elements. Luckily, since equality is also a binary operator (instead mapping onto the space of true/false), we found we could simply reuse the table lookup method.
    Select item in table of True and False as before
    Replace True and False with combinator representations
    We can synthesise this idea as a single function to check if any two combinator expressions are equal:
    The equality multiplication table looks quite similar to the identity matrix, with True values down the diagonal and False everywhere else.
    Notably, equality can also be thought of as an operation that is reflexive, symmetric, and transitive. It should also be noted, however, that the strongest definition of equality on a given magma is not necessarily the only operation that is reflexive, symmetric, and transitive. For example, the Boolean operator on two elements which always evaluates to True is reflexive, symmetric, and transitive, despite being a very weak definition of equality. The forAll (∀) operator may be helpful in finding a combinator which evaluates whether a combinator is or is not the strongest possible definition of equality on a magma, but constructing forAll as a combinator wouldn’t solve the underlying issue of lacking a method of generating a complete list of unique elements without external information about the magma.

    Inverse operator as a combinator

    We also found it desirable to construct combinators which could express the inverse operator on various groups. Since inverse is only a unary operator, taking a single input index when in lookup form, it has a much simpler structure.
    Compile combinator that maps each element to its correct inverse
    The inverse of an element is defined as what that element needs to be composed with to become the identity element, so we can simply apply the combinator we want to the position of the identity element, 1, in each row and pass that into SKCombinatorCompile.

    Verifying axioms constructively

    Now that we have created these functions to recreate various aspects of the axioms like the == symbol (equality) and the inverse symbol, we can use combinators to find groups that conform to the group axioms.
    The above functions can be used to construct axiomatic statements via combinators
    The canonical cyclic group 3 combinator has identity as its first group element.
    Now we can verify that the first element conforms to the identity axiom by applying it to all three elements and checking that we get the same result for all three.
    Map the identity axiom check across all elements
    We can do something very similar for the inverse axiom, first finding the inverse with our function, then constructing our axiom, and finally applying it to all three elements.
    Apply axiom to all three elements
    Finally, the last group axiom is associativity. As a reminder, this means parentheses can be reordered to compose elements in a different order without a different result. We can use our EqualityCombinator function to check if the different orders of operations produce the same result.

    Conclusion

    We demonstrated a specific encoding for magma elements through combinators, along with a method to create arbitrary operators over a set of elements. This method applies to both the creation of unary operators and binary operators, along with the creation of operators closed over a set of elements, or operators mapping to different set of elements, notably operators mapping from group elements to Boolean values. We also demonstrated the construction of combinators representing Boolean tests of the group axioms for specific elements.

    Further Work

    We would like to extend our formulation of group axioms to general tests taking the group axiom itself as an argument, and verifying the axioms over all group elements. This would necessitate a combinator capable of performing a ForAll (∀) operation, which would be a unique structure in comparison to the unary and binary mappings between elements, instead mapping a Boolean operation to a truth value for a given size of magma. This work may lead to a more general understanding of formal logic in combinators.