Introduction
Introduction
The overall goal of this project is to explore computing with combinators and to analyze the completeness of combinatory bases.
Computing with Combinators
Computing with Combinators
Introduction
Introduction
Combinators can be thought of as higher order functions. They take in other combinators as arguments and return another combinator. The combinators S and K are a common basis that form a simple Turing-complete language.
The reduction rules for S and K combinators:
In[]:=
SKBasis= k[x_][y_]x, s[x_][y_][z_]x[z][y[z]];SKBasis//Column
Out[]=
k[x_][y_]x |
s[x_][y_][z_]x[z][y[z]] |
A program is represented by the initial state of the combinator and computation is the act of applying all reductions until nothing more can be reduced (this process does not always terminate).
The goal here is to find out how to compute interesting things using combinators.
The goal here is to find out how to compute interesting things using combinators.
Reducing Combinators
Reducing Combinators
Given a combinator and the rules for reducing the primitive combinators it is composed of, this code will continue reducing step by step until no more reductions can be done. (ReplaceAll is much more concise but unfortunately does certain steps incorrectly.)
The following replaces a single part of the combinator according to the rules.
Single combinator reduction:
In[]:=
CombinatorReplace[expr_, rules_] := Replace[expr,rules]
This finds what part of the combinator should be reduced first by trying outermost reduction first (try to reduce arguments last).
Find which part of the combinator to reduce:
In[]:=
CombinatorEvaluate[expr_, rules_] := With[{next = CombinatorReplace[expr, rules]}, next /; next =!= expr ]CombinatorEvaluate[expr: f_[g_], rules_]:= With[{next = CombinatorEvaluate[f, rules][g]}, next /; next =!= expr ]CombinatorEvaluate[expr: f_[g_], rules_]:= With[{next = f[CombinatorEvaluate[g, rules]]}, next /; next =!= expr ]CombinatorEvaluate[expr_, rules_]:=expr
This tries to apply all reductions until nothing more can be reduced in the combinator.
Fully reduce a combinator:
In[]:=
CombinatorEvaluateAll[expr_, rules_, n_: 100] := FixedPoint[(CombinatorEvaluate[#, rules])&, expr, n]CombinatorEvaluateAllSteps[expr_, rules_, n_: 100]:= Drop[ FixedPointList[CombinatorEvaluate[#, rules]&, expr, n], -1 ]
Example combinator computation with steps:
In[]:=
CombinatorEvaluateAllSteps[s[k[s]][k][s],SKBasis]//Column
Out[]=
s[k[s]][k][s] |
k[s][s][k[s]] |
s[k[s]] |
Lambda Calculus
Lambda Calculus
In order to compute interesting things with combinators, it will be necessary to build up representations of logic and lists in terms of combinators. Given how simple combinators are, this becomes very lengthy and overwhelming quite quickly. In order to avoid this, the more complicated logic will be built in lambda calculus and then converted into SK combinators.
Terms in lambda calculus are just pure anonymous functions. They work almost exactly like Function, however the terms in lambda calculus look like λx.(λy.xy)
Terms in lambda calculus are just pure anonymous functions. They work almost exactly like Function, however the terms in lambda calculus look like λx.(λy.xy)
λx.(λy.xy) represented in terms of Function:
In[]:=
Function[{x},Function[{y},x[y]]]
Out[]=
Function[{x},Function[{y},x[y]]]
I use the head Lambda instead of Function because then I can add step-by-step evaluation and other key features for properly representing lambda calculus.
Details of Lambda Calculus Implementation
Details of Lambda Calculus Implementation
Example
Example
Example of lambda calculus:
In[]:=
lambdaExample=Lambda[{x,y},y[x]][Lambda[{x},x]];LambdaEvaluateAllSteps[lambdaExample]//Column
Out[]=
Lambda[{x,y},y[x]][Lambda[{x},x]] |
Lambda[{y},y[Lambda[{x},x]]] |
Lambda To SK Combinators
Lambda To SK Combinators
The goal of using lambda calculus is representing logic and lists in it and then converting that to SK combinators because working directly with SK combinators is not reasonable. So now we need a way to convert from lambda calculus to SK combinators.
If a lambda is given whose body is another lambda, then first convert that lambda to an SK combinator and then convert that overall lambda to an SK combinator.
Convert a nested lambda to SK combinators:
In[]:=
LambdaToSK[expr: Lambda[vars_List, body_Lambda]] := LambdaToSK@Lambda[vars, LambdaToSK[body]]
This first curries the given lambda and then creates the SK combinators. If the body of the lambda has an application in it, then the S combinator is used. Otherwise either the identity or the K combinator is used.
Convert a single lambda to SK combinators:
LambdaToSK[expr_Lambda] := With[{lambda=CurryLambda[expr]}, With[{body=LambdaBody[lambda], var=First@LambdaVars[lambda]}, If[MatchQ[lambda, Lambda[_List, _Lambda]], LambdaToSK[lambda], If[Length@body 0, If[var === body, s[k][k], k[body] ], s[ LambdaToSK[Lambda[{var}, LambdaToSK[body[[0]]]]] ] [ LambdaToSK[Lambda[{var}, LambdaToSK[body[[1]]]]] ] ] ] ] ]
This tries to convert any lambdas found in the given expression to SK combinators.
Convert all parts of the given lambda term:
In[]:=
LambdaToSK[expr: f_[g_]] := LambdaToSK[f][LambdaToSK[g]]LambdaToSK[expr_] := expr
Example of LambdaToSK:
In[]:=
lambdaExample=Lambda[{x,y},y[x]][Lambda[{x},x]];LambdaToSK[lambdaExample]
Out[]=
s[s[k[s]][s[s[k[s]][k[k]]][k[k]]]][s[k[k]][s[k][k]]][s[k][k]]
Church Encoding
Church Encoding
Church encoding is a specific way of representing data and operations in lambda calculus. The choice of how things should be represented in terms of lambda calculus does not matter so long as it can function and be used to represent what is intended.
Encoding for basic logic:
In[]:=
true = Lambda[{x,y}, x];false = Lambda[{x,y}, y];if = Lambda[{p,c,a}, p[c][a]];and = Lambda[{x,y}, if[x][y][false]];or = Lambda[{x,y}, if[x][true][y]];
Lists are implemented as cons lists.
This means that the list {a, b, c} is built as a binary tree: Cons[a, Cons[b, Cons[c, null]]]
Car gives the left child of the cons tree and cdr gives the right child of the cons tree.
This means that the list {a, b, c} is built as a binary tree: Cons[a, Cons[b, Cons[c, null]]]
Car gives the left child of the cons tree and cdr gives the right child of the cons tree.
Encoding for lists:
This encodes numbers by using the idea of the starting with zero and applying a successor function. The number of times the successor function is applied is what the number is. This implementation is slightly different to that usual method because the successor function is not actually what is being nested, but instead a variable. The successor function just further nests that variable.
Encoding for numbers (Church numerals):
Factorial Function
Factorial Function
Now that we have the tools to more easily work with combinators, we can build a combinator that will compute factorials for us.
What does it mean for an SK combinator to compute the factorial of a number?
It means we have some initial combinator made up of S and K combinators that when fully reduced terminates with a combinator the is the representation of the resulting number.
In order to implement the factorial function recursively, we need to create recursion with the Y combinator. The Y combinator applies its given argument to itself infinitely many times. This allows for recursion because it means the function has itself provided as an argument.
In this case three factorial is being computed.
In lambda calculus that is represented by nesting a function six times as can be seen in the output.
The equivalent SK combinator representation is shown, although the nesting is less clear.
What does it mean for an SK combinator to compute the factorial of a number?
It means we have some initial combinator made up of S and K combinators that when fully reduced terminates with a combinator the is the representation of the resulting number.
In order to implement the factorial function recursively, we need to create recursion with the Y combinator. The Y combinator applies its given argument to itself infinitely many times. This allows for recursion because it means the function has itself provided as an argument.
In this case three factorial is being computed.
In lambda calculus that is represented by nesting a function six times as can be seen in the output.
The equivalent SK combinator representation is shown, although the nesting is less clear.
Y Combinator:
Factorial function:
The lambda evaluation of three factorial:
The output of the lambda interpreted as number:
The SK combinator version of the lambda:
I would show the actual unreduced combinator that represents the 3 factorial here, but unfortunately it is 8 MB of text.
Two Tag System Simulation
Two Tag System Simulation
SK combinators are Turing-complete which means that they can simulate any other Turing machine. In order to see this power in action, we can make a combinator that simulates any 2-tag system (the set of 2-tag systems is Turing-complete).
Two Tag System
Two Tag System
A two tag system starts with a list of symbols (one of them is designated the halting symbol) and a set of rules that each take one symbol and give back a list of symbols. The two tag system looks at the first symbol in the list, appends the resulting symbols from the associated rule to the end of the list, and finally deletes the first two elements of the list (the symbol currently being looked at and the symbol immediately following). This process repeats until the halting symbol appears as the first in the list.
Here I implemented a program for running any two tag system so that I could verify the results of the simulation. Both the simulation and this implementation use digits for symbols and the digit 0 as the halting symbol because I can only encode numbers.
Here I implemented a program for running any two tag system so that I could verify the results of the simulation. Both the simulation and this implementation use digits for symbols and the digit 0 as the halting symbol because I can only encode numbers.
Two Tag System:
Simulation of Two Tag System
Simulation of Two Tag System
The following simulates any two tag system using lambda calculus and thus using SK combinators.
This tries applying each rule until one that works is found.
Try two tag system rules:
The following continues trying to apply rules until the halt symbol (zero) is hit.
Simulate the Two Tag System:
The following is an example comparing the result of the actual two tag system to the simulated two tag system.
The actual two tag system:
The simulated two tag system:
Analyzing Combinatory Bases
Analyzing Combinatory Bases
A combinatory basis is the set of primitive combinators used to build other combinators. So far we have seen S and K as the basis because it is simple and is Turing-complete.
The goal here is to create a function that classifies a given basis as being complete or incomplete. A complete basis can recreate all other combinators and is Turing-complete. An incomplete basis will not be able to do this.
The goal here is to create a function that classifies a given basis as being complete or incomplete. A complete basis can recreate all other combinators and is Turing-complete. An incomplete basis will not be able to do this.
Combinator Equality
Combinator Equality
In order to better analyze combinatory bases, it will be necessary to know if two given combinators are equivalent. Here I am looking at what is called extensional weak equality. This means that if two combinators reduce to the same thing when given their arguments, they are considered equal. I use this form of equality because what matters when trying to find out if combinatory bases are equivalent is knowing what they can do to their arguments, not their specific implementation.
Example
Example
Example of combinator equality:
Enumerating Combinators
Enumerating Combinators
In order to see if a basis is complete, it is sufficient to check if it can recreate the S and K combinators. I am using a brute force approach to convert which requires enumerating all combinators.
All Possible Brackets
All Possible Brackets
First I enumerate all possible ways of creating brackets of a given length and then I have a function that takes a combinator and returns a list containing all the possible brackets put on this combinator.
Enumerating all possible brackets:
Example of All Possible Brackets:
Adds all possible brackets to a combinator:
Example of adding brackets:
Removes anything is not a bracket:
This is used later to check if a combinator has nested terms.
Example of removing non-brackets:
Enumerating All Combinators
Enumerating All Combinators
I enumerate all combinators without any brackets and then I add in all the possible brackets for each combinator.
Generate all combinators without brackets:
Example of no bracket combinators:
Enumerate all combinators:
Example of enumerating all combinators:
Conclusion
Conclusion
For computing with combinators, I created a framework for creating programs for SK combinators. First the program is written at a higher level using the Church encoding. Then the program can be converted directly to SK combinators or first reduced at the lambda calculus level and then converted to SK combinators.
For analyzing combinatory bases, I created a function that attempts to find out whether or not a combinatory basis is complete. It first tries to use experimentally found rules to check if a given basis is able to create combinators of all necessary classes. It then tries to create an equivalent combinator in the given basis for both the S and K combinators.
For analyzing combinatory bases, I created a function that attempts to find out whether or not a combinatory basis is complete. It first tries to use experimentally found rules to check if a given basis is able to create combinators of all necessary classes. It then tries to create an equivalent combinator in the given basis for both the S and K combinators.
Further Work
Further Work
Much of the code in computing combinators is not very efficient. It works for reasonably sized combinators, but combinators that compute interesting things are rarely reasonably sized.
It would also be much better if what classes could be built from other classes was proven and not found experimentally as I could be missing combinations that never came up randomly.
It would also be much better if what classes could be built from other classes was proven and not found experimentally as I could be missing combinations that never came up randomly.
Keywords
Keywords
◼
Combinators
◼
Combinatory basis