←2008-01-12 2008-01-13 2008-01-14→ ↑2008 ↑all
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 <RodgerTheGreat> so, what's everyone up to tonight
01:26:47 <oklopol_> chillin'
01:26:49 -!- Jontte has quit ("Konversation terminated!").
01:26:55 <oklopol_> 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 <ihope> Unification?
01:30:30 <ihope> Like figuring out the type of ab given the types of a and b?
01:30:43 <faxlore> 1 sec
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:31:59 <ihope> Sounds like it.
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:10 <oklopol_> :D
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:30 <faxlore> hmm
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:39:56 <faxlore> oh.. I see
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:45:43 <RodgerTheGreat> I can see Rubik's and Rush Hour
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:09:36 <RodgerTheGreat> erm... I don't see how that would be useful
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:13:17 <RodgerTheGreat> wait, wait, wait
02:13:51 <RodgerTheGreat> I question the logic of that assertion
02:14:09 <ihope> The assertion that the set of real numbers is countably infinite?
02:14:35 <ihope> Or your assertion?
02:14:44 <RodgerTheGreat> I'm thinking.
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.
04:10:19 <oklofok> '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 <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:34 <oklofok> redistributed?
15:01:43 <oklofok> like multiplied all around the code
15:02:20 <oklofok> if so, it's trivial
15:02:21 <oklofok> is it so?
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:03 <oklofok> and _ is the input oper?
15:03:06 <Slereah> Yes.
15:03:10 <oklofok> function
15:03:17 <oklofok> okay... well, one possibility is this
15:03:25 <oklofok> each time you evaluate an input function
15:03:29 <oklofok> it reads the input byte
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:03:39 <oklofok> and stores what that was
15:04:02 <oklofok> sorry, lag.
15:04:03 <oklofok> okay
15:04:20 <oklofok> actually, my scheme doesn't work
15:04:22 <oklofok> forget about it
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:04 <oklofok> for that input problem
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:33:27 <oklofok> *-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 <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:47:56 <oklofok> oh...
15:47:59 <oklofok> what's that?
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:50:34 <slereah_> `ma conv. `aa
15:50:39 <slereah_> It's quite useful
15:51:33 <oklofok> oh, sii
15:51:57 <oklofok> fun guy to chat with, if you like yourself
15:52:46 <slereah_> Well, I do like myself.
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 _
15:56:34 <slereah_> And work from there.
15:58:06 * slereah_ wikis for monads
16:11:03 <oklofop> monads are a simple concept that is impossible to explain in any way.
16:11:13 <oklofop> no way in the world
16:11:14 <oklofop> period.
16:12:07 <oklofop> oh, right, i was supposed to go ->
16:12:08 <oklofop> cya
16:17:57 <slereah_> 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 <RodgerTheGreat> howdy, folks
22:08:14 <oklopol> hies
22:08:27 <RodgerTheGreat> hey, oklopol
22:09:04 <oklopol> heiß
22:09:11 <oklopol> took a while to find that
22:09:17 <oklopol> was on "b"
22:09:24 <RodgerTheGreat> yeah, it kinda makes sense
22:09:41 <oklopol> well, it's "sz"
22:09:46 <RodgerTheGreat> option+S = ß for me, which makes more sense
22:09:49 <oklopol> but indeed, it does look like a b
22:09:50 <RodgerTheGreat> "ss" in german
22:09:56 <RodgerTheGreat> it's actually a Beta
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:30 <oklopol> never realized xD
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:11:17 <RodgerTheGreat> Groß <-> Gross, depending on your spelling convention
22:11:51 <oklopol> you know german?
22:11:52 <oklopol> vie viel?
22:11:54 <oklopol> *wie
22:11:57 <oklopol> lol, i fail :)
22:12:07 <RodgerTheGreat> Nicht so viel
22:12:18 <oklopol> verstehst du aber?
22:12:33 <RodgerTheGreat> Iche lerne Deutsch im Schule für drei jahre.
22:13:00 <oklopol> ich hab deutsch in der schule seit drei jahren gelernt, i think
22:13:23 <RodgerTheGreat> Und ja, ich verstehe.
22:13:34 <RodgerTheGreat> "ich denke"
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:27 <RodgerTheGreat> yeah, that is most of it
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:25 <oklopol> yeah, think so too.
22:15:31 <RodgerTheGreat> spelling is much more consistent than english, so that part isn't too bad
22:15:44 <oklopol> hmm?
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:14 <RodgerTheGreat> As the germans would say, Wortstellung.
22:17:17 <RodgerTheGreat> Word order
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:20 <oklopol> as is NORWEGIAN
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:20:54 <oklopol> ->
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.
←2008-01-12 2008-01-13 2008-01-14→ ↑2008 ↑all