Hi Jason, people,

I will send my post on the Church-Turing thesis and incompleteness later. It is 
too long.

So, let us proceed with the combinators.

Two seconds of historical motivation. During the crisis in set theory, Moses 
Schoenfinkel publishes, in 1924, an attempt to found mathematics on only 
functions. But he did not consider the functions as defined by their behaviour 
(or input-output) but more as rules to follow.

He considered also only functions of one variable, and wrote (f x) instead of 
the usual f(x).

The idea is that a binary function like (x + y) when given the input 4, say, 
and other inputs, will just remains patient, instead of insulting the user, and 
so to compute 4+5 you just give 5 (+ 4), that is you compute
 ((+ 4) 5). (+ 4) will be an object computing the function 4 + x. 


The composition of f and g on x is thus written  (f (g x)), and a combinator 
should be some function B able on f, g and x to give (f (g x)).

Bfgx = f(gx), for example. 

When I said that Shoenfinkel considered only functions, I meant it literally, 
and he accepts that a function applies to any other functions, so (f f) is 
permitted. Here (f f) is f applied to itself.

A first question was about the existence of a finite set of combinators capable 
of giving all possible combinators, noting that a combinators combine. 
Shoenfinkel will find that it is the case, and provide the S and K combinators, 
for this. I will prove this later.

A second question will be, can the SK-combinators compute all partial 
computable functions from N to N, and thus all total computable functions?  The 
answer is yes. That has been proved by Curry, I think.

OK? (Infinitely more could be said here, but let us give the mathematical 
definition of the SK-combinators:

K is a combinator. 
S is a combinator.
If x and y are combinator, then (x y) is a combinator.

That is, is combinator is S, or K or a combination of S and K.

So, the syntaxe is very easy, although there will be some problem with the 
parentheses which will justified a convention/simplifcation.

Example of combinators.

Well, K and S, and their combinations, (K K), (K S), (S K), (S S), and the (K ( 
K K)) and ((K K) K), and (K (K S)) and …… (((S (K S)) K) etc.

I directly introduce an abbreviation to avoid too many parentheses. As all 
combinator is a function with one argument, I suppress *all* parentheses 
starting from the left:
The enumeration above is then:  K, S, KK, KS, SK, K(KK), KKK, K(SK) and … 
S(KS)K ...

So aaa(bbb) will be an abbreviation for (  ((a a) a) ((b b) b) ). It means a 
applied on a, the result is applied on a, and that results is applied on  .. 
well the same with b (a and b being some combinators).



OK?

Of course, they obeys some axioms, without which it would be hard to believe 
they could be
1) combinatorial complete (theorem 1)
2) Turing complete (theorem 2)

What are the axioms?

I write them with the abbreviation (and without, a last time!)

Kxy = x
Sxyz = xz(yz)

That is all.

A natural fist exercise consists in finding an identity combinator. That is a 
combinator I such that Ix = x.

Well, only Kxy can give x, and Kxy does not seem to match xz(yz), so as to 
apply axiom 2, does it? Yes, it does with y matching (Kx), or (Sx). (Sometime 
we add again some left parenthesis to better see the match. 

So, x = Kxy = Kx(Kx) = SKKx, and we are done! I = SKK

Vérification (we would not have sent Curiosity on Mars, without testing the 
software, OK? Same with the combinators. Let us test SKK on say (KK), that 
gives SKK(KK) which gives by axiom 2 K(KK)(K(KK)) which gives (KK) = KK, done!

Note that SKK(KK) is a non stable combinators. It is called a redex. It is 
triggered by the axiom 2. The same for KKK, which gives K. A combinators which 
remains stable, and contains no redex, is said to be in normal form.  As you 
can guess, the price of Turing universality is that some combinators will have 
no normal form, and begin infinite computatutions. A computation, here, is a 
sequence of applications of the two axioms above. It can be proved that if a 
combinators has a normal form exist, all computations with evaluation staring 
from the left will find it.

I will tomorrow, or Monday, show that there is a combinator M such that Mx = 
xx, a combinators T such that Thy = yx, a combinator L such that Lxy = x(yy), … 
and others, Later, I will prove theorem 1 by providing an algorithm to build a 
combinator down any given combinations.That will prove the combinatorial 
completeness. Then I will prove that all recursive relation admits a solution, 
i.e. you can always find a combinator A such that Axyzt = x(Atzz)(yA), say. 
Then I will show how easy we can implement the control structure IF A then B 
else C, and follow Barendregt and Smullyan in using this to define the logical 
connectives with combinators, then I will provides some definition of the 
natural numbers, and define addition, multiplication, all primitive recursive 
function, and then the MU operator, which is the while and which will make easy 
to get Turing universality.

I let you digest all this. You can try to Sind some combinators, or to apply 
some random combinators to sequence of variable.

A (difficult) question: would you say that SK = KI? That are different 
combinators in normal form, but SKx remains normal, where KIx is trigged 
immediately and give I. Yet, SKx computes the same function as I, (verify) so? 
I will say that they are indeed equal, but this illustrates some other, less 
extensional, and more intensional, definition of equality.

By being Turing universal, the combinators give a complete universal 
programming language. We will meet its cousin, the lambda terms, and some 
descendants, like LISP.

I have not allowed Smullyan, and I have given what he called “The secret” (the 
combinatorial completeness of S and K). I hope I have not spoiled too much your 
reading of “To Mock a Mocking Bird”. The mocking bird is the bird M such that 
Mx = xx. Can you find it? Hint: xx = Ix(Ix) which match axiom 2. We can of 
course use combinators already defined, but it just abbreviates the normal 
expression SKK,

Other very difficult exercice, can the physical reality truly implement K? 
(Hint Hawking).

Anyone can ask any question.


Bruno

 




-- 
You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.

Reply via email to