Hi Bruno, Just to thank you for this and let you know that I am (finally) following. Will try to finish the combinator 2 exercises this weekend, but I think it's all clear so far.
Best, Telmo. On 20 August 2018 at 20:01, Bruno Marchal <[email protected]> wrote: > Hi, > > > Don’t hesitate to enlarge your font if this post is printed too small. > > Summary of what we have seen so far: K, S and all combinations of K and S > are called combinators. > We write KSK for ((K S) K) , and K(SK) for (K (S K)). > > We have only two axioms/rules/laws: > > Kxy = x. (For all combinators x y) > Sxyz = xz(yz). (For all combinators x y and z). > > We have solved some exercises: > > - find a combinator A such that Ax = x (Solution: A = SKK) > - find a combinator A such that Ax = xx (Solution: A = S(SKK)(SKK) ) > - find a combinator A such that Axyz = x(yz) (Solution: A = S(KS)K ), > Etc. > > > Now, I will provide an algorithm to solve all the previous exercises. > > Actually, for reason which will be clear, I will give more than one > algorithm. I will give three algorithms. > (From the original one by Schoenfinkel to one in the book by Curry & Feys). > > It will helpful to clarify some notions, and to use also good notations. It > will make the algorithms clearer, and it will ease the proof that the > algorithms do well what they are supposed to do. > > All the problems we have encountered have the following shape: find a > combinator A (i.e. a combination of S and K) such that Axy = x(yx), say. I > have put the combination x(yx) but the idea is to solve that problem for any > combination. If we succeed in finding such an algorithm, and prove its > correctness, we will know that all combinations can be produced by some > combinators. We say that the (SK)-combinators are combinatorially complete. > > What is exactly a combination? It is not a formal object of the theory, but > we can see it as an informal description of an indeterminate combinator. > Like "y = ax + b" is not a line equation but a collection of line equations > (one for each choice of value for a and b). For example S(Kx) is a > combination, and it describes all combinators having that shape. > > Precisely a combination is defined by being either K, or S or a variable x, > or y, z, … , and if X is a combination, and Y is a combination we can build > a new combination (X Y), written again simply XY. > > So, x, y, xx, xxx(yx), xK, KS, KSx(yz), etc. are all combinations. All > combinators are combinations (indeed of S and K), but some combinations are > not combinator, as they might contain some variables, or only variable. > > Now, we have the problem to find a combinator building some combination from > its arguments x, y, z., and this from some combination, x(yx) (say). > > The algorithm will proceed by elimination of variable, and their (hopefully > correct) replacement by K or S, or perhaps both at some adequate place. > > We will eliminate each variable, one at a time. > > Let A be any combination (like x(yx) to have an example in mind). > > I will write [x] A for the result of the (hopefully) correct elimination of > the variable x (and some replacement with K and S). > > So [x] A must give a combinator, or a combination, G such that Gx = A. Put > in another way ([x] A)x = A, where A designates some combination, like > x(yz). > > The relation ([x] A)x = A is really just the definition of elimination. It > is a combinator, or a combination, still unknown and written [x] A, in which > x does not occur, but which when applied on x do provide the combination A > which was asked, with perhaps some remaining indeterminate. > > A is used for the combination here. Usually not the combinators. > > If there are many variables in the specification of the combinator G (we > search for Gxyz = A (A some combination)), we will first eliminate z, then > y, then x, one variable at a time. > > First we eliminate z, and that gives ([z] A), then we eliminate y for the > result: [y] ([z]A), then we eliminate x from the result: > > [x] [y] [z] A = [x] ( [y] ([z] A) ) ) > > And we want the combinator where all variables have been eliminated (and > replaced with occurence of S and K), i.e ( [x] [y] [z] A), to do its job, > i.e. > > ([x] [y] [z]A)xyz = A (the given combination). > > Just to illustrate the notation, let us write this for a combinator that we > have already found. > > Bxyz = x(yz) > > (Remind: we found that B = S(KS)K, and indeed > > S(KS)Kxyz = (KS)x(Kx)yz (by the second law Sxyz = xz(yz). > = KSx(Kx)yz (cleaning up some parenthesis) > = S(Kx)yz (By the first law Kxy = x, thus KSx = S) > = (Kxz)(yz) (by the second law) > = x(yz) (by the first law).) > > So "S(KS)K” would be a successful elimination of x, y and z of the > combination x(yz), > > > [x] [y] [z] x(yz) = S(KS)K > > > and so (in case we get it by the algorithm) we see that > > > ([x] [y] [z] x(yz) )xyz = x(yz), as S(KS)Kxyz = x(yz). > > So, the verification is well described by > > ([x] [y] [z] A)xyz = A, with A being x(zy) and ([x] [y] [z] A) = S(KS)K. > > I call the formula ([x] [y] [z] A)xyz = A, the verification formula, with > any number of variables. > > ([x]A)x = A > ([x][y]A)xy = A > ([x] [y] [z] A)xyz = A > > Take it easy, as this will be used again, again and again. > > Let us handle two simple cases, indeed already solved in Combinator 1. > Let us solve the case when the combination is just the variable x. > > [x] x = ? > > Again [x]x must be a combinator Z such that Zx = x. Well, we found it: it is > SKK. > > So [x] x = SKK > > Verification. > > We must verify that ([x]A)x = A, when A is the combination x. i.e. SKKx = x, > well SKKx = Kx(Kx) = x. As we knew. > > > What about [x]y ? How to eliminate x from a combination in which x does not > appear? We have just to keep in mind that we search a combinator Z such that > Zx = y, so we see that Z = Ky would do the job. Vérification: > Zx =(Ky)x = y. [x]y is the constant function sending any x on y. So to > speak: y is a constant with respect to x. > > And this remains correct for any combination in which x does not occur. For > example [x] SK = K(SK), indeed > ([x]SK)x) = K(SK)x = SK, so we see again that the verification formula > ([x]A)x = A (with A = SK) is well verified. > > What about [y]y? It better should be the same as [x]x. The algorithm is the > same for all variable, taken at a time, up to the renaming of the variable. > > We have just obtained the terminating condition of the algorithm, indeed of > all the algorithms I will give. > > > I will now give the first algorithm. It is often called the ABF algorithm, > as there are three lines in it. The second algorithm will be the ABCF one, > and the last algorithm will be the ABCDEF one. > > From now on, N is any combinations in which the variable x does NOT occur. A > and B are any combinations. > > > ABF bracket algorithm > > A) [x]N = KN. (x not in N) > > B) [x]x = SKK > > F) [x](AB) = S ([x]A) ([x]B) > > > Exemple. Let us search the mocking bird Mx = xx. So the combination is xx, > and we have to eliminate x from it. > We can write Mx = xx => M = [x]xx (that is another way to say the > verification formula: ([x)xx)x) = xx. OK? > > Neither A), nor B) can be applied, as xx contains x and is different from x. > S we need to apply the line F). > That gives: > > = S ([x]x) ([x]x) by F). > = S(SKK)(SKK) by B). > > And we are done. > > Verification: Mx = ([x]xx)x = S(SKK)(SKK)x = SKKx(SKKx) = xx. OK? > > We will often use I to abbreviate SKK. So M = SII. > > That algorithm is nice, and it is easy to prove that it works well. We have > already verified the terminating conditions above. So we need to prove only > the case F) > > We must verify that ([x]AB)x = AB, assuming (induction hypothesis) that we > have already A = ([x]A)x and B = ([x]B)x. > > But ([x]AB)x = (S ([x]A) ([x]B) x = S ([x]A) ([x]B) x . And by the second > law, that gives (([x]A)x) (([x]B)x) = AB. QED. > > We have proven that the SK-combinators are combinatorially complete. > > Now, look at this: what is [x] Sx ? We have to search search a combinator G > such that Gx = Sx, i.e. G = [x] Sx. Again we need to start with the line F). > That gives: > > S ([x]S) ([x]x) by line F). > = S(KS) ([x]x) by line A). > = S(KS)I, by line B) (with I abbreviating SKK). > > Is it correct? Verification: ([x]Sx)x) = S(KS)Ix = KSx(Ix) by the second > law, and that gives S(Ix) by the first law, and that gives Sx. So that was > correct. Yet, a simpler solution is just S. That is a genuine combinator, > and of course Sx = Sx. So S is a better solution, and the ABF algorithm > missed it. It provides a combinator, but a rather complex one. > > The second algorithm is better in that regard, and indeed much better (as > illustrated even more below). It admits the line C) which says directly that > [x]Ax = A, when A does not contain x. This will entail that we identify the > combinators which have the same input-output behaviour. It is a form of some > extensionality principle. This should not be confused with the definition of > elimination formula ([x]A)x = A. In case of doubt add the left parenthesis > in [x]Ax = A. i.e. [x](Ax), which is quite different from ([x]A)x = A. In > the first case we eliminate x from the combination Ax, in the second case we > apply the combinator [x]A on x. In the first case x cannot occur in A, in > the second case A is any combination. > > > The ABCF algorithm: Again, x does not occur in N. > > A) [x]N = KN > > B) [x]x = SKK > > C) [x]Nx = N > > F) [x](AB) = S ([x]A) ([x]B) > > > > Exercise. Find the combinator B such that Bxyz = x(yz) using the ABCF > algorithm (gentle exercise) and using the ABF algorithm (Horrible exercise). > > Let me solve this, first with the ABCF algorithm > > Bxyz = x(yz) > B = [x][y][z] x(yz) (We have to eliminate x, y and z from x(yz)) > B = [x][y] ([z]x(yz)) (We have to eliminate z first) > B = [x][y] (S [z]x [z]yz) line F). > B = [x][y] (S (Kx) [z]yz) line A). > B = [x][y] (S (Kx) y) (line C). Do you see this? y is a constant with > respect to the elimination of z! > B = [x] ([y] S(Kx)y) Now we prepare the elimination of y. > B = [x] S(Kx) (y is quickly eliminated by using the line C). Now we have > just x which remains to be eliminated. > B = S [x]S [x](Kx) By line F). > B = S(KS) [x](Kx) By line A). > B = S(KS)K (by line C). Again. > > And we are done: B = [x][y][z] x(zy), and Bxyz = ([x][y][z] x(zy))xyz = > S(KS)Kxyz which gives x(yz) as we have seen already in combinator 1. The > ABCF algorithm found the same combinator as us. Not better, nor worst. > > To see how much the line C). saves us time and build simpler combinator, let > us solve the “horrible exercise”: > I will apply sometimes two rules/laws at once, and I let you search which > line has been used. I abbreviate SKK by I. > > The beginning is the same. It changes a lot when we can’t apply the > extensionality rule c). > > Bxyz = x(yz) > B = [x][y][z] x(yz) > B = [x][y] ([z]x(yz)) > B = [x][y] S [z]x [z]yz > B = [x][y] S (Kx) [z]yz > B = [x][y] S (Kx) (S [z]y [z]z) > B = [x][y] S (Kx) (S (Ky) I) > B = [x] [y] S (Kx) (S (Ky) I) > B = [x] S [y]S(Kx) [y]S(Ky)I > B = [x] S (K(S(Kx))) (S ([y]S(Ky) [y]I ) > B = [x] S(K(S(Kx))) (S (S [y]S [y]Ky) (KI) ) > B = [x] S(K(S(Kx))) (S (S (KS) (S [y]K [y]y)) (KI) ) > B = [x] S(K(S(Kx))) (S (S (KS) (S (KK) I)) (KI) ) > > OK, now the x elimination, > > B = S [x]S(K(S(Kx))) [x](S(S(KS)(S(KK)I))(KI)) ) > B = S [x]S(K(S(Kx))) (K(S(S(KS)(S(KK)I))(KI))) %x does not appear in > (S(S(KS…)! > > Let us compute [x]S(K(S(Kx))) separately: > > [x]S(K(S(Kx))) > = S ([x]S [x]K(S(Kx)) > = S (KS) (S [x]K [x]S(Kx) ) > = S (KS) (S (KK) (S [x]S [x]Kx ) ) > = S (KS) (S(KK) (S (KS) (S [x]K [x]x))) > = S(KS) (S (KK) (S (KS) (S(KK)I)) ) > > So (replacing I by SKK), and [x]S(K(S(Kx))) by its results, the ABF > algorithm provides the following blue bird B: > > B = S (S(KS)(S(KK)(S(KS)(S(KK)(SKK)))))(K(S(S(KS)(S(KK)I))(K(SKK)))) > > (Which is slower and perhaps not as cute as S(KS)K found by the ABCF > algorithm, all right?). > > OK, now I’m a little bit tired. > > Exercise ( I will provide the solutions in the next post). Find (again > perhaps) all the combinators we have studied in Combinator 1. > > Oh! Wait! Let me give you the full ABCDEF algorithm before. It uses the fact > that we have already B and C to take some shortcut before using S (in F).). > B is the" blue bird" Bxyz = x(yz). C is the “Cardinal” Cxyz = xzx. > > The third algorithm (again, A is any combination, N is any combination > without x) > > > The ABCDEF algorithm > > A) [x]N = KN > > B) [x]x = SKK > > C) [x]Nx = N > > D) [x]NA = B N [x]A > > E) [x]AN = C [x]A N > > F) [x](AB) = S ([x]A) ([x]B) > > (this “B” is of course not the blue bird, just the argument of A > in the combinator (AB)) > > > Supplementary exercises: > > 1) prove that the line “D)” and line “E)” are correct, do well their job. B > is the compositor/applicator (the blue bird), and C is a permuter Dxyz = xzy > (it permutes its “last two arguments). > > 2) Is there a combinator A such that Axy = Sxz ? (Hint: compute [x][z] Sxz, > and meditate about variable and parameter). > > Oh! I see that the ill tampered student want to ask a question, yes? > > “What all that fuss about S and K? Why not just take all the combinations at > the formal level, with simple substitution rules, and then we can > distinguish the variables from the parameters perhaps using your brackets > [x]… hmm… And when will we see all this to be Turing Universal?” > > Whoa! Congratulation! You have just (re)invented or (re)discovered Lambda > Calculus. The ABF algorithms, and its extensions are compilers from lambda > calculus to the combinators. > The lambda calculus starts from all combinations, and abstract the variable > to make the combinations into functions, and tells which argument can be > substituted in the combination, directly. Indeed. > You can see that the combinators and the lambda calculus are closely > related. More on this later. > And, well yes, some works remains to be done to show that the combinators > (and thus the lambda expressions) can emulate all Turing universal machines, > or compute all partial recursive (computable) functions. > > I expect this will be for Combinator 5. > > Bruno > > > > > > On 17 Aug 2018, at 20:10, Bruno Marchal <[email protected]> wrote: > > Hi, > > A last thing about K, which concerns all combinators. > > Let me recall what is curryfication: transforming a function of two > variables in two functions of one variable. > > The curryfication of the binary addition, using the combinator presentation > would be (+ 2 4), which is seen as the abbreviation of ((+ 2) 4). When + got > his first argument (+ 2) it gives as a result a function which on any x will > add 2 to that x. > > Similarly I have said that K can be seen as a function of two arguments, the > curryfication of the projection on the first coordinate: Kxy = x. > > But what is the function (K x), i.e. Kx ? It does not contain a redex, so Kx > is a stable molecule, I mean combinator. For example KS, K(SS), are all > stable. But what is the function KS? Well, on any x we have that > > KSx = S (by the law Kxy = x for all x y) > > So KS is the constant function which sends any combinator x on S. > > KSS)x = (SS) for all x, and so is the constant function which sends any > combinator x on (SS). > > So, as a function of one argument, K is a builder of a constant function.Kx > build the constant C send all combinators to that x. K comes from Konstant > in German (in which it appears in 1924, in a paper by Moses Shoenfinkel, a > Russian (Soviet) logician from Moscow. > > That will help for the next task: to find an algortihm building the > combinator X specified by its behaviour Xxyz = yx(xy) for example. That > algorithm should solve all previous exercises. That is for the next post, > and thread “Combinators 2”. > > A good training useful for that algorithm consists also in seeing well that > all combinators, with the exception of K and S, comes from the marriage of > two combinators. That follows of course directly from the definition, but it > is not always easy to find which is the “function” and which is the > argument”, as they are called when married. > > For example which is which in abc(def)gh ? Answer: it is (abc(def)g) married > to h. Just add (metal) the left parenthesis, or the most large one. > > Which is which in abc(def) ? It is (abc) married with (def). > > Which is which in KSKK and in K(SKK) ? It is KSK with K in the first, and K > with I in the second. > > OK? > > No question? > > Only questions can slow me down … (a lot of job-work await me, so I > accelerate also because I will be busy the next week and more after…). > > … > > Maybe much later I will reunite the current thread and explain a bit of the > quantum combinators or lambda calculus, some categories of Coecke and show > how the information flow is local in the quantum computations, even when > using only “measurement” as a (Deutsch-Turing) universal (quantum) machine. > Of course (?), those have to be extracted from the “theology” G* if we want > to solve the “classical indexical computationalist” mind body problem. To be > sure. > > > Bruno > > > > > > > On 16 Aug 2018, at 19:33, Bruno Marchal <[email protected]> wrote: > > Hi, > > No problem so far? Jason? Brent? > > Here is a short post on what happens when you mock a mocking bird, to use > Smullyan’s terminology. > > I recall that a “mocking bird” is a combinator M such that Mx = xx, i.e. M > apply to x will mimic what x do when apply to itself. > > Now, what happens when we apply M to itself? What does MM, the “mocked > mocking-bird”? > > I guess you have all seen that it leads to a non terminating sequence of > reductions. It is a non terminating computations. > > MM gives MM (as Mx gives xx for all x). But MM match the “redex” Mx, and so > it triggered again, and that new MM gives MM, which gives MM, which gives > MM, … and now you have to unplug the computer running that combinator, as it > will never stop. > > So MM is equivalent to the BASIC instruction “10 goto 10”. That illustrates > the existence of non stopping computation, which is (of course?) needed if > we hope that the combinators are Turing universal. > > But now, I have officially defined a non stopping computation by one which, > at all steps, has still some redex, and the official redex are “Kxy" and > “Sxyz". > > So let us see if that is the case with MM. > > But first let us see what combinator (combination of S and K) could be a > mocking bird. > > Mx = xx, but that is equal to Ix(Ix), OK? (Ix = x). > > And ix(Ix) match xz(yz) which is the reduction of Sxyz, so Ix(Ix) = SII. > > Let us quickly verify: SIIx = Ix(Ix) = xx. OK. > > So MM is SII(SII), and that contains the redex Sxyz with x = I, y = I and z > = SII. OK? > > So, by the second law (Sxyz = xz(yz)), we have successively: > > SII(SII) = I(SII)(I(SII) = SII(SII), and we see that we have the same redex > than initially: this cannot stop. > > To be sure, SII is S(SKK)(SKK), as we have seen that I is SKK. But that > leads to the same reasoning with SKK in place of I, given that we already > know that SKKx = x. (SKKx = Kx(Kx) = x, OK?). > > Just to say that we have only two redex, but we can say that any defining > relation, like Bxyz = x(yz) introduce new redex forms, which just hide the > old and “official” redex. > > Next: I will give an algorithm to solve all exercises seen so far. Mainly, > how to synthetise a combinator from its defining specification (like Lxy = > x(yy), or Wxy = xyy, or Pxy = y, etc.). That post will be longer, as I > intend to give three algorithm, and to illustrate them on many examples, and > then give the proof that they do their jobs, which will prove the > combinatorial completeness of the SK-combinators. With the combination of S > and K, we can build all combinators doing all combinations of their > arguments. > > Be sure you handle well the notations, and the very few concepts introduced > so far. > > Please, ask question if anything looks weird, or if you don’t understand a > solution in the preceding post. In math, missing one step leads quickly to > the erroneous feeling that something is complicated, when actually, things > are rather easy (up to now). > > > Best, > > Bruno > > > > > > > > On 13 Aug 2018, at 13:55, Bruno Marchal <[email protected]> wrote: > > Hi Jason, Brent, others, > > > In this post, I sum up what we have seen so far, and provide the solutions > to the (suggested) exercise. Skip the solutions if you still want to find by > yourself. > > The motivation is to better appreciate what is a computation, and why, when > we assume Mechanism, the two axioms Kxy = x and Sxyz = xz(yz) are enough, > and cannot be completed with other axioms, unless we describe observer (and > not “reality”). > > ------------ > > A combinator is a combination of S and K, i. e. S is a combinator, K is a > combinator, and from two combinators x y you can build the combinator (x y). > > From this you can enumerate already easily all combinators. K, S, (K K), (K > S), (S K), (S S), ((K K) K), (K (K K)), … > > Now, we use a convention to help the readability: we suppress the left most > parentheses (and their right corresponding parenthesis). > > So > > abc(def)ghu > > can be be read as the combinator abc(def)gh applied to u. But abc(def)gh can > be seen itself as the combinator abc(def)g applied to h, and then abc(def)g > can be seen as abc(def) applied to g. Then abc(def) is abc applied to (def). > abc is ab applied to c: ((a b) c), and def is de applied to c. > > You can also read from the left: in abc(def)ghu, it means a is applied to b: > (a b) and that is applied to c: ((ab)c) which is applied on (def), which is > ((de)f), and the result of that is applied to g, and the result is applied > to h, and the result is applied to u. > > With those conventions, the only two axioms, or laws, (besides some equality > rules) are that, with x and y being any combinators. > > Kxy = x > > Sxyz = xz(yz) > > It means that the combinators K, when he get two arguments x y, it becomes > instable and reacts and gives x as a result. > > S “reacts” only when he got his three arguments (in the “Curry” way: Sxyz is > really (((Sx)y)z), and that gives xz(yz): S applies x on z, and that is > applied on the result of applying y on z. > > The expression Kxy and Sxyz are called redex, and a combinators is instable > as long as it contains redexes. When it does no more contain a redex, we say > that a combinator is in normal form (I use often “stable” also). > > The computation are not deterministic. If a combinator contains two > different regexes, you can reduce them in any order. It can be proved that > if the combinator has a normal form, then all converging path will give the > same result (but we will see this is untrue if some path are infinite). > > > Summary: combinators are combination of K and S, and their have a sort of > dynamic provided by the two laws above. > > > The only difficulty is due to the explosion of parentheses, which is limited > by our convention of not writing the left parentheses when there is no > ambiguity. > That can lead to a new difficulty, due to forgetting that those parenthesis > are still there. For example, let us compute: > > KSxyz > > x and y and z are just any combinators. Someone could wrongly claim that it > contains the redex Sxyz, and that it might reduces to Kxz(yz), and then x. > But that is incorrect. It would be correct if it was K(Sxyz). KSxyz gives > (KSx)yz = Syz, not x. > > If you substitute the combinator ab for c in cxyz, you can write abxyz. But > if you substitute ab for x, that gives c(ab)yz. In that case the parentheses > are obligatory, as a(bc) is different from abc = (ab)c. > > OK. Please ask question if anything seems unclear. > > > Let us see the combinators that we have already met. > > Is there an identity combinator, i.e. a I such that Ix = x ? Yes I = SKK. > Indeed SKKx = Kx(Kx) = x. So SKK is the identity bird. Note that SKA is an > identity bird for any combinator A. Exemple SK(KK)x = Kx(KKx) = x. > > Is there a combinator M such that Mx = xx ? Yes. Mx = xx = Ix(Ix) = SIIx, so > M = SII. Verification Mx = SIIx = Ix(Ix) = xx. > > Is there a combinator f such that fxy = y ? Yes. f = KI. Verification fxy = > KIxy = (KIx)y = Iy = y. So KI is the projection on the second coordinate. > Why do I use the matter f for its name? Because later KI will play the role > of the constant propositional false. We will come back on this. Similarly K > will play the role of the truth constant t. > > Is there a combinator B such that Bxyz = x(yz) ? Yes. Bxyz = x(yz) = > (Kxz)(yz) = ((Kx)z)yz) (I added left parenthesis to help seeing the > matching with the second S redex) = S(Kx)yz = ((KS)x(Kx))yz = KSx(Kx)yz = > S(KS)Kxyz, so B = S(KS)K. Verification: S(KS)Kxyz = KSx(Kx)yz = S(Kx)yz = > Kxz(yz) = x(yz). > > OK? > > I suggested some “exercises”. > > 1) Is there a W such that Wxy = xyy ? > 2) Is there a T such that Txy = yx ? > 3) is there a L such that Lxy = x(yy) ? > 4) is there a C such that Cxyz = xzy ? > > The method consist is trying to introduce K and S, or other combinators > already defined, to match the right hand part of the regexes, and go > backward. > > Solutions: (you can skip this if you want take more time to find them. > Later, in "combinator 2”, I will give an algorithm to solve those problem. > > 1) Wxy = xyy = (xy)(Iy) = SxIy = Sx(KIx)y = SS(KI)xy, so W = SS(KI). > Verification: SS(KI)xy = Sx(KIx)y = xy(KIx)y = xy(Iy) = xyy > > 2) Txy = yx = y(Kxy) = Iy(Kxy) = Iy((Kx)y) = SI(Kx)y = B(SI)Kxy, so T = > B(SI)K. (B is handy to suppress the right parentheses). Verification: > B(SI)Kxy = SI(Kx)y > = Iy(Kxy) = yx > > 3) Lxy = x(yy) = x(My) = BxMy = Bx(KMx)y = SB(KM)xy, so L = SB(KM). > Vérification: Lxy = SB(KM)xy = Bx(KMx)y = x(KMxy) = x(My) = x(yy). > > 4) Cxyz = xzy > > This one is a bit harder. xzy = xz(Kyz) = Sx(Ky)z = B(Sx)Kyz = BBSxKyz = > BBSx(KKx)yz = S(BBS)(KK)xyz, so C = S(BBS)(KK). > > Vérification: S(BBS)(KK)xyz = BBSx(KKx)yz = B(Sx)(KKx)yz = B(Sx)Kyz = > Sx(Ky)z = xz(Kyz) = xzy. > > OK? Take the time to understand well the verification. Ask any question if > you have some doubt at some steps. > > > Next post: the algorithm to solve this task. It helps to train oneself a bit > before. > > > Bruno > > > > > > On 5 Aug 2018, at 21:05, Bruno Marchal <[email protected]> wrote: > > Hi Jason, > > > On 5 Aug 2018, at 05:24, Jason Resch <[email protected]> wrote: > > > > On Sat, Jul 28, 2018 at 2:19 PM Bruno Marchal <[email protected]> wrote: >> >> Hi Jason, people, >> > > Hi Bruno, > > Thank you for this. I've been trying to digest it over the past few days. > > > No problem. It was hard to begin with , and I was about sending few easy > exercise to help for the notation. But you did very well. > > > > >> >> >> 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. > > > So am I correct to say a combinator "B" is a function taking a single input > "fgx”, > > > Three inputs. B on f will first gives (B f), written Bf, then when B will > get its second input that will give ((B f) g), written Bfg, which is a new > function which on x, will now trigger the definition above and give the > combinator (f (g x)), written f(gx) and which would compute f(g(x)) written > with the usual schoolboy notation. > > > > > but is itself capable of parsing the inputs and evaluating them as > functions? > > > It just recombine its inputs, the functions will evaluate by themselves. > Don’t worry, you will see clearly the how and why. > > B is called an applicator, because given f, g and h has arguments, Bfgh, it > gives f(gh). I have used f and g and h has symbol, but I can use x and y and > z instead. Those variables are put for combinators. Bxyz = x(yz). Formally B > only introduce those right parenthesis. With full parentheses we should > write: > > (((Bx)y)z) = (x(yz)). But we suppress all leftmost parentheses: Bxyz =x(yz). > > The interesting question is: does B exist? Which here means —is there a > combinator (named B) which applied on x, then y, then z, gives x(yz). > > Later I will provide an algorithm solving the task of finding a combinators > doing some given combination like that. But here I just answer the > question: YES! > > Theorem B = S(KS)K, i.e. Bxyz = S(KS)Kxyz = x(yz) > > Proof: it is enough to compute S(KS)Kxyz and to see if we get x(yz) > > Let us compute, and of course I remind you the two fundamental laws used in > that computation: > > Kxy = x > Sxyz = xz(yz) > > S(KS)Kxyz = > > OK let see in detail that is the combinator S, which got a first argument, > the combinator (KS) this gives (S (K S)) written S(KS), which remains stable > ("not enough argument”), then S(KS) get the argument K which gives S(KS)K, > which remains stable (indeed it is supposed to be the code of B) and indeed > S has still got only his first two argument and so we can’t apply any laws > to proceed, but now, S get its third argument x so > > we are at S(KS)Kx, that is S (KS) K x, and here S has three arguments and so > match the left part of the second law S x y z, with x = KS, y = K and z = x. > > Now the second law is triggered, so to speak, and we get xz(yz) with with x > = KS, y = K and z = x, and that is gives (KS)x(Kx) = KSx(Kx). OK? > > You always add the left parentheses, or some of them to be sure what we have > obtained. KSx(Kx) = ((KSx) (Kx)), but “KSx” is a redex, as it match Kxy, > with x = S and y = x, and so get “reduces” into S, so we get S(Kx) (starting > from S(KS)Kx, which is Bx, waiting now for y and then z. > > We are at Bxy = S(KS)Kxy = (we just computed) S(Kx)y, which is S with “not > enough argument” so we give the remains z and get > > S(Kx)yz > > Which triggers again the second law to give (x = (Kx), y = y, z = z) > > (Kx)z(yz) = Kxz(yz) > > And again, Kxz gives x (by the first law) so we get > > x(yz). > > OK? > > How could we have found that B was computed by the combinators S(KS)K? > > We can do this by guessing and computing in reverse, introducing K or other > combinators so that we can reverse the fundamental laws. So in x(yz), we can > replace x by (Kxz) that is ((Kx)z) so that we can apply axiom 2 to x(yz) = > (Kxz)(yz) = S(Kx)yz, then, well the “yz” are already in the good place, but > the x is still in a parenthesis which has to be removed: we just do the same > trick and replace S(Kx) by (KSx)(Kx), and so we get S(KS)Kx and we are done: > B = S(KS)K. > > Don’t worry too much, I will soon or a bit later provide an algorithm which > from a specification Xxyzt = xt(ytxzx) find a combinator X doing that task. > > To summarise the computation: > > S(KS)Kxyz > = KSx(Kx)yz > = S(Kx)yz > = (Kxz)(yz). (In passing Here we use that S is an applicator) > = x(yz) > > Each reduction of a redex (“Kxy” or “Sxyz”) counts as one computational > step. > > >> >> >> 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. > > > So are input and output values themselves considered as functions, with > fixed values just being identities which return themselves? > > > Yes, you can see all combinators as function of one argument. Take K for > example. The first law says Kxy = x. Typically you can interpret K as the > projection on the first coordinate: you give (x y) and it outputs x. But K > is also a function of one argument (K x) is the constant function x. > > Ley us train ourself with computing the first combinators made only of K. > > We must compute K. Obviously, it has not enough argument, so that gives K > (and that stops!). We stop when the combaintors has no more regexes, that > is, an occurence of the pattern Kxy or Sxyz. > > KK = ? > > Well, KK gives KK. It is a function, as KK is the constant K. KKS = K, > KK(SS) = K, KKK = K for all x, by the first law. > > KKK = ? > > Well, that gives K, in one computational step, by the first law (of course > without S only the first law applies). > > KKKK = ? That is (KKK)K, and that is KK. > > From this you can guess (and prove by induction) that KKKKKK…K with an odd > number of K will give K, and with an even number of K will give KK. > > K(KK) = ? > > Hmm… here K got only one argument (and the difficulty for some will be in > not using the schoolboy meaning: K(KK) is not K applied to two arguments (K, > K), but is K applied to the (stable) combinator KK. Now K need two argument > for the first law to be triggered, and so K(KK) remains stable. > > K(KK)K = ? > > That gives (KK) = KK by the first law. > > What gives (KK) applied to (KK)? > > Beginners get easily wrong on this one, presented in this way! They think > that each KK is stable, and that this cannot evolve. > Nervetheless, In full parentheses notation, ((K K) (K K)) does match ((K x) > y), with x = K and y = (K K) = KK, so that gives K. But it is even clear > with the convention to eliminates all leftmost parenthesis and their match. > KK applied to KK is KK(KK), with match clearly Kxy, with x = K and y = KK, > so KK(KK) = K. > > > > >> >> >> 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? > > > The syntax is a bit unfamiliar to me but I think I follow so far. > > > > Yes, the notation takes some time to get familiar with. It is normal. > > > > >> >> >> 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!) >> >> Kxy = x >> Sxyz = xz(yz) >> >> That is all. >> >> A natural fist exercise consists in finding an identity combinator. That >> is a combinator I such that Ix = x. > > > > I am having trouble translating the functions and their arguments (putting > the parenthesis back in), is this translation correct? > > K(x(y)) = x > S(x(y(z))) = x(z(y(z))) > > > > It is > > ((Kx)y) = x > (((Sx)y)z) =((xz)(yz)) > > You “currified” the combinators in the wrong direction. Think about xyztr as > x waiting for y (x y) waiting for z ((x y) z) waiting for ... > > KKK = ((KK)K) = K > K(KK) = well, it remains K(KK). It is (K(K K)) with full parenthesising. > > > > > >> >> >> 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. > > > This seems reminiscent of a part of Gödel, Escher, Bach, where he was > describing univerality (or maybe it was proof systems), in terms of string > manipulation? Is this the spirit of combinators? Manipulating strings > through operations that parse (K), or re-arrange (S), and through any > combination of K and S can map any input string to any other? > > > > It is not really strings, as the combinators (x y) are better seen as the > result of the application of some function/combinators x to some function > combinators y. > Combinators are very liberal, you can apply any combinators on any > combinators. And they are both “programs” and “data”. Combinators combine, > mainly, but (x y) might evolves if xy contains redexes (Kxy, or Sxyz). It is > more like living strings. (And that will at some point shows that they are > not good for the string manipulation, that we usually want to be static > object, except for my type writer which correct my typo errors). > > > > > > > >> >> >> I will tomorrow, or Monday, show that there is a combinator M such that Mx >> = xx, a combinators T such that Thy = yx, > > > What is "x" here when it is not defined? Is it meant to represent some > arbitrary constant that depends on T? > > > x and all variables represent some arbitrary combinators. The law Kxy = x, > means that for all combinators x and y (Kx)y = x. A bit like the law x + 0 = > x means that any number added to 0 gives that same number. > > > > >> >> 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. >> > > Interesting. I have trouble imagining how to construct a while loop from S > and K at this time. I am interested to see it. > > > > I will be able to show rather quickly how to implement the if then else. > That is incredibly beautiful, and that provides a shortcut to implement > logic. > > For the MU operator, I will need “recursion”, and that is also rather > beautiful. Now, the MU operator itself is not that much of a beauty, and you > will have to be slightly patient. > > > >> >> I let you digest all this. You can try to Sind some combinators, or to >> apply some random combinators to sequence of variable. > > > It helps me to understand to implement something in software. If I were to > implement a simulation of processing S and K, is the idea to simply > represent the values of the functions as strings, or is that not sufficient? > For example, the input string "Kxy" returns "x", and the input string "Sxyz" > returns "xz(yz)" -- what does the added parenthesis here do? Is this not > the same as "xzyz”? > > > For readability we suppress all leftmost parentheses. But we cannot suppress > the right because it becomes ambiguous, as you should realise with the > computation above. ((KK)K) = KKK = K, but K(KK) just remain quietly itself > K(KK), because that match only Kx with x = the combinator KK. So K(KK) is > waiting for a second argument. For example K(KK)S = KK. > > > > > > >> >> >> 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? > > > Doesn't S require 3 inputs? How does SKx function, does it assume the > expanded SKx = SKxy = Ky(xy)? But this equals "y" does it not? > > > Let us compute both SK and KI on K (using Ix = x). > > (SK K) = SKK gives, well it remains itself as S needs its three arguments > for using the second law. > > (KI K) = KIK = I, by the first law. > > Verdict: SK and KI are different, as there is a combinator x such such that > SKx is different from I. Indeed SKK. > > Oh! Wait we have seen that I = SKK (let us verify this quickly: > > SKKx > = Kx(Kx) by the second law > = x by the first law.) > > So SK and KI are equal, after all. We will come back on this. By default we > will say that two combinators are equal when they do the same things. In > some more intentional context, we can adopt a weaker identity, and decide > that SK and KI (which is K(SKK) are not equal. > > > >> >> 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. > > > Is the distinction you are making here of whether functions are identical if > their outputs for the same input are identical, > > > That is extensional equality that I will use by default. Smullyan does that > also. > > > > as opposed to functions are identical IFF they implement the same > intermediate computations/operations in the course of their evaluation? > > > > Yes, sometimes we want weaken the extensional criteria, to compare more the > computations than the combinators, indeed. As you can guess, there are many > options. The nice thing is that those option can be formalised by > combinators identities, a but like adding the axiom SK = K(SKK) (i.e. SK = > KI). > > > > > > > > >> >> >> I have not allowed Smullyan, > > > I meant (followed). > (My computer is in the mode, if not the mood, to correct all my typo errors, > but it has too much imagination, and with combinators, he always wrote “key” > when I type “Kxy”, and when I type “Sxyz” he corrects me without saying and > wrote “sexy” ! Lol. > > > >> 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, > > > Hmm, so the problem is getting a set of combinators which outputs the same > string twice. I notice S takes in one "z" term and produces two of them, so > I think it has something to do with the "z" term of the S combinator. Then > the K combinator can be used to eliminate x and y, or perhaps using I. > > > Good start! > > > > I am thinking something like: SII which would be S(SKK)(SKK)x, but I don't > know if this is right or if it is what you are looking for.. > > > Good arrival! > > Yes, the infamous Mocking Bird, the M which mimics all bird x on themselves > is indeed given by SII, which is indeed S(SKK)(SKK), but without the x, > which would be the argument. > Why don’t you verify? Mx must give xx, so let us try SIIx. that gives Ix(Ix) > by the second law, which gives xx. > > Of course we can also verify without using the macro I. > > S(SKK)(SKK)x = > (SKKx)(SKKx) = > (Kx(Kx)(Kx(Kx)) > xx > > > > > > >> >> >> Other very difficult exercice, can the physical reality truly implement K? >> (Hint Hawking). > > > Is this asking the question of whether information can be destroyed (as K > discards information)? > > > Yes. > > > > > Thanks for this. It has done a lot to demystify what the combinators are, > even if I still don't have an intuitive understanding of how to solve > problems or implement functions from them yet. > > > That will come very soon. Tell me if this post has helped. > > In the next post, I will present you with other combinators, and you can > meditate on how to find the combinators W, L, T and C, which are such that > > Wxy = xyy > Lxy = x(yy) > Txy = yx > Cxyz = xzy > > W and L are duplicators, but L is a bit of an applicator too. T and C are > permutators. You can of course use the combinators B, I, and M, as we have > already found them. I guess C is a bit harder. > Note that S is both a duplicator (some variable/imputs are duplicated), and > an applicator: it introduce some right parenthesis. > > Also, a last question. Why is the mocking bird so infamous? What happens if > we mock a mocking bird? Can you compute MM? > > Best, > > Bruno > > > > Jason > >> >> 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 [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. > > > > -- > 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. > > > > -- > 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. -- 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.
