00:00:26 <oerjan> messed up at the start
00:07:18 <oerjan> nope, there is no shorter than six X'x
00:08:50 <oerjan> i have missed some cases
00:12:19 <bsmntbombdood> for P it makes sense but I don't understand the K part
00:13:42 -!- ShadowHntr has quit (Client Quit).
00:14:36 <oerjan> ok now i think i have all 5 X cases, still no I
00:29:44 <bsmntbombdood> apparently some guy named "Rosser" came up with X = \x.xKSK
00:30:06 <oerjan> probably the Rosser of the Church-Rosser theorem
00:32:23 <oerjan> http://en.wikipedia.org/wiki/J._Barkley_Rosser
00:45:33 -!- crathman has joined.
01:30:07 <bsmntbombdood> I wonder if there's an X such that XX = S and X(XX) = K
01:42:12 -!- Arrogant has joined.
01:42:47 <oerjan> Senatus PopulusQue Romanum
01:47:04 <oerjan> ok, P=I, R=KK, Q=K(K(KS))
01:48:50 <oerjan> what should X look like then?
01:51:15 <oerjan> =K(KS)(K(K(KS)))(KK)=KS(KK)=S
01:52:17 <oerjan> that was the point of that Q
01:54:22 <oerjan> aha. then XX=XPQR=PPQRQR=S and X(XX)=XS=SPQR=K
01:54:58 <oerjan> and here i thought your equations looked arbitrary.
01:55:15 <oerjan> or at least complicated.
02:01:48 <oerjan> you cannot have XX=V and XV!=V, I think.
02:02:09 <oerjan> so XX and X(XX) cannot be chosen arbitrarily.
02:04:02 -!- ihope has joined.
02:04:21 <ihope> ~exec self.raw("JOIN #math\r\nPRIVMSG #math :zomg bot")
02:04:41 <ihope> ~exec self.raw("PART #math")
02:05:02 <oerjan> 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:41 <oerjan> 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:27 <ihope> Unlambda's v operator?
02:06:38 <ihope> If that's it, you really don't want XX=V.
02:07:17 <oerjan> you might want to try and solve XX=A, X(XX)=B for A, B arbitrary
02:07:39 <bsmntbombdood> this method needs the number of arguments that B takes
02:07:54 <ihope> 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:30 <oerjan> that's essentially what i think too
02:09:13 <oerjan> although not entirely.
02:09:27 <ihope> Then again, maybe I'm wrong for the "if it pays any attention to its first argument" case.
02:09:28 <oerjan> you could have XV=KV, say
02:09:59 <ihope> Well, KV is... well, it's V.
02:09:59 <oerjan> yeah, it's more subtle than that.
02:10:25 <ihope> X could simply pass its first argument on as arguments to other things.
02:10:27 <oerjan> you could have XV=\y.yV
02:10:51 <ihope> Therefore, XVX = XV, which... hmm.
02:13:11 <oerjan> V essentially takes an infinite number of arguments, yes. It doesn't have what is called a "head normal form"
02:14:10 <ihope> ...What is a head normal form, exactly?
02:14:14 <oerjan> And in a sense every combinator which doesn't is semantically equivalent.
02:14:50 <ihope> I guess one could say V is equivalent to (\x.xx)(\x.xx)...
02:15:12 <oerjan> It's \v1v2...vn.v E1E2...Em
02:15:59 <oerjan> The first expression inside the lambda must be a variable.
02:18:54 <oerjan> 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:24:44 <oerjan> 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:29:09 <oerjan> Good, then I won't have to go to that snail ircbrowse
02:30:25 <oerjan> actually i could have gone to tunes, they are much quicker but poorer formatting.
02:32:06 <oerjan> I wonder why meme/ircbrowse has become so slow. Too much growth?
02:36:18 <oerjan> nah, looks pretty minimal
02:36:39 <ihope> S(Kx)yz = Kxz(yz) = x(yz)?
02:37:33 <oerjan> you could reduce it with either B or C, I never remember which is which
02:37:52 <ihope> C is composition, isn't it?
02:38:16 <ihope> Hey, S(KS)K = C, even... right?
02:39:30 -!- digital_me has joined.
02:39:39 <ihope> So that's... uh, what was it?
02:41:17 <ihope> (a -> a -> b) -> a -> b, isn't it?
02:43:54 <oerjan> well, but only in the Reader monad
02:45:19 <ihope> Is there an equivalent whose principal type is that?
02:46:39 -!- oklopol has quit (Remote closed the connection).
02:46:44 <ihope> Like join, but not monadic, I mean.
02:46:51 -!- oklopol has joined.
02:49:32 <ihope> I suddenly feel an urge to combine this with set theory.
02:49:57 <ihope> How can functions in lambda calculus be expressed as sets?
02:51:15 <oerjan> http://en.wikipedia.org/wiki/Domain_theory
02:51:21 <SimonRC> (BTW, Unlambda uses c for call-with-current-continuation, which produces "escape continuations".)
02:52:55 <oerjan> It's part of unlambda's weird impure functions
02:53:29 <oerjan> and has nothing to do with BCKW.
02:54:01 <ihope> bsmntbombdood: if you can interpret it in software, and processors interpret software...
02:54:43 <oerjan> you need some kind of automatic memory allocation and garbage collection.
02:54:56 <ihope> bsmntbombdood: do I?
02:55:34 <oerjan> 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 <oerjan> 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:40:54 -!- Sgeo has joined.
04:28:07 -!- ihope has quit ("http://tunes.org/~nef/logs/esoteric/06.08.09").
04:45:51 -!- digital_me has quit ("leaving").
05:22:03 -!- crathman has quit (Read error: 110 (Connection timed out)).
05:54:43 <oerjan> Excuse me, I think I got my tongue stuck in my cheek.
05:55:01 <bsmntbombdood> Is it possible to have a language that uses S,K,I, but doesn't have any explicit order of application symbols?
05:56:30 <oerjan> Given that combinators aren't commutative...
06:02:11 <oerjan> some kind of structure is necessary.
06:02:32 <bsmntbombdood> with the X combinators it's possible to define S and K if xyz is x(y(z))
06:03:51 <oerjan> if you can define S and K then you still need to keep the order of those.
06:04:22 <oerjan> you can dispense with some of the order.
06:05:09 <oerjan> The pi-calculus for example, independent processes whose order doesn't matter.
06:05:23 <oerjan> But those aren't combinator based that I know of.
06:06:08 <oerjan> It's sort of a lambda calculus for concurrent programming.
06:07:40 -!- crathman has joined.
06:08:49 <oerjan> And there are calculi inspired by chemical processes. Instead of ordering, there is a distinction between active and inert data.
06:10:03 <oerjan> but if you had no structure what so ever, and say something called S,K and I:
06:10:20 <oerjan> then the only thing mattering would be the number of each.
06:10:47 <oerjan> Not much to base computation on.
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:22:34 <lament> it's a convenient shortcut, like i
08:26:07 <lament> bottom is the bottom of an infinite loop :)
08:31:44 <lament> it could be a primitive exception mechanism
08:32:05 <lament> for example, division by zero would return v
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:20:57 <SimonRC> Currying is the tautology: ((A & B) -> C) -> (A -> (B -> C))
19:23:24 <SimonRC> also, IIRC, S is (p -> q -> r) -> ((p -> q) -> (p -> r)
19:24:49 <SimonRC> also K is p -> q -> q and I is p -> p
19:25:07 <SimonRC> which means that S-K-I corresponds to that logic I can't remember the name of
19:37:53 -!- goban has quit (Remote closed the connection).
19:38:07 -!- goban has joined.
19:39:49 -!- voodooattack has quit.
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:57:09 -!- nazgjunk has quit ("night silly sheep").
22:51:23 -!- ihope has joined.
22:51:48 -!- sebbu2 has joined.
22:54:38 <ihope> ~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 <ihope> #exec self.ihope = 3
23:04:03 <ihope> ~exec self.ihope = 3
23:04:23 <ihope> Well, that sure didn't kill it, did it?
23:04:26 <ihope> ~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:30:11 -!- ihope has quit (Read error: 131 (Connection reset by peer)).
23:42:29 -!- SevenInchBread has changed nick to CakeProphet.
23:54:22 -!- sebbu2 has changed nick to sebbu.