For those who are interested in the comp hypothesis,
it is hardly a luxury to dig a little bit in computer science.
If only to go toward explicit definition of notion like computations,
computational history, consistent extensions, models, etc.
I open this thread for the very long term.
One of the jewel of computer science is the theory of combinators.
They have been discovered and presented in a talk by Moses
Schoenfinkel (from Moscow) in 1920. And rediscovered
independently by Haskell Curry (USA) in 1930. Church
rediscovered them too under the form of closed lambda _expression_,
for which he will postulate his famous "Church thesis": the closed lambda
_expression_ are enough to define all computable functions (from N to N, where
N = the set of positive integers).
There is no "Schoenfinkel thesis" nor any "Curry thesis", as
opposed to "Church thesis". Indeed the goal of both Schoenfinkel
and Curry was to "rebuild" an alternative to the whole of mathematics.
One of Schoenfinkel's motivation was to eliminate all variables.
Curry's motivation was to find the most elementary finitary operations
rich enough to (re)build mathematics, and this preferably without formal
sets, but only a finite set of primitive operations.
Actually Combinatory Logic can "easily" be shown
rich enough to represent the partial recursive function, so that
the combinators gives a nice and pleasant computer programming
language. (And indeed LISP and functionnal programming languages
are all descendants or cousins of the combinators/lambda calculus).
But at some fundamental level combinatory logic is much more than
a programming language: it is really a possible road to tackle the problem
of the nature of mathematics, and with comp: the nature of reality.
Also, combinatory logic is very fine grained, and this will enable us to
introduce at a very cheap price important nuances.
Here is a short descrition of combinatory logic (beware: in the preceding post
I made a typo error):
STATIC:
1) K is a molecule (called the "kestrel" is Smullyan's terminology)
2) S is a molecule (the "Starling")
3) if x and y are molecules then (x y) is a molecule. From this you can easily enumerate all possible molecules: K, S, (K K), (K S), (S K), (S S), ((K K) K), ((K S) K) ...
DYNAMICS: (X and Y are put for any molecules)
1) ((K X) Y) = X (Law of the Kestrel)
2) (((S X) Y) Z) = ((X Z) (Y Z)) (Law of the Starling)
1) means that on any molecules X the molecules (K X) is stable and does not evolves (except by the evolution of X perhaps). I will say that a molecules of the shape (K X) is a charged Kestrel.
Now if (K X) comes to interact with some other molecules Y giving ((K X) Y) you get an explosion leaving as result of the reaction just the molecule X.
So for example
K is stable
(K K) is stable
(K (K K)) is stable
((K K) K) is unstable, indeed it matches the law "1)", with X = K, and Y = K, so the reaction
is trigged giving K.
((K (K K)) (K K)) gives (K K), ok?
Well the price of having a conceptually very simple syntax (static) is that the notation can be very quickly a little bit cumbersome. The tradition is to neglect the left parenthesis abbreviating
(((a b) c) d) by abcd. The laws becomes:
KXY = X
SXYZ = XZ(YZ)
The examples becomes
K is stable
KK is stable
K(KK) is stable
KKK is unstable and "decays" into K, and finally
K(KK)(KK) gives (KK) ok?
What gives S(KK)(KK) ? Solution: it remains S(KK)(KK). It is stable because
S needs "three" molecules to trigger its dynamic. So S(KK)(KK)(KK) gives KK(KK)(KK(KK)), as
SKKK gives KK(KK) which is still unstable and gives K.
Exercices (Taken from the course "My First Everything Theory" Primary school Year 2127 :)
Evaluate:
(SS)KKK = ?
KKK(SS) = ?
(KK)(KK)(KK) = ?
(KKK)(KKK)(KKK) = ?
Evaluate:
K
KK
KKK
KKKK
KKKKK
KKKKKK
KKKKKKK
KKKKKKKK
KKKKKKKKK
KKKKKKKKKK
A little more advanced exercices: is there a molecule, let us called it I, having
the following dynamic: (X refers to any molecule).
IX = X
So a solution is some molecule made up from K and S which applied on any
molecule give as result of the reaction that very molecule unchanged.
For example KXS is not a solution, although it gives X, it is not of the shape (molecule X).
Of course you can learn a lot by searching "combinators" or "lambda calcul"
on the net. Two samples:
For those "who knows", here is a paper on
Kolmogorov Complexity viewed through the
combinators. It can be used as a quick introduction to combinators.
Kolmogorov Complexity in Combinatory Logic
John Tromp
http://homepages.cwi.nl/~tromp/cl/CL.pdf
And here is a much more technical paper on some advanced stuff translating
an amazing idea of Girard, the geometry of interaction (GOI) in terms
of combinator.
http://www.mathnet.or.kr/papers/Pennsy/Haghverdi/main7.pdf
(Need Category Theory).
Soon I will give the solution of the exercices. I will give you "my second everything
theory (Year 2127)". Then a third ... I let you meditate on the following "philosophical"
question "does Kestrel really exist?", doesn't Classical General Relativity entails the
existence of Kestrels? Does not a "physical" time arrow need kestrels?
Look closely: KXY = X, kestrels eliminate information, Y has been erased).
To doubt on the physical existence of kestrels leads to quasi-physicalist view of logic
(not unlike the one by *the other Schmidhuber*Strings from Logic:
http://arxiv.org/abs/hep-th/0011065 I tend to think for
now that Newton's lesson can (admittedly roughly) be sum up by saying there are no
Kestrels. And perhaps the no-cloning theorem gives us empirical reason to doubt
about the Starling too, because they clone (duplicate)
one of their argument (Einstein Podolski Rosen Bell ... Diecks Zurek Wootters lesson).
In fine combinators provide tools for building models of weak logics. Strictly speaking
abandoning the kestrel is abandoning the a priori axiom: p->(q->p). This is a step toward
quantum or toward relevance logics. But I guess I anticipate too much.
I am not hiding you that one of my motivation is to make my thesis easier. Until now
I have attempt to describe the SHORT path (the interview of the lobian machine). Now I
will give you the LONG path, including a precise sequences of formal theories.
The result is that Lobian machine should prove that if Kestrels and Starling exist then
they cannot be *observed* by Lobian machine. Feel free to make comments or
metacomments. I see this thread as an aside thread which I hope will not perturbate
more general discussions, only that with comp some computer science could be helpful.
Bruno
