00:00:05 oerjan: dear diary 00:00:32 and i really cannot quite decide whether it was an illusion or not 00:01:15 well this was mostly to oklopod, we were talking about northern lights a day before 00:02:00 the nights are swiftly getting lighter up here, so the northern lights are supposed to become invisible around this time or so 00:03:05 back to the logs -> 00:06:28 my raindrops feel a bit boring compared to northern lightning :< 00:07:55 rain is boring. that's what it _does_. 00:08:07 its purpose of existing, almost. 00:08:26 with the occasional flood exception 00:08:43 oh, and rainbows 00:11:11 drizzle 00:11:30 -!- augur has quit (Ping timeout: 252 seconds). 00:16:33 what's a good prime? <-- http://en.wikipedia.org/wiki/Good_prime 00:16:58 * oerjan cackles maniacally 00:17:08 strange name 00:18:09 well with perfect, abundant, friend etc. around, it was only a matter of time 00:18:11 ais523: no more strange than "perfect number" 00:18:19 I should define, say, an "awesome real" 00:18:25 go for it 00:18:34 so long as all instances of it are over 9000 00:18:59 :| 00:19:23 * oerjan regretfully concludes that is probably not a known term 00:23:27 ais523: I'm trying to make it something computers can actually find instances for 00:23:34 so that we can maintain, say, a list of known awesome reals 00:23:40 yes 00:23:50 actually the current interp can barely handle operations on numbers of size 7, but you could easily go to 20 with simple optimizations 00:23:53 either that, or something that's undecidable in general but decidable in specific cases 00:23:58 which would have a similar effect 00:24:27 trying to do something with the riemann zeta function cuz I HEAR IT'S MYSTICAL 00:24:30 i think with hash consing done properly, the basic operations of toi should be at most O(n log n) or thereabouts... 00:24:49 oh hm 00:24:56 -!- ais523 has quit (Remote host closed the connection). 00:25:10 n would be the number of elements of elements of S, or something 00:25:17 http://pastie.org/private/5esc4wqvtk2uzrkqfvpkw series expansion of zeta(1/x)^-x at x=oo 00:25:40 More fun in image form, where it's 7465x37 pixels. 00:25:42 anyway the point would be that no primitive operation looks very deep at the set 00:25:49 It has rather large tops of fractions. 00:25:55 And it's all in a fucking exponent! 00:26:00 The wonders of computers. 00:27:39 it might also be an idea to optimize ([r], i think 00:31:06 * alise wonders if "madame" is correct for this nick's customised gender structure.. <-- mademoiselle, surely? 00:31:14 lol 00:31:30 unless you're customizing as an old married woman 00:33:02 oerjan: i mostly just meant simple optimizations to what i had 00:33:20 "Stuck"; a nice word to describe Britain. 00:33:32 Well; being in Britain. 00:34:02 currently emptying with ([r] takes O(n^2) time or something, i think 00:34:17 the media here (well at least the largest paper) have for recent obvious reasons invented the word "askefast", which means "ash-stuck" and which they use all the f*ing time 00:35:26 oklopod: well it repeats r depth(S) times... 00:35:49 oerjan: Oh, I didn't mean it in that way. 00:35:58 I don't care about Iceland's volcanoes, much. I just don't like this island. 00:36:00 oklopod: oh, you haven't implemented hash consing yet? 00:36:00 currently i have numbers stored as python numbers which are converted to sets and back to numbers at every step 00:36:06 Particularly its government. 00:36:06 alise: i just found it apropos 00:36:10 oerjan: Yes. 00:36:11 i have, but that didn't help, maybe i did it wrong somehow. 00:36:12 oerjan: It is that. 00:36:18 so now i special case numbers 00:36:26 currently in a pretty stupid way 00:36:35 i've had a headache all day 00:37:17 oklopod: as i implied, the thing is that no basic operations should recurse. so comparing two already cached sets should be constant time 00:37:38 pointer comparison, presumably 00:37:39 comparing was constant time 00:37:47 but building numbers was not 00:37:56 yes it was pointer comparison 00:38:03 sort of 00:38:06 including for ordering? 00:38:17 what do you mean? 00:38:37 ordering is nice for building sets quickly, since you can sort the list of subsets 00:38:54 *elements 00:39:14 it doesn't matter _what_ ordering, it's just so you have a unique sorting 00:39:23 oh hmm actually i did have that 00:39:35 ok 00:39:35 but i'm not sure i used it?!? 00:39:41 oh 00:39:44 anyway the point is it was still exponential to build a numbre. 00:39:48 *nombre 00:39:55 ah that would be bad 00:40:04 building a number shouldn't be exponential 00:40:12 now it's constant time 00:40:24 i mean, even without special casing on numbers 00:40:47 why don't you implement this thing if it's so fucking easy :D 00:40:53 well i guess it could still end up O(n^4) or something like that 00:40:59 because i'm lazy, of course 00:41:11 or i could once i get a good night sleep 00:41:52 especially r and a would benefit from using ordering, i guess 00:42:14 hmm why? 00:42:20 oh 00:42:31 since you combine a lot of elements at the end 00:42:55 combine? 00:43:06 union 00:43:19 r is taking the union of all subsets 00:43:34 and a does that + one more element 00:43:44 *of all elements 00:43:44 so you'd have like a merge 00:43:52 of all subsets 00:44:00 I'm having a hard time defining an awesome real :( 00:44:18 all the awesome reals have been invented already 00:44:46 go for it, alise 00:44:55 are the awesome reals dense on R 00:45:00 *in 00:45:03 I'm trying! But all the instances must be above 9000. 00:45:07 oh 00:45:08 Preferably there should be infinitely many of them. 00:45:09 then i guess not 00:45:15 oklopod: ais dictated. 00:45:20 Also the equation must be suitably long and ridiculous. 00:45:25 or otherwise you have one crazy ass topology 00:45:34 I do have one crazy ass-topology 00:46:32 only one? 00:46:52 well. many 00:46:53 to be crazy, an ass-topology must have at least two holes 00:47:09 just so you know 00:47:15 alise: there's a note to you in the logs from this week, btw 00:47:17 well i guess none could also work 00:47:39 pineapple: Do you know what day? 00:47:47 alise: oh and we were supposed to remind you about the link you put in the topic just before you left 00:47:49 monday i think, although grep by your name 00:47:58 oerjan: yeah i found that 00:47:58 whatever it was ;D 00:47:59 pineapple: no downloaded logs 00:48:18 umm... 00:48:34 i _think_ it was monday 00:48:44 but i don't remmeber 00:48:45 04:52:12 alise for the logs: the iPhone developer contract is getting even crazier, see http://www.wired.com/epicenter/2010/04/with-new-developer-agreement-apple-unlevels-the-iad-playing-field/ 00:48:46 was that it? 00:48:49 yes 00:49:13 alise: did you find that interesting 00:49:15 ok, thanks 00:49:16 oklopod: no 00:49:33 alise: did i tell you about toi yet ?!? 00:49:38 oklopod: OMG# 00:49:51 HI PINEAPPLE WANNA HEAR SOMETHING INTERESTING 00:49:58 i should really stop this 00:50:28 did you know that (Z, .-., Pos) where Pos(x) = x > 0 expresses the relation greater-than?? 00:50:32 AMAZING AMIRITE 00:50:49 i did not 00:51:15 because i don't know what that means 00:52:00 well unless it means "use the things in this tuple in a sensible way" 00:52:14 we say (S,F,T) expresses a binary relation R on A where F : A -> A -> S and T is an unary relation on S, if 00:52:26 T (Fxy) <=> xRy 00:52:31 we say this for no particular reason 00:53:14 parti cular 00:55:02 a partyious cular 00:55:45 i wanna make another esolang 00:56:14 unfortunately i'm out of awesome ideas 00:56:24 maybe i could base a language on awesome reals 00:56:44 i'm gonna go away now 00:57:18 oklopod: make an esolang based on type theory 00:57:21 or, you know, awesome reals 00:57:26 make a real computation language 00:57:31 uncomputable, so just approximate! 00:58:36 yes a bit of topology and ergodic theory 00:59:36 maybe i'll do real computation 01:00:12 oklopod: how can you /not/ implement somethingcalled the blum-shub-smale machine 01:00:39 *something called 01:00:59 http://en.wikipedia.org/wiki/Blum-Shub-Smale_machine ;; only three operations so clearly the perfect tarpit 01:03:40 16:18:15 Gregor: Well, yeah. I think if the President gave a blowjob, the entire right wing would just have a heart attack and die. 01:03:43 Please make this happen quickly. 01:04:02 alise: Hah. 01:04:23 What if the President performed autofellatio? 01:04:44 He'd be giving /and/ receiving a blowjob; he'd be Lewinsky and Clinton simultaneously, in a sort of quantum construction. 01:04:47 I do believe their heads would asplode. 01:05:26 I should note, though: the key to this is the President not being a Republican. 01:05:46 If he's a Republican, they will gladly back him banning heterosexuality. 01:05:56 (there's a funny thought) 01:09:35 -!- Rugxulo has joined. 01:09:52 alise: Vi vejnas unan Interneton. 01:09:57 uh oh 01:09:58 s/Interneton/Interreton/ 01:10:03 phew 01:10:08 arch/x86/kernel/head_32.S:64: Warning: shift count out of range (32 is not between 0 and 31) 01:10:22 you can't shift by 32 (anymore), that would be a effectively a NOP 01:10:41 8086 allowed it, but 386+ masks to lower five bits (e.g. 32 or less value) 01:10:44 which is why he quoted it. 01:11:29 BinUtils' GAS does allow ".arch" nowadays, presumably to tighten up such sub-architectural differences 01:15:08 Rugxulo, that was from the kernel 01:15:12 which was pretty strange 01:15:22 night → 01:24:18 hmmm, awib don't work for me 01:24:53 o 01:26:22 " alise: Vi vejnas unan Interneton." " uh oh" " s/Interneton/Interreton/" " phew" 01:26:28 classic alise 01:26:56 am i having a dream? 01:27:09 nope 01:27:21 Nope, you're not. 01:27:29 But don't take my word for it. 01:27:36 why not? 01:27:52 Because you don't know whether you're dreaming or not, meaning I'm not a reliable source. 01:28:13 Try cutting the mushroom; if anything around is orange, that will heal the tortilla wounds. 01:28:25 If that made any sense, you're dreaming. 01:28:47 but my brain doesn't lie to me 01:29:01 Uh oh, we've lost him. 01:29:05 * uorygl mourns. 01:29:20 well it dunnot! 01:29:30 good brain mine one 01:30:24 Mourning the lost is more difficult when they're still standing around and saying stuff. 01:30:32 The walking dead. 01:30:53 yes that's the worst kind of death 01:31:25 * uorygl builds a wall in front of oklopod. 01:31:34 * uorygl builds a wall to the left of oklopod. 01:31:42 * uorygl builds a wall to the right of oklopod. 01:31:49 * uorygl builds a wall behind oklopod. 01:31:57 There, now we can't see you, so we can mourn properly. 01:31:59 :o 01:32:06 \o/ 01:32:06 | 01:32:06 >\ 01:32:08 * oerjan sneaks oklopod out through an underground tunnel 01:32:13 stuff -> 01:32:14 yay 01:32:16 -> 01:32:35 Darn, I knew I should have built a wall below oklopod and above oklopod. 01:32:42 Now I have to start all over. 01:32:45 * Rugxulo uses the wand of digging to go through the wall ... an orc wizard appears! 01:33:32 * uorygl builds a wall in front of oklopod and builds a wall to the left of oklopod and builds a wall to the right of oklopod and builds a wall behind oklopod and builds a wall under oklopod and builds a wall above oklopod. 01:33:52 * oerjan uses zzo38's Zwischenzug on the orc wizard 01:34:04 uorygl: oklopod already left, pay attention 01:34:17 I'm building a wall around his new position. 01:34:23 * Rugxulo gives oerjan a scroll of recharging but needs scroll of identify to understand "Zwischenzug" 01:35:05 * Rugxulo uses a wand of teleportation to secretly follow from far away ... 01:35:10 Rugxulo: i think you'll have to ask zzo38 for that, at your own risk 01:35:31 * Rugxulo sacrifices zzo38 to Trog ... Trog is greatly pleased 01:36:26 would you like fries with that 01:36:45 * Rugxulo eats a snozzcumber 01:36:55 * Rugxulo thought it was bland 01:37:43 * oerjan throws a critical failure on his Recognize Reference skill 01:39:37 * oerjan uses one google point to reroll 01:43:35 http://crawl.develz.org ;-) 01:55:52 "Real" is such a bad name for the real numbers. 01:56:08 Considering how many of them are quite thoroughly not real, and in fact their whole existence can be questioned. 01:59:06 In what sense can any mathematical construct be said to exist? 01:59:13 They're certainly no *more* real than, say, the natural numbers. 01:59:34 Or even the natural numbers mod a convenient power of 2. 01:59:39 a hamster is something that hams 01:59:59 Ah but the reals are much, much more questionable than the naturals. 02:00:12 Even if you accept reals as a whole, some things are as unreal as you can get -- in fact, bordering on the impossible. 02:00:25 The reals are a fairly non-obvious construction, yes. 02:00:31 For instance, http://en.wikipedia.org/wiki/Chaitin%27s_constant, the probability that a random program will halt in a given language. 02:00:42 The non-computable reals in particular make you go "WTF". 02:00:46 Totally uncomputable; lets you solve the halting problem; and yet still, a bona-fide real. 02:00:49 And then consider this. 02:00:51 *hamsts 02:01:00 Almost all reals -- mathematically -- are uncomputable. 02:01:10 o rly? (couldn't resist) 02:01:13 So really there are not many reals that are real, and many reals that are not real at all! 02:01:31 "Almost all"? Hmm. ... Actually, yeah. 02:01:39 oklopod: is http://www.vjn.fi/oklopol/toi.py your current implementation? 02:01:45 almost all with the lebesque measure 02:01:47 oerjan: yes 02:01:48 Any non-computable real plus a computable real is itself non-computable... 02:02:07 pikhq: it's been proved yeah 02:02:07 * Sgeo reviews an app on the Market 02:02:09 i think i uploaded the most recentest of changes 02:02:11 Which I *think* makes the set of non-computable reals larger than the set of computable reals. 02:02:18 it is 02:02:22 the computable reals are countable 02:02:24 Mmkay then. 02:02:27 computable = computable by a turing machine 02:02:32 ... Oh, *duh*. 02:02:36 consider a brainfuck algorithm as a list of naturals mod 8 02:02:39 Didn't show up on AppBrain 02:02:40 sum up appropriately 02:02:41 Q.E.D. 02:02:42 The computable reals have a Godel numbering. 02:02:44 yeah 02:03:04 the computable reals are harder to prove results about though :( 02:03:13 like the cauchy-sequence definition doesn't even let you prove the trichotomy of the reals 02:03:17 a zero real times a nonzero real is a zero real, this makes the zero reals a larger set than the nonzero reals 02:03:18 Yeah, but they most *certainly* exist. 02:03:24 definitely 02:03:26 as real as the naturals 02:03:39 You can point at the programs that produce them. "See, there it is." 02:03:43 and i'm pretty strong on my faith in naturals 02:03:48 though it /has/ wavered once or twice 02:04:18 also constructivism has greener grass 02:04:22 it's more satisfying 02:04:23 Whereas the non-computable reals are pretty much an arbitrary, abstract construct, which exists pretty much because the definition was easy (near as I can tell). 02:04:32 classical bozos, they define a bunch of constraints that their reals have to satisfy 02:04:36 and say "there's only one. that's ours" 02:04:38 you don't see it, feel it 02:04:43 it's all symbol manipulation 02:04:52 us constructivsts get actual concrete code and functions we can compute with 02:04:57 actual, well, constructions 02:05:27 I just care about what lets me do interesting things, myself. :P 02:05:41 oklopod: it looks like you are reimplementing the one thing which iirc python already does _extremely_ well built in, namely hash table dictionaries 02:06:08 constructivism is so goddamn boring 02:06:16 oklopod: yeah well so's your mom 02:06:18 oerjan: i'm not using the hash thingie 02:06:28 pikhq: btw if you disagree with the uncomputable reals then you're half-way to rejecting forall P, P \/ ~P anyway 02:06:46 alise: I don't care if something's an abstract construct. 02:06:52 I'm just noting that it is one. ;) 02:07:05 since the computer-age rejection of that is that, since propositions:types and proofs:values, 02:07:06 forall P, P \/ ~P 02:07:18 would have to be a decision procedure that can formulate a proof or disproof of any proposition you hand it! 02:07:49 and indeed in some cases we can prove that some propositions cannot be proved or disproved... and then the law of the excluded middle conjurs up one anyway! (not that we know /which/, but if we know it cannot prove /either/...) 02:08:21 i'm not a constructivist in that i reject abstract constructions... everything's abstract 02:08:41 I just don't accept magical decision procedures :p 02:08:44 i would've thunk p v ~p just says in any model of the system one is true, if we can't prove either then it depends on the model which one is true 02:08:59 yeah but the curry-howard interpretation is 02:09:09 (P:Prop) -> P \/ ~P 02:09:11 where ~P = P -> Void 02:09:17 and \/ is just a disjoint union type 02:09:19 i.e. Either 02:09:23 now if P:Prop 02:09:29 then p:P means "p is a proof of P" 02:09:54 oklopod: oh. 02:09:54 so L.E.M. takes an arbitrary proposition -- even a statement independent of the axioms -- and conjurs up "either a proof or a disproof" 02:10:02 we can't inspect which it is computationally; but that's the sematncis 02:10:03 *semantics 02:10:21 oerjan: and the code is not exactly my best work, i just wanted to quickly hack some half-working shit up 02:10:34 I'm pretty sure that p \/ ~p just implies that the veracity of p is a Bool, not True | False | FileNotFound or some shit. :P 02:10:35 ...and then i've hacked optimizations in on top of each other all day 02:10:47 pikhq: yeah but this is a fundamental misunderstanding of the entirety of curry howard 02:10:51 it's got nothing to do with booleans at all 02:10:55 which isn't a very fruitful approach always 02:11:06 relating logic to booleans is presupposing the law of the excluded middle which is the whole thing i'm arguing against 02:11:18 -!- Rugxulo has quit (Quit: gone back to Befunge ...). 02:11:43 oklopod: if i implement toi will you love me 02:11:47 Yes, well, fuck you and your system of logic that I can't reason about. 02:11:50 thought so; implementing 02:11:55 pikhq: <3 02:12:01 type theory is here when you want it 02:12:19 Screw that, we're forcing all of math into C. 02:12:29 the problem with constructivism is it's not at all interesting 02:12:29 If it doesn't fit into the system memory it doesn't exist. 02:12:34 it's really boring and stupid 02:12:43 i hate it 02:12:47 and i hate everyone around it 02:12:51 And for the sake of pain, 8-bit system. 02:13:10 in fact i'm gonna convert to destructivism 02:13:23 oklopod: You are become Shiva? 02:13:32 alise: yes, i will love you despite your constructivist doctrine 02:13:54 pikhq: not just my mathlosophy 02:13:58 *no 02:14:14 oerjan: i didn't know you actually read code 02:14:22 i figured mathematicians aren't allowed 02:15:01 alise: just kidding though, constructivism is kind of sexy too 02:15:16 * alise realises that 02:15:19 data Set = Empty -- ∅ 02:15:20 | Cons Set Set -- X ∪ {t | t ∈ s, s ∈ S} 02:15:22 needs a singleton :P 02:15:49 data Set = Empty -- ∅ 02:15:49 | Singleton Set -- {A} 02:15:49 | Cons Set Set -- A ∪ {t | t ∈ s, s ∈ B} 02:15:50 that's better 02:15:56 hey it's worth a try :P 02:16:11 succS :: Set -> Set 02:16:11 succS n = Cons n (Singleton (Singleton n)) 02:16:19 oklopod: why exactly do you use ordinals? 02:16:20 is it ready soon? 02:16:49 mostly because they're exponential in size i guess 02:16:54 The Android browser feels jumpy 02:16:57 von neumanns 02:17:27 oklopod: yeah but do you actually use any infiniteness? 02:17:34 no 02:18:42 right 02:18:56 * Sgeo hopes he doesn't fill up his SD card too soon 02:20:52 what's the trichotomy of the reals? 02:21:06 forall n, n<0 \/ n=0 \/ n>0 02:21:08 exactly one is true 02:21:15 substitute 0 for arbitrary m, etc. 02:21:32 or at least fax says you can't prove it on the cauchy sequence computable reals 02:21:49 oklopod: you will be pleased to know that my set representation works 02:21:59 yeah because a sequence could -> 0 without there being a proof of it 02:22:01 any more lovely infrastructure before the boring lang? 02:22:14 oerjan: yeah 02:22:38 alise: now express omega_1 in your representation! 02:22:54 see oklopod promised me it was all finite :P 02:23:01 Oh. 02:23:25 let s r = Cons r (s (succO r)) in s zeroO 02:23:26 that works though 02:23:28 What's the smallest ordinal you can't express? 02:23:37 enumeration doesn't yield anything though :P 02:23:37 alise: i notice you are not using hash consing (somewhat tricky in haskell i should think) so you'll have the same exponential blowup problem 02:23:48 oerjan: well... foo to you 02:23:57 maybe i should just do it as {elem:true, ...} in python 02:23:59 that would work :P 02:24:16 python has sets 02:24:18 too 02:24:26 yeah 02:24:29 they're represented by that 02:24:47 well if that's so then i'll complain about you writing true as True 02:24:49 err 02:24:51 the other way around 02:25:10 i'm almost tempted to write my own version, but i would have to download python and relearn some things first... 02:25:13 and if you say both are okay in the new python then i'll complain about your mother 02:25:33 yay competition 02:26:11 well okay oerjan can't really be competition since he either does nothing or owns me completely 02:26:18 :D 02:26:58 sdfjsdfsdf python's add method of sets is destructive 02:27:15 yeah there's a separate immutable set 02:27:33 hmm could mutability work 02:27:35 I mean S is global 02:27:41 i used it at first 02:27:56 but had to change it when i started sharing 02:28:10 "Do not manipulate this application while driving. Traffic data is not real-time, and directions may be wrong, dangerous, prohibited, or involve ferries." 02:28:23 sharing, just like a polygamist 02:28:30 oklopod: so what did you just use immutable sets 02:28:43 no 02:28:49 meh, you still have to union with a singleton with frozenset 02:28:51 i used something really weird 02:29:01 i think i now use lists 02:29:41 heh 02:29:46 sets have to contain hashable things 02:29:48 sets aren't hashable 02:29:51 yes 02:29:54 need frozenset 02:30:11 i think that's why i didn't use sets, didn't want to use frozensets 02:30:16 because their name sounds scare 02:30:18 *y 02:32:26 def a(S): return S.union(frozenset(S)) 02:32:29