> On 30 Jul 2018, at 21:54, Brent Meeker <meeke...@verizon.net> wrote: > > I always look forward to your tutorials in logic...even if I don't mistake > them for reality. :-)
Well, thanks. Did you get my post “Combinators 1 (introduction) ? (I put it below in case you missed it). Well, it is already a slight amelioration. Tell me if you understand. Soon I will soon solve some exercice so that people can get some training. The price of the conceptual simplicity of the combinators is that the notation can be a bit tricky. > Brent > > On 7/30/2018 8:12 AM, Bruno Marchal wrote: >> If some people are interested, I can show how the two axioms Kxy = x and >> Sxyz (+ few legality axioms and rules, but without classical logic (unlike >> Robison arithmetic) gives a Turing complete theory. I have all this fresh in >> my head because I have just finished a thorough course on this. Combinators >> are also interesting to explain what is a computation and for >> differentiating different sorts of computation, including already sort of >> “physical computation”. Yet it would be treachery to use this directly. To >> distinguish 3p and 1p, and 3-1 quanta with 1-p qualia, we need to extract >> them from Löb’s formula, and use Löbian combinators. I will probably type a >> summary here. >> >> Bruno =============== combinators 1 (introduction) ================ 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!) Axiom 1 Kxy = x Axiom 2 Sxyz = xz(yz) That is all. With the parentheses: Axiom 1 ((K x) y) = x Axiom 1 (((S x) y) z) = ((x z)(y z)) Exemple: (K K) gives … well, it gives (K K), because K needs two arguments to do something. K, Smullyan’s Kestrel, can be seen as a projection on the first coordinate, but with that delayed answer when it has not enough argument, like the combinators do. But ((K K) (K K)) = KK(KK) = K, as KK(KK) is a redex: it match the left hand-side of the axiom 1, with x = K and y = KK. A natural first 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.
