00:15:53 -!- oklopol_ has joined. 00:51:36 -!- jix has joined. 01:23:45 -!- RodgerTheGreat has joined. 01:26:12 -!- jix has quit ("CommandQ"). 01:26:18 so, what's everyone up to tonight 01:26:47 chillin' 01:26:49 -!- Jontte has quit ("Konversation terminated!"). 01:26:55 like every night 01:29:30 * faxlore wants to write a theorem prover that uses unification but doesn't know how to :S 01:29:57 Unification? 01:30:30 Like figuring out the type of ab given the types of a and b? 01:30:43 1 sec 01:31:32 given two formulas e1, e2 and a logic.. any substitution ø for the free variables in e1 and e2 such that øe1 = øe2 is a unifier 01:31:59 Sounds like it. 01:32:10 it sounds a good idea but I have no idea how ot do this :D 01:32:21 What gives you the idea? 01:33:54 how does this prove a theorem? 01:34:07 oklopol.. that's what I don't know 01:34:10 :D 01:34:30 do you know it does prove a theorem, or did you just make a guess? 01:34:40 I think someone said it can be used to 01:36:02 -!- oklopol has quit ("for the need to encumber"). 01:36:11 I guess I'd convert to a logic where you have a couple simple axioms and modus ponens as the one rule of inference. 01:37:59 yeah, you've always been a bit of an oddball 01:38:09 -!- oklopol_ has changed nick to oklofok. 01:38:15 Make a -> b, a |- b your rule of inference and (a -> b -> c) -> (a -> b) -> a -> c, a -> b -> a, F -> a and ((a -> b) -> a) -> a your axioms? 01:39:30 hmm 01:39:36 does F -> a have to be an axiom? 01:39:52 How else are you going to represent falsehood? 01:39:54 I thought there was some way to prove it 01:39:56 oh.. I see 01:43:26 Also, I have this odd feeling that the Rubik's cube, the Rush Hour puzzle, and knots are all instances of the same general concept. 01:45:29 can you link those if you have them open 01:45:35 it's so hard opening a browser 01:45:43 I can see Rubik's and Rush Hour 01:47:00 I was thinking about how I'd go about solving a Rubik's cube from a naive standpoint once, and I started by making a data structure that represents the cube. It's like 6 circularly linked lists that share edges 01:47:57 Rubik's and Rush hour are both about making a series of moves to make specific changes in a pattern, and then reversing most of those moves so that only the desired changes remain 01:48:26 Ah, good way of putting it. 01:49:14 I guess it's not knots so much as braids. Braids form a simple noncommutative group, so the braid a * b * c * d * c' * b' * a' might... be something. 01:50:28 umm... of course they're about taking a sequence of complex permutations and finding compound permutations that are simpler so you can find the solution 01:50:41 i assumed a deeper similarity 01:51:36 I guess it's not all that deep. They're noncommutative groups. 02:06:27 Now all we have to do is prove all noncommutative groups isomorphic! >:-) 02:06:41 Er, countably infinite ones. 02:07:10 Or at least find a countably infinite group that all other countable groups are subgroups of. 02:09:36 erm... I don't see how that would be useful 02:10:41 and besides, an infinite set that contained all countably infinite sets with a given property would by definition be countably infinite itself 02:11:24 I am quite familiar with the meaning of countably infinite. 02:12:35 An infinite set containing all countably infinite sets with a given property is countably infinite? 02:12:58 One real number can be expressed as a countably infinite set; therefore, the set of real numbers is countably infinite. 02:13:17 wait, wait, wait 02:13:51 I question the logic of that assertion 02:14:09 The assertion that the set of real numbers is countably infinite? 02:14:35 Or your assertion? 02:14:44 I'm thinking. 02:16:26 alright, the flaw in my reasoning above was that I *ASSUMED* that "all countably infinite sets with a given property" is itself a countably infinite group- that's circular reasoning, or at best a tautology. 02:46:44 -!- ihope has quit (Read error: 110 (Connection timed out)). 02:48:33 -!- calamari has joined. 03:02:45 -!- RodgerTheGreat has quit. 03:32:19 -!- Corun has quit ("This computer has gone to sleep"). 03:35:37 -!- pikhq has quit (Read error: 104 (Connection reset by peer)). 03:39:16 -!- pikhq has joined. 03:56:36 -!- GreaseMonkey has joined. 04:10:19 'night 07:22:51 -!- calamari has quit ("Leaving"). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 09:05:43 -!- GreaseMonkey has quit ("Hi Im a qit msg virus. Pls rplce ur old qit msg wit tis 1 & hlp me tk ovr th wrld of IRC. Man who run behind car get exhausted"). 10:04:46 -!- oerjan has joined. 10:32:12 -!- oerjan has quit ("leaving"). 10:43:10 -!- slereah_ has quit (Read error: 104 (Connection reset by peer)). 11:16:10 -!- jix has joined. 11:55:07 -!- Corun has joined. 12:22:48 -!- Slereah has joined. 12:53:22 -!- Jontte has joined. 13:04:21 -!- RedDak has joined. 13:37:50 -!- ihope has joined. 13:49:23 -!- Corun_ has joined. 13:50:41 -!- Corun has quit (Read error: 104 (Connection reset by peer)). 13:57:51 -!- Corun_ has quit ("This computer has gone to sleep"). 14:07:40 -!- timotiis has joined. 14:13:56 -!- ihope has quit ("ChatZilla 0.9.79 [Firefox 2.0.0.11/2007112718]"). 14:51:06 -!- RedDak has quit (Remote closed the connection). 14:59:45 What would be a simple way to avoid the input combinator in mah lazy language getting redistributed through the code before it's evaluated? 15:01:34 redistributed? 15:01:43 like multiplied all around the code 15:02:20 if so, it's trivial 15:02:21 is it so? 15:02:28 -!- jix has quit ("CommandQ"). 15:02:45 Well, for instance, if there's ```sAB_, I'll end up with ``A_`B_ 15:03:03 and _ is the input oper? 15:03:06 Yes. 15:03:10 function 15:03:17 okay... well, one possibility is this 15:03:25 each time you evaluate an input function 15:03:29 it reads the input byte 15:03:33 I didn't think of it first, but then I ended up with demands of input during all the program's execution. 15:03:39 and stores what that was 15:04:02 sorry, lag. 15:04:03 okay 15:04:20 actually, my scheme doesn't work 15:04:22 forget about it 15:04:37 I was thinking maybe using the delta sort-of combinator. 15:04:50 why should it not be redistributed? 15:05:17 Well, for instance, suppose I have a program C and some input. 15:05:44 I'd like to have just one input i so that it's `Ci 15:06:17 But since it's lazy, the input operator might be evaluated multiple times, or at wrong places. 15:07:00 Which is pretty much what happened with my print-n-times-*-and-decrease-n program 15:08:08 -!- jix has joined. 15:11:25 -!- Corun has joined. 15:14:22 It was (^x^y (print it n times if n>0 else terminate)y (xx pred(y))) (^x^y (print it n times if n>0 else terminate)y (xx pred(y))) IIRC. 15:14:58 So the _ was distributed at least twice. 15:17:08 -!- Slereah has changed nick to slereah_. 15:29:54 why, you need the m combinator, of course! 15:30:04 for that input problem 15:30:16 -!- jix has quit (Nick collision from services.). 15:30:18 -!- jix__ has joined. 15:33:17 slereah_: you could have an x-combinator, or the strict combinator 15:33:26 whose only purpose is to evaluate a input! 15:33:27 *-a 15:33:57 * oklofok has a lot of great ideas 15:39:48 -!- jix__ has quit (Nick collision from services.). 15:39:54 -!- jix has joined. 15:40:31 oklofok: : I was trying pretty hard to avoid an anti-d operator 15:40:50 Which would make it BIZARRO UNLAMBDA 15:41:44 well, there's always the possibility of just making the m combinator 15:43:15 * oklofok waits for someone to ask what it is, so he can tell the punchline 15:43:25 and don't you start guessing! 15:44:53 rush hour is a different game from what i recalled, btw, the game i thought of had a much more obvious connection to rubik's cubes 15:45:31 not that either of the people in the conversation were here. 15:47:42 Well, I already have an m combinator :( 15:47:56 oh... 15:47:59 what's that? 15:48:25 it's kinda obvious what i meant, a monad combinator that is! 15:49:53 I once had the wiki page on monad open, but never read it! 15:50:08 The only monads I know of are the 0 dimensional topological objects. 15:50:25 My m combinator is the Mockingbird one. 15:50:34 `ma conv. `aa 15:50:39 It's quite useful 15:51:33 oh, sii 15:51:57 fun guy to chat with, if you like yourself 15:52:46 Well, I do like myself. 15:53:45 they say that's a good thing 15:53:58 -!- oklofok has changed nick to oklofop. 15:54:42 oerjan should come in and tell us how a monad combinator should behave (although it would probably not be a combinator) 15:55:45 One of my idea was to use the delta dude, the one that can make the difference between two lambda expressions (considered the same if they only differ by an alpha conversion) 15:56:28 Like maybe a test such as (delta _) C, to return k or `ki if C is or isn't _ 15:56:34 And work from there. 15:58:06 * slereah_ wikis for monads 16:11:03 monads are a simple concept that is impossible to explain in any way. 16:11:13 no way in the world 16:11:14 period. 16:12:07 oh, right, i was supposed to go -> 16:12:08 cya 16:17:57 Bai 16:42:15 -!- tesseracter has quit (Read error: 110 (Connection timed out)). 18:15:28 -!- slereah_ has changed nick to Slereah. 18:20:08 -!- cherez has quit ("Leaving."). 18:43:58 -!- faxlore has quit ("If there are any aliens, time travellers or espers here, come join me!"). 19:26:51 -!- GreaseMonkey has joined. 19:58:15 -!- Slereah has changed nick to slereah_. 20:47:11 -!- RedDak has joined. 21:05:17 -!- bsmntbombdood has quit (Read error: 110 (Connection timed out)). 21:05:41 -!- bsmntbombdood has joined. 21:30:24 -!- jix has quit ("CommandQ"). 21:47:49 -!- oklopol_ has joined. 21:50:54 -!- oklofop has quit ("for the need to encumber"). 21:51:02 -!- oklopol_ has changed nick to oklopol. 21:57:16 -!- RedDak has quit (Remote closed the connection). 22:07:07 -!- RodgerTheGreat has joined. 22:07:15 howdy, folks 22:08:14 hies 22:08:27 hey, oklopol 22:09:04 heiß 22:09:11 took a while to find that 22:09:17 was on "b" 22:09:24 yeah, it kinda makes sense 22:09:41 well, it's "sz" 22:09:46 option+S = ß for me, which makes more sense 22:09:49 but indeed, it does look like a b 22:09:50 "ss" in german 22:09:56 it's actually a Beta 22:10:08 yeah, but they say "es tset" 22:10:27 well, indeed, it's the same char as beta 22:10:30 never realized xD 22:10:52 that's the name of the symbol in german, not the sound 22:11:11 i know i know, just explained why i said "sz" instead the "ss" 22:11:17 Groß <-> Gross, depending on your spelling convention 22:11:51 you know german? 22:11:52 vie viel? 22:11:54 *wie 22:11:57 lol, i fail :) 22:12:07 Nicht so viel 22:12:18 verstehst du aber? 22:12:33 Iche lerne Deutsch im Schule für drei jahre. 22:13:00 ich hab deutsch in der schule seit drei jahren gelernt, i think 22:13:23 Und ja, ich verstehe. 22:13:34 "ich denke" 22:14:01 ich bin viel besser grammar zu bessern, als selbst was sprechen... 22:14:19 mostly been learning grammar 22:14:25 i have no idea about vocabulary :D 22:14:27 yeah, that is most of it 22:14:39 what is most of what, though? 22:14:54 the nice thing is that german grammar is close enough to english that people will be able to understand what you mean even if you screw up a little 22:15:15 vocabulary is most of learning the language, in my opinion 22:15:17 heh, finnish is closer in many aspects though :) 22:15:25 yeah, think so too. 22:15:31 spelling is much more consistent than english, so that part isn't too bad 22:15:44 hmm? 22:15:45 and for simple sentences, the grammar is almost exactly like English. 22:15:56 spelling is more consistent in english than german? 22:16:41 well, for simple sentences, every language is pretty much the same ;) 22:16:51 what aspect of grammar you mean? 22:17:14 As the germans would say, Wortstellung. 22:17:17 Word order 22:17:27 oh, that's much closer in finnish than german. 22:17:40 that's the one thing germans have that's weird in their grammar 22:17:58 -!- immibis has joined. 22:18:08 if you'd learn, say, swedish, you'd see it's almost exactly the same 22:18:20 as is NORWEGIAN 22:18:28 i love highlighting oerjan. 22:20:52 i think i'll go to sleep early today, you keep the sails up and head for north 22:20:54 -> 22:46:20 -!- Jontte has quit ("Konversation terminated!"). 23:09:17 -!- timotiis has quit ("leaving"). 23:59:38 -!- lament has quit (Remote closed the connection). 23:59:47 -!- lament has joined.