00:00:26 messed up at the start 00:03:41 wow that paper printed terribly 00:07:18 nope, there is no shorter than six X'x 00:07:22 *X's 00:08:17 fun 00:08:36 eh, wait... 00:08:50 i have missed some cases 00:09:41 i'm trying to understand their derivation 00:09:55 in the paper? 00:10:55 yeah 00:12:19 for P it makes sense but I don't understand the K part 00:13:42 -!- ShadowHntr has quit (Client Quit). 00:14:36 ok now i think i have all 5 X cases, still no I 00:20:29 i sorta understand it now 00:23:19 their method is interesting 00:29:44 apparently some guy named "Rosser" came up with X = \x.xKSK 00:30:06 probably the Rosser of the Church-Rosser theorem 00:32:23 http://en.wikipedia.org/wiki/J._Barkley_Rosser 00:45:33 -!- crathman has joined. 01:30:07 I wonder if there's an X such that XX = S and X(XX) = K 01:34:14 * bsmntbombdood tries the method in the paper 01:37:21 * SimonRC goes 01:38:08 find a P,Q,R such that PPQRQR == S 01:41:18 P=K(K(K(K(KS)))) 01:41:27 :) 01:42:12 -!- Arrogant has joined. 01:42:18 find a P,Q,R such that PPQRQR == S and SPQR = K 01:42:22 :) 01:42:47 Senatus PopulusQue Romanum 01:43:21 well, SPQR=PR(QR) 01:43:50 yeah 01:44:14 P=R=K 01:44:55 so then KKQKQK=S 01:45:12 KKQKQK=KKQK=KK, alas 01:45:52 yeah :( 01:46:06 what about P=I, R=KK 01:46:30 IIQ(KK)Q(KK)=S 01:46:38 =Q(KK)Q(KK) 01:47:04 ok, P=I, R=KK, Q=K(K(KS)) 01:48:50 what should X look like then? 01:50:15 what is (K(K(KS)))(KK)(K(K(KS)))(KK)? 01:51:09 S 01:51:15 =K(KS)(K(K(KS)))(KK)=KS(KK)=S 01:52:17 that was the point of that Q 01:52:22 wowzers it works 01:52:52 so X = \f.fPQR 01:53:32 so X = \f.f(K(K(KS)))(KK) 01:54:22 aha. then XX=XPQR=PPQRQR=S and X(XX)=XS=SPQR=K 01:54:41 yep 01:54:42 :) 01:54:58 and here i thought your equations looked arbitrary. 01:55:15 or at least complicated. 01:56:47 mission accomplished 01:57:23 yep 01:58:59 X = \f.fI(K(K(KS)))(KK) 01:59:59 or X = \f.f I (\xyz.S) (\x.K) 02:01:02 hm... 02:01:48 you cannot have XX=V and XV!=V, I think. 02:02:09 so XX and X(XX) cannot be chosen arbitrarily. 02:03:08 what? 02:03:25 Vx=V 02:03:37 oh 02:04:02 -!- ihope has joined. 02:04:10 I don't get what you are saying 02:04:21 ~exec self.raw("JOIN #math\r\nPRIVMSG #math :zomg bot") 02:04:27 ihope: we are brillant 02:04:33 (sic) 02:04:35 You are? 02:04:41 ~exec self.raw("PART #math") 02:04:45 ihope: me and oerjan 02:05:02 I mean, if you can find X such that XX=K and X(XX)=S or such that XX=S and X(XX)=K then you might think you could choose XX and X(XX) to be whatever you want. 02:05:15 * ihope logreads 02:05:41 But I don't think you can get XX=V and XX!=V, because then X would have to simultaneously use its argument and not 02:06:07 *X(XX)!=V 02:06:12 it couldn't be of the form \f.fE 02:06:20 V? 02:06:27 Unlambda's v operator? 02:06:30 Vx=V 02:06:31 yep 02:06:38 If that's it, you really don't want XX=V. 02:07:17 you might want to try and solve XX=A, X(XX)=B for A, B arbitrary 02:07:39 this method needs the number of arguments that B takes 02:07:54 The next things up would be (XX)X = XX and X(XX) = XV. If X pays any attention to its first argument, XV = V, and if it doesn't, X = KV meaning XV = V. 02:08:12 A, rather 02:08:30 that's essentially what i think too 02:08:53 then you solve \f.f PQR...upto A's # of args 02:09:13 although not entirely. 02:09:27 Then again, maybe I'm wrong for the "if it pays any attention to its first argument" case. 02:09:28 you could have XV=KV, say 02:09:59 Well, KV is... well, it's V. 02:09:59 yeah, it's more subtle than that. 02:10:11 hm... 02:10:25 X could simply pass its first argument on as arguments to other things. 02:10:27 you could have XV=\y.yV 02:10:37 Indeed. 02:10:51 Therefore, XVX = XV, which... hmm. 02:11:07 it would have to be \f.(E)f 02:11:15 instead of \f.fE 02:13:11 V essentially takes an infinite number of arguments, yes. It doesn't have what is called a "head normal form" 02:13:53 \f.E_a_1 ... E_a_n f E_b_1 ... E_b_n 02:13:59 It's headless! 02:14:10 ...What is a head normal form, exactly? 02:14:14 And in a sense every combinator which doesn't is semantically equivalent. 02:14:50 I guess one could say V is equivalent to (\x.xx)(\x.xx)... 02:15:12 It's \v1v2...vn.v E1E2...Em 02:15:31 oerjan: I... see. 02:15:59 The first expression inside the lambda must be a variable. 02:18:54 And if you reduce the Ei expressions recursively to their head normal forms (or to V if they don't have any) then you get a tree structure which may sometimes be infinite. 02:22:47 Bõhm trees. 02:24:44 Here is one article which mentions it: http://pauillac.inria.fr/~huet/PUBLIC/Bohm.pdf 02:25:27 -!- oerjan has quit ("Restart"). 02:27:51 -!- oerjan has joined. 02:28:38 Anyone said anything? 02:28:44 no 02:29:03 Logs are nice. 02:29:09 Good, then I won't have to go to that snail ircbrowse 02:29:22 we now have 3 decent single combinator bases 02:29:23 I was trying avoid it 02:29:31 *to 02:30:25 actually i could have gone to tunes, they are much quicker but poorer formatting. 02:32:06 I wonder why meme/ircbrowse has become so slow. Too much growth? 02:35:07 is S(KS)K reducable? 02:35:29 maybe eta, lessee 02:35:42 Reduceable? 02:35:57 S(KS)Kx = S(Kx) 02:36:07 Ah, yes. 02:36:11 so no 02:36:18 nah, looks pretty minimal 02:36:39 S(Kx)yz = Kxz(yz) = x(yz)? 02:36:50 that's what I got 02:37:05 right 02:37:33 you could reduce it with either B or C, I never remember which is which 02:37:52 C is composition, isn't it? 02:38:03 So S(KS)K = CSK? 02:38:16 Hey, S(KS)K = C, even... right? 02:38:28 yep, C 02:38:37 no b 02:38:45 (B a b c) = (a (b c)) 02:39:03 What's C, then? 02:39:16 (C a b c) = (a c b) 02:39:23 according to wikipedia 02:39:30 -!- digital_me has joined. 02:39:39 So that's... uh, what was it? 02:39:42 flip! 02:39:52 something like that 02:40:13 B = (.), C = flip 02:40:23 And W = join. 02:40:44 join? 02:40:55 http://en.wikipedia.org/wiki/B%2CC%2CK%2CW_System 02:41:17 (a -> a -> b) -> a -> b, isn't it? 02:43:54 well, but only in the Reader monad 02:45:19 Is there an equivalent whose principal type is that? 02:46:10 what? 02:46:39 -!- oklopol has quit (Remote closed the connection). 02:46:44 Like join, but not monadic, I mean. 02:46:51 -!- oklopol has joined. 02:46:57 Let's ask hoogle 02:48:01 apparently not 02:49:32 I suddenly feel an urge to combine this with set theory. 02:49:56 zzzzz 02:49:57 How can functions in lambda calculus be expressed as sets? 02:50:11 Domain theory 02:51:00 Domain theory? 02:51:15 http://en.wikipedia.org/wiki/Domain_theory 02:51:21 (BTW, Unlambda uses c for call-with-current-continuation, which produces "escape continuations".) 02:51:24 zzzzz 02:51:38 SimonRC: ? 02:52:55 It's part of unlambda's weird impure functions 02:53:26 I wonder if you can interpret SKI in hardware 02:53:29 and has nothing to do with BCKW. 02:54:01 bsmntbombdood: if you can interpret it in software, and processors interpret software... 02:54:19 ihope: you know what I mean 02:54:43 you need some kind of automatic memory allocation and garbage collection. 02:54:56 bsmntbombdood: do I? 02:55:34 there are plenty of functional virtual machines, i am sure some of them could be hardware implemented. 03:03:13 -!- goban has quit (Remote closed the connection). 03:04:36 here is a design from '86: http://content.ohsu.edu/cgi-bin/showfile.exe?CISOROOT=/etd&CISOPTR=127 03:05:18 -!- goban has joined. 03:09:09 loooong 03:40:54 -!- Sgeo has joined. 04:22:29 longcat is 04:23:16 thinporcupine 04:28:07 -!- ihope has quit ("http://tunes.org/~nef/logs/esoteric/06.08.09"). 04:45:51 -!- digital_me has quit ("leaving"). 05:12:35 SII(S(KK)(SII)) 05:14:40 = V 05:15:48 yep 05:19:39 combinatory calculus is fun 05:19:58 who would want to give names to arguments? 05:22:03 -!- crathman has quit (Read error: 110 (Connection timed out)). 05:23:35 ooh fun 05:23:38 S(K(SI))(S(KK)I) 05:24:00 S(K(SI))K even 05:53:47 I have a wonder. 05:54:22 It's a miracle! 05:54:43 Excuse me, I think I got my tongue stuck in my cheek. 05:55:01 Is it possible to have a language that uses S,K,I, but doesn't have any explicit order of application symbols? 05:55:16 *turing complete language 05:56:30 Given that combinators aren't commutative... 05:57:40 i guess that's a no 06:01:03 s/S,K,I/any combinators/ 06:02:11 some kind of structure is necessary. 06:02:32 with the X combinators it's possible to define S and K if xyz is x(y(z)) 06:03:10 iota too 06:03:51 if you can define S and K then you still need to keep the order of those. 06:04:00 yeah 06:04:22 you can dispense with some of the order. 06:04:33 in other calculi 06:05:09 The pi-calculus for example, independent processes whose order doesn't matter. 06:05:23 But those aren't combinator based that I know of. 06:05:38 never heard of pi-calculus 06:06:08 It's sort of a lambda calculus for concurrent programming. 06:07:40 -!- crathman has joined. 06:08:49 And there are calculi inspired by chemical processes. Instead of ordering, there is a distinction between active and inert data. 06:10:03 but if you had no structure what so ever, and say something called S,K and I: 06:10:20 then the only thing mattering would be the number of each. 06:10:47 Not much to base computation on. 06:11:00 yeah 06:18:09 -!- Sgeo has quit ("Leaving"). 06:44:25 -!- crathman has quit (Read error: 110 (Connection timed out)). 06:52:48 -!- oerjan has quit ("leaving"). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:08:53 -!- Arrogant has quit (Read error: 104 (Connection reset by peer)). 08:18:03 VVVVVVV 08:19:44 why does unlambda have V? 08:21:44 why not? 08:22:17 because it's stupid? 08:22:26 it's not stupid 08:22:34 why not? 08:22:34 it's a convenient shortcut, like i 08:23:19 v is bottom, no? 08:23:33 er, no 08:23:38 er, yes, it is 08:24:16 bottom? 08:24:37 _|_ 08:26:07 bottom is the bottom of an infinite loop :) 08:28:32 I don't see any applications of V 08:31:44 it could be a primitive exception mechanism 08:32:05 for example, division by zero would return v 08:35:03 hmmm 08:51:36 -!- nazgjunk has joined. 09:18:17 -!- sebbu has joined. 12:20:05 -!- tgwizard has joined. 12:20:26 -!- voodooattack has joined. 13:26:11 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)). 13:26:41 -!- nazgjunk has joined. 13:42:28 -!- crathman has joined. 13:51:32 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)). 13:51:53 -!- nazgjunk has joined. 14:01:37 -!- tgwizard has quit (Remote closed the connection). 15:10:42 -!- helios24 has quit (Read error: 60 (Operation timed out)). 15:21:16 -!- crathman has quit (Read error: 104 (Connection reset by peer)). 15:21:51 -!- crathman has joined. 15:51:55 -!- sebbu has quit ("reboot time soon"). 16:09:50 -!- helios24 has joined. 16:23:10 -!- goban has quit (Connection timed out). 16:23:31 -!- goban has joined. 16:28:59 -!- sebbu has joined. 16:31:24 -!- helios_ has joined. 16:32:08 -!- helios24 has quit (Read error: 110 (Connection timed out)). 16:57:55 -!- crathman_ has joined. 16:58:09 -!- crathman has quit (Read error: 104 (Connection reset by peer)). 16:58:10 -!- crathman_ has changed nick to crathman. 17:01:51 -!- goban has quit (Read error: 104 (Connection reset by peer)). 17:01:54 -!- goban has joined. 17:14:18 -!- helios_ has quit ("Leaving"). 17:17:34 -!- crathman_ has joined. 17:27:30 -!- crathman_ has quit ("Chatzilla 0.9.77 [Firefox 2.0.0.1/2006120418]"). 17:30:01 -!- crathman has quit (Read error: 110 (Connection timed out)). 17:33:14 -!- calamari has joined. 17:41:16 -!- goban has quit (Connection timed out). 17:41:34 -!- goban has joined. 18:07:05 -!- crathman has joined. 18:09:49 -!- Sgeo has joined. 18:30:08 -!- sebbu2 has joined. 18:35:19 -!- calamari has quit (Read error: 104 (Connection reset by peer)). 18:49:11 -!- sebbu has quit (Read error: 110 (Connection timed out)). 18:49:49 -!- calamari has joined. 19:08:11 -!- sebbu2 has changed nick to sebbu. 19:19:45 hmm 19:20:57 Currying is the tautology: ((A & B) -> C) -> (A -> (B -> C)) 19:20:58 heh 19:23:24 also, IIRC, S is (p -> q -> r) -> ((p -> q) -> (p -> r) 19:24:23 yeah, that's right 19:24:49 also K is p -> q -> q and I is p -> p 19:25:07 which means that S-K-I corresponds to that logic I can't remember the name of 19:25:55 hmm, Y = SII, so 19:37:53 -!- goban has quit (Remote closed the connection). 19:38:07 -!- goban has joined. 19:39:49 -!- voodooattack has quit. 20:37:51 ((A & B) -> C) -> (A -> (B -> C)) ? 20:37:54 what's that mean? 20:38:04 Y isn't SII 20:38:18 (SII)x = xx 20:39:17 Y = SII \f.\x.x(fx) 20:40:10 i think 20:41:15 -!- UpTheDownstair has joined. 20:41:29 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)). 20:43:25 -!- UpTheDownstair has changed nick to nazgjunk. 20:44:00 Y=SII(S(K(SI))I) 20:44:17 by abstraction elimination 20:57:09 -!- nazgjunk has quit ("night silly sheep"). 20:57:30 hmm that doesn't seem right 20:58:08 because (S(K(SI))I) is SI 20:58:20 so that would mean Y=SII(SI) 20:58:29 I wouldn't know. 21:00:06 SII(SI)x == (SI)(SI)x == Ix(SIx) == x(SIx) 21:00:08 hmmm 22:03:42 stupid haskell and its typeness 22:51:23 -!- ihope has joined. 22:51:48 -!- sebbu2 has joined. 22:54:38 ~exec self.ihope = IRCbot("80.32.164.76", "bot", "nope", "ihope", "Now 100% Real", 9999, "#lobby", True, ["#lobby"], "#", True); self.ihope.listen() 23:03:42 #exec self.ihope = 3 23:04:03 ~exec self.ihope = 3 23:04:23 Well, that sure didn't kill it, did it? 23:04:26 ~exec self.ihope.raw("QUIT") 23:08:35 -!- digital_me has joined. 23:10:21 -!- sebbu has quit (Read error: 110 (Connection timed out)). 23:26:29 sweet, the calculi of lambda conversion got here 23:30:11 -!- ihope has quit (Read error: 131 (Connection reset by peer)). 23:42:29 -!- SevenInchBread has changed nick to CakeProphet. 23:53:59 uuuuh 23:54:20 this book defines Snfx as f(nfx) 23:54:22 -!- sebbu2 has changed nick to sebbu.