Hi, The next combinator thread (“combinator 6”) will be the proof of the (Turing/Church) universality.
Here, I correct the typo error, which was that I forgot the predecessor P in the last formula. See below. It is time to revise, and to ask any question if anything remains unclear. After the Turing universality, I will give the definition of the first and third person “pronouns”, and go toward the notion of Löbian combinator or Löbian number, and explain the Curry-Löb paradox. That will be the thread Combinator 7. The main results will be the first and second recursion theorems (or fixed-pint theorem): 1) For any combinator F there is a combinator X such that FX = X. 2) For any combinator F there is a combinator X such that F’X' = X. ‘X’ will be a Gödel numbering, or code, of the combinator X. Bruno > On 16 Sep 2018, at 12:05, Bruno Marchal <[email protected]> wrote: > > Hi, > > We will implement the numbers with the combinators. In particular we will > emulate Robinson Arithmetic(*) with the combinators. > > Robinson arithmetic is classical logic + > > 1) 0 ≠ s(x) 0 is not a successor of any number x > 2) s(x) = s(y) -> x = y Different numbers have different > successors > 3) x = 0 v Ey(x = s(y)) Each number has a predecessor > 4) x+0 = x Adding nothing keep a number invariant > 5) x+s(y) = s(x+y) Recursion equation of addition > 6) x*0=0 Multiplying by 0 gives 0 > 7) x*s(y)=(x*y)+x Recursion equation of multiplication > > On the right I have put the intended intuitive semantic. > > Usually I use the "Church numerals”, but I will use those of Barendrecht. > Smullyan’s book convinced me of their elegance, and it gives a nice > opportunity to use our new recursion tools, as they strikes the eyes in line > “5)” and “7)”. Isn’t it? “+” is defined from itself. “*” also. > > > Barendrecht's Numerals > > Definitions. > > The number 0 is defined by I, that is SKK, but I will abbreviate it by I. > The successeur function is defined by the combinator Vf. V is the Vireo, > Vxyz = zxy. f is KI. We have seen that V = BTC (and that B = S(KS)K, …). I > mean V is a combinator (a combination of K and S), and it does what it does > (that circular permutation of its argument). Reread previous post if > necessary. > > f is the “logical” abbreviation for false, that is KI, i.e. K(SKK), as > defined in the logical interlude. > > Does it work? > > We have that > > 0 = I > 1 = VfI which remains stable, as V has not enough of its > “arguments”. > 2 = Vf(VfI) idem > 3) = Vf(Vf(VfI) It looks everything is fine and (by induction) will > remain fine. > Etc. > > So a number n, which is defined by s(s(s(s(…(0))…), with n “s“ in, or by, > Robinson Arithmetic is defined, or represented by > > Vf(Vf(Vf(Vf( …(I))…) with n “Vf”. > > It will be handy to have a predecessor. > You might try to find one by yourself before reading what follows, but there > is no obligation. What is obligatory is to verify that it works. Barendrecht > proposes Tf. (Where T is the “trush”: Txy = yx). > > OK, but does it works? We need to verify this. So let us try it on 0, just to > see! > > TfI = If = f. > > Well, that is OK. All we need is that it does not give some number, and > giving f is not so bad, almost an “error message” :) > > I will abbreviate Vf(Vf(Vf(Vf( …(I))…) by n (hoping the underline will not > disappear). > > We have tested the predecessor Tf on 0, now we must test it on some > successor, that is some Vfn > > Tf(Vfn) > Vfnf (Vfn)f for the beginners > ffn f is KI, KIxy = y, revise the preceding posts if needed) > n > > It works! > > Now, to implement “x + y” we need an ability to distinguish between a null > and a non null number, to decide between using axiom “4)” or “5)”. > > So we need a combinator Z which answer truth, i.e t, that is K, when given 0, > that is I, and gives KI when given a non null n. > > We want Z0 = ZI = K, and Zn = KI in case n is different from 0. > > Barendregt's solution: Z = Tt. > > We have already met Tt. It played the role of the “OR” in logic, and works > very well also to test if a number is null or not: > > TtI = It = t > Tt(Vfn) = Vfnt = tfn = f. > > Let me sum up: > > t = K > f = KI > > 0 = I > s = Vf (successor) > p = Tf (predecessor) > > Z = testing “nullness” = Tt. > > And I recall that, thanks to t = K and f = KI, we have that > > if A then B else C > > becomes simply ABC, as tBC = B, and fBC = C. > > =================== > > ADDITION > > > Now, we have all we need to program addition. > > Addition is defined by its recursive equation (cf above) > > 4) x+0 = x Adding nothing keep a number invariant > 5) x+s(y) = s(x+y) Recursion equation of addition > > I replace “5)" by > > 5’) x+y = s(x + (py)) > > which is more suitable here. > > So a (recursive) program, for adding x + y, could be > > If y = 0 then output x else output s applied to the addition of x and py. > > I will use “a" for the combinator doing the addition. It is the one we are > searching. > > axy = if (Zy) then x else (Vf(ax(py))) > > And thus (cf: if A then B else C = ABC. I wrote (Zy)x = Zyx, as always. > > axy = Zyx(Vf(ax(py))) > > Do you see this? You should read it: If Zy then x else Vf(ax(py)). > > Of course, we need to solve the recursion. You might need to revise the post > on Recursion (Combinator 4). > > 1) renaming of the variables: > > azy = Zzy(Vf(ay(pz))) > > 2) There is a combinator A such that (a is replaced by x) > > Axyz = Zzy(Vf(xyz)) Typo error. Read instead Axyz = Zzy(Vf(xy(pz))) > > Indeed A = [x][y][z]Zzy(Vf(xyz)) Same here: A = = [x][y][z]Zzy(Vf(xy(pz))) > > Then, the adding combinator a is just the fixed point of A: > > a = YA = Y[x][y][z]Zzy(Vf(xyz)) Same here: a = = YA = Y[x][y][z]Zzy(Vf(xy(pz))) > > Done. > > We know that the paradoxical combinator does well its job, so let us test the > recursion directly, on 2+2=4, say: > > a 2 2 = a(Vf(VfI))(Vf(VfI) > = Z(Vf(VfI))(Vf(VfI))(Vf (a (Vf(VfI)) (p (Vf(VfI)))) > = Z(Vf(VfI))(Vf(VfI))(Vf (a (Vf(VfI)) (VfI))) > = Vf(a (Vf(VfI)) (VFI)) as Vf(VfI) is not null. > = Vf(Z(VfI) (Vf(VfI)) (Vf(a (Vf(VfI)) (p (VfI))) > = Vf(Z(VfI) (Vf(VfI)) (Vf(a (Vf(VfI)) I)) > = Vf(Vf (a (Vf(VfI))I) > = Vf(Vf(ZI(Vf(VfI))(a <whatever>) “whatever is not needed, as ZI = t. > = Vf(Vf(Vf(VfI))) > = 4 > > It works well! > > Exercise: > > Find combinators doing the following task: > > Multiplication > Exponentiation > Parity testing (is a number even or odd) > Test of which number is is greatest. > > Solution is the next post. > > Later, in combinator 6, we will prove the Turing universality of the > SK-combinator. What is still lacking is the MU operator, allowing the > unbounded search on numbers verifying some decidable property. I will revisit > and re-explain the definition of Turing universality before proving it (of > course). > > Time to revise all the posts, as the material accumulates. I hope that those > who have read the posts see how all this is very simple (compared to the > mathematics needed for quantum mechanics, for example). If you find anything > difficult here might mean you have not grasped the notation. Yesterday, some > student of mine showed that they have still difficulties to decompose a > combinator in two. In a test, they saw SI(xx) as S on I(xx), where SI(xx) is > (SI)(xx), that is SI applied on xx. Eventually, add the left parentheses if > needed, then suppress them as it will become unreadable if not. > > Good Sunday! > > Bruno > > > > > > > > > > > > > > > > > >> On 10 Sep 2018, at 19:08, Bruno Marchal <[email protected] >> <mailto:[email protected]>> wrote: >> >> Hi, >> >> >> All right, now the almost last fundamental result before showing the Turing >> Universality of the SK-combinators (or simply combinators). >> >> (Except for an important but easy arithmetical interlude). >> >> We have solved the following problem: to find a combinator A, i.e. a >> combination of S and K, such that, in virtue of the two laws (Kxy =x, Sxyz = >> xz(yz)), we have: >> >> Axyz = xy(yxz) (or any other combinations). >> >> Indeed A is given by the ABF algorithm (or the others): >> >> A = [x] [y] [z] xy(yxz). >> >> The new problem of the day is, ‘---can you find a combinator A such that >> >> Ax = x(Ax), >> >> or >> >> Axy = xAy(yA), >> >> or similar? >> >> You see the difficulty? The unknown combinator A appears at both sides of >> the equation. It is not clear at first sight if such a combinator A can even >> exist. >> Such an equation is called a recursion equation. A is somehow defined in >> term of itself. >> >> The fundamental result explained here is that the solution to the recursion >> equation always exists! >> >> So can we find it? I will again prove that such equations have always a >> solution by providing an algorithm which gives the solution (and proving >> that the algorithm is correct). >> >> You will recognise a variant of the little song-question that I have used >> many times: “If Dx gives xx, what gives DD?”, which also appeared when we >> defined the Mocking Bird M (Mx gives xx). And we know the trouble when we >> apply M to itself, which is that MM gives a combinator without normal form, >> or unstable. The two laws keep being triggered and MM does not halt on some >> normal or stable combinator. >> >> So, we might expect that the solution of the recursion equation have not >> necessarily a normal form (i.e. are stable). But that can be OK, given that >> our goal consists in implementing the computations, including the infinite >> computations (the processes) and what is an infinite computation but an >> unstable combinators? >> >> >> In Smullyan's book (How to Mock a Mocking Bird?) Smullyan is very quick on >> this, and he is right, because it is simpler that way. He made his hero, >> Craig, particularly “alert” that day, and Craig found very quickly two ways >> to solve the problem. One using a “sage bird”, and one “from scratch”. >> >> The “sage birds” are known in the old literature as the “paradoxical >> combinators”, and are known in the modern literature as the “fixed point >> combinators”. >> >> I have not talked much about them, and so I will give the method “from >> scratch” first. Then I will use it to define the sage, paradoxical, birds, >> and the relation with the fixed points theorems, and give the first method, >> which will be more efficacious and provide shorter solutions. >> >> Instead of reasoning on arbitrary combinations, let us reason with the >> particular exercise above: to find A such that >> >> Axy = xAy(yA). >> >> I will first rename the variable x -> y, and y -> z. The reason for this is >> that I want x playing some role related to A. >> >> >> Ayz = yAz(zA). (This change nothing of course. OK?) >> >> Then I replace A by x. And we know that there is a combinator A’, such that >> >> A’xyz = yxz(zx). (Which is the right hand side above with A replaced by x). >> >> A’ has one more variable than A, and A, being replaced by x in the right >> hans side has become into an argument. >> >> We know that such combinator A’ exist, because we can eliminate the variable: >> >> A’ = [x][y][z]yxz(zx). >> >> Then we give A’ to as sage bird, and that gives the (first) solution! >> >> But wait! We don’t have yet studied the sage bird yet! >> >> So, in the method from scratch, instead of A’, we use A’’, which is exactly >> like A’ except that it duplicates the variable x: >> >> A’’xyz = y(xx)z(z(xx)) >> >> Of course A’’ exists too: >> >> A’’ = [x][y][z]y(xx)z(z(xx)). >> >> You can, or not, compute this at your time and convenience (if you are >> masochist), but you need only to understand that this expression defined >> some precise combinator (with extensional identity, that is up to >> syntactical differences). >> >> Now, apply A’’ on itself, taken as first argument: you get >> >> A’’A’’yz = y(A’’A'')z(z(A’’A'’)) >> >> And that solves the problem! The solution is A’’A’’, as you can see. >> With A = A’’A’', we do have Ayz : yAz(zA), or, changing the variable again: >> Axy = xAy(yA), like we wanted. >> >> Now the task of eliminating z, y and x in y(xx)z(z(xx)) is tedious. I will >> not illustrate it. >> >> >> So let us search a better solution, and for this we need to use Smullyan’s >> Sage Birds, or Curry's paradoxical combinators. >> >> >> Definition. A combinator X is a fixed point of a combinator F if FX = X. >> (Smullyan says that F is fond of X). >> >> Crazily enough all combinators have a fixed point. A student thought, at >> first, that if that is true, a combinator should not be able to mimic a >> translation in the plane (say), as a translation is a typical transformation >> having no fixed point, unlike a rotation. But of course that does not >> follow. If a combinator mimic a translation in the plane, his fixed point >> will just denote an element which is not representing an element of the >> plane. >> >> How is that possible? By the result above we know that >> >> Ax = x(Ax) >> >> admits a solution. We will need it, and thus will derive it with the method >> “from scratch”. But having that solution A, we can see now that for any F >> >> AF = F(AF) >> >> that is, >> >> F(AF) = AF. >> >> So AF is the fixed point of F, and we see that A is a combinator which gives >> us, for any combinator F, its fixed point AF. >> A is called a paradoxical combinator, or the fixed point combinator, or a >> sage bird! >> >> OK? >> >> So let us derive some precise paradoxical combinators, and search with them >> some combinator fixed point. >> >> The paradoxical combinator(s) is very often named Y, (Smullyan uses the >> majuscule greek Theta), and is defined by its recursion equation: >> >> Yx = x(Yx). >> >> I hope you directly see that x(Yx) = Yx, so that Yx is a fixed point of x. >> >> Let us solve the recursion equation Yx = x(Yx) with the method from scratch. >> >> 1) renaming of the variable Yy = y(Yy) >> 2) Y (the unknown) is replaced by xx at the right: y(xxy), and that gives >> our A’’, which happens to be a celebrity: U, a combinator discovered by >> Turing: >> >> Uxy = y(xxy) >> >> Let us find it. >> >> U = [x][y] y(xxy) >> = [x] [y]y(xxy) >> = [x] (S [y]y [y]xxy) (by rule “F)”) >> = [x] (SIxx) (by rule “A)" and rule “C)”) >> = (S [x]SI [x]xx) >> = (S (K(SI)) M) >> >> Verification: >> Uxy = S(K(SI))Mxy >> = K(SI)x(Mx)y (Law 2) >> = SI(Mx)y (Law 1) >> = Iy(Mxy) (Law 2) >> =y(xxy) OK. >> >> SI is Smullyan’s Owl, Oxy = SIxy = Iy(xy) = y(xy), so U can be written >> S(KO)M. >> O = SI = S(SKK). >> >> You would find U = BOM when using the ABCDEF algorithm. >> Let us verify BOMxy = O(Mx)y (B is the blue bird (Bxyz = x(yz)))) >> = O(xx)y = y(xxy). >> >> So Y = A’’A’’ = UU = BOM(BOM) = S(KO)M(S(KO)M). >> >> But note that we could have find it also by using the Lark L (Lxy = x(yy)). >> LOxy = O(xx)y = y(xxy). >> >> So U = (also) LO, and Y = LO(LO). Not to be confused with the TV series >> “Hello Hello” (grin). >> >> Another simple fixed point combinator is provided by SLL. Indeed SLLx >> = Lx(Lx), and I let you show that this is always a fixed point of x. >> >> Now, to find a fixed point of a combinator F, we just need to apply Y on F. >> YF is a fixed point of F. >> >> Now, let me explain the first method to solve the recursion axiom, with the >> example above. We were searching A such that Axy = xAy(yA). >> >> 1) we rename the variable: >> Ayz = yAz(zA) >> 2) we substitute A by x, and consider the corresponding combinator A’ >> A’xyz = yxz(zx) >> 3) the solution is given by YA’. Indeed YA’ = B such that A’B = B (A’ is >> fond of B, B is fixed point of A’), so, let us replace x by B just above (B >> is just a metavariable here, not the blue bird): >> >> A’Bxyz = yBz(zB) >> >> But A’B = B, so >> >> A’Bxyz = Bxyz = yBz(zB). And we see that B, the fixed point of A’, is the >> solution of the recursion equation. >> >> ============== examples/exercices ========== >> >> Exercise 1: find a bird A such that Ax = A >> >> So A should be a combinator such that A applied on any bird gives itself (I >> will use “bird” as a shorter name for combinator). >> >> Solution: >> 1) variable renaming: Ay = A >> 2) A’xy =x >> 3) A’ = [x][y]x = K >> 4) so A = YK = BOM(BOM)K >> >> Verification BOM(BOM)Kx = O(M(BOM))Kx, I recall that Oxy = y(xy), so that >> gives >> K(M(BOM)K)x = M(BOM)K = BOM(BOM)K. It works. >> >> Of course, here I have used the fact that Mx = xx. >> >> A shorter and simpler verification is by using similarly directly Y, defined >> by its recursion equation Yx = x(Yx): >> >> YKx = (YK)x = K(YK)x = YK. YK applied on any x gives YK. >> >> >> Exercice 2: find a bird A such that >> >> Ax = xA >> >> (A applied on any x gives x applied to itself). >> >> Solution: >> 1) variable renaming Ay = yA >> 2) A’xy =yx >> 3) A’ = T (the trush T which is the elementary permuter Txy = yx) >> 4) Thus A = YT >> >> Verification YTx = T(YT)x = x(YT). It works! >> >> Exercise 3: Find A, and/or verify the solution >> >> Ax = Ayx (sol: A = YC) >> Ax = Axx (sol: A = YW) >> Ax = A(xx) (sol: A = YL) >> Ax = AA (sol: A = Y(SBK)) >> >> ===== >> What if we search now the solution of Ax = x(Ax) with the first method, that >> is what gives the first method for the paradoxical bird? >> >> 1) renaming: Ay = y(Ay) >> 2) A’xy = y(xy) >> 3) so A’ is the owl O, and so >> 4) A = YA’ = YO. >> >> We see that if Y is a paradoxical bird, then Y applied to an owl O is again >> a paradoxical combinator. We can also see that all fixed point A of O is a >> paradoxical combinator: if OA = A, then Ax = OAx = x(Ax). So, a sage bird, >> alias a paradoxical or fixed point combinator can also be defined by being a >> fixed point of the combinator O. Note the resemblance between O and U >> >> Oxy = y(xy) >> Uxy = y(xxy). >> >> Here is a small gallery of paradoxical birds: >> >> LO(LO) >> UU >> BOM(BOM) >> SLL >> BML >> BM(BWM) >> BM(RMB) >> BM(CBM) >> >> A famous one is the original one by Curry: >> >> WS(BWB). >> >> It is, I think, the first one. It’s Curry’s Paradoxical Combinator. >> >> OK? Please work all this out by hands, pen and papers. Be sure nothing >> remains unclear, as now, we have all the pieces of the puzzle to prove that >> the SK theory is Turing complete, or said differently, that the combinators >> provides a Universal Machinery. >> >> The only things which are still missing to show this are … the Numbers. >> >> So the next chapter is simply arithmetic, seen through the combinators, like >> we have already seen how to implement elementary logic, entirely with the >> fact that if we use K for true and KI for false, the combinator ABC >> implements if "A then B else C”. >> >> A last thing, why “paradoxical”? You can imagine that the fact that all >> recursion equations have solutions will make the combinators very powerful, >> and indeed so much powerful that its mathematics can lead to contradiction >> and paradoxes very easily. Church ’s initial theory, and Curry's one where >> shown inconsistent, by Kleene and Rosser, and attempts in that direction are >> very rich, leads rather quickly to category theory and many interesting >> things, but out of the direct scope of machine theology. I might say a bit >> more if the opportunity happens to give the Curry-Löb’s paradox, very close >> to the usual “proof" of the existence of Santa Klaus. >> There are many subject which I don’t talk about, like the semantics of >> combinator theories (Scott Models), or the ultra large field of typed >> combinators. Combinators are so powerful that sometimes the computer >> scientist, wanting to keep a bit of control, types the combinators, and >> suddenly not all combinators can be applied to any combinators, the variable >> are declared, and things get secure. The price is the loss of Turing >> universality, but that is necessary when solving complex particular >> problems. Not all man made universal machine are as lucky as Curiosity and >> Opportunity, to walk around freely on Mars and take some initiative ... >> >> 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 [email protected] >> <mailto:[email protected]>. >> To post to this group, send email to [email protected] >> <mailto:[email protected]>. >> Visit this group at https://groups.google.com/group/everything-list >> <https://groups.google.com/group/everything-list>. >> For more options, visit https://groups.google.com/d/optout >> <https://groups.google.com/d/optout>. > > > -- > 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 [email protected] > <mailto:[email protected]>. > To post to this group, send email to [email protected] > <mailto:[email protected]>. > Visit this group at https://groups.google.com/group/everything-list > <https://groups.google.com/group/everything-list>. > For more options, visit https://groups.google.com/d/optout > <https://groups.google.com/d/optout>. -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
