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:49 -!- Jontte has quit ("Konversation terminated!").
01:29:30 * faxlore wants to write a theorem prover that uses unification but doesn't know how to :S
01:30:30 <ihope> Like figuring out the type of ab given the types of a and b?
01:31:32 <faxlore> 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:32:10 <faxlore> it sounds a good idea but I have no idea how ot do this :D
01:32:21 <ihope> What gives you the idea?
01:33:54 <oklopol_> how does this prove a theorem?
01:34:07 <faxlore> oklopol.. that's what I don't know
01:34:30 <oklopol_> do you know it does prove a theorem, or did you just make a guess?
01:34:40 <faxlore> I think someone said it can be used to
01:36:02 -!- oklopol has quit ("for the need to encumber").
01:36:11 <ihope> 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 <oklopol_> yeah, you've always been a bit of an oddball
01:38:09 -!- oklopol_ has changed nick to oklofok.
01:38:15 <ihope> 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:36 <faxlore> does F -> a have to be an axiom?
01:39:52 <ihope> How else are you going to represent falsehood?
01:39:54 <faxlore> I thought there was some way to prove it
01:43:26 <ihope> 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 <oklofok> can you link those if you have them open
01:45:35 <oklofok> it's so hard opening a browser
01:47:00 <RodgerTheGreat> 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 <RodgerTheGreat> 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 <ihope> Ah, good way of putting it.
01:49:14 <ihope> 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 <oklofok> 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 <oklofok> i assumed a deeper similarity
01:51:36 <ihope> I guess it's not all that deep. They're noncommutative groups.
02:06:27 <ihope> Now all we have to do is prove all noncommutative groups isomorphic! >:-)
02:06:41 <ihope> Er, countably infinite ones.
02:07:10 <ihope> Or at least find a countably infinite group that all other countable groups are subgroups of.
02:10:41 <RodgerTheGreat> 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 <RodgerTheGreat> I am quite familiar with the meaning of countably infinite.
02:12:35 <ihope> An infinite set containing all countably infinite sets with a given property is countably infinite?
02:12:58 <ihope> One real number can be expressed as a countably infinite set; therefore, the set of real numbers is countably infinite.
02:14:09 <ihope> The assertion that the set of real numbers is countably infinite?
02:14:35 <ihope> Or your assertion?
02:16:26 <RodgerTheGreat> 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.
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 <Slereah> 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:43 <oklofok> like multiplied all around the code
15:02:28 -!- jix has quit ("CommandQ").
15:02:45 <Slereah> Well, for instance, if there's ```sAB_, I'll end up with ``A_`B_
15:03:17 <oklofok> okay... well, one possibility is this
15:03:25 <oklofok> each time you evaluate an input function
15:03:33 <Slereah> I didn't think of it first, but then I ended up with demands of input during all the program's execution.
15:04:20 <oklofok> actually, my scheme doesn't work
15:04:37 <Slereah> I was thinking maybe using the delta sort-of combinator.
15:04:50 <oklofok> why should it not be redistributed?
15:05:17 <Slereah> Well, for instance, suppose I have a program C and some input.
15:05:44 <Slereah> I'd like to have just one input i so that it's `Ci
15:06:17 <Slereah> But since it's lazy, the input operator might be evaluated multiple times, or at wrong places.
15:07:00 <Slereah> 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 <Slereah> 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 <Slereah> So the _ was distributed at least twice.
15:17:08 -!- Slereah has changed nick to slereah_.
15:29:54 <oklofok> why, you need the m combinator, of course!
15:30:16 -!- jix has quit (Nick collision from services.).
15:30:18 -!- jix__ has joined.
15:33:17 <oklofok> slereah_: you could have an x-combinator, or the strict combinator
15:33:26 <oklofok> whose only purpose is to evaluate a input!
15:39:48 -!- jix__ has quit (Nick collision from services.).
15:39:54 -!- jix has joined.
15:40:31 <slereah_> oklofok: : I was trying pretty hard to avoid an anti-d operator
15:40:50 <slereah_> Which would make it BIZARRO UNLAMBDA
15:41:44 <oklofok> 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 <oklofok> and don't you start guessing!
15:44:53 <oklofok> 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 <oklofok> not that either of the people in the conversation were here.
15:47:42 <slereah_> Well, I already have an m combinator :(
15:48:25 <oklofok> it's kinda obvious what i meant, a monad combinator that is!
15:49:53 <slereah_> I once had the wiki page on monad open, but never read it!
15:50:08 <slereah_> The only monads I know of are the 0 dimensional topological objects.
15:50:25 <slereah_> My m combinator is the Mockingbird one.
15:51:57 <oklofok> fun guy to chat with, if you like yourself
15:53:45 <oklofok> they say that's a good thing
15:53:58 -!- oklofok has changed nick to oklofop.
15:54:42 <oklofop> oerjan should come in and tell us how a monad combinator should behave (although it would probably not be a combinator)
15:55:45 <slereah_> 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 <slereah_> Like maybe a test such as (delta _) C, to return k or `ki if C is or isn't _
16:11:03 <oklofop> monads are a simple concept that is impossible to explain in any way.
16:12:07 <oklofop> oh, right, i was supposed to go ->
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:09:49 <oklopol> but indeed, it does look like a b
22:10:08 <oklopol> yeah, but they say "es tset"
22:10:27 <oklopol> well, indeed, it's the same char as beta
22:10:52 <RodgerTheGreat> that's the name of the symbol in german, not the sound
22:11:11 <oklopol> i know i know, just explained why i said "sz" instead the "ss"
22:13:00 <oklopol> ich hab deutsch in der schule seit drei jahren gelernt, i think
22:14:01 <oklopol> ich bin viel besser grammar zu bessern, als selbst was sprechen...
22:14:19 <oklopol> mostly been learning grammar
22:14:25 <oklopol> i have no idea about vocabulary :D
22:14:39 <oklopol> what is most of what, though?
22:14:54 <RodgerTheGreat> 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 <RodgerTheGreat> vocabulary is most of learning the language, in my opinion
22:15:17 <oklopol> heh, finnish is closer in many aspects though :)
22:15:31 <RodgerTheGreat> spelling is much more consistent than english, so that part isn't too bad
22:15:45 <RodgerTheGreat> and for simple sentences, the grammar is almost exactly like English.
22:15:56 <oklopol> spelling is more consistent in english than german?
22:16:41 <oklopol> well, for simple sentences, every language is pretty much the same ;)
22:16:51 <oklopol> what aspect of grammar you mean?
22:17:27 <oklopol> oh, that's much closer in finnish than german.
22:17:40 <oklopol> that's the one thing germans have that's weird in their grammar
22:17:58 -!- immibis has joined.
22:18:08 <oklopol> if you'd learn, say, swedish, you'd see it's almost exactly the same
22:18:28 <oklopol> i love highlighting oerjan.
22:20:52 <oklopol> i think i'll go to sleep early today, you keep the sails up and head for north
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.