A Simple SK Combinator Calculus Tutorial in Qi
As a juxtaposition of my previous use of the Qi type checker to define the SK combinator calculus, I'll now define it very simply in the Qi language directly. I'll present this as a tutorial to those new to the SK combinator calculus.
The SK calculus shows us that at maximum there are only three rules of logic: Pattern Matching, Deleting, and Copying. It also shows that their is only one way of evaluating them, namely by application. You can think of the three rules as "Highlighting", "Cutting", and "Pasting." With those three simple operations, the entirety of logic and mathematics can be reproduced with only your mouse!
Let us take a loot at deletion... We'll call the operation K. Look at the following transformation. Copy the [[kx]y] into a text editor. Now highlight and "cut" all but the x using only the "cut" command and your mouse.
[[kx]y] -> x
Now, we'll make a new function S which stands for "paste". Try to make the following transformation of [[[sx]y]z] in a text editor. Remember you can only use "cut" and "paste".
[[[sx]y]z] -> [[xz][yz]]K deletes information and S copies things and applies it to other functions.
Now it should be very easy to understand what the first two lines of following code is doing.
(define sk-eval*The last 2 lines simply tell the function to evaluate the inside of our 2 element lists and return anything it doesn't know how to handle.
[[k X] Y] -> X
[[[s F] G] X] -> [[F X] [G X]]
[ X Y] -> [(sk-eval X) (sk-eval Y)]
X -> X)
But you should notice that we have defined sk-eval* but not sk-eval, so we are not quite done yet. What do we mean by evaluation? We should mean that every element has been reduced and modified until we get the same thing back out of our evaluation function as we put into it. In math, an x for a function f with the properties f(x)=x is known as a fixed point. It simply means that we get the same input as output. You should notice that "X -> X" in the sk-eval* function (especially being last), makes this a case where we get to use the fix built-in function in Qi. It keeps applying the function to itself until it reaches a fixpoint. Then it stops.
(define sk-eval
X -> (fix sk-eval* X))
That's it! That's all it takes to complete the evaluator. In our cut and paste metaphor, we would continue to make the required copy and pastes until we could no longer match s and k's with the rules defined above.
Now let us see it in action.
(36-) (sk-eval [[[s k] k] a])
a
(37-) (sk-eval [[[s [[s k] k]] [[s k] k]] a])
[a a]
That's pretty easy. Now let us define some helper functions and show that this sk-eval function knows math.
(define sk -> [s k])
(define kk -> [k k])
(define ks -> [k s])
(define z -> (sk))
(define succ -> [ s [ [ s (ks)] k]])
(define plus -> [ [ s (ks)] [ [ s [ k [ s [ k s]]]]
[ s (kk)]]])
(define mult -> [ [ s (ks)] k])
(define one -> [ (succ) (z)])
(define two -> [ (succ) (one)])
(define three -> [ (succ) (two)])
(define four -> [ (succ) (three)] )
(define five -> [ (succ) (four)] )
And now it is time for it to do some math. We will use 1 and 0 to as markers for our functional application to ensure that our evaluator will output a string of the answer in 1's but ended by a 0.
(40-) (sk-eval [[[[(plus) (one)] (two)] 1] 0])You could easily host an named SK calculus with the addition of 2 lines of code. I'll leave that as an exercise to the reader.
[1 [1 [1 0]]]
(41-) (sk-eval [[[[(mult) (three)] (two)] 1] 0])
[1 [1 [1 [1 [1 [1 0]]]]]]
That's all there is to the SK Combinator Calculus. It is a powerful enough system to define the entirety of mathematics and computation. It shows that all you need is a basic way to match symbols, delete symbols, and copy symbols and you have a Turing Complete system. (I know some squishy bio-computers that do this all the time and perhaps I'll explore that idea in another post.) From this very basic system, you get the entirety of reasoned knowledge. The universe is a strange place indeed.
I hope this helped spread understanding about the SK combinator calculus. Let me know of any questions you have!
0 Comments:
