00:03:49 -!- ehird has quit.
01:09:47 -!- Gregor has quit (Remote closed the connection).
01:11:07 -!- Pthing has quit (Remote closed the connection).
01:11:37 -!- bsmntbombdood has quit (Read error: 113 (No route to host)).
01:15:23 -!- bsmntbombdood has joined.
01:24:01 -!- fax has quit ("Leaving").
03:28:41 -!- pingveno has joined.
03:39:34 -!- madbrain has joined.
04:04:31 -!- Gregor has joined.
04:19:39 -!- ineiros has quit (verne.freenode.net irc.freenode.net).
04:19:39 -!- Ilari has quit (verne.freenode.net irc.freenode.net).
04:20:05 -!- ineiros has joined.
04:20:05 -!- Ilari has joined.
05:27:40 -!- Asztal has quit (Read error: 110 (Connection timed out)).
05:30:24 -!- oerjan has joined.
05:40:49 -!- Gracenotes_ has joined.
05:43:35 -!- Gracenotes has quit (Nick collision from services.).
05:43:40 -!- Gracenotes_ has changed nick to Gracenotes.
05:55:14 -!- coppro has quit (Remote closed the connection).
05:55:48 -!- coppro has joined.
05:59:16 -!- zzo38 has joined.
06:00:50 <zzo38> When playing crap, one guy biased one of the dice to be fixed at 5 (no other numbers may be rolled). Now, you have the chance to bias the other dice using whatever probabilities you want (within range, of course). What allotment of probabilities for the second dice would make the smallest probability of winning? (assuming the first dice is fixed at 5)
06:03:08 <oerjan> (1) I don't know crap (2) Do your own homework
06:04:45 <zzo38> In case you don't know the rule of crap, here it is: You roll two dice. If the first roll makes a total of 7 or 11, you immediately win, if the first roll is 2 or 3 or 12, you immedately lose, otherwise you continue until you get the same total as at first, in which case you win, or a total of 7, in which case you lose.
06:05:08 <zzo38> It isn't my homework. I have tried it myself, but I want to see if anyone else has anything to say, too.
06:11:57 -!- zzo38 has quit ("Post laters").
06:13:18 <oerjan> hm you cannot lose at first throw with a fixed 5
06:16:50 <oerjan> 2 and 6 on the second die are special.  the rest should obviously be uniform to minimize the chance of repeating them.
06:17:56 <oerjan> well, "obviously"
06:21:07 <oerjan> 6 after the first just gives a reroll and so is ignored.  thus probability of 6 should be 0 to avoid an immediate win.
06:23:50 -!- pingveno has quit (Remote closed the connection).
06:31:32 -!- Sgeo has quit (Read error: 60 (Operation timed out)).
06:32:17 * coppro just had a bad idea
06:32:25 <oerjan> p2 + (1 - p2)*(sum_{n=1,3,4,5} pn/(p2+pn))
06:34:26 <oerjan> um wait
06:34:42 <oerjan> p2 + (1 - p2)*(sum_{n=1,3,4,5} pn^2/(p2+pn))
06:34:52 <oerjan> argh
06:35:17 <oerjan> p2 + sum_{n=1,3,4,5} pn^2/(p2+pn)
06:42:00 -!- oerjan has quit ("Hmph").
06:45:59 -!- puzzlet has quit ("leaving").
06:46:25 -!- puzzlet has joined.
06:57:36 * coppro has finally figured out the grammatical construct to ask a question, then explain why you're asking it
07:00:02 -!- FireFly has joined.
07:11:28 -!- jix has quit (Read error: 110 (Connection timed out)).
07:35:22 -!- MigoMipo has joined.
07:56:09 -!- FireFly has quit ("Later").
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:03:14 -!- madbrain has quit ("Radiateur").
08:04:59 -!- kar8nga has joined.
08:13:33 -!- MigoMipo has quit ("Page closed").
08:38:26 -!- coppro has quit (Read error: 110 (Connection timed out)).
08:41:34 -!- ais523 has joined.
08:43:22 <ais523> wow, complete spam which is presumably some sort of 419: "I am Mrs. Claire Page sending you a letter from my sickbed in the hospital. Please contact my lawyer (Bar.curtisparkinson@bentegy.com)right away for an urgent matter. God bless."
08:43:46 <ais523> (I don't see anything wrong with posting that email publicly, spammers deserve to get more spam...)
08:52:41 <fizzie> I got this particular rather different spam in three or four email addresses: http://www.flyertalk.com/forum/omni/759752-really-weird-spam-wants-wood-stove.html
08:53:02 <fizzie> (The forum is completely random, I just googled for the spam text since I deleted my copies already.)
08:54:17 <fizzie> (It wasn't completely identical to that, though, because I remember the price of the "portable wood stove" being mentioned.)
09:09:30 -!- puzzlet has quit (Remote closed the connection).
09:14:35 -!- puzzlet has joined.
09:15:05 -!- puzzlet has quit (Read error: 104 (Connection reset by peer)).
09:19:36 -!- puzzlet has joined.
09:27:04 <ais523> this is probably old news, but: apparently when RMS wants to read a web page, he emails a daemon that wgets it and emails him back with the resulting page
09:36:50 -!- jix has joined.
10:18:10 -!- ais523 has quit (Read error: 110 (Connection timed out)).
11:01:15 -!- ais523 has joined.
11:06:44 <oklopol> i got a question wrong at the automata exam, someone kill me
11:06:55 <oklopol> fucking trivial rookie mistake
11:17:53 <ais523> the occasional mistake isn't /that/ bad...
11:22:09 <oklopol> but what if i have four more mistakes like it in this midterm, and the other one together, and not get a 5/5
11:22:22 <oklopol> i would probably get a stroke
11:22:46 <oklopol> WHAT IF ALL MATHEMATICS IS WRONG, WHAT IF EVERYONE MADE A MISTAKE
11:22:54 <oklopol> calm down, calm down
12:16:17 <ais523> <Ubuntu updates> "Disable DST switch for Argentina tomorrow, as the Argentia government decided yesterday. Careful planning is boring."
12:16:28 * ais523 wonders how quickly the other OSes will get that particular bit of political information...
12:26:53 -!- sebbu2 has joined.
12:28:21 -!- puzzlet has quit (Remote closed the connection).
12:28:36 -!- puzzlet has joined.
12:31:12 <lifthrasiir> ais523: is that change postponed? (iirc from tz list)
12:31:26 <ais523> I'm not sure of the details
12:31:39 <ais523> presumably if you really cared about argentinian daylight-saving you could read the patch
12:32:36 -!- sebbu has quit (Read error: 60 (Operation timed out)).
12:32:43 <lifthrasiir> "As this paper news (http://www.lanacion.com.ar/nota.asp?nota_id=1187055 <http://www.lanacion.com.ar/nota.asp?nota_id=1187055>) that Arnaldo just sent to the list, confirms, there will be no DST change in Argentina this weekend (although the Decree wasn't published in time)."
12:33:50 <lifthrasiir> anyway, what a shame. :(
12:49:58 -!- kar8nga has quit (Read error: 110 (Connection timed out)).
13:06:48 -!- oerjan has joined.
13:09:15 * oerjan swats oklopol to death per request -----###
13:10:25 -!- kar8nga has joined.
13:10:33 -!- kar8nga has quit (Remote closed the connection).
13:11:37 -!- FireFly has joined.
13:13:09 -!- kar8nga has joined.
13:16:03 -!- ehird has joined.
13:19:46 -!- Pthing has joined.
13:31:23 -!- Gracenotes has quit ("Leaving").
13:35:26 -!- Asztal has joined.
13:37:37 -!- ehird has quit.
13:47:40 -!- ais523 has quit (Read error: 104 (Connection reset by peer)).
13:47:46 -!- ais523 has joined.
14:05:01 -!- BeholdMyGlory has joined.
14:21:13 -!- augur has quit (Read error: 110 (Connection timed out)).
14:23:36 -!- MigoMipo has joined.
15:09:47 <AnMaster> oerjan, iwc
15:10:42 <oerjan> read it hours ago.  barely.
15:10:55 <oerjan> no wait
15:10:58 <oerjan> barely not
15:11:12 <oerjan> just under two hours
15:11:19 <oerjan> these things are *important*
15:11:29 <oerjan> also, food
15:52:30 <AnMaster> ais523, you remember that course length issue you ran into?
15:53:40 <AnMaster> I suspect I ran into similar administrative issues, Not about length but about what course I'm registered to currently. And how long I have been studying. Sigh...
15:55:53 <oklopol> if this is a university story, i'm going to need you to elaborate
15:56:06 <oklopol> i am a keen university boy.
16:01:02 -!- eurythmia has joined.
16:01:24 <eurythmia> Thanks FireFly :)
16:01:32 <FireFly> np :P
16:02:39 <eurythmia> I'm pretty sure that the set of all regular expressions over a given alphabet is a context-free language, but I'm not 100% sure ... is this the case?
16:04:07 <oklopol> eurythmia: of course it is
16:04:41 <eurythmia> oklopol, awesome. For my benefit, could you please give me a clue as to why it is not a regular language?
16:05:03 <oklopol> just have like S -> (S) | S + S | S* | terminal (ambiguous)
16:05:15 <oklopol> err and
16:05:16 <eurythmia> ah. I get it.
16:05:17 <oklopol> S -> SS
16:06:07 <eurythmia> oklopol, thanks. :)
16:06:47 <oklopol> you'll get things like S => SS => SS + S, so this is not actually a grammar you'd use to parse regexps because the tree doesn't represent the correct precedence, but should generate the correct stuff
16:08:00 <eurythmia> oklopol, yeah, I was just trying to decide whether to draw an FSA or a PDA to deal with the language ... I started using a PDA because I couldn't figure out how to effectively match parentheses with an FSA, but I'd have hated to get so far all for naught ;)
16:09:30 <oklopol> "doesn't represent the correct precedence", well hopefully i don't need to explain what that means, basically you'd usually want to think of the tree representing S => SS => SS + S as meaning S(S + S), basically with that grammar you need a separate step to get the correct precedences
16:09:55 <oklopol> yeah FSA can't match parens
16:10:15 <oerjan> easy to prove with the pumping lemma
16:10:16 <oklopol> think about (^n )^n, and pump ('s
16:10:28 <eurythmia> oklopol, well, not a deterministic FSA, anyways ;)
16:10:41 <oklopol> eurythmia: deterministic and nondeterministic FSA are exactly as strong
16:10:47 <oklopol> good, was faster than oerjan
16:11:02 <eurythmia> oerjan, hm ... I can't remember the pumping lemma ... guess I'll have to wikipedia that.
16:11:11 <oklopol> eurythmia: so they can't be matched by nondeterministic FSA either
16:11:16 -!- fax has joined.
16:11:30 <oerjan> there's one pumping lemma for FSAs and one for CS langs
16:13:05 <oerjan> also, to get the precedence right you just have to separate S into a number of different nonterminals
16:13:06 <eurythmia> k ... I'll go look at those.
16:13:21 <oerjan> (one for each precedence level)
16:13:26 <oklopol> eurythmia: also if you're a human, it will probably be enough of a convincer to know a finite state automaton only remembers a finite amount of data, and matching an arbitrary amount of parens can clearly require any amount of memory, because you need to remember an arbitrary integer.
16:14:17 <oerjan> s/CS langs/CF langs/
16:14:26 <oklopol> isn't there one for CS?
16:14:33 * oklopol dunno bout CS :<
16:14:35 <oerjan> heck if i know
16:14:48 <oklopol> oerjan also did you hear i failed on my automata exam
16:14:57 <oklopol> that's kinda important to know
16:15:02 <oklopol> well
16:15:06 <oerjan> * oerjan swats oklopol to death per request -----###
16:15:07 <oklopol> i suppose you already swatted me for it
16:15:26 <eurythmia> hm. Well ... looks like I've got some studying to do for my compiler exam on friday :P
16:15:33 <oklopol> just rechecking, in case you didn't read *why* you wanted me to swat me to death
16:16:18 <oklopol> i bet for most compiler courses you could just say what i said about finite memory.
16:16:20 <AnMaster> <oklopol> if this is a university story, i'm going to need you to elaborate <-- yes it is I guess. But I don't know yet. Things are extremely confused.
16:16:33 <oklopol> is that so
16:17:17 <AnMaster> Don't miss the next episode of this horror drama. Aired tomorrow (hopefully)
16:17:21 <eurythmia> oklopol, I'll keep that in mind for anything we do regarding parens ;)
16:17:39 <oerjan> no mention of CS langs on wp's pumping lemma page
16:17:54 <AnMaster> <oklopol> eurythmia: of course it is <-- even with lookahead/behind and backreferences?
16:18:09 <oklopol> AnMaster: huh
16:18:22 <AnMaster> oklopol, perl regular expressions has those. So does re in python
16:18:26 <oklopol> we're talking the grammar of regexps
16:18:30 <AnMaster> oh right
16:19:05 <eurythmia> AnMaster, yeah ... I'm not actually parsing REs ... just recognising whether or not they belong to a language :)
16:19:14 <oklopol> lookahead/-behind sounds CS
16:19:15 <oerjan> back references sound like they would make things hard to make CF
16:19:18 <oklopol> backreferences?
16:19:19 <eurythmia> s/reconising/recognizing/
16:19:23 <oklopol> what are those
16:19:29 <AnMaster> oerjan, CF being?
16:19:35 <oerjan> context-free
16:19:36 <oklopol> context-free
16:19:40 <AnMaster> ah right
16:19:55 * oklopol smells redundancy
16:20:06 <AnMaster> (?<!pcre)grep
16:20:19 <AnMaster> would match "grep" that is *not* preceded by "pcre"
16:20:28 <AnMaster> that is negative lookbehind
16:20:30 <oklopol> is that lookbehind?
16:20:31 <oklopol> okay
16:20:35 <oklopol> that sounds CS.
16:20:38 <oklopol> context-sensitive
16:20:48 <AnMaster> oklopol, there is "is preceded" too.
16:20:48 <oklopol> what's a back reference
16:21:11 <AnMaster> oklopol, back reference is like: (foo|bar)\1 would match foofoo barbar but not foobar or barfoo
16:21:18 <oklopol> okay
16:21:24 <oklopol> that doesn't sounds like CS either, does it?
16:21:25 <AnMaster> that is, refer to what a previous () "captured"
16:21:39 <AnMaster> oklopol, I wouldn't know
16:21:52 <oklopol> also i guess even the syntax isn't CF anymore, if those can't have errors, guess that's what oerjan meant
16:21:52 <oerjan> i don't think lookahead/behind actually makes regexps more powerful afa what languages they can recognize...
16:22:02 <fax> oklopol perl -wle 'print "Prime" if (1 x shift) !~ /^1?$|^(11+?)\1+$/'
16:22:21 <oerjan> oklopol: heh true
16:22:26 <AnMaster> oklopol, (?<=pcre)grep   would match grep if preceded by pcre. But the string "pcre" is not part of the match itself
16:22:29 <oerjan> and no
16:22:31 <AnMaster> there is lookahead too
16:22:35 <AnMaster> that goes on the other side
16:22:37 <oerjan> i wasn't even thinking about that
16:22:42 <AnMaster> that is, same but after string instead of before it
16:23:19 <AnMaster> <oerjan> i wasn't even thinking about that <-- about what? backrefereces?
16:23:57 <AnMaster> fax, hm I fail to parse the perl bit of that (though the regex bit I understand).
16:24:00 <oerjan> it's pretty clear to me that l.a./b. can simply be implemented using a FSA if its contents are regular
16:24:01 * AnMaster knows PCRE not perl
16:24:52 <lifthrasiir> oklopol: RE syntax is context-free if you don't use back references.
16:24:53 <oerjan> or, hm, they would have to start from opposite sides.  but you still could fold it in i thinkø.
16:24:57 <oerjan> *-ø
16:25:03 <AnMaster> lifthrasiir, what about lookbehind though?
16:25:03 <oklopol> oerjan: l.a./b.?
16:25:08 <oklopol> lifthrasiir: yeah i know
16:25:29 <AnMaster> lifthrasiir, are you saying it is still CF with lookaheads and lookbehinds?
16:25:34 <lifthrasiir> AnMaster: does look-behind syntax force certain semantic restrictions?
16:25:35 <oerjan> oklopol: goddammit can't i abbreviate the terms we used 30 seconds ago without explaining? :D
16:25:45 <lifthrasiir> i think no.
16:25:48 <AnMaster> lifthrasiir, what ones are you thinking about?
16:25:49 <lifthrasiir> not*
16:25:50 <oklopol> oerjan: :P
16:26:03 <oklopol> oerjan: too much talk, my brain gets confused.
16:26:20 <lifthrasiir> a set of _RE_, not a language (aka a set of strings) represented with given RE.
16:26:24 <AnMaster> some implementations restrict look-behind to be fixed length. But not all ones.
16:26:25 <oklopol> (i did decrypt it just after asking)
16:27:37 <lifthrasiir> AnMaster: ah, then i'm not sure.
16:27:56 <lifthrasiir> but i think perl starts to support unlimited look-behind... right?
16:28:08 <AnMaster> lifthrasiir, hm?
16:28:24 <lifthrasiir> (not pcre though)
16:28:24 <AnMaster> as I said, I work with PCRE. not perl :P
16:28:36 <lifthrasiir> :p
16:28:44 <AnMaster> and I'm pretty sure that the regex stuff in .NET has variable length lookbehind at least.
16:29:13 <lifthrasiir> .NET regex has some strange features, like run-time capture removal etc.
16:29:31 <AnMaster> lifthrasiir, possibly. I haven't actually used them. Just read about it.
16:29:35 <lifthrasiir> (practically this is equivalent to recursive RE call though)
16:29:36 -!- ineiros has quit (Read error: 104 (Connection reset by peer)).
16:29:43 -!- ineiros has joined.
16:29:58 <AnMaster> lifthrasiir, PCRE allows stuff like (foo|baaar) in lookbehind at least
16:30:04 <AnMaster> but not bar{1,2} it seems
16:30:34 <AnMaster> some googling suggest java allows finite repetition (but not infinite like + or *)
16:30:45 <lifthrasiir> what?!
16:30:49 <AnMaster> lifthrasiir, hm?
16:31:01 <lifthrasiir> ah i missed the context
16:31:09 <AnMaster> eh
16:31:14 <lifthrasiir> you mean, {num} in look-behind is permitted?
16:31:25 <AnMaster> lifthrasiir, or ? or {num,num}
16:31:46 -!- KingOfKarlsruhe has joined.
16:31:51 <lifthrasiir> okay
16:31:59 <AnMaster> see http://www.regular-expressions.info/lookaround.html but it seems slightly outdated
16:32:09 <AnMaster> section "Important Notes About Lookbehind"
16:32:27 <lifthrasiir> hmm... everything is fun when the exam is coming. :p (i have that one within next 16 hrs)
16:32:36 <AnMaster> <lifthrasiir> .NET regex has some strange features, like run-time capture removal etc. <-- what does that actually mean btw?
16:34:16 <lifthrasiir> AnMaster: something like the direction that "removes alerady-existing capture if we reached this point".
16:34:19 <oklopol> i have number theory on thursday, should probably close irc, clearly it was irc's fault that i made an error in today's one.
16:34:27 <lifthrasiir> (if i recall correctly..)
16:34:27 <oklopol> exam that is
16:34:31 <AnMaster> lifthrasiir, ah
16:34:32 <oklopol> so
16:34:33 <AnMaster> sounds cool
16:34:38 <oklopol> why don't you stop talking about regexps
16:34:44 <AnMaster> oklopol, why should we?
16:34:47 <AnMaster> it is interesting
16:34:57 <oklopol> and get working on your usual OS/compiler garble :P
16:35:00 <AnMaster> in perl you can embed perl code inside regexes iirc
16:35:18 <oerjan> oklopol: :<
16:35:25 <lifthrasiir> oklopol: are you sure that is usual ever? :p
16:35:51 <oklopol> yeah the automata theory lecturer said smth like "if you've used perl, you've probably bumped into CS languages", probably some time since he programmed his last perl :D
16:36:13 <oklopol> lifthrasiir: well i dunno what they talk about, but something i can't parse anyway
16:36:21 <AnMaster> lifthrasiir, hm pcre has this (not sure what it does actually):
16:36:22 <AnMaster>          (?|...)         non-capturing group; reset group numbers for
16:36:22 <AnMaster>                           capturing groups in each alternative
16:36:39 <AnMaster>          (?:...)         non-capturing group
16:36:39 <AnMaster>          (?>...)         atomic, non-capturing group
16:36:43 <oklopol> i just do pure and simple stuff.
16:36:48 <AnMaster> and not sure what the diff is between those to
16:36:50 <AnMaster> two*
16:37:05 <AnMaster> ooh cool: (?#....)        comment (not nestable)
16:37:18 <oklopol> COOL, A COMMENT!
16:37:30 <lifthrasiir> AnMaster: not that. pcre one just renumbers the group number, so (?| ... (...) ... \1 ... ) would work correctly no matter where it is
16:37:37 <AnMaster> and doing (?i) makes the regex matching case insensitive until changed back
16:37:48 <lifthrasiir> and see http://msdn.microsoft.com/en-us/library/az24scfc.aspx and search for "balancing group" for what i said.
16:37:52 <AnMaster> would that break CF
16:38:04 <oklopol> lifthrasiir: do you remember the original numbering once out of the nesting?
16:38:33 <AnMaster>          \g{-n}          relative reference by number
16:38:37 <lifthrasiir> iirc it would be treated as like the whole (?|...) is omitted
16:38:40 <oklopol> like does (?| ... (...) ... \1 ...) start a subnumbering, and once out of that thingie, numbers return to normal
16:38:43 <AnMaster> lifthrasiir, why not that ^
16:39:11 <AnMaster> ooh
16:39:11 <AnMaster>          (?R)            recurse whole pattern
16:39:11 <lifthrasiir> AnMaster: just for convenience? as i said i'm not sure about them. :p
16:39:12 <AnMaster>          (?n)            call subpattern by absolute number
16:39:14 <AnMaster> stuff like that
16:39:28 <oerjan> oklopol: it said it was a non-capturing group so it must be
16:39:41 <oklopol> oerjan: yeah i didn't realize what non-capturing meant right awya
16:39:42 <oklopol> *away
16:39:47 <AnMaster> oerjan, what about calling previous sub-patterns like it was a subroutine?
16:39:49 <AnMaster> :D
16:40:01 <lifthrasiir> regular expression fail!
16:40:02 <AnMaster>          (?(condition)yes-pattern)
16:40:02 <AnMaster>          (?(condition)yes-pattern|no-pattern)
16:40:03 <oklopol> (i'm not that great at guessing based on names)
16:40:04 <AnMaster> that too
16:40:22 <AnMaster>          (?(Rn)...       specific group recursion condition
16:40:22 <AnMaster>          (?(R&name)...   specific recursion condition
16:40:22 <AnMaster>          (?(DEFINE)...   define subpattern for reference
16:40:22 <AnMaster>          (?(assert)...   assertion condition
16:40:23 <AnMaster> wow
16:40:24 -!- puzzlet has quit (Remote closed the connection).
16:40:31 -!- puzzlet has joined.
16:40:32 <AnMaster> is PCRE TC by any chance?
16:40:42 <AnMaster>          (*ACCEPT)       force successful match
16:40:42 <AnMaster>          (*FAIL)         force backtrack; synonym (*F)
16:40:54 <AnMaster> there is more back track control too
16:41:00 <oklopol> lol, that's just ugly :P
16:41:10 <oklopol> but kinda beautiful at the same time.
16:41:11 <AnMaster> oklopol, agreed. BUT IS IT TC?
16:41:42 <oklopol> that is easily settled if you can execute arbitrary code in (condition)
16:41:42 <AnMaster> I seriously suspect it may be. This sounds like something that oerjan should prove/disprove
16:41:54 <oerjan> argh
16:41:57 <AnMaster> oklopol, not as far as I know. It isn't perl
16:41:58 <oklopol> or anywhere
16:42:02 <AnMaster> as in
16:42:07 <AnMaster> you can't embed perl
16:42:10 <AnMaster> in PCRE
16:42:13 <oklopol> i see
16:42:16 * oerjan suggests googling since someone almost certainly has thought of it
16:43:01 <oklopol> turns out i don't have to submit the first piece of my bachelor's thesis for a grammar check sort of thing tomorrow
16:43:07 <lifthrasiir> AnMaster: i think it would be, with unlimited look-behind and subpatterns
16:43:17 <oklopol> this means i'm probably going to waste the few days i could've worked on it before next courses start :|
16:43:31 -!- kar8nga has quit (Remote closed the connection).
16:43:36 <oklopol> (have to submit in a week)
16:43:41 <AnMaster> lifthrasiir, well the recursion stuff too
16:43:49 <lifthrasiir> ah of course.
16:43:54 <AnMaster> lifthrasiir, and conditions.
16:44:16 <AnMaster>          (?C)      callout
16:44:16 <lifthrasiir> is there any RE engine that doesn't support conditions while supporting other features? :p
16:44:16 <AnMaster>          (?Cn)     callout with data n
16:44:18 <AnMaster> wonder what they are
16:44:31 <lifthrasiir> AnMaster: that is a PCRE replacement for perl's (?{})
16:44:33 <AnMaster> possibly calling a function in the host language?
16:44:38 <lifthrasiir> exactly.
16:44:51 * AnMaster looks at man pcrecallout
16:44:58 <AnMaster> yeah pcre docs are split in several man pages
16:45:05 <AnMaster> it is THAT complex
16:45:14 <AnMaster> only other example I can think of is zsh.
16:45:45 <oerjan> also perl itself :D
16:45:46 <lifthrasiir> anyway, one can define subpatterns as like (?<patternname> (?<=context) (?subpattern) (?subpattern) ... (?=context) ) and you're done
16:46:20 -!- puzzlet_ has joined.
16:46:30 <eurythmia> heh, I'm glad that I was able to spark such a deep and meaningful conversation on regular expressions :P
16:46:51 <AnMaster> lifthrasiir, yeah
16:47:17 <AnMaster> eurythmia, does this affect your original question though?
16:47:38 <AnMaster> or was that about the grammar for regexes themselves?
16:48:13 <eurythmia> AnMaster, nope ... my question was whether the language was classified as regular or context free ... I've already finished drawing up the PDA for it :P
16:48:38 <AnMaster> eurythmia, it certainly isn't context free with back references I guess
16:49:36 <AnMaster> and I'm not sure about "option flags" like foo(?i)bar(?-i)quux (would match "foobarquux" and "fooBaRquux" but not "foOBarquux" for example)
16:50:11 <eurythmia> AnMaster, that's probably a fair assumption ... my PDA only has 3 states and 20 transitions.
16:50:14 <AnMaster> also I don't even want to think about how those option flags works when inside a group
16:50:32 <eurythmia> so, relatively speaking, it's pretty simple.
16:50:46 <AnMaster> possibly it might be case sensitive or case insensitive depending on if a previous group matched or not
16:53:55 -!- ais523_ has joined.
16:55:22 <AnMaster> oh it seems that setting case sensitive/insensitive inside a group only affects that group
16:55:23 <AnMaster> meh
16:55:50 <AnMaster> however it affects all branches of said group
16:55:52 <eurythmia> my alphabet is pretty simple too: A={a,b}   ;)
16:56:50 -!- ais523 has quit (Nick collision from services.).
16:56:56 -!- ais523_ has quit (Nick collision from services.).
16:57:28 -!- BeholdMyGlory has quit (Remote closed the connection).
16:59:46 <fax> oh hey does anyone know a term in combinatory logic T(X) such that,  T(S) --> S, T(K) --> K, T(S) --> Y, T(K) --> Y?
16:59:55 <fax> --> meaning there is some reduction sequence to
17:00:14 <oerjan> fax: um you are contradicting yourself there
17:00:23 <fax> oerjan well I'm thinking church rosser property of lambda calculus makes it impossible
17:00:52 <oerjan> there is a church rosser for combinatory logic too iirc
17:01:18 <oerjan> and yes, if that's what you mean
17:01:39 -!- puzzlet has quit (Read error: 110 (Connection timed out)).
17:02:03 <fax> is  ~(S = K)  and axiom?
17:02:24 <oerjan> without it you get forall x=y pretty easily
17:02:37 <oerjan> *forall x,y x = y
17:02:43 <fax> without what?
17:03:02 <oerjan> sheesh.  if S = K, then everything is equal to everything
17:04:40 <AnMaster> oerjan, if you mean ∀ then write it
17:04:54 * oerjan swats AnMaster -----###
17:05:13 <AnMaster> oerjan, you confused me by using weird syntax!
17:05:43 <oerjan> i REFUSE to use your cursed unicode DAMMIT :D
17:05:46 -!- ais523 has joined.
17:06:10 <oerjan> also, i just see a question mark
17:06:16 <AnMaster> oerjan, you mean ∃x(RefusesToUseUnicode(x))
17:06:26 <AnMaster> that is "exists"
17:06:31 <AnMaster> oerjan, font fail
17:07:18 <oerjan> font, utf-8, everything in a long chain from irssi back to putty
17:08:39 <AnMaster> oerjan, yay for ℵ₀ = |ℕ|
17:08:51 <AnMaster> what parts can you read of that
17:09:12 <oerjan> <AnMaster> oerjan, yay for ?? = |N|
17:09:19 <AnMaster> should be aleph_0
17:09:35 <AnMaster> as in, the Aleph symbol followed by subscript 0
17:09:49 <oerjan> i can see that in the logs
17:09:49 <AnMaster> and that N should be blackboard bold
17:10:59 <AnMaster> oerjan, what about: ±n = -1(∓n)
17:11:01 <fax> ₀_₀
17:11:10 <oerjan> <AnMaster> oerjan, what about: ±n = -1(?n)
17:11:20 <AnMaster> oerjan, that was - above plus in the second one
17:12:06 <AnMaster> 13 ≡ 1 (mod 12)
17:12:50 <oerjan> AnMaster: i can see iso-8859-1 and nothing else.
17:13:15 <AnMaster> oerjan, seriously fix your setup
17:13:34 <AnMaster> oerjan, what does the command locale output on the server you are sshing to?
17:13:45 <oerjan> AnMaster: SHUT. UP.
17:13:54 <oklopol> :D
17:13:56 <oerjan> </ehird>
17:13:59 <oklopol> see this is what i mean
17:14:00 <AnMaster> the variable values should all end with .UTF-8
17:14:14 <AnMaster> if not, export those in your .bashrc, .profile or similar
17:14:15 <oklopol> irc stuff works as uninteresting talk
17:14:24 <oklopol> and all sortsa bickering
17:14:26 * AnMaster has no clue what shell oerjan uses
17:14:36 <AnMaster> oerjan, I know you are just joking
17:14:41 <AnMaster> and want to get it fixed too
17:14:44 <oerjan> AnMaster: and you will never know because i am tired of this discussion.
17:15:14 <AnMaster> oerjan, wait, you aren't ehird. You must always be joking when angry. Fundamental law of the universe
17:16:21 <oklopol> he can't be angry, but he can be tired of discussions
17:16:24 <oklopol> not even very rare
17:16:39 <AnMaster> oklopol, sure is rare
17:17:04 <oklopol> there are rarer things
17:17:07 * AnMaster makes a mental note to always use as much unicode notation when talking to oerjan as possible
17:17:10 <oklopol> like your mom
17:17:21 <AnMaster> oklopol, that one wasn't even very good
17:17:29 <oklopol> you mean like your... nm
17:18:26 <oklopol> grrrrr why didn't my parents force me to learn math when i was young
17:18:29 <oklopol> shoppe time
17:18:35 <AnMaster>          ⎧ n + 1                   if m = 0
17:18:35 <AnMaster> A(m,n) = ⎨ A(m - 1, 1)             if m > 0 and n = 0
17:18:35 <AnMaster>          ⎩ A(m - 1, A(m, n - 1))   if m > 0 and n > 0
17:18:38 <AnMaster> oklopol, like it?
17:18:40 <AnMaster> oerjan, you too
17:18:43 <AnMaster> look in logs
17:18:50 <AnMaster> it looks awesome here
17:18:53 <oklopol> that's ackermann, i notice the shape.
17:19:11 <AnMaster> oklopol, well yes. But see the unicode case thingy
17:19:12 <oklopol> well recall the shape
17:19:17 <oklopol> i don't see unicode
17:19:25 <AnMaster> oklopol, oh?
17:19:25 <oklopol> i see random characters
17:19:31 <AnMaster> oklopol, your client fails too
17:19:35 <oklopol> orly
17:19:39 <AnMaster> yes
17:19:42 <oklopol> orly
17:19:53 <AnMaster> fax, eurythmia, lifthrasiir: surely you can see this?
17:20:05 <AnMaster> at least I expect lifthrasiir to be able to
17:20:13 <oklopol> i've told countless times my nnscript refuses to show unicode correctly.
17:20:14 <Deewiant> I see a 1px or so space between the lines
17:20:21 <AnMaster> Deewiant, looks good here
17:20:22 <lifthrasiir> AnMaster: curly braces are too large, but others are fine
17:20:25 <Deewiant> Why do you use nnscript?
17:20:36 <AnMaster> lifthrasiir, how large in what way?
17:20:44 <oklopol> Deewiant: the few others i've tried have been even more annoying
17:20:58 <fax> AnMaster fail
17:21:04 <AnMaster> fax, how so?
17:21:07 <Deewiant> Why do you need a script?
17:21:12 <lifthrasiir> AnMaster: twice large as ordinary letters (and as consequence line height are tripled or even quadrupled)
17:21:23 <AnMaster> lifthrasiir, eeh. What is that font
17:21:27 <oklopol> Deewiant: mirc doesn't let me paste multiple lines without excess flooding
17:21:38 <AnMaster> lifthrasiir, in Dejvavu Sans Mono they look perfect
17:21:50 <oklopol> also nnscript is prettier by default, but i suppose you would consider that even less important
17:22:06 <lifthrasiir> AnMaster: Tahoma?
17:22:26 <AnMaster> lifthrasiir, don't have it myself as far as I can see. So no clue
17:22:30 <Deewiant> Yeah, I suppose I would
17:22:31 <AnMaster> isn't it some windows only font?
17:22:53 <AnMaster> which raises the question: why the hell windows?
17:22:53 <lifthrasiir> originated from windows, but i think there is some corefont package for them
17:23:41 <AnMaster> lifthrasiir, actually it might be that your font render thingy is substituting from some other font
17:23:52 <AnMaster> if Tahoma is missing
17:24:06 <AnMaster> is missing those*
17:24:07 <lifthrasiir> that's possible, but then i don't know what the alternative font is
17:24:41 <AnMaster> lifthrasiir, gucharmap, find symbol, set font to tahoma, right click the symbol, see what font it says in there
17:24:49 <AnMaster> I think it was in some "misc technical" block
17:25:17 <lifthrasiir> i'm using windows for now btw
17:25:19 <lifthrasiir> wait a moment
17:25:38 <AnMaster> U+23A8  is the middle segment
17:25:46 <AnMaster> the upper/lower ones are close
17:26:04 <fax> AnMaster bad line spacin
17:26:15 <AnMaster> fax, hm? there is no unusual line spacing here
17:26:22 <lifthrasiir> it is clear that tahoma doesn't have such glyph
17:26:41 <lifthrasiir> fax: i have similar problem, what irc client are you using?
17:26:47 -!- puzzlet has joined.
17:26:51 <lifthrasiir> (and OS)
17:27:32 <AnMaster> lifthrasiir, fax: http://omploader.org/vMmtzYw is how it renders here
17:27:50 <AnMaster> which is xchat on Linux
17:28:05 <AnMaster> (I'm using multiple clients on the bouncer)
17:28:26 <lifthrasiir> wait, my font was not Tahoma (sorry!) but some korean font, which obviously doesn't have glyphs for U+23A8 etc.
17:28:38 <AnMaster> lifthrasiir, mhm
17:29:00 <AnMaster> Dejavu Sans Mono is pretty decent for irc. Not sure how good it is on Korean
17:29:14 <eurythmia> AnMaster, sorry, delayed response, but yeah, I can see it.
17:29:18 <lifthrasiir> that doesn't have korean glyphs at all
17:29:26 <eurythmia> looks very nice ;)
17:29:34 <AnMaster> odd that ± is sharp and crisp but ∓ is kind of blurry
17:29:38 <lifthrasiir> and korean glyphs in Code2000 etc. simply suck.
17:29:45 <AnMaster> maybe font issue too? *looks*
17:34:06 <fizzie> The ± ∓ thing is not so odd, given that those chars come from completely different blocks.
17:34:29 <lifthrasiir> AnMaster: hmm, i don't know where the U+23A8 glyph originated... it is not in even Arial Unicode MS
17:34:30 <fizzie> ± is in latin-1, while for ∓ you need to go into the Unicode mathematical operator block.
17:35:05 <Deewiant> fizzie: What does the blockness have to do with how they display in a font?
17:35:58 <fizzie> Deewiant: It means that very many fonts might have ± since it's latin 1, while ∓ is rarer; so it's not very strange that they happen to come from different fonts to your screen.
17:37:05 <pikhq> Same glyphs on my screen. Hooray, Dejavu Sans Mono.
17:37:06 <fizzie> (Even if they happen to come from the same font, the glyphs might be made by different people / come from different sources / whatever; in any case, the point was that since the characters are so far away "logically", it's not strange that they display differently.)
17:37:06 <AnMaster> fizzie, Actually dejavu sans mono has it
17:37:08 <Deewiant> fizzie: In this case they're in the same font, though.
17:37:17 <AnMaster> yet still, one is more blurry
17:37:23 <AnMaster> and yes I use dejavu sans mono
17:37:34 <Deewiant> I guess that it could just be because they're from different people
17:37:40 <AnMaster> maybe
17:37:59 <pikhq> On my screen, one is merely the translation of the other. Granted, it's 9 point font.
17:38:12 <AnMaster> pikhq, 9 pt too
17:38:12 <pikhq> Erm, mirror.
17:38:24 <pikhq> AnMaster: Your hinting sucks?
17:38:26 <Deewiant> ∓ also has an asymmetric +
17:38:29 <AnMaster> pikhq, maybe
17:38:39 <Deewiant> Or it just looks like it because of the blurriness
17:38:53 <Deewiant> As I stare at it it shifts between symmetric and asymmetric.
17:39:04 <AnMaster> Deewiant, asymetrical left/right or up/down?
17:39:18 <Deewiant> left/right
17:39:29 <AnMaster> Deewiant, nop. Though the + is wider than it is tall
17:39:37 -!- puzzlet_ has quit (Read error: 110 (Connection timed out)).
17:39:41 <Deewiant> On occasion it looks like the | is more left than it should be
17:39:50 <AnMaster> <Deewiant> As I stare at it it shifts between symmetric and asymmetric. <-- hit that auto button on your TFT front panel RIGHT NOW!
17:40:04 <Deewiant> I did, and?
17:40:07 <AnMaster> :P
17:40:09 <AnMaster> bbl food
17:40:15 <Deewiant> It popped up "Digital video input no access"
17:42:54 <fizzie> Actually, I might be wrong; maybe it's just some strange rendering issue. I looked at both glyphs (in DejaVu Sans Mono) in fontforge, and they really should be just vertical mirrors of each other; relative distances between the points seem to be the same there.
17:42:59 <Deewiant> http://iki.fi/deewiant/tmp/pm.png zoom in to see the difference
17:46:46 <fizzie> Deewiant: DejaVu glyphs: http://zem.fi/~fis/pm.png
17:47:05 <Deewiant> Aye, the problem is in rendering
17:48:02 <lifthrasiir> the problem in font hinting?
17:48:19 <Deewiant> I dunno
17:49:29 <fizzie> I guess it could be; Deewiant's pm.png looks a bit like the ∓ would just be not perfectly aligned with the screen pixels, causing those antialiasing artifacts there.
17:50:16 <fizzie> FWIW, they look pretty identical (except the flip) here, as closely as I can make out.
17:51:35 <fizzie> Zooming in actually shows some antialiasing in *both*, so my font rendering sucks the most out of these.
17:56:22 <fax> can you prove that I = SKK doesn't equal S (or K)?
17:58:04 -!- ais523 has quit ("Page closed").
17:59:36 <pikhq> SKK = \x->SKKx = \x->kx(kx) = \x->x
17:59:52 <pikhq> \x-> /= S & \x->x /= K.
17:59:59 <pikhq> QED.
18:00:35 -!- ais523 has joined.
18:01:00 <ais523> wow: Darl McBride was sacked
18:01:11 <pikhq> Wow.
18:01:12 <ais523> well, technically speaking, made redundant
18:01:17 <fax> How do you know  F = \x -> Fx  ?
18:01:29 <ais523> although it's pretty rare for a company to eliminate the position of CEO
18:01:29 <fax> is that an axiom or theorem?
18:01:33 <ais523> I didn't even realise that was possible...
18:01:50 <ais523> fax: definition of \, pretty much
18:01:56 <pikhq> Definition of \.
18:02:15 <fax> hum I don't think I undertsand
18:03:01 <pikhq> It's called "currying".
18:03:56 <fax> what's the definition of \?
18:04:30 <pikhq> (\x->f x) y = f y
18:04:47 <ais523> cancel the ys, and you get (\x->f x) = f
18:04:56 <FireFly> [18:18:34] <AnMaster>          ⎧ n + 1                   if m = 0
18:04:59 <fax> yes I agree with that but just because  A y = B y  doesn't mean that  A = B  or does it?
18:05:00 <ais523> and currying basically says that you're allowed to do that
18:05:05 <FireFly> I assume that thingy was supposed to be an integral sign?
18:05:16 <FireFly> (after checking the first char in uh.. kate)
18:05:16 <ais523> A y = B y doesn't necessarily imply A = B
18:05:20 <ais523> it does if it's true for all y, though
18:05:20 <AnMaster> back
18:05:46 <pikhq> fax: A y = B y for all y does.
18:05:46 <AnMaster> <Deewiant> It popped up "Digital video input no access" <-- ah DVI
18:05:46 <AnMaster> or such
18:05:46 <FireFly> Oh
18:05:46 <FireFly> It was a '{'
18:05:46 <AnMaster> well then, odd it changes as you described
18:05:49 <fax> so it that called currying?  A y = B y -> A = B
18:06:24 <pikhq> No, currying says that \x->f x == f.
18:06:24 <fax> (forall y, A y = B y) -> A = B
18:06:37 <fax> I thought that was eta conversion
18:07:04 <AnMaster> <ais523> wow: Darl McBride was sacked <-- hmmm... SCO?
18:07:10 <ais523> yes
18:07:13 <fax> what's the proof of (forall y, A y = B y) -> A = B?
18:07:15 <AnMaster> wow
18:07:22 <ais523> fax: definition of =
18:07:28 <fizzie> AnMaster: It's not that odd; Deewiant probably still doesn't have digital eyes, old-fashioned person that he is.
18:07:44 <ais523> one of the commenters at Groklaw seems to think that his next step will be an attempted hostile takeover of SCO
18:07:48 <ais523> which would be hilarious, IMO
18:07:53 <AnMaster> fizzie, I have analogue monitor cable *and* eyes
18:07:55 <fax> all I know about = is that it's the smallest reflexive, symmetric, transitive relation
18:07:58 <fax> is that enough?
18:08:10 <fax> I guess "the smallest" is the important thing here
18:08:12 <ais523> fax: it's not enough
18:08:21 <fax> what more could I say about =?
18:08:28 <ais523> well, when are two functions the same?
18:08:37 <ais523> you've defined = in terms of reflexiveness
18:08:43 <ais523> and reflexiveness is defined in terms of =
18:08:44 <fax> ahhh
18:08:47 <ais523> so this isn't really getting anywhere
18:09:06 <fax> I'm looking for nonstandard models of SK calculusu
18:09:32 <fax> so I can add as an axiom, the rule of right cancellation
18:10:19 <AnMaster> ais523, wait, why is reflexiveness defined in terms of =?
18:10:40 <ais523> AnMaster: an operator is reflexive if it means that A o A for all A
18:10:52 <ais523> in other words, it's reflexive if it's true whenever the left and right are equal
18:11:13 <AnMaster> ais523, is that o as in ∘ ?
18:11:28 <AnMaster> if so, why not use the proper notation? ;P
18:11:48 <ais523> AnMaster: because I can't easily type ∘ in a hurry?
18:12:09 <AnMaster> ais523, ah I still have http://en.wikipedia.org/wiki/Table_of_mathematical_symbols open after talking to oerjan above :P
18:14:40 -!- MigoMipo has quit (Ping timeout: 180 seconds).
18:18:48 <oerjan> fax: what do you mean by rule of right cancellation?  that (forall y, A y = B y) -> A = B thing?
18:19:17 <fax> oerjan: pikhq used it, I just wanted to make it formal
18:19:43 <oerjan> anyway as you said that follows from eta reduction in lambda calculus
18:19:48 <fax> I've not assumed that my model of SK axioms IS lambda calculus
18:19:49 <oerjan> assuming you have free variables
18:20:08 <oerjan> no, but lambda calculus _is_ a model of it...
18:20:19 <fax> is it the only model?
18:20:33 <oerjan> so it's obviously consistent to add the additional axioms that hold in it...
18:21:03 <fax> no that's not obvious
18:21:26 <fax> if I didn't have the axiom S <> K, then the trivial model applies, and that has the thoerem forall x y, x = y
18:21:34 <oerjan> sure
18:21:50 <oerjan> but that axiom does not hold in lambda calculus...
18:21:55 <oerjan> er
18:21:58 <oerjan> the opposite
18:22:46 <oerjan> lambda calculus _is_ a model of SK calculus
18:23:24 <oerjan> thus you have at least one model of SK calculus satisfying all theorems of lambda calculus.  thus those theorems are consistent with SK calculus.  Q.E.D.
18:23:26 <fax> the set with one element o and application operator \x y -> o, is also a model
18:23:39 <fax> that's why I added the axiom S <> K
18:23:50 <oerjan> well duh
18:24:25 <oerjan> i think there are lots of other models coming from those CPOs used in denotational semantics
18:24:37 <fax> uh?
18:26:21 <oerjan> in fact i vaguely recall something about those being used to prove you could model lambda calculus as something resembling actual set functions
18:26:23 <AnMaster> ais523, feather progress?
18:26:31 <ais523> on hold
18:26:34 <ais523> due to me going temporarily insane
18:26:41 <ais523> well, I hope it's temporary
18:26:46 <ais523> I'm waiting for my brain to cool again
18:27:27 -!- oerjan has set topic: World temporarily saved: ais523 no longer thinking about Feather | http://tunes.org/~nef/logs/esoteric/?C=M;O=D.
18:27:39 <fax> what is feather
18:27:41 <fax> ?
18:27:45 <AnMaster> ais523, what from? feather?
18:27:52 <ais523> yes
18:27:56 <AnMaster> ah
18:27:59 <ais523> put it this way: I've been here for several years now
18:28:07 <ais523> it takes a special brand of insanity to actually send me over the edge
18:28:08 <AnMaster> yes I know that...
18:28:13 <AnMaster> ais523, agreed.
18:28:18 <AnMaster> brb
18:28:18 <ais523> fax: please don't ask, it takes too long to explain and I don't want my head to explode again
18:28:43 <ais523> suffice it to say, that it's a) awesome, b) esolang-related, and c) vaporware, possibly forever so
18:30:34 <oklopol> so this openoffice i've been hearing so much about for the last day or 10 years or something
18:30:47 <oklopol> does it have some sorta equation editor in the default installation
18:31:34 <ais523> yes, IIRC
18:31:56 <oklopol> i have no idea where the cd is for my office
18:32:09 <AnMaster> back
18:32:20 <oklopol> and the only other things i know that can do math stuff are mathematica and that latex thing
18:32:44 <AnMaster> fax, quick description: a time travelling esolang involving rewriting the interpreter what interpreted you.
18:32:53 <fizzie> Misread "that latex lung"; it sounded like some sort of occupational-hazard disease.
18:33:05 <AnMaster> XD
18:33:21 <ais523> Feather has really messed-up causality, which is really frustrating my attempts to write an interp for it
18:33:22 <fizzie> "Ooh, I've got bad LaTeX lung from my days as a slave in the math mines of our university."
18:33:29 <AnMaster> oklopol, LaTeX is awesome though
18:33:35 <AnMaster> fizzie, XD
18:33:40 <oklopol> AnMaster: but can i just pick it up on the fly?
18:33:58 <oklopol> i'm tempted to use something that just lets me press buttons with the correct looking math thingies.
18:34:01 <AnMaster> oklopol, depends on how strong the back of the fly is I guess.
18:34:07 <AnMaster> a common house fly, maybe not
18:34:23 <oklopol> mine is a pretty common house fly, as you probably know
18:34:31 <oklopol> well, more like a retarded, lazy house fly
18:34:38 <AnMaster> oklopol, LyX then. Awesome WYSIWYG frontend for LaTeX
18:34:39 <AnMaster> actually
18:34:41 <fax> thanks AnMaster
18:34:42 <AnMaster> WYSIWYM
18:34:46 <oklopol> but latex is something i'd *want to* learn, so probably i actually would learn it.
18:34:47 <AnMaster> that is "meant"
18:34:52 <ais523> the OO formula-generation thing basically has a WYSIWYG just-press-buttons in one pane
18:34:59 <ais523> and a LaTeX-like version in another
18:35:00 <oklopol> AnMaster: yeah i guessed it was meant
18:35:02 <fax> I'm rubbish at this :/  how do I find combinator F such that F(K) = S, F(I) = K?
18:35:03 <fizzie> OpenOffice.org and insert/object/formula at least gave me a formula editor.
18:35:05 <fax> or vice versa
18:35:05 <ais523> and they both update whenever you change either
18:35:36 <AnMaster> ais523, "LaTeX-like"?
18:35:52 <ais523> AnMaster: it's probably a subset of LaTeX
18:36:00 <AnMaster> mhm
18:36:05 <ais523> maybe with a few extra commands thrown in
18:36:11 <AnMaster> ais523, surprised it doesn't use MathML instead or such
18:36:19 <ais523> AnMaster: that's the format it saves in, IIRC
18:36:22 <oklopol> KSK = S, IIK = I
18:36:23 <fizzie> Ohh, right, it had that fancy thing. It also displays (at least here) inverse question marks in the "rendered output" thing occasionally, when there's an incomplete structure.
18:36:23 <ais523> as opposed to the format you edit in
18:36:27 <AnMaster> uh ok
18:36:29 <oklopol> errr
18:36:30 <AnMaster> that is pretty weird
18:36:38 <oklopol> sorry, too hasty :P
18:36:42 <ais523> fizzie: yes, to me too
18:36:51 <AnMaster> hm?
18:37:07 <AnMaster> LaTeX usually just renders empty instead iirc
18:37:41 <oerjan> fax: it's easier to start with F(K) and F(KI)
18:37:46 <ais523> but then the empty wouldn't be clickable
18:37:56 <oerjan> Kxy = x, KIxy = y
18:38:02 <ais523> k and ki are amazingly good logic levels for Unlambda, though
18:38:19 <oerjan> precisely
18:38:41 <AnMaster> <oerjan> fax: it's easier to start with F(K) and F(KI)
18:38:41 <AnMaster> <ais523> but then the empty wouldn't be clickable
18:38:41 <ais523> hmm... I generally use i and ki
18:38:46 <AnMaster> before I noticed not same person
18:38:51 <AnMaster> I was REALLY confused
18:38:55 <ais523> for church numerals
18:38:56 <fax> oerjan well how does that apply?
18:39:01 <fax> I don't see the link
18:39:09 <AnMaster> ais523, oerjan: stop having nicks of same length :P
18:39:41 <oerjan> fax: F = \b -> b x y gives something that is F(K) = x, F(KI) = y
18:39:49 <AnMaster> ais523*=2
18:39:56 <AnMaster> there, should fix it
18:40:09 <ais523> <fax> does f(x) = ((xi)(s))(((xi)(ki))(k)) work?
18:40:14 <ais523> I'm not entirely sure I've got that one right, though...
18:40:34 <fizzie> That OOo syntax is only very vaguely LaTeX-like; for example, \over{x}{y} is "{x} over {y}", and "\sum_{i=1}^n 42" is in fact "sum from{i=1} to{n} 42".
18:40:35 <ais523> I was trying to compile from the Underlambda in my head
18:40:59 <ais523> fizzie: I think there were LaTeXy and less LaTeXy synonyms for most operations
18:41:12 <fizzie> Probably; those were what came out of the buttons.
18:41:20 <fax> ais523 it reduces to SI = K
18:41:33 <fax> I mean,  f(I) = f(K) reduces to that
18:42:15 <ais523> ugh, I know what I did
18:42:22 <fax> hmm I think I can do ti from there perhaps
18:42:24 <ais523> I applied rather than composed...
18:42:32 <fax> because SIxy = y(xy) and Kxy = x
18:42:52 <fax> so if I produce let y = KK and x = S
18:44:04 <fax> no I made a mistake :/
18:44:36 <oerjan> fax: KKIxy = Kxy = x, IKIxy = KIxy = y
18:45:23 <oklopol> KABCD = ACD, IABCD = ABCD, so ACD = S, ABCD = K; guess A = K => KCD = S => C = S; KBSD = K => BD = K => B = I, D = K, so, apply KISK to your combinator
18:45:32 <oklopol> does that work?
18:47:26 <oklopol> assuming i'm not failing miserably at combinatory logic, that should be a straightforward derivation of a working combinator, assuming you know how to apply stuff to the param
18:48:01 <oerjan> fax: so F = \b -> b K I x y gives you F(K) = x, F(I) = y
18:48:02 <oklopol> actually is that exactly what oerjan is trying to hint at
18:48:26 <oklopol> looks like it
18:48:29 <oerjan> oklopol: i don't know if yours is the same
18:48:49 <oklopol> mine is the exact same, just not for general x, y
18:49:00 <oerjan> ah
18:49:01 <oklopol> you apply KIxy to the combinator, i apply KISK
18:49:38 <oklopol> but my point is mostly you can just apply general stuff, and solve, that way.
18:49:45 <oerjan> well i went by K and KI as i noted above
18:49:56 <oklopol> well i didn't read your derivation, maybe i should now
18:52:05 <oklopol> okay so you find a way to differentiate between K and KI, then find a way to get those outta I and K, which turns out to be trivial
18:52:39 <oklopol> i love combinators.
18:53:27 <fax> that's cool, that proof that I <> K doesn't use 'curry'
18:53:28 <oerjan> K and KI are as implied the "obvious" way to implement booleans in lambda calculus/combinators/unlambda
18:54:19 <oerjan> (although unlambda uses I and V in places just to be horrible :D)
18:54:27 <fax> okay so hypothetically..
18:54:39 <fax> I could probably produce a sequence of combinators, all distinct
18:54:46 <oklopol> i don't think i ever really made sense of how C/V/I booleans work
18:55:01 <fax> (N = {0, 1, 2, ...} with a proof x y in N, x <> y)
18:55:02 <oerjan> fax: church numerals
18:55:29 <fax> and this would let me make a bijection between that sequence and the sequence of natural numbers
18:55:46 <oerjan> oklopol: the wicked part is that you _need_ C in order to do anything useful with V
18:55:52 <oklopol> bijection? try isomorphism!
18:55:59 <oklopol> oerjan: i know.
18:56:00 <fax> what's the difference?
18:56:21 <oklopol> for a bijection you just need to find some combinator for each natural number
18:56:30 <oklopol> for isomorphism you have to have some sorta addition
18:56:31 <fax> :| I was going to say that then could I find a term like inf = suc inf such that size inf = 1 + size inf but that's not possible by church rosser
18:57:08 <oerjan> fax: it will just be non-terminating...
18:57:32 <oerjan> you always have fixpoints
18:58:25 <fax> I want to try and produce a contradiction from the non-terminating term
18:59:11 <oerjan> well size inf = 1 + size inf is pretty much the definition of an infinite cardinality in set theory :)
18:59:31 -!- eurythmia has quit (Read error: 145 (Connection timed out)).
18:59:33 <oerjan> er
18:59:54 <oerjan> "size" being defined by existence of bijections
19:00:16 <fax> Ysucc = succ(Ysucc)
19:00:32 <fax> and I can biject {zero,succ(zero),...} with {0,1,...}
19:00:51 <oerjan> naturally
19:00:56 <fax> but that doesn't let me that there exists a number n = 1 + n
19:01:16 <fax> because I can't prove that Ysucc is in {zero,succ(zero),...}, can I?
19:01:24 <oerjan> of course not
19:01:27 <fax> why not?
19:01:56 <oerjan> well assuming you define succ so it doesn't cycle
19:02:15 <fax> zero <> succ(zero) etc
19:02:51 <oerjan> you are basically constructing a new model of the peano axioms
19:03:03 <oerjan> for which succ n = n has no solution
19:04:46 <oerjan> anyway standard church numerals give you such a sequence
19:06:17 <fax> I think I have to internalize the notioin of 'is inductive'
19:06:44 <fax> and say that SK is not inductive so it can't exist
19:06:54 <oerjan> huh?
19:07:31 <fax> the existence of Ysucc = succ(Ysucc) means that SK isn't inductive because there is a term produced only by iteration of succ to zero but it is not in N
19:07:32 <oerjan> SK calculus is a perfectly consistent algebraic system
19:08:08 <fax> what exactly does that mean?
19:08:26 <oklopol> that it has a model?
19:08:28 <oerjan> that it certainly exists in set theory
19:08:37 <fax> alright
19:09:21 <fax> but there is no set in set theory X = X -> X
19:09:26 <fax> there is only X ~ X -> X
19:09:30 <oerjan> also why should that kind of inductive apply to SK - it contains _much more_ than just your succ sequence
19:09:45 <fax> so the equality of SK terms is more like a quotient of set equality than actual set equality
19:09:59 <fax> if a b in SK, a == b then the set a might not equal the set b
19:10:01 <oerjan> yeah it cannot be modeled with set functions
19:10:36 <fax> hmmmmm
19:10:40 <oklopol> oerjan: there is a bijection between naturals and all SK expressions though, so if you define succ as enumerating them, doesn't it contain exactly the succ sequence?
19:11:09 <fax> it can't be modelled by set functions because X <> X -> X
19:11:09 <fax> is that the proof?
19:11:10 <fax> I don't know how to show that X = X -> X is the only possible model of SK
19:11:10 <oerjan> there _is_ however a model using continuous set functions such that the space of functions is topologically equivalent to the space of arguments
19:11:30 <oerjan> see that CPO denotational semantics stuff
19:11:49 <oklopol> yeah topologically equivalent whoosh
19:11:54 <fax> hehe
19:13:06 <oerjan> oklopol: it would be hard, probably impossible, to make succ be given by an SK expression itself for that complete enumeration
19:13:32 <oklopol> oerjan: yeah i was just wondering that, didn't realize succ was an sk expression
19:13:33 <oerjan> in fact that's obvious from the existence of fixpoints
19:13:53 <oklopol> all combinators have fixpoints?
19:13:56 <oerjan> yes
19:14:04 <oerjan> Y f = f(Y f)
19:14:04 <oklopol> holy shit that's sexy
19:14:16 <fax> oklopol you can prove it yourself
19:14:27 <fax> it only uses composition and Ux = xx
19:15:00 <fax> you don't need S or K or anything
19:15:40 <oklopol> could someone link me to a download button that gives me a fucking english openoffice
19:16:04 <oerjan> fax: i expect the impossibility of modeling lambda calculus using X = X -> X as sets was a major motivation for the invention of that CPO theory.
19:16:21 -!- BeholdMyGlory has joined.
19:16:54 <ais523> oklopol: http://openoffice.bouncer.osuosl.org/?product=OpenOffice.org&os=winwjre&lang=en-US&version=3.1.1 (OpenOffice.org US English version, and a bundled JVM)
19:17:00 <ais523> that's the Windows version
19:17:18 <AnMaster> strange... when I X-forward a gtk application over ssh it uses the local theme to the computer with the screen
19:17:19 <AnMaster> as in
19:17:27 <ais523> strangely, there doesn't seem to be a UK English version on that list
19:17:28 <oklopol> i actually found it, "English version" button linked to the page with the link to downloading the finnish version
19:17:38 <AnMaster> not the gtk theme on the computer the application is running on
19:17:41 <oklopol> but that page also had a small link with "more languages and versions"
19:17:49 <AnMaster> anyone has any clue why?
19:18:06 * AnMaster looks at fizzie and ais523 as most likely to know
19:18:14 <oklopol> why the fuck can't people make good webpages, you know, ones that have a fucking button that lets you download the one size fits all english basic product.
19:18:25 <oklopol> nothing else, just a big button
19:18:27 <ais523> AnMaster: I don't know, although it doesn't strike me as ridiculously strange
19:18:36 <AnMaster> ais523, oh?
19:18:36 <ais523> I'm not sure why it doesn't strike me as strange, though
19:18:46 <ais523> strange that it doesn't strike me as strange...
19:19:11 <AnMaster> ais523, I mean, I can't see what the other computer can know about the GTK+ theme on here
19:19:21 <ais523> maybe it doesn't have to
19:19:28 * AnMaster tries a QT application too
19:19:29 <ais523> it might just be sending generic "render GTK widget" commands
19:20:04 <AnMaster> ais523, I don't think that X has such a thing
19:20:08 <oerjan> maybe there's an X resource for it - i remember setting those, way back when...
19:20:10 <AnMaster> it isn't done on that level I mean
19:20:27 <ais523> "X doesn't have" is a statement whose falseness is of a par with "Slash'EM doesn't have"
19:20:32 <AnMaster> how does one list X resources...
19:20:36 <AnMaster> ais523, well ok
19:21:43 <AnMaster> ais523, I know something Slash'EM lacks though
19:21:48 <AnMaster> want to know what?
19:21:59 <AnMaster> balancedness
19:22:07 * oerjan has forgotten
19:22:09 <ais523> heh
19:22:40 <AnMaster> ais523, It is WAY easier to win slashem than nethack if you play as val
19:22:43 -!- Rembane has joined.
19:23:00 <AnMaster> on the other hand, winning as pretty much anything else is near impossible
19:23:01 <ais523> really?
19:23:11 <ais523> val is rather nerfed early-game in slashem
19:23:18 <ais523> I thought monk was the most broken slashem class
19:23:21 <AnMaster> ais523, "nerfed"?
19:23:29 <ais523> weakened by making arbitrary changes
19:23:35 <ais523> in an attempt to balance
19:23:38 <AnMaster> ais523, and monk isn't too bad in slashem either
19:23:48 <ais523> broken = too powerful for balance
19:23:57 <AnMaster> ais523, but I meant later on. As in "after the quest"
19:24:19 <ais523> post-quest, you can generally win with anything in NetHack, and I doubt Slash'EM is that different from what I've seen of it
19:24:20 <AnMaster> ais523, val is pretty easy in nethack too
19:24:34 <ais523> val's easy in NetHack because it has the best early-game, and the late-game's irrelevant
19:24:47 <ais523> (wiz late-game blows everyone else out of the water, tou late-game is pretty good too...)
19:24:56 <AnMaster> well yes
19:25:19 <AnMaster> b
19:25:31 <AnMaster> err, why was there a b in the buffer heh
19:26:59 <ais523> because you screwed up C-x b to switch?
19:27:18 <AnMaster> ais523, I'm actually using xchat atm
19:27:25 <AnMaster> over X forwarding
19:27:28 <ais523> ah
19:27:37 <ais523> well, you tried to type emacs commands into a non-emacs program, then
19:27:41 <AnMaster> ais523, that is the GTK app I mentioned above
19:28:05 <AnMaster> ais523, I usually mix up nano and emacs. No problems with other apps
19:28:39 <AnMaster> like: Ctrl-O to save in emacs and C-x C-s to save in nano
19:28:44 <AnMaster> (instead of the reverse)
19:30:08 <fizzie> I don't know any GTK details; but I don't think it's done via X resources. "xrdb -query" lists at least what you set. Oh, and if you change your .gtkrc, you can gdk_event_send_clientmessage_toall an _GTK_READ_RCFILES event, which to me sort of implies that all the GTK clients themselves are responsible for reading the settings. (This doesn't explain why it would use the GTK theme on the local X server, though. But maybe it can query that somehow. Who knows.)
19:30:41 <AnMaster> fizzie, KDE/QT apps seems to not do this
19:31:40 <AnMaster> huh why is there stuff like:
19:31:46 <AnMaster> Netscape*selectForeground:      #ffffff
19:31:46 <AnMaster> Netscape*thermo.slider.background:      #dcdcdc
19:31:46 <AnMaster> Netscape*thermo.slider.foreground:      #0a5f89
19:31:46 <AnMaster> Netscape*topShadowColor:        #ffffff
19:31:51 <AnMaster> in that command's output
19:32:17 <AnMaster> (no I didn't set it, no I don't use netscape)
19:32:38 <oerjan> _really_ old global settings?
19:32:49 <oerjan> s/settings/defaults/
19:33:11 <AnMaster> oerjan, possibly
19:33:21 <fax> what's the axiom of lambda calculus that prohibits the trivial model?
19:33:34 <AnMaster> oerjan, but this system I'm checking on is from, like, 2006. And X was updated last week on it
19:33:48 <oerjan> fax: i don't think lambda calculus is usually thought of that way
19:33:59 <oerjan> the expressions are symbolic
19:34:18 <oerjan> and you define "equality" by reductions
19:34:33 <fax> oh so you say: these are equal, and nothing else is
19:34:39 <oerjan> yeah
19:34:45 <fax> I see
19:35:36 <oerjan> but you could probably define other models - but then you'd probably include the trivial one
19:35:54 <fizzie> X resources might come from any of the myriad moving parts involved in the X startup. At least my system has a /etc/X11/Xsession.d/30x11-common_xresources to pull in all files defined in $SYSRESOURCES; and that comes from /etc/X11/Xsession; and refers to all files in /etc/X11/Xresources/; if your system uses the same layout, maybe something left some old files there.
19:36:25 <fizzie> I have a bit curious "*customization: -color" resource from there.
19:37:03 -!- Slereah_ has joined.
19:37:13 <oerjan> AnMaster: well i meant it could be old cruft that nobody has bothered to delete
19:37:26 <AnMaster> fizzie, yes me too
19:37:28 <AnMaster> err XD
19:37:50 <AnMaster> fizzie, only on my ubuntu system too
19:37:59 <AnMaster> not on my gentoo desktop
19:38:05 <AnMaster> it has netscape stuff though
19:38:16 <fizzie> Yes, everyone seems to do X startup a bit differently.
19:38:24 -!- eurythmia has joined.
19:38:27 <AnMaster> fizzie, also the system *never* had netscape installed
19:38:35 <AnMaster> due to being 64-bit from the beginning
19:38:48 <fizzie> This was Debian, but Ubuntu and Debian are best pals and all.
19:38:53 <fax> math is hard :P
19:38:58 <AnMaster> fizzie, I meant the colour stuff is only on my ubuntu laptop
19:39:01 <fax> I don't think I can complete my proof
19:39:03 <AnMaster> not on my gentoo desktop
19:39:18 <oerjan> fax: what proof?
19:39:49 <fax> was trying to show that the theory of SK has no model in a strongly normalizing lambda calculus
19:40:05 <oerjan> oh.
19:41:06 <fax> I'm sure it's true that's good enough yeah?
19:41:18 <AnMaster> fizzie, you have macs on your network right? And ubuntu systems?
19:41:23 <oerjan> huh?
19:41:50 <fizzie> AnMaster: Er, well, not simultaneously, no; the iBook dualboots to OS X and Ubuntu, but that's my only Ubuntu system.
19:41:56 <AnMaster> oh ok
19:42:06 <oerjan> that succ fixpoint does sound like a good idea for that
19:42:18 <AnMaster> was about to ask you to install mdns-scan on a ubuntu system and run it and see how many lines was returned
19:42:29 <AnMaster> it is fairly interesting how 90% of it is macs on all networks I tried it on
19:43:21 <AnMaster> fizzie, of course, any linux computer would do I guess
19:43:33 <AnMaster> and doesn't fungot run on that OS X system?
19:43:34 <fungot> AnMaster: yeah, and it's about what sounds good when it's spoken. or read or whatever. :)
19:43:43 <AnMaster> sounds like OS X...
19:43:48 <AnMaster> all about the user experience
19:43:59 <AnMaster> how very relevant fungot's comment was
19:44:00 <fungot> AnMaster: they don't really think so? :) that just makes it nicer to still name the new function.
19:44:15 <AnMaster> well less so now
19:46:07 <fizzie> Fungot typically runs on my in-DMZ virtual-server laptop; that's a Debian system. And I'm pretty sure there's nowadays no other mdns-based services floating around, but I used to have a media server thing setup with Avahi's mdns-repeater across the network segments here.
19:46:53 <AnMaster> fizzie, "no other" than what?
19:47:06 <fizzie> No other than what the iBook blubbers about when it's on.
19:47:14 <AnMaster> fizzie, ah
19:47:20 <AnMaster> + MacBook Nr093380 [00:1b:63:37:41:f5]._workstation._tcp.local
19:47:20 <AnMaster> + MacBook Nr093380._sftp-ssh._tcp.local
19:47:20 <AnMaster> + MacBook Nr093380._ssh._tcp.local
19:47:23 <AnMaster> for example
19:47:40 <AnMaster> no need for nmap there. Can just ask it nicely
19:47:42 <AnMaster> :P
19:48:38 <AnMaster> bbl in a bit
19:53:27 -!- Slereah has quit (Read error: 110 (Connection timed out)).
20:08:45 <AnMaster> back
20:08:59 <AnMaster> hm did I actually say "bbl in a bit" XD
20:10:08 <fax> bbiab back later
20:14:13 -!- adam_d has joined.
20:19:05 -!- eurythmia has quit (Read error: 60 (Operation timed out)).
20:20:21 <AnMaster> Gregor, there? Prod
20:20:37 <AnMaster> wasn't it you who was behind that extra-www site?
20:20:46 <AnMaster> (or do I completely misremember?)
20:37:21 -!- kar8nga has joined.
20:45:39 <AnMaster> oerjan, I have a math question
20:46:14 <AnMaster> Is 3↑↑↑↑3 too large to write out in this universe? (that is g₁ btw)
20:46:28 <AnMaster> I know of course g₆₄ is
20:46:36 <AnMaster> but I was wondering about g₁
20:46:59 * oerjan cannot hear you because of the unicode LALALALA
20:47:21 <AnMaster> oerjan, that was 3^^^^3 and g_1 and g_64
20:47:23 <AnMaster> better?
20:47:30 <oerjan> yeah
20:47:31 <AnMaster> except ^ is not Knuth's up-arrow
20:47:43 <oerjan> it isn't?
20:47:48 <AnMaster> oerjan, no ↑ is
20:47:55 <AnMaster> you forgot the base of the arrow
20:47:56 <AnMaster> basically
20:47:58 <oerjan> how unfortunate
20:48:08 <Slereah_> AnMaster : It's obviously not too large to write, since you just did it
20:48:18 <Slereah_> OR DO YOU MEAN USING SCIENTIFIC NOTATION
20:49:26 <oerjan> http://en.wikipedia.org/wiki/Knuth's_up-arrow_notation#Tables_of_values
20:49:31 <oerjan> see second table
20:50:06 <AnMaster> Slereah_, I meant expanded using scientific notation yeah
20:50:11 <AnMaster> or actually full one
20:50:16 <AnMaster> as just integers
20:50:25 <AnMaster> full value
20:50:31 <AnMaster> s/integers/digits/
20:50:39 <oerjan> yes that would be far too large
20:50:54 <oerjan> it's not even written in the table...
20:50:56 <AnMaster> oerjan, eh that table. Fail to read it
20:51:00 <AnMaster> what is what in it
20:51:08 <AnMaster> m\n
20:51:09 <AnMaster> wait what
20:51:21 <AnMaster> the difference between the set m and the set n?
20:51:26 <AnMaster> *blink*
20:51:53 <oerjan> see the caption above
20:52:06 -!- MigoMipo has joined.
20:52:08 <oerjan> the \ is to separate the axes
20:52:12 <AnMaster> ah
20:52:20 <AnMaster> and it uses 2 not 3
20:52:32 <AnMaster> in front I mean
20:52:41 <AnMaster> oh wait
20:52:43 <AnMaster> wrong table
20:54:17 <AnMaster> oerjan, is it correct to say that each up arrow adds another "level of operator"ish. Like addition is related to multiplication?
20:54:40 <AnMaster> same is the relationship change between ^^ and ^^^ . Between n ^ and n+1 ^
20:54:46 <oerjan> more or less
20:55:08 <AnMaster> oerjan, "more or less"?
20:55:56 <oerjan> or, exactly that
20:57:33 <AnMaster> ah
20:57:42 <AnMaster> oerjan, why "more or less" first time then :P
20:57:58 <AnMaster> (just time to think about it without admitting you had to?)
20:58:49 * oerjan swats AnMaster for knowing too much -----###
20:58:53 <AnMaster> oerjan, you know *way* more math than I do
20:59:16 <oerjan> *MWAHAHAHA*
20:59:33 <AnMaster> oerjan, that is why I keep asking you :P
21:03:25 -!- augur has joined.
21:03:32 <oklopol> my dream is to surpass oerjan in 3 years.
21:03:47 <oklopol> that's pretty much my only goal in life
21:04:02 <augur> so ive designed a modification of the lambda calculus that has absolutely no nesting, but instead has explicit scopal relationships.. :T
21:06:15 <oklopol> you and your crazy get rich quick schemes
21:06:48 <augur> :P
21:07:42 <oklopol> well are you going to explain it?
21:07:54 <oklopol> DO DO SO
21:09:09 <augur> well, essentially what you do is you mark out all of the applications and variable bindings explicitly
21:09:12 <augur> so in a simple case
21:09:22 <augur> say you have the expression <f x>
21:09:54 <augur> this would convert to the set { f[i][], x[][i] }
21:09:59 <oklopol> application of f with argument x?
21:10:03 <augur> yeah
21:10:21 <augur> the first slot there indicates the functions unique identifier index
21:10:40 <augur> and the second slow indicates what function that value is taken as argument to
21:11:08 <augur> f (g x) becomes { f[i][], g[j][i], x[][j] }
21:12:02 <oklopol> and (f g) x?
21:12:17 <oklopol> what's the name of the result of (f g)
21:12:26 <augur> { f[i][], g[][i], x[][i] }
21:12:40 <oklopol> so it's not a set it's ordered?
21:12:47 <augur> eh. sure. :p
21:12:53 <oklopol> alright.
21:13:08 <augur> all things with the same lower index are mutually totally ordered
21:13:12 <augur> so for instance
21:13:32 <augur> f 1 2 => { f[i][], 1[][i], 2[][i] }
21:13:45 <augur> f 2 1 => { f[i][], 2[][i], 1[][i] }
21:14:11 <augur> but things with different lower indexes are not ordered relative to one another
21:14:19 <oklopol> (((s (s k)) k) i) => { s[1][] s[2][1] k[][2] k[][1] i[][1] }
21:14:44 <augur> so f 1 2 also => { 1[][i], f[i][], 2[][i] }, { 1[][i], 2[][i], f[i][] }
21:14:56 <oklopol> yes, i get it
21:15:12 <augur> for lambda abstractions
21:15:15 <oklopol> also that's a very weird kind of set.
21:15:17 <oklopol> :P
21:15:21 <augur> well, it is sort of
21:15:25 <augur> its a partially ordered set
21:15:30 <oklopol> (if you want to think of it as a kind of set)
21:15:37 <augur> the cool part is the reduction rules
21:15:47 <augur> so let me tell you about lambda abstractions first
21:16:13 <augur> \x.x => { [i][]\x, [][i]x }
21:16:48 <augur> \x.(f x) => { [i][]\x, [][i]f[j][], [][i]x[][j] }
21:17:34 <augur> an application of the first looks like so:
21:18:22 <augur> (oh, btw, i was omitting the [][] after things since [][] is recoverable)
21:18:50 <oklopol> isn't it simply ((\x.x) f) => { f[][i] [i][]\x, [][i]x }
21:18:53 <augur> \x.x 5 => { [i][]\x[j][], [][i]x[][], [][]5[][j] }
21:18:59 <oklopol> *f[][i],
21:19:14 <oklopol> hmm
21:19:16 <oklopol> lessee
21:19:34 <augur> the left brackets tell you the bindings, the right brackets tell you the applications
21:19:35 -!- KingOfKarlsruhe has quit (Remote closed the connection).
21:20:28 <augur> so to reduce this, what you do is you take everything in the set that is pre-subscripted [i] (e.g. stuff like [_][i]_[_][_])
21:21:04 <augur> and you replace it with [_][]_[_][_] if its _not_ the variable bound by the lambda
21:22:27 <augur> and if it IS the variable bound by the lambda, you remove it, and substitute into the set a copy of the value application-bound by the lambda
21:22:48 <augur> but where that copy has all the application bindings of the variable its replacing
21:22:51 <augur> so:
21:23:27 <augur> { [i][]\x[j][], [][i]x[][], [][]5[][j] } becomes { [][]5[][] }
21:24:24 <augur> because you drop lambda, drop the [][i]x[][], copy [][]5[][j] over, retaining the lambda bindings [][] from its left, and replacing the application bindings [][j] with the application bindings of [][i]x[][], namely, [][]
21:24:27 <augur> thus, [][]5[][]
21:24:40 <augur> a more complicated version might be this:
21:25:44 <augur> \x.(sqrt x) 25 => { [i][]\x[j][], [][i]sqrt[k][], [][i]x[][k], [][]25[][j] }
21:26:01 <augur> here we drop the \x part, and the x part
21:26:43 <augur> we also replace [][i] on the things that have it with [][]
21:26:44 <augur> and
21:26:51 <AnMaster> hm
21:26:56 * AnMaster thinks this printout got messed up (translated from Swedish): "Travel time: 41.00 SEK   Date: 2   Changes: 675.00   Number of zones: 2009-10-20   Cost: 00:52"
21:27:13 <augur> copy 25 over, keeping its lambda bindings ([][]) on its left, and replacing it's application bindings ([][j]) with the application bindings of the x ([][k])
21:27:15 <augur> resuling in
21:27:19 <AnMaster> from router planner for local commuter bus company
21:27:30 <augur> { [][]sqrt[k][], [][]25[][k] }
21:27:43 <olsner> AnMaster: good day axe handle
21:27:46 <augur> which is the the translation of sqrt 25
21:27:57 <AnMaster> olsner, XD
21:28:15 <AnMaster> olsner, the worst part is that there is 1 change and somewhere between 6 and 10 zones
21:28:31 <AnMaster> so the values 2 and 675.00 doesn't fit in *anywhere*
21:29:37 <augur> the only things that must be lambda bound are the highest thing in the body of the lambda (so if the lambda were \x.\y.x+y, + would only be lambda bound by \y, and \y would be bound by \x)
21:29:42 <olsner> maybe the travel planner is taking you on a 668 zone round-trip
21:29:47 <augur> as well as the variables bound by the lambda
21:29:55 <augur> is make sense, oklopol?
21:32:10 <olsner> AnMaster: do you have a link or something? this calls for public ridicule
21:32:35 <oklopol> augur: i'll read
21:32:37 <oklopol> was away
21:32:44 <oklopol> :P
21:32:51 <AnMaster> olsner, nah it seems kind of generated. Because it keeps changing when I reload the page
21:33:03 <AnMaster> now it is mixed up so that the zone count is 41:00
21:33:10 <augur> infact, oklopol, you might even say that you can, in principle, not lambda-bind other lambdas, if you lambda-bind everything multiple times
21:33:24 <AnMaster> oh olsner Länstrafiken Örebo Län anyway
21:33:30 <AnMaster> ,*
21:34:18 <AnMaster> olsner, not sure if it matters but I'm planning a route that is first a landsvägsbuss then a city bus
21:34:46 <AnMaster> (don't want to pinpoint where I live or where I'm going on irc)
21:34:57 <augur> you end up with multiple bindings anyway in cases like \P.\x.Px and \x.\P.Px
21:35:12 <augur> because P is both bound by one lambda, and the value of another
21:35:13 <augur> so
21:36:21 <olsner> AnMaster: but, then we can't use the knowledge to implicate you in a fake terrorist attack or something
21:37:46 <olsner> weird, I can't reproduce your bug
21:37:46 <AnMaster> olsner, that hadn't even come to my mind... I was more thinking about weird IRC people showing up around here (axe optional)
21:38:07 <oklopol> augur: it makes sense, although i'm not sure i could translate a complicated expression into it without further pondering.
21:38:15 <augur> thats ok.
21:38:16 <AnMaster> olsner, it seems fairly reproducible here. Though exactly how it is messed up varies
21:38:31 <oklopol> what do multiple bindings look like?
21:38:34 <AnMaster> strange
21:38:39 <augur> whats cool i think is that doing it this way, oklopol, might make points-free trivial
21:38:43 <augur> howdja mean multiple bindings
21:38:46 <AnMaster> <oklopol> what do multiple bindings look like?
21:38:46 <AnMaster> <AnMaster> strange
21:38:47 <AnMaster> XD
21:38:53 <oklopol> :P
21:39:03 <oklopol> augur: you end up with multiple bindings anyway in cases like \P.\x.Px and \x.\P.Px
21:39:08 <augur> oh
21:39:10 <augur> just like
21:39:10 <oklopol> translate
21:39:13 <olsner> searching for something like storgatan fjugesta to studentgatan universitetet just gives me a normal travel plan with everything in the right column
21:39:16 <AnMaster> olsner, maybe it only messes up for those living here?
21:39:32 <AnMaster> olsner, what tab? it wasn't the first one
21:39:44 <AnMaster> it was "reseväg"
21:39:47 <AnMaster> oh and only in print view
21:39:58 <augur> \P.\x.Px becomes { [i][]\P[][], [j][i]\x[][], [][i,j]P[k][], [][j]x[][k] }
21:40:07 <AnMaster> forgot to mention that
21:40:10 <oklopol> okay so just comma, makes sense
21:40:16 <augur> P gets two lambda bindings
21:40:21 <augur> one for \P where its a variable
21:40:30 <augur> and one for \x where it's the return value
21:40:30 * oklopol scrutinizes
21:40:35 <AnMaster> olsner, does everything look correct?
21:40:41 <augur> it might be useful to distinguish those two
21:40:43 <augur> im not sure
21:41:06 <AnMaster> olsner, also why studentgatan? *suspicious look*
21:41:26 * AnMaster wonders if olsner lives in Örebro or around
21:42:00 <olsner> AnMaster: I searched for storgatan and götgatan and hoped there would be some streets with similar names somewhere in or near or far outside örebro
21:42:00 <AnMaster> because how else could you have guessed that there is studentgatan universitetet
21:42:03 <AnMaster> ah
21:42:13 <AnMaster> storgatan yes
21:42:25 <AnMaster> götgatan sounds like Göteborg or Stockholm to me
21:42:40 -!- oerjan has quit ("leaving").
21:42:49 <oklopol> augur: alright makes sense, although i don't see why you couldn't just link P to x, and inherit bindings through the chain... or does that make reductions uglier?
21:42:57 <AnMaster> olsner, anyway you managed to pick my destination ± a few hundred meters :P
21:43:12 <olsner> then I picked something in the list of matches that sounded like it was well outside örebro (fjugesta) and something else that was in örebro but would require a bus trip inside örebro (to get a city bus in the itinerary)
21:43:18 <augur> oklopol, you might be able to. im just toying around with this right now.
21:43:45 <AnMaster> olsner, I would assume some high numbered bus (>100) to Resecentrum then bus 12 from there?
21:43:55 <olsner> right, the print view picks a previously displayed price as the number of zones
21:44:14 <AnMaster> olsner, which price?
21:44:22 <AnMaster> and I got more errors than that
21:44:28 <AnMaster> as I mentioned above
21:44:55 <olsner> it seems to have picked the price of an ungdom pendlarkort as the number of zones for me
21:44:59 <AnMaster> ah.
21:45:14 <AnMaster> actually that could be quite accurate for the 675.00 figure I got
21:45:21 <augur> oklopol, yeah. awesome. points free is trivial. :)
21:45:26 <AnMaster> (I don't have that card myself)
21:45:35 <oklopol> augur: cool
21:46:04 <olsner> I don't get the travel time or date or changes or price columns mixed up though, just random data in the number of zones
21:46:20 <olsner> Alternativ 1Restid: 00:59Giltig: 2009-10-19Byten: 1Antal zoner: 785,00Pris: 20,00 SEK
21:46:23 <AnMaster> olsner, ah. Lucky you
21:46:41 <AnMaster> olsner, if it matters I only had alternativ 2 checked on the first page
21:46:44 <augur> ok so heres how it works, oklodilly
21:46:44 -!- fax has quit (Remote closed the connection).
21:46:47 <augur> if you have something like this:
21:47:07 <AnMaster> olsner, also I consistently get one change too much
21:47:08 <augur> (\f.\x.fx) sqrt 2
21:47:12 <AnMaster> that is 2, instead of 1
21:47:44 <AnMaster> olsner, also what the hell... 20 SEK... 785.00 and 59 minutes of travel Huh.
21:48:07 <AnMaster> I live closer and it costs more, almost as long travel time, but the card is cheaper
21:48:13 <AnMaster> how very strange logic
21:48:44 <augur> this becomes { [i][]\f[j][], [k][]\x[l][], [][]sqrt[][j], [][]2[][l] }
21:48:44 <olsner> you're adult?
21:48:56 <AnMaster> olsner, 19.
21:48:59 <AnMaster> still a student
21:49:10 <AnMaster> but well it would cost the same without a special card I think?
21:49:12 <AnMaster> well,*
21:49:20 <augur> (im sure theres a way to calculate this automatically but for now you need to explicity say which value will go into which lambda)
21:50:03 <AnMaster> olsner, still. It wouldn't know how old I am afaik.
21:50:07 <AnMaster> I never told the site.
21:50:14 <AnMaster> and I *do* have a card. A different one though
21:50:23 <AnMaster> (rabattkort vuxen)
21:50:31 <olsner> well, I was thinking that you might have picked a random different card in the drop-down than me
21:50:39 <AnMaster> olsner, I didn't pick any
21:50:48 <AnMaster> didn't notice that menu at all
21:50:56 <augur> er
21:51:01 <augur> sorry oklopol, that was wrong
21:51:42 <AnMaster> olsner, it says "vuxen kontant" here
21:51:45 <AnMaster> if that is what you mean
21:52:25 <augur> \f.\x.fx sqrt 2 becomes [i][]\P[v][] [j][]\x[w][] [][i,j]P[k][] [][j]x[][k] [][]sqrt[][v] [][]2[][w]
21:53:22 <augur> which reduces to points free [i][]\P[v][] [][i]P[w][] [][]sqrt[][v] [][]2[][w]
21:53:22 <olsner> ah, looks like there's quite some variation depending on exactly how far you go... that's why my price never matched yours
21:53:38 <augur> if you didnt have the actual argument value 2, you'd get the same things, minus the 2 values
21:54:00 <augur> because of the way the de-pointing works
21:54:18 <AnMaster> olsner, interestingly is cost half as much to take the "local city bus in small town -> station -> landsvägsbuss -> other landsvägsbuss -> city bus in Örebro" as just "landsvägsbuss -> city bus in Örebro"
21:54:25 <AnMaster> that doesn't quite make sense to me
21:54:46 <AnMaster> hell I didn't even know there were city buses in this small town
21:55:03 <augur> which is cool
21:56:08 <augur> depointing is essentially just application, too. because the lambdas are such that order is irrelevant, it's _essentially_ as if it were a lambda expression with multiple, unordered arguments
21:56:14 <augur> \{x,y,z}.E
21:57:26 <augur> infact, i think what i've done is almost get to a tarskian style system without lambdas... hm
21:58:59 <augur> i think ill just make it tarskian
22:00:55 -!- kar8nga has quit (Read error: 54 (Connection reset by peer)).
22:02:28 -!- MigoMipo has quit (Ping timeout: 180 seconds).
22:03:42 <augur> hm. tarskian logic makes points free so easy
22:04:01 <augur> well, its not _really_ points free, but
22:04:19 <augur> then again, neither is what i just did
22:06:51 <oklopol> i don't know trsk
22:08:40 <augur> its pretty cool stuff
22:08:43 <augur> basically
22:08:50 <augur> you have three sets of primitives
22:09:15 <augur> primitive values, lets denote those as v, v', v'', ...
22:09:21 <augur> primitive variables
22:09:28 <augur> denote them as x, x', x'', ...
22:09:50 <augur> primitive values are finite in number, variables are infinite
22:09:53 <augur> you also have open sentence classes
22:09:56 <augur> where
22:10:41 <augur> Fx, Gxx', ... denote multiple open sentences, with arbitrary variables in each spot
22:10:58 <augur> so Fx as a family denotes the sentences {Fx, Fx', Fx'', ... }
22:11:41 <augur> Fxx' as a family denotes { Gxx, Gxx', Gxx'', ... Gx'x, Gx'x', Gx'x'', ... Gx''x, Gx''x', Gx''x'', ...}
22:11:45 <augur> ok?
22:12:45 -!- Raevel has joined.
22:12:59 -!- Raevel has left (?).
22:15:58 -!- fax has joined.
22:19:54 -!- ehird has joined.
22:21:15 <oklopol> what's x', x'' etc?
22:21:19 <oklopol> errr
22:21:21 <oklopol> nm that
22:21:23 <oklopol> go on
22:21:27 <ehird> 01:27:04 <ais523> this is probably old news, but: apparently when RMS wants to read a web page, he emails a daemon that wgets it and emails him back with the resulting page
22:21:28 <ehird> Seriously?
22:21:41 <ais523> I had a link to it open a while ago
22:21:43 <ehird> We've been mocking that for at least a year. Maybe a year and a half.
22:21:47 <Deewiant> Seriously as in is he seriously spreading such old news or seriously... yeah.
22:21:51 <ais523> I guessed it was old news
22:21:59 <ehird> (You, on the other hand, wait a year and then start up w3m, I guess. :D)
22:22:01 <ais523> really, you should tell me the things you've known for ages
22:22:05 <ais523> so I don't end up telling you
22:22:07 <oklopol> Deewiant: uh this is ehird we're talking about
22:22:14 <ehird> ais523: But IRC isn't high-bandwidth enough!
22:22:19 <ehird> <oklopol> CONDESCENDING ANTI-EHIRD STATEMENT
22:22:23 <oklopol> :D
22:22:32 <oklopol> how is knowing everything not a good thing
22:22:56 <ehird> i thought it was going to be something like "HE ALWAYS GOES FOR THE MORE INSULTING OPTION"
22:22:59 <ehird> :D
22:23:15 <oklopol> well partly that too :P
22:23:26 <oklopol> but that's getting a bit old
22:24:44 <ehird> 04:16:28 * ais523 wonders how quickly the other OSes will get that particular bit of political information...
22:24:45 <ehird> Let me check Software Update!
22:25:22 <ehird> (Theory: Apple names a good portion of its applications without metaphor so as to monopolise their respective markets on OS X.)
22:25:36 <ehird> Who needs a mail client if you can just open Mail?
22:25:46 <ais523> that's a clever theory
22:25:55 <ais523> allegedly, Microsoft try to do the same thing but with icons
22:25:59 <ehird> heh
22:26:04 <ehird> Yes, that e is so... unmetaphoric.
22:26:07 <ais523> the theory being that half their users can't use Firefox
22:26:16 <ais523> because they wouldn't be able to open it, because the icon is wrong
22:26:24 <ehird> Yes, but IE's icon is not literal or anything.
22:26:30 <ehird> It's just a well-known symbol.
22:26:33 <ais523> yes
22:26:39 <ais523> they try to ingrain it in conciousness
22:26:44 <ais523> it was all over the place in Win98, for instance
22:27:26 <oklopol> i had to look to remember what it's like
22:27:34 <ais523> wow
22:27:53 -!- fax has quit (Remote closed the connection).
22:27:54 <ehird> Contrast: "Automator", "Calculator", "Chess", "Dictionary", "DVD Player", "Image Capture", "Preview" (admittedly it should probably be called "View" to fit into this perfectly, but eh), "System Preferences" (Okay, okay, it's a system tool, this is fine), "Time Machine" (I'm joking, I'm joking, OS X does not, in fact, contain a time machine)
22:27:57 <oklopol> then again i'm oklopol
22:28:09 <ehird> ais523: So more "monopolising the obvious namespace" as opposed to "ubiquitising an abstract".
22:28:14 <ais523> yes
22:28:16 <ehird> (FUN TECHNOBABBLE! ^____^)
22:28:30 <ehird> Nope, no timezone update.
22:28:34 <ais523> Ubuntu's been doing that too to some extent, but only on the menus
22:28:38 <augur> oklopol
22:28:40 <ais523> not on the application names themselves
22:28:41 <ehird> Poor Argentinean OS X users!
22:28:44 <ehird> ais523: no, that's a GNOME policy
22:28:47 <ais523> ah
22:28:49 <augur> ok well once you have these primitive objects
22:28:55 <augur> you can define certain combinatorics
22:28:58 <augur> for instance
22:29:05 <ehird> ais523: Anyway, my conspiracy theory is very silly; more obvious names are better.
22:29:09 <ais523> I'm pretty sure I've seen blog posts about Ubuntu themselves being involved with it too
22:29:13 <augur> if S and S' are sentences (open or closed) so is S & S'
22:29:24 <ais523> ehird: why can't it be a me-style conspiracy
22:29:31 <ais523> when you go around doing actual useful and beneficial things
22:29:32 <augur> so if your sentences are Fx and Gxx', then Fx & Gxx' is also a sentence
22:29:35 <ais523> that just happen to aid a conspiracy too?
22:29:44 <ehird> ais523: because that's additional work?
22:30:10 <ehird> [[FatELF - the Linux equivalent of what Mac OS X calls "Universal Binaries."]]
22:30:14 <ehird> What a terrible idea!
22:30:24 <ais523> it should be able to do them, IMO
22:30:27 <augur> also, if S is a sentence with an open variable x any number of times, then you can replace all occurances of that variable with a primitive value and get another sentence
22:30:28 <ais523> although, nobody should actually use them
22:30:29 <ehird> "Bigger executable files! Dumber package management! RAAAAAAAAAAR!"
22:30:34 <ehird> ais523: "Benefits:" *huge list*
22:30:39 <ehird> This guy wants people to actually use it ;__;
22:30:47 <augur> so if your sentence is Fx & Gxx', you can replace x with v to get Fv & Gvx'
22:31:02 <ehird> On OS X, it makes sense; people are downloading applications without a package manager.
22:31:13 <augur> and notice this conveniently abstracts away from lambda binding orderings
22:31:14 <ehird> (Although not so any more! Snow Leopard dropped support for PowerPC.)
22:31:28 <ehird> (So... everyone who bought a Mac before 2005-2006... fuck you!)
22:31:32 <augur> Gxx' = both \x.\x'.Gxx' and \x'.\x.Gxx'
22:31:43 <augur> you can substitute for either variable in either order
22:31:50 <oklopol> yeah
22:32:24 <augur> the & combinator also abstracts over forking over primitive conjunction
22:32:45 <augur> in tarski's logic, tho, you cant get things like G(Fx)x'
22:32:55 <augur> where whole sentences substitute for variables
22:33:01 <augur> but, i would extent that and say they can
22:33:31 <augur> which means you can define a extend the combinator to a more general notion
22:34:05 <augur> if S and S' are sentences, and x is a variable in S that's not in S', you can substitute S' for x in S to derive a new sentence
22:34:36 <augur> e.g. Gxx', Fx'' => G(Fx'')x'
22:34:54 <augur> but not Gxx', Fx => G(Fx)x'
22:35:11 <augur> but definitely Gxx', Fx => Gx(Fx)
22:35:35 <ehird> "Much easier to distribute, users don't have to care about what their machine precisely is, they get a single download and that single download Just Works."
22:35:48 <ehird> ais523: ah, FatELF is targeted at people who can't condition on a uname call in a shell script
22:35:51 <augur> and this essentially is a general combinator that handles all sorts of things simultaneously
22:35:52 <ehird> it all makes sense now
22:35:55 <ehird> :P
22:35:55 <augur> forking is trivial
22:36:45 <ehird> "A fat Elf is called a Gnome, and that name is already taken."
22:36:48 <augur> let x+x' be a primitive sentence, and let Fx'' and Gx'' be primitive sentences, you can substitute Fx'' for x and Gx'' for x' in x+x'' to derive Fx''+Gx''
22:37:04 <ais523> ehird: gnomes are much shorter than elves, though...
22:37:08 <augur> and you've just build yourself a fork over + F and G
22:37:22 <ehird> augur: could you take this to /msg oklopol?
22:37:28 <augur> ehird, no.
22:37:36 <ehird> my mental filter algorithms overfloweth with eths
22:37:37 <oklopol> hehe
22:37:57 <augur> s'at make sense oklopol?
22:37:58 <ehird> oklopol: start singing about bees to augur, please
22:38:31 <oklopol> augur: somewhat.
22:38:36 <oklopol> less than you'd hope
22:38:40 <augur> :p
22:38:56 <augur> its even better tho because you can abstract away from variable names
22:38:59 <augur> and just use _'s
22:39:03 <augur> e.g.
22:39:17 <oklopol> let's say i'm feeling it
22:39:37 <augur> so like
22:39:45 <augur> say F(_) and G(_) are primitive sentences
22:39:55 <augur> F(_) & G(_) is a derived sentence
22:40:10 <augur> (with _two_ distinct variables)
22:40:18 <ehird> augur: Bees!
22:40:20 <ehird> Everyone likes bees!
22:40:24 <ehird> Bees grow on trees!
22:40:31 <ehird> Bees're the bees kneeeeeeeeeeees!
22:40:33 <ehird> Bees!
22:40:34 <augur> but you could also sort of ... connect the _'s with lines under then to denote that they're the "same"
22:40:36 <ehird> Everyone loves bees!
22:40:42 <ehird> Bees are ... great?
22:40:45 <ehird> Beeeeeeeeeeeeeeeeeeeees!
22:40:53 <ehird> Everyone loves trees! Trees grow on beeeees!
22:40:56 <ehird> Treeeeeeeeeeeeeeeeeeeeeeees!
22:41:26 <augur> if you did that, the sentence would have only one variable
22:41:26 <oklopol> yes i see what you mean
22:41:26 <ehird> augur! TREEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEES! BEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEES!
22:41:26 <oklopol> aaaaaaanyway what are sentences? :P
22:41:51 <oklopol> we had values and variables, are sentences another axiomatic sorta set of things we have
22:41:56 <augur> just strings like F(_) or G(_,_) or F(1) or G(4,_) etc
22:41:58 <ais523> ehird: ooh, it's pretty fun to see what the T-Mobile/Danger/Microsoft conspiracy theorists are saying now
22:42:02 <augur> right
22:42:06 <ehird> ais523: You know what's more fun?!?!?!
22:42:08 <ehird> BEEEEEEEEEEEEEEEEEEEEEEEEEEEEES!
22:42:17 <ehird> (what is it?)
22:42:21 <ehird> I bet it involves beeeeeeeeeeeeeeeees
22:42:27 <augur> now we're just saying sentences are things like F(_), G(_,_), etc. and all the combinations and bindings thereover
22:42:36 <ais523> apparently a) the problem was that they deleted the backups to make room for another set, then did the update halfway through the backup process, and b) the data wasn't actually recovered, Microsoft are just lying to get everyone to forget the story
22:42:43 <ais523> this is a conspiracy theorist value of "apparently"
22:42:52 <oklopol> augur: can you have F(G(5))?
22:42:52 <ehird> Treeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeees beeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeees kneeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeees!
22:43:01 <oklopol> sheeeeeeeeeeesh, ehird...
22:43:06 <ehird> ais523: i'm sure all those dataless sidekick owners will just move on
22:43:10 <augur> make sense oklopol?
22:43:11 <ehird> oklopol: what an unoklopolic sentence!
22:43:15 <ehird> maybe you need BEES
22:43:23 <oklopol> yeeeeeeeeeeeeeeeeeeeees
22:43:26 <ais523> ehird: luckily, it's a rather easily disprovable conspiracy theory
22:43:29 <augur> so
22:43:33 <ais523> let's see if the disproof happens, it shouldn't take too long
22:43:38 <ehird> ais523: EVERY SIDEKICK OWNER IS IN ON IT
22:43:44 <oklopol> (pronounced as the pattern requires ofc.)
22:43:46 <ehird> also, burden of proof btw
22:43:47 <augur> any sentence can be turned into a fork by unifying two variables with a joining line
22:43:56 <ais523> ehird: but, but this is conspiracy theories!
22:43:57 <ehird> we shouldn't wait for disproof we should wait for proof from the conspiracy theorists
22:44:15 <augur> which makes points free trivial because you just link things up
22:44:17 <ehird> ais523: You're right. I hear that http://glennbeckrapedandmurderedayounggirlin1990.com/
22:44:33 <ais523> I'm not clicking that link, it would drive the filters here crazy
22:44:36 <ais523> is that even a real website?
22:44:37 <ehird> He hasn't denied it. And Microsoft haven't denied this either.
22:44:39 <ehird> Hmmmmmmmmmmmmmmmmmm...
22:44:40 <ehird> ais523: Yes.
22:44:43 <ais523> ouch
22:44:44 <augur> wanna make \x.f(x,g(x)) points free? well, f(_,g(_)) with both vars linked, and thats it.
22:44:59 <ehird> ais523: With a bunch of plastered "parody" markers on it and enough media coverage to make that obvious.
22:45:05 <oklopol> augur: so fork just means you have a var in many places and thus rewrite them at the same time when that var is binded?
22:45:13 <ehird> But I see no parody markers ... on Microsoft's website!
22:45:19 <ehird> (That makes sense shut up.
22:45:21 <ehird> s/$/)/
22:45:33 <ais523> it would be funnier if Microsoft did mark their website as a parody
22:45:33 <augur> for tarskian stuff, yeah
22:45:57 <ehird> ais523: Anyway, maybe Glenn Beck deleted all the data.
22:45:59 <ehird> It's a possibility.
22:46:11 <ais523> does he know of the site? and does he mind?
22:46:24 <ehird> I think his lawyers rabbled a bit, maybe.
22:46:31 <ais523> I've got it! that site itself is a coverup
22:46:38 <ais523> it's designed to make the proposition in question seem ludicrous
22:46:40 <ehird> He'd probably mind, being an authoritarian Republican nutjob.
22:46:43 <ais523> such that any genuine accusations of that are ignored
22:46:49 <ehird> !
22:46:54 -!- adam_d has quit ("Leaving").
22:47:04 <ehird> "9/11 was an inside job" was an inside job. Wake up "sheeple"!
22:47:12 <ais523> (note: this amount of convolutedness occasionally happens in Agoran scams I plan, but rarely in the real world)
22:49:12 <ehird> ais523: there's now a Wolfram Alpha app for the iPhone
22:49:15 <ehird> It costs $50.
22:49:21 <ais523> wait, what?
22:49:23 <ais523> also, what does it do?
22:49:25 <ehird> I'm not joking.
22:49:29 <ehird> I don't know.
22:49:30 <ehird> Probably queries their service.
22:49:33 <ais523> if it's the obvious, then why would anyone buy it?
22:49:47 <ehird> $50! And this is in an age where apps that cost $10 are considered overpriced in the App Store.
22:50:02 <ehird> (Most cost, like, $1.99. It's a sorry state of affairs, the App Store.)
22:50:25 <ehird> ais523: Who would buy ANY mobile software for $50?
22:50:31 <pikhq> ais523: It's Wolfram.
22:50:36 <ehird> Heck, I wouldn't even buy DESKTOP software that cost that much!
22:50:49 <pikhq> Wolfram thinks that everyone else fellates him on a regular basis.
22:50:49 <ais523> is it actually an official app, I wonder?
22:50:54 <ehird> Yes...
22:50:55 <ehird> http://www.techcrunch.com/2009/10/18/wolfram-alpha-miscalculates-what-its-iphone-app-should-cost/
22:50:57 <ais523> ehird: I might, if I really needed it for my job
22:51:03 <ehird> (Sorry; TechCrunch link. Please shield your eyes.)
22:51:15 <ehird> ais523: Well, sure, if I was a designer I'd fork over the, what is it, $1,000? For Photoshop.
22:51:30 <ais523> if you needed it; and you might well do
22:51:36 <ais523> I suppose it depends on what you're designing
22:51:42 <ehird> Graphic designer, that is.
22:51:48 <ais523> and if any sensible rivals have arrived since you got your graphic design degree, or whatever
22:51:58 <ehird> I highly doubt that'll happen for many years.
22:52:23 <ehird> "I’m going to mainly focus on second point here, because if you’ve used Wolfram Alpha, you don’t really need much explanation about this app, which is a slick interface for the service. And while I get Wolfram Alpha’s logic behind selling the app for $50, I think it’s faulty logic. Here’s what they’re telling us:
22:52:23 <ehird> A note on price — it is listed at $49.99, which is basically less than 1/2 the price of a graphing calculator with inferior functionality in comparison, which is how the company came to that number. Or, as we’ve been saying, the price of 12 lattes from Starbucks…"
22:52:38 <ehird> 12 lattes from Starbucks might be the only way to spend $50 worse than buying this app
22:52:40 <ais523> but I don't drink lattes
22:52:45 <ais523> and therefore, wouldn't want to spend money on them
22:52:49 <ehird> 12 anythings from Starbucks!
22:53:04 <ais523> unless I really badly needed to buy someone else a drink, I suppose, and assuming they liked that sort of drink
22:53:17 <ehird> But I like the graphing calculator thing; it's not like I can't just, oh, HIT UP WOLFRAMALPHA.COM
22:53:22 <ehird> For a whole $0
22:53:50 <ehird> "That’s fine, but with the exception of the $90 Navigon GPS turn-by-turn app" Wow that's expensive.
22:53:53 <ais523> <quote in that article> egonomics
22:54:11 <ehird> ais523: It's TechCrunch; please, try and set up your "FUCK THIS FUCKING SITE" shield.
22:54:24 <ais523> ehird: except, that's from a quote in the article
22:54:27 <ehird> Shoddy journalism, self-righteousness, smarmy new media assholes and awful writing await.
22:54:28 <ais523> not from the article in itself
22:54:34 <ais523> IOW, it's the wolfram people who wrote that
22:54:40 <ehird> ais523: TechCrunch infects EVERYTHING IT TOUCHESE
22:54:42 <ehird> *TOUCHES
22:54:46 <ais523> although TechCrunch did call them on it mercilessly
22:55:04 <ehird> http://cache0.techcrunch.com/wp-content/uploads/2009/10/IMG_0003.PNG
22:55:09 <ehird> How big is the moon? The $50 question.
22:55:36 <ehird> ais523: Rich coming from them, they who don't verify stories before posting them, who ruthlessly demolish companies over idiocy, who... okay, I'll shut up.
22:55:43 <ais523> according to the comments, they reduced the price to $5 already
22:55:52 <ehird> (TechCrunch is really bad for the tech industry...)
22:55:59 <ehird> ais523: Hah
22:56:02 <ehird> *Ha!
22:56:14 <ehird> (Am I the only person who uses corrections for making statements better as opposed to fixing typos?)
22:56:46 <ais523> it lets you have said the right thing first time
22:56:58 <ais523> the strange thing about IRC corrections is, they're normally obvious
22:57:03 <ais523> and yet you still feel the urge to make them
22:57:04 <ehird> "It’s also interesting to note that despite talk of a deal with Bing, the defautl web search"
22:57:08 <ehird> ais523: egonomics, defautl.
22:57:10 <ehird> Oh, the irony!
22:57:36 <ais523> "invovle" is a very common typo of mine, when I actually try to type "involve"
22:57:42 <ais523> in fact, I did it in that line at the end and had to correct it
22:57:52 <ehird> Ahem. I was laughing at TechCrunch. Stop disturbing me :D
22:59:18 <ais523> fair enough
23:00:06 <ehird> 3+2=1111
23:02:06 <ais523> ?
23:02:17 <ais523> please tell me you somehow got that result from Alpha
23:02:23 <ais523> say by confusing it with special characters
23:03:19 <ais523> (I still love the way that SCO's trustee got rid of Darl by eliminating the position of CEO...)
23:07:12 <ehird> ais523: http://www.techcrunch.com/2009/10/18/wolfram-alpha-miscalculates-what-its-iphone-app-should-cost/#comment-3044256 marvel at the cognitive dissonance of someone prescribing a (terrible) "brilliant" marketing strategy to the inept, bumbling fools at Wolfram Research
23:07:37 <ehird> I got utterly confused by [[the name “Wolfram Alpha” becomes associated with luxury high-end computing power]]...
23:07:57 <ais523> heh
23:08:00 <ehird> [[this is a smart business decision, and brand enhancing for Wolfram Alpha]] dude...
23:08:28 <ais523> well, it was proved that if you make an iPhone app sufficiently expensive, people will buy it even if it does nothing
23:08:32 <ais523> (the "I Am Rich" debacle)
23:09:18 <ais523> incidentally, some of my RL friends were under the impression that the iPhone was the only high-end mobile phone in existence
23:09:23 <ais523> Apple's marketers are doing their job well
23:10:01 <ehird> To be honest, looking at the alternatives they're not *completely* wrong...
23:10:15 <ehird> ais523: the I Am Rich thing was handled terribly
23:10:16 <ais523> heh
23:10:28 <ehird> removing it from the app store was silly... although I'd still give refunds
23:10:34 <ehird> but WHAT is the mental process of the buyers?
23:10:48 <ehird> "Ha ha ha so hilarious... hmm this buy button... click... Password? This can't really work! Tap tap tap. Ahahaha."
23:10:51 <ehird> *time passes*
23:10:57 <ehird> *gets bill*
23:11:05 <ehird> "B... but I didn't think it would ACTUALLY charge me!"
23:11:17 <ehird> "I thought it was some ... hilarious joke? By... Apple?"
23:11:32 <ais523> I wonder what the most expensive iPhone app at the moment is?
23:11:41 <ehird> Possibly that $90 GPS app?
23:11:58 <ais523> given that that one's popular, I doubt it's the /most/ expensive
23:12:05 <ais523> (also, why has nobody undercut them yet?0
23:12:06 <ais523> *)
23:12:11 <ais523> we need more repos in general
23:12:30 <ehird> Yes, we need more ... source code repositories!
23:12:34 <ais523> I think the app store is proving that even amongst people generally willing to spend a lot of money on things, repos bring the price of things more in line with their actual worth
23:12:46 <ehird> (Expand repos plz)
23:13:12 <ais523> ehird: I'm using it as a general term that encompasses things like the App Store and the Ubuntu software repositories
23:13:33 <ais523> basically, sites from which you can download a large variety of software, which are relatively centralised
23:13:34 <ehird> Also, more in line with their actual worth would be "closer to $0", which, while true, that isn't the reason; iPhone piracy is hard, and piracy is what is pushing other digital information to its true worthlessness.
23:13:49 <ais523> not everyone pirates, though; some people are too honest
23:13:50 <ehird> I think it's more the fact that buying is *so easy* — you press buy, wait a few seconds to download, it's done.
23:13:54 <ehird> Or you put in the password.
23:13:55 <ais523> again, it's a case of only honest people being published
23:13:59 <ais523> *punished
23:14:06 <ehird> ais523: "honest" isn't a synonym for "law-abiding"
23:14:08 <ais523> if only the uncorrected sentence were true!
23:14:11 <ais523> ehird: it can be
23:14:20 <ais523> it means either "law-abiding" or "truth-telling" depending on context
23:14:54 <ais523> gah, Google disagrees with me
23:16:24 <ehird> "honest man" is the only context the former applies in, I believe
23:16:53 <ais523> strange
23:17:00 <ais523> besides, I was using that context!
23:17:05 <ais523> so even stranger that you call me on it
23:17:17 <ehird> "honest people" is not "honest man".
23:17:43 <ehird> Anyway, I'm not sure I can agree with "if only [law-abiding people were published] [was] true!".
23:17:46 <ais523> yes it is, it's a straightforward generalisation
23:17:54 <ehird> ais523: Yes, and idioms are repellant to that.
23:18:01 <ais523> not really
23:18:22 <ehird> Your mom
23:18:38 <ais523> you have to realise I'm part of organisations where the good sort of political correctness is so ingrained in the mentality that things that are, say, gender-biased for no good reason almost feel grammatically incorrect
23:19:29 <oklopol> your parent
23:19:33 <ehird> Hey, I totally agree (http://www.cs.virginia.edu/~evans/cs655/readings/purity.html is one of my favourite things ever) with the gender-neutral thing, it's just that a whole bunch of idioms only work because they're archaic; their literal meaning being entirely different.
23:19:38 <ehird> So "honest people" doesn't really work.
23:19:42 <oklopol> is what you should've said
23:19:45 <ehird> It sort of does, but eh.
23:19:49 <ehird> oklopol: hyuk hyuk hyuk
23:19:50 <oklopol> basic punology
23:20:01 <oklopol> it's not about fun
23:20:04 <oklopol> it's about duty
23:21:09 <ehird> Pun Force!
23:21:16 <ehird> For Punly Meanderings Forevertothmorse!
23:21:49 <oklopol> forevertothmorse
23:23:28 <ehird> yes
23:23:51 <oklopol> as if that's a word man!
23:24:03 <ehird> It's a word person.
23:24:14 <oklopol> xDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDD
23:24:28 <ehird> E
23:24:42 <oklopol> okay i actually laughed out loud at your E too
23:24:54 <oklopol> so maybe the person thing wasn't very funny either
23:24:54 <ais523> I'm laughing out loud now too
23:24:58 <ais523> but I'm not sure why
23:25:02 <ais523> or if this conversation's related
23:25:06 <oklopol> i think i'm being tired.
23:31:38 -!- Sgeo has joined.
23:32:03 <ehird> jhgfcx'
23:35:16 -!- ais523 has quit (Remote closed the connection).
23:36:05 <ehird> asdfghjkl;'
23:37:13 -!- BeholdMyGlory has quit (Remote closed the connection).
23:37:32 -!- FireFly has quit ("Later").