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 <marc...@ulb.ac.be> 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 <marc...@ulb.ac.be >> <mailto:marc...@ulb.ac.be>> 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 everything-list+unsubscr...@googlegroups.com >> <mailto:everything-list+unsubscr...@googlegroups.com>. >> To post to this group, send email to everything-list@googlegroups.com >> <mailto:everything-list@googlegroups.com>. >> 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 everything-list+unsubscr...@googlegroups.com > <mailto:everything-list+unsubscr...@googlegroups.com>. > To post to this group, send email to everything-list@googlegroups.com > <mailto:everything-list@googlegroups.com>. > 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 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.
