Boolean logic in SK combinators​
​By Gleb Rusyaev
The goal of this project is to analyze combinatory representation of boolean logic. This is interesting because combinators are kind of “building blocks for logic” (a sort of “machine code”). Here we analyze multiway graphs of boolean functions and provide a general framework for further analysis.

Introduction

SK-combinators are expressions of 'S', 'K' and brackets that obey the following rules:
◼
  • S[x][y][z]  x[z][y[z]]
    • ◼
  • K[x][y]  x
    • We can emulate boolean operators with SK combinators. By setting arguments s[k] to true and k to false, one can take an operator (e.g. s[s][k]), and give it arguments (e.g. s[s][k][s[k]][k]). From there, we can create and evaluate Boolean expressions/formulae.
    Here are the smallest combinators emulating each 2-argument boolean function [1]:
    Putting these into Wolfram Language so we can call them up using CombinatorBooleanExample[named-boolean-function]:
    In[]:=
    CombinatorBooleanExample = <|​​ true -> k[k[s[k]]],​​ or -> s[s][k],​​ firstbool -> k,​​ implies -> s[s[s[k]]][s],​​ lastbool -> s[k],​​ equal -> s[s[s[s[s]][s[s[s[k]]]][s]]][k],​​ and -> s[s[s]][s][s[k]],​​ nand -> s[s[s[s[s][k[k[k[k]]]]]][k[s]]],​​ xor -> s[s][k[s[s[s][k[k[k]]]][s]]],​​ notlast -> k[s[s[s][k[k[k]]]][s]],​​ notfirst -> s[s][s[s[s[s[k]]][s]]][k[k]],​​ nor -> s[s[k[s[s[s][k[k[k]]]]]]][s],​​ false -> k[k[k]]​​|>
    Out[]=
    truek[k[s[k]]],ors[s][k],firstboolk,impliess[s[s[k]]][s],lastbools[k],equals[s[s[s[s]][s[s[s[k]]]][s]]][k],ands[s[s]][s][s[k]],nands[s[s[s[s][k[k[k[k]]]]]][k[s]]],xors[s][k[s[s[s][k[k[k]]]][s]]],notlastk[s[s[s][k[k[k]]]][s]],notfirsts[s][s[s[s[s[k]]][s]]][k[k]],nors[s[k[s[s[s][k[k[k]]]]]]][s],falsek[k[k]]

    Making tools for further analysis

    In order to perform the analysis, we need to find a way to enumerate all possible boolean combinatory expressions of a particular size. Fortunately, the Wolfram Function Repository already has a function to enumerate all possible combinatory expressions and we just need to come up with a tester that selects boolean expressions out of all possible expressions.

    Testing and classifying boolean expressions

    Making a test for combinator expression to figure out if it represents boolean function

    But what is the criterion for a boolean combinatory expression? We will assume that an expression is boolean if, treating it as a function, for all possible combinations of boolean arguments the results are also boolean.
    Create a 2-argument truth table for a particular combinator (TT,TF,FT,FF):
    In[]:=
    CombinatorTruthTable[combinator_] := Flatten @ Table[combinator[firstArgument][secondArgument], ​​ {firstArgument, {s[k],k}},{secondArgument, {s[k], k}}]
    Reduce each entry in combinatory truth table to the fixed point:
    In[]:=
    CombinatorTruthTableFixedPoint[combinator_, MaxSteps_Integer : 1000, MaxSize_Integer : 10000] :=​​Enclose[Confirm[ResourceFunction["CombinatorFixedPoint"][#, "SKGlyphs"->{s,k}, "MaxSteps"-> MaxSteps,"MaxSize"-> MaxSize]] & /@​​ Confirm[CombinatorTruthTable[combinator]]]
    Get truth table for 2-valued "AND" using “CombinatorTruthTableFixedPoint" vs “CombinatorTruthTable":
    In[]:=
    CombinatorTruthTable[CombinatorBooleanExample[and]]
    Out[]=
    {s[s[s]][s][s[k]][s[k]][s[k]],s[s[s]][s][s[k]][s[k]][k],s[s[s]][s][s[k]][k][s[k]],s[s[s]][s][s[k]][k][k]}
    In[]:=
    CombinatorTruthTableFixedPoint[CombinatorBooleanExample[and]]
    Out[]=
    {s[k],k,k,k}
    Up to this point we haven't assumed that we are dealing with a boolean function, we just tried to treat it like a boolean function. Using "CombinatorTruthTableFixedPoint" we can evaluate functions which when applied to "true-true" return false, but for "true-false" return a definition of boolean implication or integer addition. Now we will define a function that given combinator will decide whether it is a two-input boolean function.
    Check if fixed point is boolean (True ("s[k]") or False ("k")) :
    In[]:=
    CombinatorFixedBooleanQ[combinator_] := MatchQ[combinator, s[k] | k]
    Check if combinator expression is boolean:
    In[]:=
    BooleanCombinatorQ[combinator_, MaxSteps_Integer : 1000, MaxSize_Integer : 1000] :=​​ Length[Select[With[reducedCombinator=ResourceFunction["CombinatorFixedPoint"][combinator, "SKGlyphs"->{s,k},​​ "MaxSteps"-> MaxSteps,"MaxSize"-> MaxSize],If[FailureQ[reducedCombinator],{False},CombinatorTruthTableFixedPoint[reducedCombinator,​​ MaxSteps, MaxSize]]], CombinatorFixedBooleanQ]]==4
    Test how “BooleanCombinatorQ" works on: boolean function (implication) vs non-halting expression (at least for 1000 steps) vs non-boolean expression:
    In[]:=
    BooleanCombinatorQ[CombinatorBooleanExample[implies]]
    Out[]=
    True
    In[]:=
    BooleanCombinatorQ[s[s[s[s]]][s[s[s]]][s[s]]]
    Out[]=
    False
    In[]:=
    BooleanCombinatorQ[s[k][s]]
    Out[]=
    False

    Classifying boolean combinatory expressions as a boolean functions

    Furthermore, one might want figure out which boolean function a particular combinator expression represents. First, one needs to convert "combinatory truth table" to the regular one.
    Convert combinatory truth table to the regular truth table:
    In[]:=
    CombinatorTruthTableConvert[truthTable_List]:= Replace[truthTable,{s[k]->True,k->False},{1}]
    Test on function "AND":
    In[]:=
    CombinatorTruthTableConvert@CombinatorTruthTableFixedPoint@CombinatorBooleanExample@and
    Out[]=
    {True,False,False,False}
    Then one needs to create mapping from 2-input boolean functions to their truth-tables, we will do it using “CombinatorBooleanExample".
    Get association from truth table to 2-input boolean function:
    Test on function "Implies":
    This is what happens when we try to cast unnamed boolean function:
    In order to deal with "unnamed" boolean function, we will convert them into "BooleanFunction"
    Perform lookup in “CombinatorTruthTableToFunctionAssociation", returning BooleanFunction for unnamed functions.
    Try to lookup named function:
    Try to lookup unnamed function:

    Enumerating & classifying boolean combinatory expressions

    Enumerating boolean combinatory expressions

    Let's try to enumerate ordinary combinatory expression of a given size using a function from Wolfram Function Repository
    Enumerate all possible combinator expressions of size 3:
    Then we will use our checker “BooleanCombinatorQ" to select the boolean ones
    Enumerating all possible boolean combinatory expressions:
    Enumerate all possible boolean combinatory expressions of length 3:
    In order to make further analysis easier, we will also add function to count the amount of boolean combinatory expressions for given size:
    Count the amount of boolean combinatory expressions for a given size:
    Count the amount of arbitrary combinatory expressions for a given size:

    Classifying boolean combinatory expressions

    Finally, we will use our combinatory classifier — CombinatorTruthTableToFunction to group boolean combinator expressions of a given size based on 16 possible 2-input boolean functions they represent.
    Group boolean functions of a given size based on boolean function they represent:
    Enumerate all possible combinatory boolean expressions and group them by functions:
    Furthermore, similar to “CombinatorBooleanExpressionsAmount" we will create a similar function that given a size and a particular boolean function or named function (and, or, implies, … — names are the names of keys of CombinatorBooleanExample)
    Get the amount of expressions of size "size" representing boolean 2-input function "func":
    Test the function:
    Also, since one might not be interested in doing computation 2^4 times, we need to make a function returning the amount of expression for each function given the size.
    Generate map from function to amount of combinatory expression equivalent to that function:
    Test for size 4:

    Converting boolean expressions to combinators

    This is the order in which (treating boolean expression as a symbolic expression), we will "convert" it into combinatory expression given shortest possible combinatory expression describing particular 2-input boolean function
    Convert arbitrary boolean expression to combinator expression:
    "Modus tollens" tautology: ((P Q) ∧ ¬Q)  ¬P :
    Test the function on the "Modus tollens" — "denying the consequent" (tautology) :
    We can then evaluate combinator and try confirm tautology using a function from Wolfram Function Repository:
    Why does our expression does not reduce to "True"? Because combinator do not have any intrinsic knowledge of boolean logic and now it tried to "reduce" statement “((PQ)∧¬Q)¬P” without any knowledge about P and Q — in this expression they aren't bounded to True or False, we can insert "the image of a tiger" as P and definition of boolean XOR as Q and this still would be a valid computation. In order to actually proof this statement we need to construct a function f[p][q] from it and evaluate this function in a truth table (but of course you can replace P's and Q's here by hand with True or False).
    Construct a combinatory function from combinatory expression (f(x,g(x,y),x,y)  t(x,y) ⇔ f(x,g(x,y),x,y)) using "combinatory compiler":
    Use combinator truth table to confirm tautology (reminder that s[k] is true):
    “BooleanExpressionToCombinatorCompiled" can be also used to create logic functions for bigger amount of inputs. Here we create 4-input XOR function (but there are possibly shorter combinatory expression representing XOR):
    One might think about boolean functions with arbitrary amount of inputs, and they are possible (since SK-combinators are capable of universal computation), but require different kinda of encoding/decoding system for boolean expressions, since right now if such function "f" would exist, something like this would happen:
    ◼
  • Let f[x][y] = True and f[x][y][z] = False
    • ◼
  • Under a certain evaluation in the statement “f[x][y][z] " we would first evaluate f[x][y] and get True, so f[x][y][z] ⧦True[z] ⧦ False, because of the Church–Rosser property

    • Analysis

    Amounts, sizes and categories

    Amount of boolean functions vs arbitrary combinators for a given size

    Compute the amount of arbitrary combinator expressions up to length 10:
    Compute the amount of boolean combinatory expressions up to length 7:
    Let's compare the amount of arbitrary vs boolean combinatory expressions:
    Make a chart of all expressions vs boolean expressions using previous data:
    Make a chart of proportions of boolean functions to arbitrary expressions:

    Amount of particular functions (Or, And, …) for a given size

    For a given size we want to create similar bar chart for any particular function using “CombinatorBooleanExpressionsAmountForAllFunctions"
    Construct a bar chart:
    Now let's evaluate this for all sizes from 1 to 7:
    Amount of combinatory expressions representing particular function:

    Amount of combinatory expression equivalent to particular function for a given size

    Let’s now graph, for a given function, how many expressions of particular size represent it? Let's do this for one function "OR":
    Graph amount of expressions equivalent to "or" vs size:
    Graph amount of expressions equivalent to given function vs size:

    Multiway graphs

    Construct an example multiway graph structure

    Let's create a multiway graph for a particular expression. Since here we are not interested in a particular values in the vertices, but the overall topological structure of a graph, we will use “StatesGraphStructure" option.
    Define combinator reduction rules:
    Visualize a multiway graph for an example combinatory expression:

    Explore all possible multiway graph structures for a particular size

    Let's first construct all possible unique multiway graph structures given an arbitrary expression enumerator [1]
    Construct all possible unique multiway graph structures present in all possible combinatory expressions of size 6:
    Then, let's use our own enumerating function and get a similar table for all possible boolean combinatory expressions.
    Construct all possible unique multiway graph structures present in all possible boolean combinatory expressions of size 6:
    On the first glance, you might consider them the same, but there is a difference, and to find it, we will use "Complement" function.
    Get the complement from the set of all possible boolean multiway graph structures to the set of all possible arbitrary multiway graph structures for size 6:
    We might also consider doing the same for an arbitrary size:
    Get the complement from the set of all possible boolean multiway graph structures to the set of all possible arbitrary multiway graph structures for size N:
    Get MultiwayGraphBooleanComplement for size 5:
    Manipulate to get complement for arbitrary size:
    Furthermore one might consider looking at multiway graphs of combinatory expressions representing a particular function.
    Get the list of unique multiway graph structures given the list of combinatory expressions:
    Get the association of all possible multiway graph structures for a given function:

    Conclusion

    Acknowledgements

    Thanks to Peter Barendse, James Boyd, Stephen Wolfram and Nik Murzin for help, ideas and review <3

    References

    1
    .
    Stephen Wolfram (2020). Combinators: A Centennial View. Stephen Wolfram | Writings.
    ​https://writings.stephenwolfram.com/2020/12/combinators-a-centennial-view/
    2
    .
    nLab authors (2022). Combinatory logic.
    ​http://ncatlab.org/nlab/revision/combinatory%20 logic