Thanks Bruno! Following so far with not problems. On 5 September 2018 at 19:41, Bruno Marchal <[email protected]> wrote: > Hi Jason, Telmo, Brent, others, > > Some of you might say “OK, combinators combine, and now we know that the > combination of S and K, that is, the combinators, can do all combination”. > The last post did prove the so-called combinatorial completeness. > > But that might still seem far from Turing universality. > > The post of today will make a simple step in that direction. > > I propose to implement elementary logic with the combinators. I expose a > solution due to Barendrecht, which is extraordinarily elegant. It is also > the one used by Smullyan in “To Mock a Mocking Bird”. > > I will first implement the control structure: > > if A then B else C > > As you can guess this is a pretty important step toward Turing Universality. > A is supposed to be some “propositional combinators”, being true or false, > on some argument(s) or not, and we want that if A is true, then the > combinators B is trigged, and if A is false, then the combinator C should be > trigged. > > For this we need some representation of the constant Boolean TRUE and FALSE. > > Barendrecht defined the constant TRUE by K. And he defined the constant > false by KI. (I is of course the identity combinator, i.e. SKK). I will use > t and f as usual for those boolean constants. > > So we define: > > t = K > > and > > f = KI > > Now, the implementation of > > if A then B else C > > Is simply > > ABC > > Indeed, if A is true, A = t = K, and KBC = B, and if A is false, A = f = KI, > then ABC = fBC = KIBC = C. > > (KIxy = (KIx)y = Iy = y) > > OK? > > Bold Summary: By choosing t = K, and f = KI, “if A then B else C” becomes > ABC. > > This will be exploited later for programming, but right now, we can use this > to implement elementary propositional logic. > > I will use minuscule for those logical combinators > > 1) conjunction: c ("x and y” is written cxy) > > We want a combinator c such that cxy = t if both x and y are equal to t, and > false in all other situations. > > But cxy, the conjunction of x and y, is really the same as "If x then y else > f". > > Indeed, if x is false, “x & y” is false, and if x is true, “x & y” is given > by the truth value of y. > > So: cxy = 'if x then y else f' = xyf (cf the bold summary above), and c = > [x][y] xyf, but that is Rfxy where R is the Robin (one of the combinator > which does a circular permutation, that we have seen previously): > Rxyz = yzx. Conclusion c = Rf. > > <<Remark. > To be sure we have seen that R = CC and that > C = S(BBS)(KK), (note the difference between c and C) > > R = CC = S(BBS)(KK)(S(BBS)(KK)) but there are still B there, which we > replace by its SK-implementation S(KS)K: > > R = S(S(KS)K(S(KS)K)S)(KK)(S(S(KS)K(S(KS)K)S)(KK)) > > So the combinator c is Rf which is R(KI), and that gives, with I = SKK, > > c = S(S(KS)K(S(KS)K)S)(KK)(S(S(KS)K(S(KS)K)S)(KK))(K(SKK)) > > But I will write it simply c = Vf. I just wanted you to remember that c is > truly a combinator, i.e.. a combination of K and S.>> > > Does it work? It should. No need to verify this with the long expression, as > we have already verified that Vxyz = zxy, etc. We can test directly the > truth table: > > ctt = Rftt = ttf = Ktf = t > ctf = Rftf = tff = Kff = f > cft = Rfft = ftf = KItf = f > cff = Rfff = fff = KIff = f > > It works! > > 2) Disjunction: d > > dxy = if x then t else y (OK?) > > So dxy = xty. So d = [x][y]xty = Tty (with Txy = yx): Ttxy = xty indeed. > > So d = Tt > > Does it work? Let us verify: > > dtt = Tttt = ttt = Ktt = t > dtf = Tttf = ttf = Ktf = t > dft = Ttft = ftt = (KI)tt = t > dff = Ttff = ftf = (KI)tf = f > > It works! > > 3) implication: i > > ixy should be false only if x is t and y is f, if you remember its truth > table. ixy is basically the (negation of x) or y. > > So ixy = if x then y else t. OK? So ixy = xyt, and i = [x][y]xyt, and that > gives i = Rt. > Vérification: > > itt = Rttt = ttt = Ktt = t > itf = Rttf = tft = Kft = f > ift = Rtft = ftt = KItt = t > iff = Rtff = fft = KIft = t > > It works! > > 4) Negation : N (I use “N” instead of “n", as “n” is so much used for > numbers …, who will soon appear) > > We know that (Not x) is the same as (x -> f), so Nx = ixf, and N =[x]ixf > would do, but we can find it again directly by the fact that > > (Not x) = if x then f else t. OK? > > So Nx = xft, and N = [x]xft, which gives N = Vft, with V being the Vireo, > the other circular permuter combinator: Vxyz = zxy. > > Vérification: > > (Not t) = Vftt = tft = Kft = f. > (Not f) = Vftf = fft = (KI)ft = t. > > It works! > > So we can do propositional logic! > > Summary: > > t = K > f = KI > > “If x then y else z” = xyz > > c = Rf > d = Tt > i = Rt > N = Vft > > > Does this close the Turing Universality question? Some of my students > thought so. The reason that they give is that with NOT and AND, or with NOT > and OR, we are supposed to be able to build the Boolean circuit of some von > Neuman computer. But that is not true, we have only the Boolean logic, and > to build NAND gates and flip flop, you need time-delay, clock and and some > implicit recursion or iteration procedure. > > In the next chapter (combinator 4), we will obtain recursion, very easily, > providing a big step for showing that the combinator gives a (high level!) > programming language, which will be the subject matter of combinator 5. In > combinator 6 I will explain a *particular* relation between the combinators > and the phi_i (and the w_i), and perhaps explain the second recursion > theorem in this setting, which is what is needed to get the mathematical > definition of the “third person self” (the one obeying to the modal logic G > and G*). > > I might let the things deepen up to the Löbian combinators and their > “theology" and “physics". Here too Löbianity is imposed by having > sufficiently strong induction axioms, which provide the strong > self-referential abilities. > > I hope you enjoy. > > Bruno > > > > > > > > > > lllopmp > > -- > 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.
-- 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.
