←2007-02-10 2007-02-11 2007-02-12→ ↑2007 ↑all
00:00:44 <oerjan> that is equivalent
00:00:50 <oerjan> essentially
00:00:55 <ihope> Tell me whether or not this Haskell program halts: main = print $ head $ filter perfect [1,3..] where perfect x = sum (divisors x) == x; divisors x = [ y | y <- [1..x-1], x `mod` y == 0 ]
00:01:07 <ihope> Or the program I meant to write, if that isn't the right one :-P
00:01:39 <bsmntbombdood> well, we know it's impossible, so this is stupid
00:02:13 <ihope> Yeah.
00:02:42 <oerjan> true, but this shows that the halting problem is somewhat connected to the existence of undecidable theorems
00:02:45 <bsmntbombdood> what about programs that don't use halt
00:03:40 <bsmntbombdood> the proof on wikipedia uses halt on a program that uses halt
00:04:12 <ihope> If Turing-machines can solve the halting problem, then "Turing machines that don't use halt" isn't Turing-complete.
00:04:26 <bsmntbombdood> i know
00:04:59 <oerjan> although i rather suspect that "this program uses halt" is undecidable, or even undefinable
00:05:22 -!- ihope_ has joined.
00:05:32 <oerjan> because you cannot decide whether a program is equivalent to halt
00:05:44 <ihope_> But since Turing machines can't solve the halting problem, "Turing machines that don't use halt" is simply all Turing machines. :-)
00:05:46 <oerjan> (even assuming it exists)
00:06:59 <bsmntbombdood> who proved that two lambda expressions couldn't be proven equivalent?
00:07:41 <oerjan> don't remember, let me see in wikipedia
00:09:10 <bsmntbombdood> Church
00:09:18 <oerjan> ah, it's Rice's theorem
00:09:35 <oerjan> ok maybe Church proved a special case
00:19:19 <ihope_> Isn't that equivalent to the halting problem?
00:19:55 <ihope_> Also, \x.x and \x.xx can't be proven equivalent. Q.E.D.
00:20:17 <oerjan> it's proven by reduction to the halting problem.
00:20:29 <oerjan> see the wikipedia page
00:21:13 <oerjan> well in _that_ case it was the Church-Rosser theorem.
00:21:49 <oerjan> which showed that _some_ expressions couldn't be proved equivalent
00:22:58 -!- ihope has quit (Read error: 110 (Connection timed out)).
00:23:19 <oerjan> i thought you meant who proved that it couldn't be decided whether two given expressions were equivalent
00:23:57 <oerjan> (as in being the same function)
00:27:16 <ihope_> ...What?
00:27:28 <oerjan> what what?
00:27:38 <ihope_> How many definitions of equivalence are there?
00:27:57 <SevenInchBread> five
00:28:06 <bsmntbombdood> bannana-grape
00:28:08 <oerjan> there is beta equivalence, beta/eta equivalence
00:28:36 <oerjan> but the Church-Rosser theorem is needed to prove each of them consistent
00:29:05 <oerjan> without it, maybe \x.x and \x.xx _could_ be turned into each other
00:29:09 <ihope_> bsmntbombdood: bananas and grapes are obsolete. Please upgrade to Cantor normal form.
00:29:15 <ihope_> :-P
00:29:22 <bsmntbombdood> cantor normal form?
00:29:47 <oerjan> cantor normal form is essentially positional notation in base omega
00:30:17 <oerjan> omega^(omega+1) + omega^1*3 + omega*3 + 5, for example
00:30:41 <oerjan> eh, *omega^2*3
00:30:51 <ihope_> Like polynomials, sort of.
00:31:00 <bsmntbombdood> whoosh
00:31:20 <ihope_> omega^a*b + omega^c*d + omega^e*f...
00:31:34 <oerjan> omega = the ordinal of the natural numbers, the first infinite one
00:31:41 <ihope_> Where a, c, e, etc. are ordinal numbers and b, d and f are natural numbers.
00:31:57 <ihope_> Bananas and grapes form a subset of the ordinal numbers, I mean.
00:32:32 <oerjan> up to omega*2, isn't it?
00:32:46 <ihope_> Something like that. I don't know.
00:33:50 <oerjan> as in, the bananas are the first omega ordinals and the grapes the next omega ordinals
00:33:59 <oerjan> or maybe it was the other way around
00:34:23 <ihope_> The other way around, I think.
00:35:08 <ihope_> Also, ordinal numbers aren't cardinal numbers. :-)
00:35:34 <oerjan> of course.
00:36:35 <oerjan> (when you know it)
00:37:55 <ihope_> Obvious iff you already know.
00:38:50 <oerjan> well, it doesn't take _that_ long to realize that omega+1 and omega have the same cardinality
00:38:55 <SevenInchBread> ....
00:39:03 <SevenInchBread> none of this makes any sense to me.
00:39:04 <SevenInchBread> at all.
00:39:08 <bsmntbombdood> me too
00:39:30 <oerjan> hm...
00:39:38 <ihope_> Essentially, an ordinal number is what I tried to get at with grapes and bananas.
00:40:06 <oerjan> do you know what a total order is?
00:40:17 <ihope_> Me?
00:40:19 <bsmntbombdood> grapes and bannanas?
00:40:23 <oerjan> no the others
00:40:33 <SevenInchBread> ooooh
00:40:37 <ihope_> bsmntbombdood: you're the one who said banana-grape. :-P
00:40:41 <SevenInchBread> ordinal - the contents of a set.
00:40:44 <oerjan> i assume you know since you know what ordinals are
00:40:44 <SevenInchBread> cardinal - the size of a set
00:40:59 <oerjan> not quite
00:41:12 <bsmntbombdood> ihope_: i was just talking about fruit
00:41:18 <oerjan> ordinal = the order type of a (well-) ordered set
00:41:54 <ihope_> Informally, an ordinal number is a set of ordinal numbers such that each of its elements' elements is an element.
00:42:10 <SevenInchBread> ...
00:42:11 <ihope_> Examples: 0 is defined as the empty set, 1 as {0}, 2 as {0,1}, 3 as {0,1,2}, etc.
00:42:13 <oerjan> that's even more confusing
00:42:22 <oerjan> the von Neumann ordinals
00:42:27 <ihope_> Not if you have no idea what an order type is :-P
00:42:28 <SevenInchBread> that's a recursive definition
00:42:33 <ihope_> Well, yes, it is.
00:42:36 <SevenInchBread> an ordinal number is a set of ordinal numbers...
00:42:42 <bsmntbombdood> {0,{0}}?
00:42:47 <ihope_> bsmntbombdood: yep.
00:42:51 <bsmntbombdood> {0,{0,{0}}}?
00:42:57 <bsmntbombdood> what's the point?
00:43:07 <ihope_> {0,{0},{0,{0}}}.
00:43:09 <SevenInchBread> I just failed Algebra 2... to give you an idea of my current level of math skills.
00:43:15 <oerjan> ouch
00:43:18 <SevenInchBread> I haven't even touched set theory... besides what I've read of it.
00:43:22 <bsmntbombdood> ouch
00:43:31 <bsmntbombdood> ihope_: what's that?
00:43:33 <ihope_> The point is that you have infinite ordinal numbers as well: omega, the first infinite ordinal number, is {0,1,2,3,4,5,6,7,8...}
00:43:34 <SevenInchBread> well... that was from laziness.
00:44:38 <bsmntbombdood> kinda like church numerals
00:44:45 <ihope_> Then the next ordinal number, omega+1, is {0,1,2,3...omega}, and omega+2 is {0,1,2,3...omega, omega+1}, omega+3 is {0,1,2,3...omega, omega+1, omega+2}.
00:45:11 <bsmntbombdood> that doesn't make sense
00:45:15 <ihope_> omega+omega or omega*2, then, is {0,1,2,3...omega, omega+1, omega+2, omega+3...}
00:45:33 <oerjan> yeah - they are used in set theory to get the natural numbers in the same way that church numerals are used to get them in lambda calculus
00:45:47 <ihope_> bsmntbombdood: is there a certain part of it that doesn't make sense, or is it just generally confusing?
00:46:04 <bsmntbombdood> the omega part
00:46:51 <ihope_> Well, omega is what you get when you go past all the natural numbers.
00:47:04 <oerjan> omega is the set of all the finite ordinals, itself infinite
00:47:08 <bsmntbombdood> what's this called so i can look it up?
00:47:14 <ihope_> An ordinal number contains all the ordinal numbers you've gone past.
00:47:25 <ihope_> bsmntbombdood: what's what called?
00:47:39 <bsmntbombdood> this ordinal-omega stuff
00:47:45 <oerjan> (transfinite) ordinal numbers
00:48:04 <bsmntbombdood> ok i have to go to dinner
00:48:38 <oerjan> btw there is a trick to remove the recursivity from the definition
00:49:21 <ihope_> An ordinal number is a set whose elements are subsets of it, and which is totally ordered under the "is an element of" operation.
00:50:29 <oerjan> i think you may want well-ordered
00:51:09 <ihope_> Totally ordered is sufficient, isn't it?
00:51:20 <oerjan> or maybe not - you get that from the axiom of foundation
00:52:34 -!- sebbu has quit ("@+").
00:53:14 <oerjan> i think it is sufficient but using well-ordered allows you not to bother with things like x = {x}
00:53:17 <ihope_> You mean the axiom of foundation has a use?
00:53:48 <oerjan> yep, without it x = {x} would be an ordinal by your definition
00:54:51 <ihope_> Wouldn't x = {x} be well-ordered anyway?
00:55:04 <oerjan> eh - good point
00:55:52 <oerjan> so you actually need to assume explicitly that x is well-founded
00:56:14 <oerjan> if you don't have the axiom of foundation
00:56:29 <oerjan> in which case total probably suffices for the order
01:02:03 -!- nazgjunk has quit ("Bi-la Kaifa").
01:33:31 * SimonRC reads up
01:35:16 * SimonRC decides that if he had a mutant power, he would be a Turing Oracle.
01:35:28 <SimonRC> (able to predict if any give Turing Machine halts)
01:38:58 <SimonRC> Hmm, bananas and grapes.... http://www.catb.org/jargon/html/O/one-banana-problem.html
01:39:16 <oerjan> This, naturally, would permit you to find out whether any mathematical hypothesis is a theorem, and by binary search to find its proof.
01:39:57 <ihope_> SimonRC: I've seen that before... :-)
01:40:07 <SimonRC> read that whole website!!!!!!
01:40:22 <ihope_> I want to be a Turing Oracle...
01:40:57 <SimonRC> failing that, you *really* must read appendix B: http://www.catb.org/jargon/html/appendixb.html
01:41:04 <SimonRC> appendix A rocks too
01:41:21 <SimonRC> oerjan: yeah, fun
01:42:29 <oerjan> actually... there might be some problems if the length of the proof is described with the Ackermann function :)
01:42:54 <oerjan> which certainly must be true for some theorems
01:43:07 <ihope_> Hmm...
01:43:18 <SimonRC> BTW, I can't see how to express that puzzle about whether "f n = if even n then f (n/2) else f (n*3+1)" always hits one for eveny starting Natural n as a halting problem
01:43:41 <ihope_> Give me a series of theorems whose proofs are longer than the corresponding values of the Ackermann function. :-)
01:44:06 <oerjan> indeed, it would seem to be in the next grape or banana
01:44:17 <SimonRC> incidentally, the busy-beaver numbers are uncomputable (in the genersal case)
01:44:18 <ihope_> SimonRC: n `div` 2, remember.
01:44:27 <SimonRC> it is pseudocode
01:44:44 <ihope_> It does a remarkably good job of being Haskell.
01:44:59 <ihope_> :-P
01:45:19 <oerjan> the question of whether _one_ number halts on 3n+1 is a halting problem.
01:45:23 <SimonRC> Haskell is almost pseudocode
01:45:40 <ihope_> There are programming languages much better than Haskell.
01:45:42 <SimonRC> oerjan: indeed
01:45:46 <SimonRC> ihope_: e.g.?
01:45:47 <ihope_> I just don't know of any. :-P
01:45:51 <SimonRC> :-(
01:46:15 <ihope_> Well, no decently fast implementations for any.
01:46:57 <SimonRC> So what are the slow ones?
01:47:02 <ihope_> I could take first-order logic, extend it to a programming language, and execute programs by brute force.
01:47:20 <ihope_> Brute-forcing proofs isn't very fast.
01:48:34 <oerjan> lessee, forall x exists n such that x_n = 1, the switch between forall and exists indicates that each loop may go up a level in the halting hierarchy
01:49:27 <SimonRC> ah, this suddenly sound familiar from my compuability theory lectures
01:49:35 <SimonRC> the "switch between forall and exists" part
01:49:44 <ihope_> Foralls and existses are nice.
01:49:46 <oerjan> yeah, it's the same as for the polynomial hierarchy
01:49:53 <SimonRC> yeah, that thing
01:49:54 <ihope_> Also known as forsomes. :-)
01:49:58 <SimonRC> fuck fuck fuck fuck fuck
01:50:08 <SimonRC> excuse the language
01:53:07 * oerjan suddenly wonders if there is an esoteric language named SOAP
01:53:47 <oerjan> nah, just an operating system
01:53:48 <ihope_> SOAP is going to be a platform for an esoteric operating system, if people ever start following my orders.
01:54:12 <ihope_> oerjan: please throw dextrose tablets at bsmnt_bot.
01:54:12 <oerjan> when Malbolge freezes over, in other words
01:54:24 <ihope_> Pff, I can do that.
01:54:31 <ihope_> ...Wait...
01:54:44 <oerjan> dextrose?
01:54:58 <ihope_> The usable form of glucose.
01:55:11 <oerjan> ~exec sys.output("Give me sugar!")
01:55:22 <oerjan> ~exec sys.stdout("Give me sugar!")
01:55:22 <bsmnt_bot> Give me sugar!
01:55:36 * ihope_ throws dextrose tablets at bsmnt_bot
01:55:55 <oerjan> I have forgotten it _every_ time except once
01:56:05 <ihope_> :-)
01:58:40 <SimonRC> ~exec sys.dlete("/")
01:58:46 <SimonRC> *cough*
01:59:06 <ihope_> ~exec sys.delete("/")
02:05:35 <SimonRC> I was deliberately not doing that
02:06:16 <SimonRC> BTW, is doing (do + ing) supposed to be spelt the same as doing (onomatapoea)?
02:06:57 <oerjan> you _do_ know that ihope is easily tempted with bsmnt_bot.
02:07:41 <oerjan> no, the latter must be spelt dhoeyng'x
02:11:09 <ihope_> D'oing.
02:13:49 <oerjan> Darn. I want to be able to combine infinite cyclic datastructures with mutable references in Haskell.
02:15:48 * ihope_ throws dextrose tablets at oerjan
02:16:08 <oerjan> yummy
02:16:18 <ihope_> IORef!
02:16:21 <ihope_> Or is it IOref?
02:16:47 <oerjan> i know, but it doesn't quite work
02:17:46 <oerjan> i cannot get an IO action to refer cleanly to an IORef which is defined later
02:18:16 <ihope_> I see.
02:19:29 <oerjan> unsafeInterleaveIO gives infinite datastructure of mutable references but not cyclic ones
02:20:24 <oerjan> and unsafePerformIO has badly defined semantics
02:31:38 <bsmntbombdood> what about bsmnt_bot ?
02:31:50 <bsmntbombdood> ihope_: you fale
02:32:07 <ihope_> ~exec throw(dextrose_tablets, bsmntbombdood)
02:32:13 <ihope_> Darn.
02:32:38 <bsmntbombdood> ~exec raise "Dextrose_tablets", "smntbombdood"
02:33:08 <ihope_> ~exec def self.dextrose(x): raw("PRIVMSG #esoteric :\001ACTION throws dextrose tablets at %s\001" % x)
02:33:15 <ihope_> Pff.
02:33:29 <ihope_> ~exec self.dextrose = lambda x: bot.raw("PRIVMSG #esoteric :\001ACTION throws dextrose tablets at %s\001" % x)
02:33:42 <ihope_> ~exec self.dextrose("bsmntbombdood")
02:33:43 * bsmnt_bot throws dextrose tablets at bsmntbombdood
02:33:52 * ihope_ throws dextrose tablets at bsmnt_bot
02:33:55 <ihope_> Not bad.
02:34:14 <bsmntbombdood> why the obbsesion with dextrose?
02:36:50 <oerjan> now they tell me at #haskell there is a fixIO.
02:42:02 <ihope_> A what?
02:42:05 <bsmntbombdood> esr is crazy
02:42:08 * ihope_ throws dextrose tablets at bsmntbombdood
02:43:42 <oerjan> fixIO :: (a -> IO a) -> IO a
02:44:00 <oerjan> to make cyclic IO actions depending on their result
02:44:48 <bsmntbombdood> cps is weird
02:45:00 <oerjan> also used with the mdo recursive monad notation
02:46:20 * oerjan invents sinistrose
02:47:24 <oerjan> being the opposite of dextrose.
02:48:13 <ihope_> mdo?
02:48:20 <ihope_> Like do, except with monads?
02:48:51 <oerjan> do is with monads
02:49:10 <oerjan> mdo vs. do is like letrec vs. let in scheme
02:49:48 <ihope_> I know nothing about Scheme.
02:50:03 <bsmntbombdood> scheme pwns haskell
02:50:47 <oerjan> in do, variables introduced with <- can only be used in later statements. in mdo they can be used in the whole mdo statement
02:50:57 <oerjan> *variables = bindings
02:51:22 <ihope_> I now know one thing about Scheme.
02:51:43 <oerjan> no you don't
02:51:48 <ihope_> Oh.
02:52:08 <oerjan> bsmntbombdood is lying :)
02:52:19 <bsmntbombdood> code as data, man!
02:52:21 <ihope_> Also, I take it this doesn't work: mdo {putStrLn x; x <- getLine}
02:52:38 <ihope_> bsmntbombdood: :-P...wait, what?
02:52:44 * ihope_ ponders
02:52:50 <bsmntbombdood> what?
02:52:54 <SevenInchBread> data as code dude!
02:53:00 <bsmntbombdood> that's why scheme is better than haskell
02:53:04 * ihope_ decides "data as code" was... darn, SevenInchBread beat me to it
02:53:12 <oerjan> nope, that would hang
02:54:25 <SevenInchBread> Well... Lisp homoiconicity makes "data as code" as well.
02:54:28 <SevenInchBread> it works both ways.
02:54:42 <bsmntbombdood> yeah
02:54:50 <bsmntbombdood> sexp!
02:54:57 <SevenInchBread> since Lisp code is just like... a parse tree.
02:56:18 <bsmntbombdood> sexp
02:59:36 <SimonRC> zzzzz
02:59:39 * SimonRC goes to bed
03:01:50 <SimonRC> oerjan: look at "mdo". It is sugar that works on any instance of MonadLoop (i.e. most Monads).
03:02:01 <SimonRC> oh, wait, you did
03:02:55 <bsmntbombdood> (> scheme haskell)
03:03:33 <SimonRC> LISPoids: code is data. Haskell: computations are data
03:03:40 <SimonRC> notice the difference
03:03:44 <SimonRC> anyway
03:03:46 <ihope_> Scheme == Haskell
03:03:46 <SimonRC> zzzzzzz
03:04:01 <oerjan> (> scheme) haskell
03:04:08 <ihope_> :-D
03:04:08 <SimonRC> lol
03:04:10 <SimonRC> zzzzzzz
03:04:22 <bsmntbombdood> sex-pee
03:04:32 <ihope_> Oh dear.
03:04:49 <ihope_> Isn't that that... stuff?
03:05:05 <bsmntbombdood> ?
03:05:16 <bsmntbombdood> what stuff
03:05:31 <bsmntbombdood> (> scheme haskell) <== sex-pee
03:05:46 <ihope_> Eew.
03:06:01 <oerjan> (> scheme) haskell <== sex-tion
03:07:03 <bsmntbombdood> '(...) <=== sex-pee
03:07:27 <bsmntbombdood> original LISP with mex-pees was ugly
03:07:56 <bsmntbombdood> ihope_: s-expression
03:07:58 <bsmntbombdood> s-exp
03:08:00 <bsmntbombdood> sexp
03:08:04 <bsmntbombdood> sex-pee
03:13:39 <bsmntbombdood> mccarthy the urophiliac
03:25:24 -!- ihope_ has quit (Connection timed out).
03:42:09 -!- oerjan has quit ("leaving").
04:03:43 -!- RodgerTheGreat has quit.
05:18:41 -!- ShadowHntr has joined.
05:24:29 -!- RodgerTheGreat has joined.
05:29:56 -!- RodgerTheGreat has quit (Read error: 113 (No route to host)).
05:30:53 -!- calamari has quit (zelazny.freenode.net irc.freenode.net).
05:30:53 -!- oklopol has quit (zelazny.freenode.net irc.freenode.net).
05:30:53 -!- GregorR has quit (zelazny.freenode.net irc.freenode.net).
05:30:53 -!- SimonRC has quit (zelazny.freenode.net irc.freenode.net).
05:30:53 -!- sekhmet has quit (zelazny.freenode.net irc.freenode.net).
05:30:53 -!- tokigun has quit (zelazny.freenode.net irc.freenode.net).
05:31:37 -!- RodgerTheGreat has joined.
05:31:57 -!- calamari has joined.
05:31:57 -!- oklopol has joined.
05:31:57 -!- GregorR has joined.
05:31:57 -!- SimonRC has joined.
05:31:57 -!- tokigun has joined.
05:31:57 -!- sekhmet has joined.
05:33:38 -!- RodgerTheGreat_ has joined.
05:33:52 -!- RodgerTheGreat has quit (Read error: 104 (Connection reset by peer)).
05:34:53 -!- RodgerTheGreat_ has quit (Client Quit).
05:35:57 -!- RodgerTheGreat has joined.
05:36:03 -!- RodgerTheGreat has quit (Client Quit).
05:37:19 -!- RodgerTheGreat has joined.
05:40:22 -!- RodgerTheGreat has quit (Client Quit).
05:41:12 -!- RodgerTheGreat has joined.
05:44:11 -!- RodgerTheGreat has quit (Client Quit).
06:02:36 -!- digital_me has quit (Connection timed out).
06:18:33 -!- calamari has quit ("Leaving").
06:25:13 -!- ShadowHntr has quit (Connection timed out).
06:52:29 -!- SevenInchBread has quit (Read error: 113 (No route to host)).
07:05:19 -!- Sgeo has quit (Read error: 104 (Connection reset by peer)).
07:05:25 -!- anonfunc has joined.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
09:12:27 -!- sebbu has joined.
10:56:01 -!- jix has joined.
10:58:18 -!- sebbu2 has joined.
11:06:39 -!- sebbu has quit (Read error: 60 (Operation timed out)).
11:10:14 -!- puzzlet has quit (Remote closed the connection).
11:11:22 -!- puzzlet has joined.
11:23:38 -!- anonfunc has quit (Read error: 60 (Operation timed out)).
11:35:15 -!- anonfunc has joined.
11:56:02 -!- helios24 has joined.
12:03:18 -!- nazgjunk has joined.
12:08:14 -!- ihope_ has joined.
12:08:24 -!- ihope_ has changed nick to ihope.
12:16:48 -!- tgwizard has joined.
12:22:59 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)).
12:23:20 -!- nazgjunk has joined.
12:37:35 -!- nazgjunk has quit (Read error: 104 (Connection reset by peer)).
12:37:40 -!- UpTheDownstair has joined.
12:38:08 -!- UpTheDownstair has changed nick to nazgjunk.
12:44:57 -!- sebbu has joined.
12:50:01 -!- sebbu2 has quit (Read error: 60 (Operation timed out)).
14:15:42 -!- helios24 has quit ("Leaving").
15:38:30 -!- UpTheDownstair has joined.
15:38:47 -!- UpTheDownstair has quit (Read error: 54 (Connection reset by peer)).
15:55:45 -!- nazgjunk has quit (Read error: 110 (Connection timed out)).
15:57:48 -!- SevenInchBread has joined.
16:04:31 -!- nazgjunk has joined.
17:03:29 -!- flagitious has joined.
17:18:33 -!- RodgerTheGreat has joined.
17:19:03 -!- RodgerTheGreat_ has joined.
17:27:30 -!- RodgerTheGreat has quit (Read error: 60 (Operation timed out)).
17:27:54 -!- RodgerTheGreat_ has changed nick to RodgerTheGreat.
18:34:16 -!- ihope has quit (Read error: 110 (Connection timed out)).
19:12:23 -!- ihope_ has joined.
19:12:35 -!- ihope_ has changed nick to ihope.
19:22:47 -!- SevenInchBread has quit (Read error: 110 (Connection timed out)).
19:29:28 -!- digital_me has joined.
20:05:08 -!- GregorR has changed nick to _D6Gregor1RFeZi.
20:17:38 * ihope throws dextrose tablets at _D6Gregor1RFeZi
20:18:28 -!- SevenInchBread has joined.
20:30:57 -!- ShadowHntr has joined.
21:01:30 -!- sebbu2 has joined.
21:20:17 -!- sebbu has quit (Connection timed out).
21:23:16 -!- Arrogant has joined.
21:34:38 -!- oerjan has joined.
21:47:47 * oerjan still wonders what the dextrose tablets are about.
21:48:14 <_D6Gregor1RFeZi> Same 'ere.
21:48:40 <_D6Gregor1RFeZi> Presumably they're placebos, but maybe I'm supposed to believe that they'll demangle me.
21:48:41 <bsmntbombdood> ~exec self.dextrose(" oerjan ")
21:48:42 * bsmnt_bot throws dextrose tablets at oerjan
21:48:57 <oerjan> wow
21:49:44 <oerjan> well dextrose is not a placebo when it comes to energy
21:50:21 <bsmntbombdood> ~exec self.dextrose(" _D6Gregor1RFeZi ")
21:50:21 * bsmnt_bot throws dextrose tablets at _D6Gregor1RFeZi
21:50:35 <ihope> Why the spaces?
21:50:41 <bsmntbombdood> tabe completion
21:50:42 <ihope> ~exec self.dextrose("_D6Gregor1RFeZi")
21:50:42 * bsmnt_bot throws dextrose tablets at _D6Gregor1RFeZi
21:50:53 <ihope> Oh.
21:52:02 -!- Arrogant has quit ("Leaving").
21:53:23 <bsmntbombdood> ~ctcp oerjan VERSION
21:54:11 <oerjan> hm... did anything happen?
21:54:28 <bsmntbombdood> yeah
21:54:42 <oerjan> i didn't see any incoming ctcp
21:54:44 <bsmntbombdood> :orwell.freenode.net 505 bsmnt_bot :Private messages from unregistered users are currently blocked due to spam problems, but you can always message a staffer. Please register! ( http://freenode.net/faq.shtml#privmsg )
21:54:53 <oerjan> oh.
21:55:00 <oerjan> anyhow i'm on irssi too
21:56:12 <oklopol> what is the tab character in html? :P
21:56:47 <oerjan> ~exec sys.stdout(r"^ *(.*[^ ]) *$" % " testing ")
21:57:22 -!- Sukoshi has joined.
21:57:33 <Sukoshi> Hey y'all.
21:57:36 <bsmntbombdood> long time no see Sukoshi
21:57:41 <Sukoshi> I know.
21:57:43 <Sukoshi> :)
21:57:56 <Sukoshi> Any Lex/Yacc wizards here?
21:58:01 <Sukoshi> Or, just Lex/Yacc users?
21:58:09 <bsmntbombdood> I've used em before
21:58:20 <oerjan> i have tried it
21:58:24 <Sukoshi> Can you use ( ) as grouping to group | ?
21:59:57 <oerjan> doesn't seem like it from "info bison"
22:01:48 <Sukoshi> Is it BNF?
22:02:00 <Sukoshi> Because I want to specify the exact repititions of something.
22:02:21 <oerjan> i guess that doesn't work because there would be no uniform way to refer to the matched tokens
22:03:50 <oerjan> you'll just have to define some helping tokens
22:04:25 <Sukoshi> I'm writing a parser for the BT bencoding, by the way.
22:05:00 <oerjan> i don't remember that one
22:05:12 <Sukoshi> I'll link it, and my Yacc file.
22:05:31 <Sukoshi> If you'd be so kind as to take a look at it and confirm if it would match correctly.
22:07:46 <Sukoshi> If this doesen't work, I write it myself. It's faster/less headache.
22:07:57 <Sukoshi> Woe to the not-pointer-arithmetic-endowed then.
22:08:16 <bsmntbombdood> pointer arithmetic is fun
22:08:25 <Sukoshi> I know, but not everyone can follow it.
22:08:44 <Sukoshi> That's why I'm choosing to use yacc/lex.
22:10:05 <oerjan> as far as i understand, | just defines a new rule with the same left side
22:10:26 <Sukoshi> It also works as or.
22:10:34 <Sukoshi> a | b != | a b
22:11:11 <oerjan> well that's what i said
22:11:46 <oerjan> a | b are two separate rules, not an expression
22:12:02 <Sukoshi> Oh, I see. Yeah.
22:12:50 <oerjan> basically it has to be this way because otherwise $1 ... $n would not refer to well-defined tokens in the rule action
22:13:05 <Sukoshi> Uggh. Now I have to decide how the C code works with the grammar.
22:13:11 <oerjan> that's my guess anyhow
22:13:51 <oerjan> where is that link you promised?
22:14:01 <Sukoshi> Well, my grammar is written up.
22:14:08 <Sukoshi> But, I have to add C code to it now.
22:15:23 <Sukoshi> http://www.anysize.org/~sukoshi/benc_parse.l http://www.anysize.org/~sukoshi/benc_parse.y
22:15:35 <Sukoshi> Havas unun bonan tempon kun tiujun.
22:15:38 <Sukoshi> *tiujn
22:16:10 <Sukoshi> *Havos :P
22:16:50 <oerjan> Dankas vin. (Maybe.)
22:17:03 <Sukoshi> Estas mian plezuron.
22:17:08 <bsmntbombdood> ?
22:17:24 <bsmntbombdood> what's this a parser for
22:17:29 <oerjan> If I got that correct it was nearly pure luck
22:17:32 <Sukoshi> Bencoding data.
22:17:38 <Sukoshi> oerjan: The ``vin'' is superfluous.
22:18:32 -!- _D6Gregor1RFeZi has changed nick to _ZN6Gregor1REd.
22:18:53 <Sukoshi> http://wiki.theory.org/BitTorrentSpecification <-- Read.
22:18:55 <bsmntbombdood> torrents?
22:18:59 <Sukoshi> Yeah.
22:20:09 -!- _ZN6Gregor1REd has changed nick to GregorR.
22:20:30 <bsmntbombdood> there's no benc_int
22:20:44 <Sukoshi> Guh. I knew I missed something.
22:21:25 <Sukoshi> benc_int: BEGINT NUMBER END ;
22:21:54 <bsmntbombdood> also you don't do anything with the values
22:22:14 <Sukoshi> <Sukoshi> Well, my grammar is written up. <Sukoshi> But, I have to add C code to it now.
22:22:25 <bsmntbombdood> oh
22:22:40 <bsmntbombdood> yacc should build a parse tree implicitly to give to you after parsing
22:22:52 <oerjan> that STRDATA rule is going to break I think.
22:23:15 <bsmntbombdood> yeah
22:23:25 <Sukoshi> Then I need to delimit it.
22:23:33 <oerjan> because it is confused with anything else
22:23:45 <oerjan> i don't quite see why you need a lex stage
22:24:09 <Sukoshi> I guess.
22:24:10 <oerjan> hm... scratch that.
22:24:28 <bsmntbombdood> yacc needs a lexer
22:24:30 <Sukoshi> But I would like to make yytext a union later on.
22:24:38 <Sukoshi> Oh?
22:26:13 <bsmntbombdood> i'm interested to see how to use that parser
22:26:16 <oerjan> the length-encoding of strings doesn't fit into a regular language definition, or context-free for that matter.
22:26:30 <Sukoshi> A custom parser then?
22:27:48 <oerjan> i am sure there is some lex rule to gulp up a fixed number of characters
22:27:59 <oerjan> *rule=method
22:28:31 <oerjan> but you need to take the number:string parsing entirely in lex
22:28:42 <bsmntbombdood> yeah
22:28:56 <Sukoshi> Oh, I see.
22:29:09 <bsmntbombdood> a string will eat up the rest of the input
22:29:10 <oerjan> which shouldn't be too difficult
22:29:52 <Sukoshi> Wait. How would you suggest I do this?
22:30:07 <Sukoshi> If I don't return the NUMBER token, then the grammar can't use NUMBER.
22:30:33 -!- jix has quit ("Bitte waehlen Sie eine Beerdigungnachricht").
22:31:16 <oerjan> you don't need the yacc stage to know that number:string has a substructure
22:31:34 <Sukoshi> Oh, durr.
22:31:41 <bsmntbombdood> how would you do that?
22:32:02 <oerjan> so just remove NUMBER and let STRING be the whole thing
22:32:13 <oerjan> or STRDATA
22:32:16 <Sukoshi> But true, how would you do it?
22:32:51 <bsmntbombdood> regexes can't match stuff like that
22:36:43 <oerjan> you can use the input() directive.
22:38:03 <Sukoshi> Can you give me an example?
22:38:20 <bsmntbombdood> what, input() reads characters in?
22:38:54 <oerjan> yep, so you could use a for loop with input() to read the required number of characters into a buffer
22:39:09 <Sukoshi> Exmpl plz :P
22:39:22 <bsmntbombdood> read()
22:40:02 <bsmntbombdood> no
22:40:09 <oerjan> i don't see any read() in the flex info
22:40:20 <bsmntbombdood> i was mistaken
22:40:33 <bsmntbombdood> "input Reads a byte from yyin"
22:40:46 <SimonRC> Wait, are we still talking about parsing BT strings here?
22:40:56 <bsmntbombdood> yea
22:40:57 <oerjan> that's the idea
22:41:02 <SimonRC> hmm
22:41:08 <SimonRC> I would use a monadic parser for that
22:41:18 <SimonRC> but yacc doesn't do monadic parsers
22:41:35 <bsmntbombdood> so you have [0-9]+: as the regex, then read in the correct number of bytes with input()
22:41:56 <oerjan> right
22:42:27 <Sukoshi> Where does the call to input() go? Lexer?
22:42:31 <bsmntbombdood> yeah
22:42:44 <SimonRC> Now a better question: Why the hell did they invent their own data encoding rather than using a standard one?
22:42:56 <bsmntbombdood> like what?
22:42:58 <Sukoshi> Their bencoding is brain-damaged.
22:43:12 <SimonRC> I can see they have there a subset of the functionality of ASN.1
22:43:27 <SimonRC> There are plenty of tools that will spit out very fast ASN.1 parsers
22:44:11 <SimonRC> It has such amazing features as being able to send the start of some data before knowing how long it is.
22:44:15 <Sukoshi> My theory is that it was a quick hack in Python.
22:44:45 <bsmntbombdood> meh
22:45:11 <oerjan> it would be a quick hack with Parsec :)
22:46:51 <oerjan> there might be another way to do it using yymore() and states
22:50:34 <oerjan> *states=start conditions
22:50:54 <bsmntbombdood> parsing is screwed up
22:51:50 <oerjan> oh wait.
22:52:06 <oerjan> the i lex rule also needs to include the number
22:52:40 <bsmntbombdood> no it doesn't
22:53:19 <oerjan> yes it does, otherwise there will be no way for lex to distinguish the number from the start of a string encoding
22:53:34 <bsmntbombdood> it doesn't need to
22:53:57 <oerjan> yes it must because it has to handle the string encoding specially
22:54:10 <oerjan> wait...
22:54:15 <bsmntbombdood> yacc just needs the tokens
22:54:41 <oerjan> it _could_ distinguish a number according to whether it is followed by :
22:54:48 <bsmntbombdood> yeah
22:55:11 <oerjan> but lex does need to know the length of the string somehow
22:56:00 -!- tgwizard has quit (Remote closed the connection).
22:56:14 <oerjan> including it in the i rule would cause earlier error detection
22:56:44 <oerjan> in the case of something like i100:
22:56:51 <bsmntbombdood> error detection is for pussies
22:57:48 <oerjan> in any case i end up with the feeling this grammar is far too simple for lex/yacc use, especially when it doesn't fit directly
22:58:22 -!- nazgjunk has changed nick to na[zZz]gjunk.
22:58:36 <oerjan> recursive descent and a switch statement might even be shorter
22:59:07 <oerjan> *would almost certainly be shorter
23:01:35 <oerjan> in fact it is practically designed to be trivial in that way
23:01:56 <bsmntbombdood> what's that?
23:02:37 <oerjan> just a simple: read the next character, switch on it to decide what to do
23:02:51 <bsmntbombdood> oh, yeah
23:03:20 <bsmntbombdood> would be pretty simple
23:08:11 * bsmnt_bot throws dextrose tablets at bsmntbombdood
23:10:54 <oerjan> one more thing - the lex parser doesn't handle negative numbers for i
23:22:24 <SimonRC> methinks that a predictive parser would be what you wanted.
23:23:22 <SimonRC> In fact, I suspect that bittorent was built before the protocol was properly written down, so there is certainly a simple parsing algorithm: that which is used by the original client.
23:24:37 -!- pikhq has joined.
23:25:18 <SimonRC> hi
23:25:33 <SimonRC> you are just in time for a predictive parsing vs. yacc flamewar
23:26:12 <bsmntbombdood> what's a predictive parser?
23:29:29 <oerjan> yacc is fine if your grammar is L(AL)R(1) but not LL(1)
23:29:56 <oerjan> but this one is nearly LL(1) at the character level
23:30:39 <SimonRC> bsmntbombdood: a parser that always knows what token type will come next.
23:30:42 <SimonRC> I think
23:30:46 <SimonRC> read the Dragon Book
23:31:21 <bsmntbombdood> how is that possible
23:31:52 <oerjan> Correction: knows what token something is after reading the first subtoken
23:32:03 <pikhq> Hear ye, hear ye! Read the Wiki!
23:32:10 <pikhq> You will sound more competent & wise.
23:32:14 <SimonRC> oerjan: maybe that, whatever
23:32:46 <oerjan> i.e. LL(1) if it is context-free
23:32:48 <SimonRC> anyway, it is a subset of most other serious parser types
23:33:08 <SimonRC> but Pascal can be parsed predictively IIRC
23:33:34 <oerjan> yes, Niklaus Wirth is known for making his grammars simple LL(1)-like
23:34:41 <oerjan> and in another note, these parsers/languages are usually the ones that one can create by hand without too much effort
23:34:55 <oerjan> using recursive descent
23:36:21 <SimonRC> Ah, of course, pascal parsers were traditionally written in Pascal, weren't they?
23:37:02 <oerjan> i think so
23:37:39 <oerjan> i think Wirth's idea was that the grammar _should_ be simple enough to write a parser manually
23:38:13 <oerjan> but of course i am as usually using my vague memory to sound competent & wise :)
23:38:33 <oerjan> *usual
23:39:43 <oerjan> but then i have always enjoyed parser theory
23:39:52 * pikhq uses an external memory enhancement at times
23:40:31 <oerjan> how many years before Wikipedia plugs directly into the brain?
23:42:22 <pikhq> With Ratpoison and Conkeror, it's close enough already.
23:43:53 -!- sebbu2 has quit ("@+").
23:45:54 -!- GregorR has changed nick to _D6Gregor1RFeZi.
23:48:21 <pikhq> Is that valid Malbolge, Gregor?
23:48:46 <SimonRC> Fe is iron and Zi is zirconium, IIRC
23:51:29 <bsmntbombdood> i'm writing a bencode parser in python
23:52:12 <pikhq> Hexadeuterium monogregor monoR moniron monozirconide?
23:53:19 <_D6Gregor1RFeZi> :P
23:53:51 <bsmntbombdood> i can't figure out how to do lists without backing up
23:53:52 <_D6Gregor1RFeZi> Seems like an unlikely chemical forumula.
23:54:05 <oerjan> map (`mod` 94) $ zipWith (+) [0::Int ..] $ map (fromEnum) "_D6Gregor1RFeZi"
23:54:18 <oerjan> gives [1,69,56,74,24,12,15,24,28,58,92,81,19,9,25]
23:54:30 <pikhq> Yeah.
23:54:31 <_D6Gregor1RFeZi> Fascinating.
23:54:42 <oerjan> which means it is probably not legal Malbolge
23:54:44 <pikhq> Hmm.
23:55:00 <pikhq> It's *perfectly* valid Brainfuck, though.
23:55:08 <pikhq> Although it's equivalent to a null program. . .
23:55:09 <_D6Gregor1RFeZi> Doesn't do much though :P
23:57:19 <_D6Gregor1RFeZi> Nobody can guess what it is? :(
23:57:44 <bsmntbombdood> ok, got lists, it's ugly though
23:57:45 <oerjan> is it an esoteric language?
23:57:51 <_D6Gregor1RFeZi> Nope
23:58:44 <oerjan> i guess with the Gregor in it it is not a chemical formula either
23:59:02 <_D6Gregor1RFeZi> Nope
23:59:08 <oerjan> what is ugly?
23:59:17 <pikhq> It's Gregorium.
23:59:20 <_D6Gregor1RFeZi> Obviously none of you mess with name mangling much :P
←2007-02-10 2007-02-11 2007-02-12→ ↑2007 ↑all