00:00:05 <alise> oerjan: dear diary
00:00:32 <oerjan> and i really cannot quite decide whether it was an illusion or not
00:01:15 <oerjan> well this was mostly to oklopod, we were talking about northern lights a day before
00:02:00 <oerjan> the nights are swiftly getting lighter up here, so the northern lights are supposed to become invisible around this time or so
00:06:28 <oklopod> my raindrops feel a bit boring compared to northern lightning :<
00:07:55 <oerjan> rain is boring. that's what it _does_.
00:08:07 <oerjan> its purpose of existing, almost.
00:08:26 <oerjan> with the occasional flood exception
00:11:30 -!- augur has quit (Ping timeout: 252 seconds).
00:16:33 <oerjan> <oklopod> what's a good prime? <-- http://en.wikipedia.org/wiki/Good_prime
00:18:09 <oerjan> well with perfect, abundant, friend etc. around, it was only a matter of time
00:18:11 <alise> ais523: no more strange than "perfect number"
00:18:19 <alise> I should define, say, an "awesome real"
00:18:34 <ais523> so long as all instances of it are over 9000
00:19:23 * oerjan regretfully concludes that is probably not a known term
00:23:27 <alise> ais523: I'm trying to make it something computers can actually find instances for
00:23:34 <alise> so that we can maintain, say, a list of known awesome reals
00:23:50 <oerjan> <oklopod> 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 <ais523> either that, or something that's undecidable in general but decidable in specific cases
00:23:58 <ais523> which would have a similar effect
00:24:27 <alise> trying to do something with the riemann zeta function cuz I HEAR IT'S MYSTICAL
00:24:30 <oerjan> i think with hash consing done properly, the basic operations of toi should be at most O(n log n) or thereabouts...
00:24:56 -!- ais523 has quit (Remote host closed the connection).
00:25:10 <oerjan> n would be the number of elements of elements of S, or something
00:25:17 <alise> http://pastie.org/private/5esc4wqvtk2uzrkqfvpkw series expansion of zeta(1/x)^-x at x=oo
00:25:40 <alise> More fun in image form, where it's 7465x37 pixels.
00:25:42 <oerjan> anyway the point would be that no primitive operation looks very deep at the set
00:25:49 <alise> It has rather large tops of fractions.
00:25:55 <alise> And it's all in a fucking exponent!
00:26:00 <alise> The wonders of computers.
00:27:39 <oerjan> it might also be an idea to optimize ([r], i think
00:31:06 <oerjan> * alise wonders if "madame" is correct for this nick's customised gender structure.. <-- mademoiselle, surely?
00:31:30 <oerjan> unless you're customizing as an old married woman
00:33:02 <oklopod> oerjan: i mostly just meant simple optimizations to what i had
00:33:20 <oerjan> <alise> "Stuck"; a nice word to describe Britain.
00:33:32 <alise> Well; being in Britain.
00:34:02 <oklopod> currently emptying with ([r] takes O(n^2) time or something, i think
00:34:17 <oerjan> 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 <oerjan> oklopod: well it repeats r depth(S) times...
00:35:49 <alise> oerjan: Oh, I didn't mean it in that way.
00:35:58 <alise> I don't care about Iceland's volcanoes, much. I just don't like this island.
00:36:00 <oerjan> oklopod: oh, you haven't implemented hash consing yet?
00:36:00 <oklopod> currently i have numbers stored as python numbers which are converted to sets and back to numbers at every step
00:36:06 <alise> Particularly its government.
00:36:06 <oerjan> alise: i just found it apropos
00:36:11 <oklopod> i have, but that didn't help, maybe i did it wrong somehow.
00:36:12 <alise> oerjan: It is that.
00:36:18 <oklopod> so now i special case numbers
00:36:26 <oklopod> currently in a pretty stupid way
00:36:35 <oklopod> i've had a headache all day
00:37:17 <oerjan> 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 <oerjan> pointer comparison, presumably
00:37:39 <oklopod> comparing was constant time
00:37:47 <oklopod> but building numbers was not
00:37:56 <oklopod> yes it was pointer comparison
00:38:06 <oerjan> including for ordering?
00:38:37 <oerjan> ordering is nice for building sets quickly, since you can sort the list of subsets
00:39:14 <oerjan> it doesn't matter _what_ ordering, it's just so you have a unique sorting
00:39:23 <oklopod> oh hmm actually i did have that
00:39:35 <oklopod> but i'm not sure i used it?!?
00:39:44 <oklopod> anyway the point is it was still exponential to build a numbre.
00:40:04 <oerjan> building a number shouldn't be exponential
00:40:24 <oerjan> i mean, even without special casing on numbers
00:40:47 <oklopod> why don't you implement this thing if it's so fucking easy :D
00:40:53 <oerjan> well i guess it could still end up O(n^4) or something like that
00:40:59 <oerjan> because i'm lazy, of course
00:41:11 <oklopod> or i could once i get a good night sleep
00:41:52 <oerjan> especially r and a would benefit from using ordering, i guess
00:42:31 <oerjan> since you combine a lot of elements at the end
00:43:19 <oerjan> r is taking the union of all subsets
00:43:34 <oerjan> and a does that + one more element
00:43:44 <oklopod> so you'd have like a merge
00:44:00 <alise> I'm having a hard time defining an awesome real :(
00:44:18 <oerjan> all the awesome reals have been invented already
00:44:55 <oklopod> are the awesome reals dense on R
00:45:03 <alise> I'm trying! But all the instances must be above 9000.
00:45:08 <alise> Preferably there should be infinitely many of them.
00:45:15 <alise> oklopod: ais dictated.
00:45:20 <alise> Also the equation must be suitably long and ridiculous.
00:45:25 <oklopod> or otherwise you have one crazy ass topology
00:45:34 <alise> I do have one crazy ass-topology
00:46:53 <oerjan> to be crazy, an ass-topology must have at least two holes
00:47:15 <pineapple> alise: there's a note to you in the logs from this week, btw
00:47:17 <oerjan> well i guess none could also work
00:47:39 <alise> pineapple: Do you know what day?
00:47:47 <oerjan> alise: oh and we were supposed to remind you about the link you put in the topic just before you left
00:47:49 <pineapple> monday i think, although grep by your name
00:47:58 <alise> oerjan: yeah i found that
00:47:59 <alise> pineapple: no downloaded logs
00:48:45 <alise> 04:52:12 <ais523> 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:49:13 <oklopod> alise: did you find that interesting
00:49:33 <oklopod> alise: did i tell you about toi yet ?!?
00:49:51 <oklopod> HI PINEAPPLE WANNA HEAR SOMETHING INTERESTING
00:50:28 <alise> did you know that (Z, .-., Pos) where Pos(x) = x > 0 expresses the relation greater-than??
00:51:15 <oklopod> because i don't know what that means
00:52:00 <oklopod> well unless it means "use the things in this tuple in a sensible way"
00:52:14 <alise> 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:31 <alise> we say this for no particular reason
00:55:45 <oklopod> i wanna make another esolang
00:56:14 <oklopod> unfortunately i'm out of awesome ideas
00:56:24 <oklopod> maybe i could base a language on awesome reals
00:57:18 <alise> oklopod: make an esolang based on type theory
00:57:21 <alise> or, you know, awesome reals
00:57:26 <alise> make a real computation language
00:57:31 <alise> uncomputable, so just approximate!
00:58:36 <oklopod> yes a bit of topology and ergodic theory
00:59:36 <alise> maybe i'll do real computation
01:00:12 <alise> oklopod: how can you /not/ implement somethingcalled the blum-shub-smale machine
01:00:59 <alise> http://en.wikipedia.org/wiki/Blum-Shub-Smale_machine ;; only three operations so clearly the perfect tarpit
01:03:40 <alise> 16:18:15 <pikhq> 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 <alise> Please make this happen quickly.
01:04:23 <alise> What if the President performed autofellatio?
01:04:44 <alise> He'd be giving /and/ receiving a blowjob; he'd be Lewinsky and Clinton simultaneously, in a sort of quantum construction.
01:04:47 <pikhq> I do believe their heads would asplode.
01:05:26 <pikhq> I should note, though: the key to this is the President not being a Republican.
01:05:46 <pikhq> If he's a Republican, they will gladly back him banning heterosexuality.
01:05:56 <pikhq> (there's a funny thought)
01:09:35 -!- Rugxulo has joined.
01:09:52 <Rugxulo> <pikhq> alise: Vi vejnas unan Interneton.
01:10:08 <Rugxulo> <AnMaster> arch/x86/kernel/head_32.S:64: Warning: shift count out of range (32 is not between 0 and 31)
01:10:22 <Rugxulo> you can't shift by 32 (anymore), that would be a effectively a NOP
01:10:41 <Rugxulo> 8086 allowed it, but 386+ masks to lower five bits (e.g. 32 or less value)
01:10:44 <alise> which is why he quoted it.
01:11:29 <Rugxulo> BinUtils' GAS does allow ".arch" nowadays, presumably to tighten up such sub-architectural differences
01:15:08 <AnMaster> Rugxulo, that was from the kernel
01:24:18 <Rugxulo> hmmm, awib don't work for me
01:26:22 <oklopod> "<Rugxulo> <pikhq> alise: Vi vejnas unan Interneton." "<alise> uh oh" "<Rugxulo> s/Interneton/Interreton/" "<alise> phew"
01:27:29 <uorygl> But don't take my word for it.
01:27:52 <uorygl> Because you don't know whether you're dreaming or not, meaning I'm not a reliable source.
01:28:13 <uorygl> Try cutting the mushroom; if anything around is orange, that will heal the tortilla wounds.
01:28:25 <uorygl> If that made any sense, you're dreaming.
01:28:47 <oklopod> but my brain doesn't lie to me
01:29:01 <uorygl> Uh oh, we've lost him.
01:30:24 <uorygl> Mourning the lost is more difficult when they're still standing around and saying stuff.
01:30:53 <oklopod> 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 <uorygl> There, now we can't see you, so we can mourn properly.
01:32:08 * oerjan sneaks oklopod out through an underground tunnel
01:32:35 <uorygl> Darn, I knew I should have built a wall below oklopod and above oklopod.
01:32:42 <uorygl> 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 <oerjan> uorygl: oklopod already left, pay attention
01:34:17 <uorygl> 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 <oerjan> 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 <oerjan> would you like fries with that
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 <Rugxulo> http://crawl.develz.org ;-)
01:55:52 <alise> "Real" is such a bad name for the real numbers.
01:56:08 <alise> Considering how many of them are quite thoroughly not real, and in fact their whole existence can be questioned.
01:59:06 <Sgeo> In what sense can any mathematical construct be said to exist?
01:59:13 <pikhq> They're certainly no *more* real than, say, the natural numbers.
01:59:34 <pikhq> Or even the natural numbers mod a convenient power of 2.
01:59:39 <alise> a hamster is something that hams
01:59:59 <alise> Ah but the reals are much, much more questionable than the naturals.
02:00:12 <alise> 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 <pikhq> The reals are a fairly non-obvious construction, yes.
02:00:31 <alise> 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 <pikhq> The non-computable reals in particular make you go "WTF".
02:00:46 <alise> Totally uncomputable; lets you solve the halting problem; and yet still, a bona-fide real.
02:00:49 <alise> And then consider this.
02:01:00 <alise> Almost all reals -- mathematically -- are uncomputable.
02:01:13 <alise> So really there are not many reals that are real, and many reals that are not real at all!
02:01:31 <pikhq> "Almost all"? Hmm. ... Actually, yeah.
02:01:39 <oerjan> oklopod: is http://www.vjn.fi/oklopol/toi.py your current implementation?
02:01:45 <oklopod> almost all with the lebesque measure
02:01:48 <pikhq> Any non-computable real plus a computable real is itself non-computable...
02:02:07 <alise> pikhq: it's been proved yeah
02:02:07 * Sgeo reviews an app on the Market
02:02:09 <oklopod> i think i uploaded the most recentest of changes
02:02:11 <pikhq> Which I *think* makes the set of non-computable reals larger than the set of computable reals.
02:02:22 <alise> the computable reals are countable
02:02:27 <alise> computable = computable by a turing machine
02:02:36 <alise> consider a brainfuck algorithm as a list of naturals mod 8
02:02:39 <Sgeo> Didn't show up on AppBrain
02:02:40 <alise> sum up appropriately
02:02:42 <pikhq> The computable reals have a Godel numbering.
02:03:04 <alise> the computable reals are harder to prove results about though :(
02:03:13 <alise> like the cauchy-sequence definition doesn't even let you prove the trichotomy of the reals
02:03:17 <oklopod> 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 <pikhq> Yeah, but they most *certainly* exist.
02:03:26 <alise> as real as the naturals
02:03:39 <pikhq> You can point at the programs that produce them. "See, there it is."
02:03:43 <alise> and i'm pretty strong on my faith in naturals
02:03:48 <alise> though it /has/ wavered once or twice
02:04:18 <alise> also constructivism has greener grass
02:04:22 <alise> it's more satisfying
02:04:23 <pikhq> 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 <alise> classical bozos, they define a bunch of constraints that their reals have to satisfy
02:04:36 <alise> and say "there's only one. that's ours"
02:04:38 <alise> you don't see it, feel it
02:04:43 <alise> it's all symbol manipulation
02:04:52 <alise> us constructivsts get actual concrete code and functions we can compute with
02:04:57 <alise> actual, well, constructions
02:05:27 <pikhq> I just care about what lets me do interesting things, myself. :P
02:05:41 <oerjan> 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 <oklopod> constructivism is so goddamn boring
02:06:16 <alise> oklopod: yeah well so's your mom
02:06:18 <oklopod> oerjan: i'm not using the hash thingie
02:06:28 <alise> pikhq: btw if you disagree with the uncomputable reals then you're half-way to rejecting forall P, P \/ ~P anyway
02:06:46 <pikhq> alise: I don't care if something's an abstract construct.
02:06:52 <pikhq> I'm just noting that it is one. ;)
02:07:05 <alise> since the computer-age rejection of that is that, since propositions:types and proofs:values,
02:07:18 <alise> would have to be a decision procedure that can formulate a proof or disproof of any proposition you hand it!
02:07:49 <alise> 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 <alise> i'm not a constructivist in that i reject abstract constructions... everything's abstract
02:08:41 <alise> I just don't accept magical decision procedures :p
02:08:44 <oklopod> 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 <alise> yeah but the curry-howard interpretation is
02:09:09 <alise> (P:Prop) -> P \/ ~P
02:09:11 <alise> where ~P = P -> Void
02:09:17 <alise> and \/ is just a disjoint union type
02:09:29 <alise> then p:P means "p is a proof of P"
02:09:54 <alise> 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 <alise> we can't inspect which it is computationally; but that's the sematncis
02:10:21 <oklopod> oerjan: and the code is not exactly my best work, i just wanted to quickly hack some half-working shit up
02:10:34 <pikhq> 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 <oklopod> ...and then i've hacked optimizations in on top of each other all day
02:10:47 <alise> pikhq: yeah but this is a fundamental misunderstanding of the entirety of curry howard
02:10:51 <alise> it's got nothing to do with booleans at all
02:10:55 <oklopod> which isn't a very fruitful approach always
02:11:06 <alise> 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 <alise> oklopod: if i implement toi will you love me
02:11:47 <pikhq> Yes, well, fuck you and your system of logic that I can't reason about.
02:11:50 <alise> thought so; implementing
02:12:01 <alise> type theory is here when you want it
02:12:19 <pikhq> Screw that, we're forcing all of math into C.
02:12:29 <oklopod> the problem with constructivism is it's not at all interesting
02:12:29 <pikhq> If it doesn't fit into the system memory it doesn't exist.
02:12:34 <oklopod> it's really boring and stupid
02:12:47 <oklopod> and i hate everyone around it
02:12:51 <pikhq> And for the sake of pain, 8-bit system.
02:13:10 <oklopod> in fact i'm gonna convert to destructivism
02:13:23 <pikhq> oklopod: You are become Shiva?
02:13:32 <oklopod> alise: yes, i will love you despite your constructivist doctrine
02:13:54 <oklopod> pikhq: not just my mathlosophy
02:14:14 <oklopod> oerjan: i didn't know you actually read code
02:14:22 <oklopod> i figured mathematicians aren't allowed
02:15:01 <oklopod> alise: just kidding though, constructivism is kind of sexy too
02:15:19 <alise> data Set = Empty -- ∅
02:15:20 <alise> | Cons Set Set -- X ∪ {t | t ∈ s, s ∈ S}
02:15:22 <alise> needs a singleton :P
02:15:49 <alise> data Set = Empty -- ∅
02:15:49 <alise> | Singleton Set -- {A}
02:15:49 <alise> | Cons Set Set -- A ∪ {t | t ∈ s, s ∈ B}
02:15:56 <alise> hey it's worth a try :P
02:16:11 <alise> succS :: Set -> Set
02:16:11 <alise> succS n = Cons n (Singleton (Singleton n))
02:16:19 <alise> oklopod: why exactly do you use ordinals?
02:16:49 <oklopod> mostly because they're exponential in size i guess
02:16:54 <Sgeo> The Android browser feels jumpy
02:17:27 <alise> oklopod: yeah but do you actually use any infiniteness?
02:18:56 * Sgeo hopes he doesn't fill up his SD card too soon
02:20:52 <oklopod> what's the trichotomy of the reals?
02:21:06 <alise> forall n, n<0 \/ n=0 \/ n>0
02:21:08 <alise> exactly one is true
02:21:15 <alise> substitute 0 for arbitrary m, etc.
02:21:32 <alise> or at least fax says you can't prove it on the cauchy sequence computable reals
02:21:49 <alise> oklopod: you will be pleased to know that my set representation works
02:21:59 <oerjan> yeah because a sequence could -> 0 without there being a proof of it
02:22:01 <alise> any more lovely infrastructure before the boring lang?
02:22:38 <uorygl> alise: now express omega_1 in your representation!
02:22:54 <alise> see oklopod promised me it was all finite :P
02:23:25 <alise> let s r = Cons r (s (succO r)) in s zeroO
02:23:28 <uorygl> What's the smallest ordinal you can't express?
02:23:37 <alise> enumeration doesn't yield anything though :P
02:23:37 <oerjan> 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 <alise> oerjan: well... foo to you
02:23:57 <alise> maybe i should just do it as {elem:true, ...} in python
02:23:59 <alise> that would work :P
02:24:29 <alise> they're represented by that
02:24:47 <oklopod> well if that's so then i'll complain about you writing true as True
02:25:10 <oerjan> i'm almost tempted to write my own version, but i would have to download python and relearn some things first...
02:25:13 <oklopod> and if you say both are okay in the new python then i'll complain about your mother
02:26:11 <oklopod> well okay oerjan can't really be competition since he either does nothing or owns me completely
02:26:58 <alise> sdfjsdfsdf python's add method of sets is destructive
02:27:15 <oklopod> yeah there's a separate immutable set
02:27:33 <alise> hmm could mutability work
02:27:35 <alise> I mean S is global
02:27:56 <oklopod> but had to change it when i started sharing
02:28:10 <Sgeo> "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 <alise> sharing, just like a polygamist
02:28:30 <alise> oklopod: so what did you just use immutable sets
02:28:49 <alise> meh, you still have to union with a singleton with frozenset
02:28:51 <oklopod> i used something really weird
02:29:46 <alise> sets have to contain hashable things
02:29:48 <alise> sets aren't hashable
02:30:11 <oklopod> i think that's why i didn't use sets, didn't want to use frozensets
02:30:16 <oklopod> because their name sounds scare
02:32:26 <alise> def a(S): return S.union(frozenset(S))
02:32:29 <alise> can't be this easy can it
02:33:08 <alise> cuz it returns wrong results.
02:33:34 <oklopod> yes i suppose it makes absolutely no sense
02:34:11 <oklopod> but it is definitely that simple
02:34:26 <oklopod> it's 0 on simpleness scale
02:38:13 <oklopod> the only nontrivial part of implementing the thing is implementing the sets and numbers
02:38:14 <alise> having to detect ordinals is way too boring
02:38:25 <alise> [[# 'E' does not add the error set to S. ]] i see
02:39:41 -!- Asztal has quit (Ping timeout: 258 seconds).
02:42:32 <alise> oklopod: what does (A{B do
02:42:38 <alise> seeing as only brackets must be balanced
02:52:16 <alise> i should make my own wonderful language
02:52:22 <alise> based on the natural numbers
02:52:37 <alise> like the whole thing is an induction over an infinite amount of natural variables
02:57:03 <oklopod> the problem is every language after this day will just be a bad copy of toi
02:58:04 <alise> you're too interesting to leave
02:58:40 <alise> hmm how about a language where the computation is solving an infinite number of polynomials...
02:59:21 <oklopod> by hilbert's basis theorem any infinite set of diophantine equations is equivalent to its finite subset
02:59:46 <oklopod> you're a constructivist, right
03:00:23 <alise> constructivism =/= finitism
03:00:42 <Oranjer> so constructivism allows for infinity?
03:00:49 <oklopod> what i meant is it requires aoc afaik
03:00:56 <alise> constructivists accept that
03:01:12 <oklopod> i haven't actually read the proof, i've just bumped into the theorem when it's been used
03:01:12 <alise> oklopod: it's probably a much less radical position than you imagine.
03:01:41 <alise> oklopod: for every R : A -> B -> Prop, (forall a, exists b, R a b) -> (exists f : A ->B, forall a, R a (f a))
03:01:54 <alise> since the exists is already a bundling of a value, it's basically just unwrapping the exists and returning the value
03:01:58 <alise> *oklopod: for every R : A -> B -> Prop, (forall a, exists b, R a b) -> (exists f : A -> B, forall a, R a (f a))
03:02:03 <alise> the AoC is provable in type theory.
03:03:22 <oklopod> i guess you win this round, constructivist bear
03:05:18 <alise> oklopod: implement http://en.wikipedia.org/wiki/Blum-Shub-Smale_machine
03:10:16 <alise> you're made of upset.
03:10:58 <alise> oklopod: write a toi selfinterp
03:11:02 <alise> actually shouldn't be so hard.
03:38:39 <alise> there is ~no documentation of plain tex without latex
03:42:58 <pikhq> The TeXbook, by Donald Knuth.
03:43:27 -!- Alex3012 has joined.
03:44:06 <alise> if it's not online easily it doesn't exist
03:44:27 <pikhq> http://www.ctan.org/tex-archive/systems/knuth/dist/tex/texbook.tex
03:45:12 <alise> heh it is so primitive you even have to do all sizings yorsuelf
03:45:25 -!- Alex3012 has quit (Read error: Connection reset by peer).
03:46:11 <alise> i kinda like it though
03:46:47 <pikhq> Yeah, LaTeX is a pretty meaty set of macros.
03:47:03 <alise> and if it's good enough for knuth..
03:47:54 <alise> \errmessage{This manual is copyrighted and should not be TeXed}\repeat
03:47:57 <alise> that's some amazing copyright protection
03:48:35 <alise> % Macros for The TeXbook=>
03:48:39 <alise> it wants the what now
03:48:52 <pikhq> Oh. Sorry. ftp://tug.ctan.org/pub/tex-archive/systems/knuth/dist/lib/manmac.tex
03:49:02 <pikhq> It comes with its own macro set. XD
03:50:11 <alise> % Macros for The TeXbook=>manmac.tex
03:50:12 <alise> \catcode`@=11 % borrow the private macros of PLAIN (with care)=>
03:50:23 <alise> oh god it's running thorugh every line with me
03:50:54 <alise> should i just cat the files together
03:53:11 <Sgeo> Raise your hand if you knew that Android had built-in MIDI support
03:54:02 <alise> jane@jane-desktop:~/texbook$ pdftex -interaction batchmode texbook.tex
03:54:03 <alise> This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6)
03:54:03 <alise> %&-line parsing enabled.
03:54:03 <alise> entering extended mode
03:54:03 <alise> % The log file now contains lines like these; I copied them=>
03:54:54 <alise> Output written on texbook.dvi (90 pages, 300556 bytes).
03:54:56 <alise> no idea what i did wrong
03:56:35 <alise> We all oughta rewrite typesetting from scratch.
03:57:39 -!- Alex3012_ has joined.
03:58:33 <alise> Output written on texbook.pdf (408 pages, 1822989 bytes).
03:58:33 <alise> Sounds about right
04:02:02 <alise> So, failing the TeXbook, I must unreliably google about.
04:05:19 <alise> pikhq: What? It seems that you even have to set paragraph spacing yourself.
04:07:22 <alise> \def\\{\par\hangindent 20pt\noindent\ignorespaces}
04:08:43 <alise> Mind, it is pretty: http://www-cs-faculty.stanford.edu/~knuth/vita.pdf
04:20:34 -!- augur has joined.
04:36:17 <alise> 4:35; start bugging me to embed myself soon.
04:40:19 <oerjan> no wait, don't google that
04:40:48 <oerjan> and _certainly_ don't click on the first google hit. go to bed instead.
04:41:09 <alise> and so the google machine fires up
04:41:43 <alise> i'm going to cry now
04:42:25 <oerjan> just close the tab. how hard can it be?
04:43:31 <alise> i'm just hardcore like that
04:43:44 <alise> clicked one or two links, you know, got bored, closed all the tabs
04:43:50 <oerjan> now i just need to follow my own advice. except the going to bed part.
04:43:51 <alise> nothing special huh eh
04:44:24 <oerjan> it just proves you're really an alien.
04:44:41 <Sgeo> The Brainfuck for Android app only allocates 300 bytes for the array
04:46:13 <alise> Sgeo: so, your android verdict?
04:46:42 <oerjan> completely worthless for your enterprise brainfuck solutions
04:47:50 <Sgeo> Not the best out-of-the-box experience, especially keyboardwise. Pinch-to-zoom in the browser has a "feature" that I really don't like, that makes the browser seem jumpy.
04:48:20 <Sgeo> With the N1, you have to be very careful that your palm doesn't end up resting on the touchscreen, but that's presumably due to multitouch issues
04:48:50 <Sgeo> It should be noted that my only basis for comparision is having typed on an iPhone keyboard yesterday.
04:49:34 <Sgeo> The Music app seems to have strange BACK semantics
04:49:58 <Sgeo> You want me to say good things/
04:51:31 <alise> I'm wondering if there are any good things.
04:52:09 <Sgeo> I can browse the web on it. I can make phone calls from it [if I had a SIM card in it]. Things like the calendar app don't waste screen space on a Menu button.
04:52:24 <Sgeo> Apart from that, I'd need to have tried another smartphone in order to be able to make any comparision
04:52:24 <alise> So it's good, right?
04:52:48 <Sgeo> alise, you'd need to try it
04:53:09 <Sgeo> Either that, or I need to really try an iPhone
04:53:42 <Sgeo> Oh, I liked how the Reddit app integrates with, say, apps that let you share things. You can share through Reddit
04:53:57 <Sgeo> Not that the reddit app is that great [it's a bit crashy]
04:55:35 <Sgeo> Can Last.fm scrobbers work on iPhone? Somehow, I doubt it
04:55:56 <Sgeo> [I'm assuming scrobber == app that reports to last.fm what music you're listening to]
04:56:37 <Sgeo> http://github.com/talklittle/reddit-is-fun/issues#issue/43 bug report on Reddit app
05:01:04 -!- Oranjer has left (?).
05:04:17 <alise> 5:03; now I've reached my threshold of snaity.
05:07:52 <oerjan> YOU BASTARD YOU ARE MAKING UP WORDS
05:09:26 <alise> my new <3ourite word
05:09:56 <oerjan> NOW YOU ARE MAKING UP PRONUNCIATIONS
05:10:46 <alise> i'm hysterically accurate
05:13:08 <Sgeo> Another bad point: The trackball FEELS as though a minute movement should equal one movement of the cursor, but it doesn't
05:13:16 <Sgeo> [mild point, really]
05:13:41 <alise> 5:13 it is light outside
05:13:42 <Sgeo> Would probably be unusable
05:13:46 <Sgeo> alise, go to sleep!
05:13:48 <alise> where is my motivation at
05:13:51 <alise> ok what do i need to do... many things
05:14:00 <alise> ok ok there are many steps involved in that process
05:14:03 <alise> firstly, i will close curtains
05:14:30 <alise> curtain turns out to actually be blanket
05:15:41 <alise> i guess i should go
05:15:53 <alise> but... you know, I'll stay logged in until I actually go to bed >_>
05:16:08 <alise> but let this be bye until tomorrow!
05:19:45 -!- augur has quit (Ping timeout: 265 seconds).
05:24:11 -!- alise has quit (Remote host closed the connection).
05:28:50 <oerjan> ïs rëgülärlÿ rëcömmëndëd
05:37:40 -!- augur has joined.
05:58:06 <Gregor> Today, I wrote a PDF viewer :P
06:05:19 * oerjan assumes there are some qualifications
06:05:30 <oerjan> besides genius, that is
06:27:53 -!- oerjan has quit (Quit: leaving).
06:30:50 <Gregor> pikhq: http://www.mobileread.com/forums/attachment.php?attachmentid=50406&d=1272083550
06:34:33 <pikhq> Not bad. I presume you linked against a PDF rendering library?
06:34:43 <pikhq> Seems like writing a full PDF implementation would take a *bit* more than a day.
06:35:13 -!- augur has quit (Ping timeout: 240 seconds).
06:43:03 <Gregor> pikhq: It's just meant to pseudo-reflow by cutting up two-column documents such that you can read a page in two half-page views instead of four.
06:43:22 <Gregor> Which is important when you're on an eInk-based reader :P
06:53:16 -!- augur has joined.
07:10:10 -!- coppro has quit (Ping timeout: 248 seconds).
07:13:53 -!- kar8nga has joined.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:03:26 <augur> Gregor: if you were on a mac, you could write a million in a day
08:05:31 <pikhq> augur: Or he could just install GNUstep and write the same code.
08:17:21 -!- augur has quit (Remote host closed the connection).
08:17:45 -!- augur has joined.
08:25:44 -!- jcp has quit (Read error: Operation timed out).
08:36:44 -!- kar8nga has quit (Remote host closed the connection).
09:53:29 -!- Rugxulo has joined.
10:15:38 <Rugxulo> new BEFI.COM, faster but still only 1014 bytes -> http://board.flatassembler.net/topic.php?t=10810
10:17:11 -!- MizardX has quit (Ping timeout: 276 seconds).
10:19:04 * Rugxulo is trying in vain to write a Befunge93 interpreter in REXX
10:19:17 <Rugxulo> I'm too dumb, I guess, too inexperienced
10:38:53 <Rugxulo> weird quirk, fixed it, now for the rest of the bugs and lacks :-/
10:40:03 -!- oklopod has quit (Ping timeout: 246 seconds).
10:43:46 -!- tombom has joined.
10:58:41 -!- oklopod has joined.
11:03:41 -!- Rugxulo has quit (Quit: ERC Version 5.3 (IRC client for Emacs)).
11:15:42 -!- kar8nga has joined.
11:34:01 -!- FireFly has joined.
12:07:44 -!- nooga has joined.
12:31:46 -!- Asztal has joined.
12:37:48 -!- tombom has quit (Quit: Leaving).
13:57:02 -!- Alex3012_ has quit (Read error: Connection reset by peer).
14:00:00 -!- Alex3012_ has joined.
14:24:31 <uorygl> Kokous jatkuu, mutta älä välitä aikaa
14:30:18 <uorygl> En halua ihmisten elää, tiedän, Internet saippua!
14:31:12 <Deewiant> I'm having trouble untranslating the latter
14:32:57 <uorygl> Joten, kaikki kanit melko emotionaalinen kidutus - kyllä!
14:37:15 <olsner> something about internet soap?
14:38:15 <uorygl> Yeah, a bad translation of "I don't want anybody in real life knowing I have soap from the Internet!".
14:38:19 <uorygl> Using a special bad translator.
14:39:11 <Deewiant> Darn, I thought the soap was just something random
14:39:41 <uorygl> Raskauteen liittyvät tulkinnat ultraääni raskaana presidentti Oklahoma.
14:39:44 <Deewiant> Hence the trouble; I was trying to figure out what could cause it
14:40:03 <uorygl> I would appreciate these more if I actually know Finnish.
14:40:09 <Deewiant> What're you using, intertran or something? :-P
14:40:18 <uorygl> Something like that, yes!
14:40:22 <uorygl> http://www.conveythis.com/translation.php
14:40:43 -!- aschueler has quit (Ping timeout: 240 seconds).
14:41:51 -!- Alex3012_ has quit (Read error: Connection reset by peer).
14:42:04 <Deewiant> Doesn't allow setting the source lang, meh
14:42:35 <uorygl> You can always enter something in Finnish and wait for it to get translated from Finnish, and then put the resulting English back in.
14:42:43 <uorygl> And see what the Finnish is.
14:42:45 <Deewiant> Except that it detected my Finnish as Afrikaans :-P
14:42:53 -!- aschueler has joined.
14:43:08 <Deewiant> Or does it always start from there
14:43:25 <Deewiant> Anyway, that uses Google's translator, which is fine
14:43:54 <Deewiant> Bad Translator!: "I am happy about this" -> "Olen erittäin onnellinen."
14:44:03 <Deewiant> InterTran: "I am happy about this" -> "I-KIRJAIN olen iloinen jokseenkin nyt kuluva."
14:44:56 <uorygl> Huh, apparently Google Translate thinks that the Portuguese word "Oklahoma" means Texas.
14:45:00 <Deewiant> BT turned it into en:"I am very happy", InterTran came up with en:"THE LETTER I I am happy somewhat now ongoing"
14:45:39 <Deewiant> I love how InterTran turns "I" into "THE LETTER I"
14:46:09 <uorygl> Since, you know, that's what I usually means.
14:46:30 <uorygl> Sherman, Texas, 24 raskaana olevia työntekijöitä.
14:46:48 <Deewiant> Except that it usually doesn't mean that.
14:47:16 <Deewiant> And never when followed by "am".
14:47:56 <uorygl> Devil ja slithy Zhimbl pehmeä ja mieto kylmä-kuin: Misebiles borogoves outgrabe nyt ja rotilla.
14:57:41 <fizzie> For what that particular translation sounds like, there are four possibly more reasonable ones at http://fi.wikipedia.org/wiki/Pekoraali
15:03:20 <Asztal> try using InterTran to translate a page from English to English. It's amusing.
15:11:46 -!- aschuele1 has joined.
15:13:15 -!- aschueler has quit (Ping timeout: 276 seconds).
15:20:27 -!- Alex3012_ has joined.
15:25:57 -!- cheater2 has quit (Ping timeout: 264 seconds).
15:31:56 -!- cheater2 has joined.
16:05:06 -!- nooga has quit (Ping timeout: 248 seconds).
16:18:15 -!- nooga has joined.
16:19:44 -!- pikhq has quit (Read error: Connection reset by peer).
16:24:09 <nooga> ooooo, that's the goddamn scottish hangover i suppose
16:24:47 -!- pikhq has joined.
16:53:59 -!- BeholdMyGlory has joined.
17:06:44 -!- Sgeo has quit (Ping timeout: 245 seconds).
17:06:45 -!- Sgeo_ has joined.
17:13:13 -!- anil has joined.
17:13:20 -!- anil has quit (Client Quit).
17:22:08 -!- Sgeo has joined.
17:22:59 -!- Sgeo_ has quit (Ping timeout: 245 seconds).
17:41:30 -!- alise has joined.
17:46:18 <alise> Amazing unamazing.
17:47:02 <alise> I had a dream where I was playing with an iPad
17:47:06 <alise> it was a lot smaller than I imagined
17:47:15 <alise> and the aspect ratio made it either too tall to be useful or too wide
17:47:22 <alise> nothing looked quite as impressive as it should
17:47:26 <alise> these are the kind of dreams i get
17:47:34 <alise> ones about the mediocrity of hyped technology
17:48:33 <Mathnerd314> I wish I could dream about the awesomeness of unhyped unpopular technology :-(
17:48:58 <alise> ais523 log reading: now Apple are denying apps that don't have enough features; http://yourhead.tumblr.com/post/539227006/apple-wont-give-you-the-time-of-day
17:49:05 <alise> this is the most hilarious slippery slope ever
17:49:21 <alise> soon you'll only be able to submit an app if Jobs himself can't tell it from one of Apple's own!
17:51:20 <Gregor> alise: Are you sure this was a dream, and not ... y'know, the actual iPad?
17:51:34 <alise> I have a feeling the iPad is significantly larger in real life.
17:51:53 <alise> I mean, all my complaints were aesthetic concerns; my subconscious can't quite handle intellectual complaints.
17:51:56 <alise> And the iPad certainly has the looks :P
17:52:21 <alise> www.mobileread.com/forums/attachment.php?attachmentid=50406&d=1272083550
17:52:25 <alise> 22:43:03 <Gregor> pikhq: It's just meant to pseudo-reflow by cutting up two-column documents such that you can read a page in two half-page views instead of four.
17:52:28 <alise> Nice; port it to Android. :P
17:52:53 <Gregor> Changing source language and all libraries hardly counts as a port :P
17:53:53 <alise> Hey, poppler works on Android. Probably. :P
17:54:13 <alise> 08:24:09 <nooga> ooooo, that's the goddamn scottish hangover i suppose
17:54:19 <Gregor> Android = Java dev platform
17:54:21 <alise> The only cure is not drinking ridiculous amounts of alcohol the night before.
17:54:27 <alise> It's such a sad illness.
17:54:37 <alise> But you can use JNI
17:54:45 <alise> Also, you /can/ use C, just only if you like interfacing with the APIs in a secret world of pain.
17:54:52 <alise> Not only a world of pain. A secret world of pain.
17:55:39 <Gregor> The IREX = X11 + GTK+ :)
17:55:42 <alise> "Microsoft stealth launches F#" --El Reg
17:56:01 <alise> iRex; isn't that the one ereader that costs several organs?
17:56:10 <alise> And looks like shit?
17:56:37 <alise> [[What hope is there for F#, the new language that Microsoft has sneaked into Visual Studio 2010, launched this month?]]
17:56:39 <fizzie> Gregor: Port it to Maemo, that's X11 + still-GTK+-a-for-a-while-before-going-Qt, and poppler's pre-packaged in the repository. Except that I have no idea what that program of yours does.
17:56:43 <alise> Man, I love the Register; they're so silly.
17:57:06 <fizzie> What is silly is this:
17:57:07 <fizzie> $ dot -Tpng -otest.png test.dot
17:57:07 <fizzie> dot: height (51515 >= 32768) is too large.
17:57:09 <alise> Gregor: btw your link was an invalid attachment
17:57:17 <alise> fizzie: That's modern, man.
17:57:32 <alise> fizzie: his program reformats + views pdfs
17:57:56 <Gregor> alise: It is now, I uploaded a new screenshot :P
17:58:11 <Gregor> http://www.mobileread.com/forums/attachment.php?attachmentid=50424&d=1272126494
17:58:13 <alise> Breaking links, often requiring you to log in, using shitty interfaces...
17:58:40 <alise> Gregor: I don't quite dig the Windows 2-style top UI controls
17:58:51 <alise> Or does the eInk magically smooth them out perfectly?
17:58:59 <alise> If so, disabling antialiasing in poppler, too.
17:59:37 <Gregor> Are you referring to the shape, or the placement?
18:00:00 <alise> Well, the raggedness, mostly.
18:00:09 <alise> But yes, the controls are too close together.
18:00:19 <alise> "Theres an array of integers, of odd size N (N%2 == 1)." ;; thanks for defining what "odd" means
18:00:21 <Gregor> Yeah, that's smoothed out on the screen.
18:00:36 <alise> "Same array, this time its size is even (N%2 == 0)." how is it the SAME array...
18:00:41 <Gregor> Hm, maybe I should disable antialiasing and see how the eInk fares ...
18:00:47 <alise> That'd be interesting. :P
18:00:53 <alise> I wonder if the built-in book reader antialiases.
18:00:58 <alise> Probably, for the levels-of-grey stuff. But who knows.
18:01:08 <Gregor> Hard to say, it's proprietary Adobe shit >_<
18:01:16 <Gregor> It's the only non-F/OSS part of the stack.
18:01:53 <alise> I wanted a Kindle but it doesn't have the nice free internet over in the UK.
18:02:11 <alise> Writing a little minimalist Javascript IRC client was pretty much the main use I had in mind for it.
18:02:29 <alise> Wow, arcanesentiment is #2 on /r/programming.
18:02:32 <alise> I almost forgot about that blog.
18:02:47 <alise> The Kindle does have the nicest form factor & looks of all the readers, I think.
18:03:04 <alise> The Sony touch ones seem a gimmick, though; I don't think I'd like poking at eink for no particular reason.
18:03:14 <Gregor> You're referring to the DX?
18:03:31 <alise> No, just the 2. Why; is the DX better?
18:03:36 <alise> I thought the DX would be too big for regular booky books.
18:03:51 <Gregor> The IREX is about the same size as a Kindle 2, but has a (much) bigger screen.
18:04:12 <alise> The black plastic looks so tacky, though. :P
18:04:17 <alise> Also, the IREX costs so, so much money.
18:04:34 <alise> iRex iLiad 2nd Edition Digital Reader
18:04:34 <alise> 590.95 new - Purelygadgets.co.uk
18:04:34 <alise> IREX iLiad Book Edition Electronic Book
18:04:34 <alise> 491.00 new - Pixmania.com
18:04:34 <alise> IREX Digital Reader 800S E-book Reader + 4 GB Micro SDHC Memory Card +
18:04:35 -!- Tritonio_GR has joined.
18:04:36 <alise> 532.82 new - D2 LEISURE GROUP
18:04:41 <alise> I am not paying 500 pounds for an ebook reader.
18:04:52 <Gregor> iLiad = dead, DR800 is cheap in the US.
18:04:55 <alise> (= $768; you uncouth guy)
18:05:05 <alise> Since when is the iLiad dead?
18:05:08 <alise> Wikipedia doesn't say so
18:05:10 <Gregor> But yeah, for some reason they're crazy-expensive in Europe ... where they're manufactured.
18:05:15 <alise> Also googling it gets stuff about bikes
18:05:22 <Gregor> alise: Well, the DR800 is roughly the same form factor but newer :p
18:05:31 <alise> Oh, that is prettier.
18:05:34 <alise> I like the look of that.
18:05:45 <alise> Uh, why the pen though?
18:05:56 <alise> Oh, http://www.techwall.org/wp-content/uploads/2009/09/irex-dr-800.jpg must be the prettiest ebook reader now.
18:05:58 <Gregor> Just for search and such, onscreen keyboard.
18:06:01 <Gregor> Usually I don't use it.
18:06:01 <alise> The Kindle loses :P
18:06:08 <alise> Gregor: Doesn't work with touch?
18:06:16 <alise> Then how am I to IRC? :(
18:06:25 <Gregor> Wait, WTF is with that enormous pen X-D
18:06:33 <Gregor> The image you have has a custom stylus, not the small one that comes with it.
18:07:23 <alise> All the other images I saw had it :P
18:07:34 <alise> Anyway, my enormous pen is entirely my own business, thank you very much.
18:08:01 <fizzie> Fungot, as seen by dot: http://zem.fi/~fis/test.png (resized to tiny 852x6439 from the original readable 5109x38636 pixels)
18:08:01 <alise> Also, the new iPhone is going to have a >300dpi, wtf apple stop it, please start sucking at /everything/
18:08:04 <alise> then I can FORGET YOU
18:08:11 <Gregor> Anywho, I actually wanted an ereader /primarily/ for reading. For anything else it wouldn't be worthwhile.
18:08:35 <alise> Yeah, I just don't read on the go... at all.
18:08:45 <alise> Books I read almost exclusively before going to sleep, papers I almost always read on a computer...
18:08:54 <alise> Gregor: Does it allow free copying of your books around?
18:09:10 <alise> fizzie: What's that squashed onion thing over half way down?
18:09:27 <Gregor> alise: Yeah, they just download to the SD card. Idonno how all the DRM garbage applies to the different formats though ...
18:09:31 <alise> fizzie: Also, make it lay it out to heavily optimise for short lines; wideness is fine. That'd be interesting.
18:10:02 <alise> Gregor: What we /really/ need is a computer screen that can switch to eink-style mode on the fly.
18:10:09 <alise> And is, say, OLED the rest of the time.
18:10:15 <fizzie> alise: I think it's the jump table for punctuation tokens.
18:10:18 <alise> Then you could have an iPad-ish thing that's actually usable for reading books on.
18:10:32 <Gregor> Have an OLED over an eInk screen that can be set "transparent"
18:10:32 <alise> Gregor: Well, they are doing it!
18:10:37 <alise> Pixel Qi. But I don't know how well they are doing with it.
18:10:39 <alise> http://www.google.co.uk/search?q=pixel+qi&ie=utf-8&oe=utf-8&aq=t&rls=com.ubuntu:en-GB:unofficial&client=firefox-a
18:11:00 <alise> From the part of the team that brought you the screen of the XO laptop -- not so impressive, I know.
18:11:10 <alise> It's not perfect right now though
18:11:29 <alise> http://www.pixelqi.com/products ;; some photos
18:11:49 <alise> [[While Pixel Qi has said that it believes a $75 laptop will be ready in 2010. However Pixel Qi isn't making a $75 laptop. We are making the screens.]]
18:12:36 <fizzie> http://zem.fi/~fis/test_neato.png -- neato's default don't-avoid-overlaps mode is always so useful for large graphs.
18:13:31 <alise> Looks like an organism of sorts.
18:13:38 <alise> fizzie: Ooh, I have an amazing idea.
18:13:55 <alise> Do an animated one, where something like: the center of the screen is where the IP is now; and cells change accordingly.
18:14:00 <alise> So it'd be relayouting a bit like a flow.
18:16:48 * alise considers writing a little ditty library for C for doing arbitrary-precision real computatio
18:17:24 <fizzie> Hrm, I don't think graphviz is very good for animation; but different sorts of real-time funge-code visualization would be nice to have.
18:17:51 <alise> fizzie: I just think the constant-relayouting would look like an organism flowing through the program, so to speak.
18:19:19 <fizzie> That particular graph is actually from a static compiler of a non-self-modifying Funge-98 subset; it traces all code paths in advance, compiles to a register-based intermediate form, outputs a single LLVM function for the program. The graph is the basic block graph for the intermediate form.
18:19:43 <alise> Can it actually run fungot?
18:19:44 <fungot> alise: " expression" instead of with /foo... i know......
18:20:48 <alise> Hmm, I could do a real as simply taking an int for a precision argument... so that, e.g. it could be passed as the upper bound for infinite sums.
18:20:50 <alise> Yeah, I'll do that.
18:21:18 <fizzie> Not yet, no. But fungot is the target I'm aiming at, since I can't ever run mycology with it. It does run that rule110.bf benchmark I made a while ago, and rot13.bf too.
18:21:19 <fungot> fizzie: very few schemes even come close
18:21:33 <alise> This also means I need bignums, for numerators and denominators of rationals. Groan.
18:22:45 -!- nooga has quit (Ping timeout: 246 seconds).
18:24:49 <alise> I guess if I want to write the ultimate CAS/dependently-typed programming language/theorem prover, I ought to write my own bignum library. After all, everybody else will get it Wrong. :P
18:29:06 -!- oerjan has joined.
18:29:28 -!- ais523 has joined.
18:30:15 <oerjan> also ais523, who nearly caused an embarassing tab expansion error there
18:32:40 <ais523> oerjan: you could have said hello in the other order, and nobody would have noticed or cared
18:32:53 <oerjan> well i aren't that clever, you know
18:33:15 <oerjan> ais523: except alise had already said hi
18:39:23 <uorygl> You're not a LIFO greeter, I see.
18:39:41 <uorygl> Hi, ais523. Hi, oerjan.
18:40:36 * alise runs a tactic in Coq while forgetting it's turing-complete
18:41:01 <alise> proving "forall x, Y * = x * (Y * x)" will /not/ proceed by computation.
18:41:46 -!- HackEgo has quit (Ping timeout: 260 seconds).
18:42:27 <alise> I'm carrying on from fax's http://muaddibspace.blogspot.com/2009/10/short-note-on-semantics.html
18:42:52 <alise> http://pastie.org/933123.txt?key=rsxttmof1dxsmaxf4iegg
18:43:00 <uorygl> Is Y * an abbreviation of Y * x?
18:43:01 <alise> we can reason about this forever but there's no actual model
18:43:13 <alise> i.e. we can't actually give concrete values to the SK, app, S and K sets
18:43:17 <alise> because coq always terminates
18:43:19 <alise> but this is good enough
18:43:22 <alise> uorygl: no; just a typo.
18:43:31 <Sgeo> The Nexus One trackball is more useful than it appears
18:45:03 <alise> Theorem Y_prop : Y * I = I * (Y * I).
18:45:09 <alise> easy, but not as general as I'd like :P
18:45:29 <alise> maybe some other fixed-point combinator would make this easier.
18:46:50 <alise> if anyone manages to prove the polymorphic case of that, you get a cookie
18:46:56 <alise> S * (K * M) * (S * (S * (K * S) * K)) * (K * M).
18:46:59 <alise> any fixed-point combinator
18:47:42 <alise> Definition M := S * I * I.
18:47:42 <alise> Theorem M_prop : forall x, M * x = x * x.
18:47:44 <alise> Ltac skim := repeat (ski || rewrite M_prop).
18:47:48 <alise> http://pastie.org/933123.txt?key=rsxttmof1dxsmaxf4iegg
18:48:25 <alise> just using "sk(i(m)?)?" doesn't halt because of course Y diverges
18:48:32 -!- jcp has joined.
18:48:34 <alise> so we need to be more careful and come up iwth a more analytic proof
18:49:29 -!- augur has quit (Ping timeout: 260 seconds).
18:49:48 <alise> Actually if we used setoid equality I think fax is saying that we could define an undecidable == to mean "computes to at some point".
18:49:51 <alise> Which I think would be possible.
18:49:56 <alise> But you couldn't use it for much, I don't think.
18:51:37 -!- pikhq has quit (Read error: Connection reset by peer).
18:56:02 <oerjan> well "reduces to the same thing at some point" is what beta-equivalence boils down to, once you've proved church-rosser for it
18:56:02 <alise> ais523: Here, you prove it. I hear you proved some thingymajic about turing-complete things, so this is clearly perfect for you to do.
18:56:09 <alise> oerjan: of course.
18:56:20 <ais523> alise: what do you want me to prove?
18:56:21 <alise> oerjan: point is that since coq terminates, we can never satisfy:
18:56:23 <alise> Parameter SK : Set.
18:56:24 <alise> Parameter app : SK -> SK -> SK.
18:56:25 <alise> Axiom S_prop : forall a b c, S * a * b * c = (a * c) * (b * c).
18:56:26 <alise> Axiom K_prop : forall a b, K * a * b = a.
18:56:28 <alise> Axiom SK_prop : S <> K.
18:56:44 <ais523> hmm, this is combinatory logic, presumably
18:56:48 <alise> oerjan: we can define stuff using it, and using S_prop and K_prop prove "equalities" (reductions) with it, and "compute" it by having a tactic that repeatedly applies these
18:56:55 <alise> but we can never actually implement a model in Coq
18:57:04 <alise> ais523: http://pastie.org/933123.txt?key=rsxttmof1dxsmaxf4iegg
18:57:23 <alise> you can't compute with skim to do it because (Y x) always diverges
18:57:31 <alise> so skim never terminates (proof tactics can be turing-complete)
18:58:27 <alise> "The Brain Editor and Fucker, or Brainfuck for TECO. (esolangs.org)" -- #13 on /r/programming
18:58:36 <alise> posted by the author, even
18:58:40 <alise> Note that I wrote that using Tom Almy's excellent TECOC so I can't guarantee it'll work on just any old TECO version. In theory, it should work on anything that's compatible with TECO-11 v40.
18:58:40 <alise> Edit: usage instructions! For the lazy: Start TECO up in the directory where you saved the .tec file, and when you get its prompt (a *), type eiBEFstarObf.tec$$ ($$ means <ESC><ESC>, ie. press the ESC key 2 times)
18:58:43 <alise> http://www.esolangs.org/files/brainfuck/impl/BEFstar.txt
18:58:44 <oerjan> so presumably you need to emulate step-by-step evaluation somehow
18:59:06 <alise> rewrite S_prop will reduce a full S_application
18:59:11 <alise> ditto for K, I, and M (M is SII)
18:59:25 <alise> skim just repeatedly does "rewrite [SKIM]_prop", basically
18:59:28 <alise> until it doesn't change
18:59:30 <alise> of course, with Y this diverges
18:59:33 <alise> we can unfold everything
18:59:37 <alise> but it still essentially boils down to
18:59:47 <alise> CRAP WITH X IN IT = x * CRAP WITH X IN IT
18:59:51 <alise> so I'm not sure where to proceed from here
19:00:24 <oerjan> alise: well my point is you _should't_ repeat, you should do the exact sequence of s,k,i and m reductions necessary, which i assume you can do by hand somehow...
19:00:43 <alise> but I ran them for a while and nothing seemed to help
19:00:54 -!- EgoBot has quit (Ping timeout: 260 seconds).
19:01:05 <alise> try S_prop; try K_prop.
19:01:11 <alise> running this over and over again until you want to stop should work
19:01:16 <alise> but will it ever actually get into the form of x = x?
19:01:31 <oerjan> well do it on paper first
19:01:35 <alise> hmm, try isn't working
19:01:38 <alise> oerjan: that won't really help
19:01:48 <oerjan> it will tell you the exact sequence you need
19:02:02 <alise> try (rewrite S_prop || rewrite K_prop); try reflexivity.
19:02:04 * alise repeatedly does this
19:02:07 <alise> oerjan: so will messing around in Coq
19:02:25 <alise> (S * S * (S * (S * S * K)) * (K * x) *
19:02:25 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x))) =
19:02:29 <alise> (S * S * (S * (S * S * K)) * (K * x) *
19:02:31 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x))))
19:02:35 <alise> I think we need some sort of induction here
19:04:04 <alise> it just keeps expanding
19:04:10 <alise> hmm... I wonder if I can do some sort of fix-point proof here.
19:06:33 <oerjan> alise: the thing is you want Y * x = x * (Y * x). once you have shown Y * x = x * _something_, show that _something_ reduces to Y * x
19:07:02 <oerjan> where you quite likely need to do equations backwards, btw
19:07:04 <alise> once you have shown Y * x = x * something
19:07:08 <alise> show that something = Y * x
19:07:12 <alise> yeah, that's just the original problem.
19:07:15 <alise> with an extra variable.
19:07:29 <alise> I don't know if you can do equations backwards
19:07:38 <oerjan> "something" was a turn of phrase
19:08:26 <oerjan> although since you _do_ have church-rosser backwards shouldn't really be necessary. assuming M doesn't ruin something.
19:08:28 <alise> there, after 9 rewrite S_prop ||| rewrite K_props, I have some sort of result
19:08:33 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x * x *
19:08:33 <alise> (K * (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x) * x)) =
19:08:33 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x * x *
19:08:36 <alise> (K * (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x) * x)))
19:08:40 <alise> I really want to just rewrite on the LHS
19:08:42 <alise> so I'll do it as an assertion
19:09:18 <oerjan> do all the K reductions. they are sure not to make things more complicated after all, so _will_ terminate.
19:09:26 <alise> assert (x * (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x * x *
19:09:27 -!- comex has quit (Ping timeout: 252 seconds).
19:09:27 <alise> (K * (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x) * x)) =
19:09:35 <alise> oerjan: good point
19:09:50 <alise> done; but there are still Ks, just unevaluated ones ofc
19:10:17 <alise> ============================
19:10:18 <alise> (S * (K * (S * S * (S * (S * S * K)))) * K * x *
19:10:18 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x)) =
19:10:32 <alise> I wonder how to do a reverse rewrite
19:11:03 <alise> oerjan: no I in this combinator
19:11:06 <alise> assert (porp_WHATEVER : y = x). symmetry. apply WHATEVER_prop.
19:11:09 <alise> rewrite porp_WHATEVER.
19:11:11 <alise> but that is gross...
19:11:27 <alise> and I can't tactic it up, I think
19:11:57 <alise> Uses the equality term1=term2 from right to left
19:12:20 <oerjan> alise: anyway those x * (x * ... up there tell me you've already done too much, you _should_ be able to get just one x * ... outside
19:12:53 -!- comex has joined.
19:12:56 <oerjan> basically, hm, whatever you do don't do more than _one_ M reduction, i think
19:13:15 <alise> S * S * K * (S * (K * (S * S * (S * (S * S * K)))) * K).
19:13:17 <oerjan> unless you really need it
19:13:20 <alise> K * x * (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x) *
19:13:21 <alise> (S * (S * S * K) * (K * x) *
19:13:21 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x)) =
19:13:21 <alise> (K * x * (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x) *
19:13:22 <alise> (S * (S * S * K) * (K * x) *
19:13:23 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x)))
19:13:26 <alise> this is the first step where I can get x *
19:13:28 <oerjan> oh so it was just an abbreviation
19:13:31 <alise> so I should stop there right?
19:13:39 <alise> and not rewrite any more Ks?
19:13:43 <alise> if I do, it turns into x * (x * ...
19:14:02 <oerjan> rewriting K's shouldn't hurt anything
19:14:11 <alise> so stop whining about my x * x *! :-)
19:14:24 <oerjan> if that does something wrong, you have _already_ done something wrong
19:14:39 <alise> I'll keep trying this
19:14:40 <oerjan> suggestion: reduce K between everything else
19:15:08 <alise> sorry, it does not work.
19:15:13 <alise> rewrite S_prop; repeat (rewrite K_prop).
19:15:13 <alise> rewrite S_prop; repeat (rewrite K_prop).
19:15:13 <alise> rewrite S_prop; repeat (rewrite K_prop).
19:15:13 <alise> rewrite S_prop; repeat (rewrite K_prop).
19:15:13 <alise> rewrite S_prop; repeat (rewrite K_prop).
19:15:19 <alise> this is simply due to the definition of Y -- it is unavoidable!
19:15:25 <alise> it is rewriting on the right hand side of the equality
19:15:27 <alise> I cannot help that
19:16:42 <alise> H : S * (K * (S * S * (S * (S * S * K)))) * K * x *
19:16:42 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x) =
19:16:42 <alise> ============================
19:16:43 <alise> (S * (S * S * K) * (K * x) * (S * (K * (S * S * (S * (S * S * K)))) * K)) =
19:16:49 <alise> (S * (S * S * K) * (K * x) * (S * (K * (S * S * (S * (S * S * K)))) * K)))
19:16:51 <alise> I can do that, at least
19:17:41 <oerjan> ssk(s(k(ss(s(ssk))))k) is a strange combinator
19:17:54 <alise> yes, and your advice with rewriting Ks broke that proof!
19:18:26 <oerjan> oh well ignore me then
19:18:33 <alise> I can get just x *
19:18:40 <alise> S * (K * x) * (S * (S * S * K) * (K * x)) *
19:18:41 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x) =
19:18:42 <alise> (S * (K * x) * (S * (S * S * K) * (K * x)) *
19:18:42 <alise> (K * (S * (K * (S * S * (S * (S * S * K)))) * K) * x))
19:19:18 <oerjan> that's something = x * something afaict
19:19:45 <alise> assert ((S * (K * (S * S * (S * (S * S * K)))) * K * x *
19:19:46 <alise> (S * (K * (S * S * (S * (S * S * K)))) * K)) = Y * x).
19:19:52 <alise> ============================
19:19:53 <alise> S * (K * (S * S * (S * (S * S * K)))) * K * x *
19:19:53 <alise> (S * (K * (S * S * (S * (S * S * K)))) * K) =
19:19:53 <alise> S * (S * S) * (S * (K * (S * S * (S * (S * S * K))))) * K * x
19:20:00 <oerjan> x * ... * ... isn't useful
19:20:15 <alise> maybe i really should do some sort of induction hypothesis
19:20:28 <oerjan> x should not be applied to two things _ever_. in fact that ought to be impossible to get i think
19:20:33 <alise> Y * x = x * (Y * y) -> y = x
19:21:22 <alise> oerjan: i /think/ this computational approach can never work
19:21:30 <alise> oerjan: shall I explain why?
19:21:35 <oerjan> is your Y combinator a well-known one?
19:21:45 <alise> John Tromp's; I can also substitute the direct translation of Y
19:21:48 <alise> we can never do any computation of the form x * foo
19:21:51 <alise> because we have no such axiom of proof
19:21:56 <alise> so it will ALWAYS be
19:22:06 <alise> (partial evaluation of (Y x)) = x * (partial evaluation of (Y x))
19:22:34 <alise> what are you referring to?
19:23:07 <alise> and the problem is
19:23:12 <alise> I don't think I can rewrite just on the left hand side
19:23:20 <alise> so it will always turn into x * x on the rhs at the same time
19:23:27 <oerjan> x = y implies f(x) = f(y) for all functions f
19:23:43 <alise> but can I prove this?
19:23:50 <alise> like, as far as this lc goes
19:23:53 <oerjan> or even P(x) <=> P(y) for all predicates P
19:24:09 <alise> yes, this is how Coq's equality is defined... but we don't have f(x)
19:24:26 <oerjan> alise: if that's not put into your = automatically, you may get by with adding it for left and right application with a constant
19:24:33 <alise> yes, I can prove it
19:24:44 <alise> Theorem SK_leibniz : forall f x y, x = y -> f * x = f * y.
19:24:49 <alise> but I'm not sure how this will help
19:25:09 <alise> in fact I am not even sure I can prove this
19:25:10 <oerjan> _now_ you can do any reduction you want on the right side of an application
19:25:35 * alise tries Admitting Y_prop first (adding it as an axiom), just to check that it doesn't lead to horrible things if it's proven (which would imply it's impossible to prove)
19:26:07 -!- augur has joined.
19:26:26 <alise> Theorem YY_prop : Y * Y = Y * (Y * Y).
19:26:33 <alise> so I wonder if I can use equality induction
19:26:37 <alise> to do infinite computation with this
19:27:52 <alise> Theorem YY_prop : Y * Y = Y * (Y * (Y * Y)).
19:27:53 <alise> rewrite <- Y_prop.
19:27:53 <alise> rewrite <- Y_prop.
19:28:09 <alise> we can actually simplify expressions by using the evaluation rules backwards to introduce combinators
19:28:43 -!- oerjan has quit (Quit: leaving).
19:30:26 -!- Oranjer has joined.
19:31:00 -!- alise_ has joined.
19:31:13 <alise_> ais523: the nice thing about my reduction rules
19:31:19 <alise_> is that instead of combinator -> result
19:31:22 <alise_> they're combinator <-> result
19:31:41 <alise_> so we can prove that the results of messy combinators like, say, plus that might return a lot of wrapping in their result
19:31:46 <alise_> still equal simple things
19:31:49 <alise_> like plus two two = four
19:32:28 <alise_> I wonder if I could prove eta-reduction
19:33:36 -!- alise has quit (Ping timeout: 258 seconds).
19:34:32 <alise_> ais523: I love how we can prove all these reasonable results about a theory that can absolutely have no possible model in Coq
19:36:26 <alise_> incidentally, you can translate any recursive data type into the lambda calculus in the same manner as church numerals
19:36:31 <alise_> with as many constructors as you want
19:36:36 <alise_> although using them gets a bit unwieldy
19:36:43 <alise_> basically you encode a type as its induction combinator
19:36:46 <alise_> aka the recursion combinator
19:36:56 <alise_> O | S nat's is X -> (X -> X) -> X
19:36:58 <alise_> O | S nat's is X -> (X -> X) -> nat -> X
19:37:34 <alise_> wow, succ is just S(S(KS)K) in SK
19:38:23 <alise_> Theorem succ_one_is_two : succ * one = two.
19:39:03 <alise_> Theorem ss1_is_s2 : succ * (succ * one) = succ * two.
19:40:02 <alise_> Theorem exp2_2_is_ss2 : two * two = succ * (succ * two).
19:40:03 <alise_> this is harder to prove!
19:40:25 -!- pikhq has joined.
19:40:39 <alise_> in fact I can't do it :)
19:40:45 <alise_> I'm proving things about SKI in Coq
19:42:34 <alise_> pikhq: I can't prove that Y*x = x*(Y*x) though, so I just added it as an axiom for now
19:42:39 <alise_> I did prove that succ*one=two, though!
19:43:34 <alise_> In fact, I should physically coerce you into proving that Y*x=x*(Y*x) for me!
19:43:40 <alise_> It has dependent types...
19:48:41 -!- lament_ has joined.
19:49:25 <pikhq> It is 2 in the afternoon and I have not caffeinated. Coffee taim
19:49:47 -!- lament_ has changed nick to lament.
19:51:35 -!- Gracenotes has quit (Quit: Leaving).
19:59:06 <Sgeo> alise_, nice things about N1 [although these are Android things]: The notification system. The ability to see a QR code to an app on a web page on your comp and just scan it in to the phone
19:59:38 <Sgeo> I usually just search for apps on the computer, and scan in the QR code to the N1 if I want it
20:00:34 <Sgeo> Bad things about N1: explorer.exe crashed. Oh wait, that WinXP
20:01:35 <Sgeo> Bad thing: The included headphone things hurt your ears
20:01:41 <Sgeo> Maybe I'm putting them in wrong
20:01:41 <alise_> Coq's "tauto" tactic shouldn't be called that. A tactic called "tauto" should prove any provable proposition. :-)
20:05:59 -!- zzo38 has joined.
20:08:52 <Sgeo> N1 seems to play MIDIs nicely
20:12:01 -!- lament has quit (Quit: lament).
20:12:26 <Sgeo> Actually, I played the wrong file
20:12:53 -!- lament has joined.
20:16:33 <Sgeo> Are earbuds supposed to hurt?
20:17:48 <pikhq> They are supposed to remove your ears.
20:18:04 * alise_ is doing reals in haskell
20:18:07 * alise_ tries to implement http://en.wikipedia.org/wiki/Chudnovsky_algorithm
20:20:10 <alise_> wtf, Haskell's Rational type doesn't have /
20:20:34 <Sgeo> alise_, do iPhones have MIDI support?
20:22:18 -!- pikhq has quit (Read error: Connection reset by peer).
20:36:24 -!- MizardX has joined.
20:38:43 -!- pikhq has joined.
20:39:37 -!- sebbu has quit (Ping timeout: 240 seconds).
20:45:08 -!- oklopod has changed nick to oklopol.
20:45:21 -!- sebbu has joined.
20:48:58 -!- nooga has joined.
20:58:58 -!- tombom has joined.
21:21:17 <pikhq> Gregor: I've got a segfault from Egobfi.
21:22:06 <pikhq> Program: awib.b. Cause: dereferencing mptr, mptr out of bounds.
21:22:36 <pikhq> In bf_interpret, "if (*mptr) {", line 56...
21:24:19 <pikhq> So. Memory somehow out of bounds.
21:25:28 <pikhq> I know you don't exactly maintain that much any more, but... Yeah. That seems like a bit of a bug. ;)
21:30:15 <pikhq> And then I tried building egobfc's output and remembered that egobfc is broken. XD
21:32:34 <pikhq> I think I'm just going to blame awib's frontend-backend design.
21:35:08 <pikhq> No, that appears to segfault *every* written-in-Brainfuck compiler.
21:35:18 <pikhq> On pretty much every implementation I've got.
21:36:00 <pikhq> LostKng is hard. :P
21:45:46 <ais523> I never got past the first few rooms of the cave
21:46:16 <ais523> pikhq: segfault probably implies going < off the start of the tape
21:46:25 <ais523> or possibly > off the end, if the tape's finitely long for some reason
21:46:42 <pikhq> ais523: Shouldn't be > off the end in egobfi8.
21:47:16 <pikhq> It *does* have a memory-limited tape there.
21:47:37 <pikhq> As for < off the start of the tape? I'm not sure why it would do that, though that is the only way for that to *happen*.
21:59:37 <pikhq> Gregor's Brainfuck interpreter.
22:00:00 <pikhq> Not the fastest, but it's fairly complete.
22:00:13 <AnMaster> pikhq, what was it that segfaulted pretty much everything? awib?
22:00:30 <pikhq> awib compiling LostKng *on* nearly everything.
22:00:50 <AnMaster> you could pretty easily run over the end of the tape
22:01:12 <pikhq> If it's running over the end of my memory, I'm scared.
22:01:18 <AnMaster> pikhq, does awib on awib segfault on lostkng?
22:01:59 <AnMaster> pikhq, anyway, does awib output as it go, or does it try to read the whole thing in first and do some optimisation?
22:02:25 <pikhq> Read the whole thing in, optimise, pass it to the selected backend.
22:02:28 <AnMaster> if the latter I wouldn't be surprised if it hit some bug easily. Heck you might even run into issues with counters overflowing
22:03:16 <pikhq> Hmm. Actually... Yeah, it probably *is* an overflowing counter.
22:03:32 <AnMaster> like current pointer position or even "number of > in a row" issue
22:04:11 <AnMaster> but if awib tries to do multiple cells to track the number that is going to cause issues
22:04:52 <pikhq> awib is designed to work on Brainfuck interpreters with 8-bit *or greater* cells.
22:05:08 <AnMaster> bbl, switching monitor to other computer (need to do some BIOS stuff on a normally headless computer)
22:05:35 <pikhq> I'm strongly suspecting this segfaulted when it was checking for loop balance, actually.
22:18:45 <AnMaster> pikhq, quite plausible in lostkng
22:20:38 <Sgeo> My not-quite-completed interpreter in Haskell doesn't check for loop balance
22:21:02 -!- jcp has quit (Ping timeout: 276 seconds).
22:21:07 <Sgeo> If there's an extra ], it truncates, if there are extra [, it assumes there are the needed ] at the end
22:21:11 <pikhq> Segfaults on larger clles, though.
22:22:08 <pikhq> My semi-functional Brainfuck interpreter inserts a QUIT command at the end of the program buffer.
22:22:30 <pikhq> So, if you happen to have not done loop balance right, you get an exit.
22:23:14 <pikhq> Oh, yeah, and it ends up setting the jump address for the loop to that QUIT command, as well.
22:23:22 -!- Gracenotes has joined.
22:24:01 <Mathnerd314> Sgeo: all that matters is that it's consistent.
22:24:30 <Mathnerd314> so consider extra ] to have needed [ at the beginning ;-)
22:25:24 <AnMaster> pikhq, what about two unclosed ones?
22:25:35 <pikhq> AnMaster: Same behavior.
22:25:36 -!- kar8nga has quit (Remote host closed the connection).
22:26:03 <AnMaster> pikhq, also, checking loop balance isn't very hard. You will get it for "free" when parsing it into <data structure of choice>
22:26:16 <AnMaster> at least if you do the parser the usual way
22:26:30 <AnMaster> (with that I mean a recursive parser)
22:27:03 <pikhq> AnMaster: It's getting parsed into a single array of pointers to goto addresses.
22:27:18 <pikhq> With arguments coming after the pointer if necessary.
22:27:32 <pikhq> I've done it twice. Twice!
22:27:46 <pikhq> And it's a very clean fit for Brainfuck.
22:27:49 <AnMaster> pikhq, I assume you fold >>> into >3 or such?
22:27:57 <AnMaster> even for an interpreter that is a good idea
22:28:16 <AnMaster> (some of the more expensive optimisations might only be a good idea for compilers though)
22:28:22 <pikhq> The +-><[] commands all take arguments.
22:29:05 <pikhq> . is output, , is input.
22:29:14 <pikhq> Not a massive benefit to folding either, really.
22:29:22 <AnMaster> . could take "constant value found by optimising"
22:29:35 <AnMaster> esotope and in-between did that kind of stuff
22:29:48 <pikhq> But that requires non-peephole optimisations. :)
22:30:01 <AnMaster> pikhq, true, they are both very slow on lostkng
22:30:12 <pikhq> Produce good output though.
22:30:36 <AnMaster> pikhq, but building dependency graphs for each section between unbalanced loops takes a while
22:31:00 <AnMaster> especially if you are re-running all optimisation passes until nothing changes any more
22:31:02 -!- jcp has joined.
22:32:12 <AnMaster> pikhq, anyway, I think what is more interesting is in which ways you can optimise unbalanced loops
22:32:39 <AnMaster> well obviously you can optimise them internally like merging ++ in [++>] but I mean into some higher level thingy
22:32:41 <pikhq> Yeah, there really is a lot you can do with them if you bother.
22:32:52 <AnMaster> possibly optimising common idioms with them and such
22:33:07 <pikhq> Brainfuck really has a lot of optimisations you can do.
22:33:25 <AnMaster> pikhq, consider turning [>] into something like strlen() plus moving the pointer
22:33:49 <pikhq> Not quite the same, but I'm still kinda proud of PEBBLE's C output.
22:34:08 <pikhq> (cheats by having C macro implementations. >:D)
22:34:17 <AnMaster> iirc libc strlen() tend to be crazily optimised "word at a time" thingies
22:34:31 <AnMaster> pikhq, I thought PEBBLE compiled to C?
22:34:39 <AnMaster> also: link to pebble, I forgot where it was
22:34:49 <pikhq> I no longer have a host.
22:34:55 <fizzie> AnMaster: Remember that befunge "benchmark" we played with a moment ago that basically does -100 until the cell wraps around?
22:34:58 <pikhq> PEBBLE has a C backend.
22:35:15 <fizzie> AnMaster: Well, where moment == few days.
22:35:28 <fizzie> AnMaster: I think I was going to say "while" there, but typoed "moment".
22:35:46 <pikhq> AnMaster: Yeah, the C backend produces some fairly swift code.
22:35:50 <zzo38> Do you mean like: ptr+=strlen(ptr);
22:36:05 <fizzie> AnMaster: Anyhow, the static Funge-98 compiler I have here that I got sidetracked with compiles it to the following LLVM code:
22:36:08 <fizzie> Code1.i: ; preds = %Code1.i, %0
22:36:10 <pikhq> Though it gets to do some nice stuff like "replacing a division with an actual division".
22:36:23 <AnMaster> zzo38, possibly. It depends on how you implement it I guess
22:36:32 <AnMaster> fizzie, that is, like cheating or something
22:37:04 <fizzie> It also fails to terminate.
22:37:12 <AnMaster> then I didn't read it correctly
22:37:17 <AnMaster> fizzie, I thought it constant folded the loop
22:37:20 <fizzie> It's just "foo: goto foo;"
22:37:31 <AnMaster> fizzie, oh wait I know. it thinks signed integer can't wrap around
22:37:34 <pikhq> LLVM is assuming that you won't overflow. :)
22:37:51 <AnMaster> pikhq, underflow in this case I think
22:38:24 <AnMaster> hopefully there is a way to tell it that is incorrect
22:39:35 <AnMaster> zzo38, anyway it would be a win since strlen() these days check the memory one word at a time, for "does any byte in this word contain a zero" with some bitmask stuff
22:39:57 <AnMaster> and when it found one, it checks which byte in said word was the zero
22:40:49 <AnMaster> sure it goes over the end of the array in theory, but that is safe since it is doing aligned reads, and that will never go over the end of a page
22:41:47 <AnMaster> and that is one of the reasons why valgrind prints "ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 7 from 7)".
22:42:06 <AnMaster> it suppresses stuff in libc and such, like strlen() doing that
22:42:21 <AnMaster> unless it provides it's own strlen()
22:42:22 <fizzie> AnMaster: I'm not quite sure how to tell it to not assume that. But if I use just "-std-compile-opts" and not "-std-link-opts" too for 'opt', it compiles to what's basically in C "for (i = 0; x-i*100 < 0; i++);" where x comes from the stack.
22:43:04 <AnMaster> fizzie, surely llvm can't assume signed overflow/underflow is undefined. After all llvm is supposed to work for other languages than C
22:43:09 <fizzie> Probably because it doesn't inline the generated code into main where the stack is initialized, and therefore can't know x = 0 at start.
22:43:52 <AnMaster> fizzie, http://llvm.org/docs/LangRef.html#i_add
22:44:06 <AnMaster> "nuw and nsw stand for "No Unsigned Wrap" and "No Signed Wrap", respectively. If the nuw and/or nsw keywords are present, the result value of the add is a trap value if unsigned and/or signed overflow, respectively, occurs."
22:44:47 <fizzie> I'm not sure. I don't use either of those words, so I think it should do the two's-complement modulo arithmetic by default.
22:45:58 <fizzie> I might not just be using it right. I'll try to make a minimal testcase of that loop.
22:46:26 <AnMaster> fizzie, you might want to find out what exact optimisation pass breaks it
22:46:47 <AnMaster> iirc there is some way to list what -std-compile-opts and such actually do
22:52:01 <fizzie> Yes, adding -debug-pass=Arguments prints them out.
22:52:19 <fizzie> It is not a short list.
22:55:08 <AnMaster> fizzie, that should give you some hint of what ones might be more probable causes
22:55:23 <AnMaster> (of course, if you are unlucky, it is causing by two or more passes interacting)
22:55:44 <AnMaster> fizzie, but yes, a test case and ask mailing list/submit bug might be best
22:55:47 <fizzie> The -std-link-opts seems to add: -internalize -ipsccp -globalopt -constmerge -deadargelim -instcombine -basiccg -inline -prune-eh -globalopt -globaldce -basiccg -argpromotion -instcombine -jump-threading -domtree -domfrontier -scalarrepl -basiccg -functionattrs -globalsmodref-aa -domtree -loops -loopsimplify -domfrontier -loopsimplify -licm -memdep -gvn -memdep -memcpyopt -dse -instcombine -jump-threading -simplifycfg -globaldce -preverify -domtree -verify
22:56:03 <fizzie> I guess I could just start removing passes one by one.
22:57:00 <AnMaster> fizzie, -preverify/-verify should not be removed
22:57:15 <AnMaster> on the current ast or whatever
22:57:39 <AnMaster> fizzie, I'm pretty sure also that some of those are run more than once
22:57:58 <AnMaster> you have memdep several times there
22:58:20 <fizzie> Sure, there's a lot of duplication; that's not so surprising.
22:58:37 <AnMaster> well, remove -preverify/-verify if you remove all the passes between them
22:58:53 <fizzie> Removing "-jump-threading -simplifycfg -globaldce" from near the end turns the loop into:
22:58:54 <fizzie> Code1.i: ; preds = %Code1.i, %space_init.exit
22:58:54 <fizzie> br i1 false, label %funcot.exit, label %Code1.i
22:59:06 <AnMaster> that doesn't look quite right?
22:59:14 <AnMaster> fizzie, iirc llvm has some tool to automatically find these
22:59:31 <fizzie> Well, it's "foo: if (0) return; else goto foo;" now.
22:59:42 <AnMaster> fizzie, that is still incorrect though
23:00:10 <AnMaster> fizzie, anyway http://llvm.org/docs/Bugpoint.html might help
23:01:21 <fizzie> Yes, the miscompilation debugger sounds sensible, though I'm a bit uncertain how well it works with a non-terminating program, since it's based on comparing outputs.
23:02:04 <fizzie> I'll see if I can manage a testcase myself. I still think it could be just my own misuse of llvm somewhere; that's usually the case.
23:03:29 <fizzie> Removing that -instcombine just before the three others I removed makes for a sensible-looking loop.
23:05:45 <fizzie> Hrm, well, the optimization is in fact legal, given what is before the loop.
23:06:04 <fizzie> It starts the loop with: %tmp1.i = add i32 undef, -100
23:06:30 <fizzie> Right. It's legal to do a lot of stuff to computations involving undef values.
23:06:42 <AnMaster> fizzie, sounds like it shouldn't be undef then?
23:07:07 -!- augur has quit (Remote host closed the connection).
23:07:08 <fizzie> Right. Or, well, wait.
23:07:28 -!- augur has joined.
23:08:02 <fizzie> Actually! While the runtime has a proper stack-pop macro, I think the codegen still has the version that does not check for stack underflow, and the benchmark indeed starts from the value that's below the start of the stack, which is undef.
23:12:38 <AnMaster> fizzie, you mean you stopped doing the sigsegv trick?
23:13:29 <fizzie> This is not jitfunge, this is another thing. And in any case jitfunge's current LLVM backend doesn't do it either. I haven't yet quite figured out how to, since you can't really predict what sort of assembly LLVM decides to spew out for accessing the stack.
23:13:46 <fizzie> I'm sure it's doable, it might just need some more twiddling with the LLVM side.
23:14:07 <pikhq> Some sort of static compiler.
23:14:11 <fizzie> I got sidetracked with a static compiler, yes.
23:14:19 <AnMaster> fizzie, static compiler for befunge?!
23:14:33 <pikhq> No support for "p" modifying actual code I presume?
23:14:36 <fizzie> Well, the subset of it I use personally in fungot. :p
23:14:36 <fungot> fizzie: to the person executing the program makes sense ( a script, so i have a favorite sushi, but that seems much saner to me.
23:14:57 <fizzie> Yes, a boring non-self-modifying sort of befunge.
23:15:01 <pikhq> Might be fun to define a compilable subset of Befunge.
23:15:03 <AnMaster> fizzie, so fungot never uses p to self modify?
23:15:03 <fungot> AnMaster: here is one that surrounds me", etc
23:15:23 <fizzie> AnMaster: Well, there's the ^reload command, but I don't remember when I've used it last.
23:15:25 <pikhq> Bit of a boring language to implement, but could be handy for some programs that could be done quickly.
23:15:35 <AnMaster> fizzie, the loader loads the main file
23:15:37 <pikhq> Could do with running
23:15:49 <fizzie> And yes, the loader/program split is there, but that's just a matter of concatenating the two files.
23:16:07 <AnMaster> pikhq, I prefer the "no 93" subset of 98 then
23:16:34 <AnMaster> there was a bit of an argument if there should be a hole in the 98-funge space where the 93 funge space was
23:16:36 <ais523> AnMaster: you have to use abcdef just to push constants? and x and [] to change direction?
23:16:43 <AnMaster> but I think the conclusion was "only commands are removed"
23:16:46 <pikhq> AnMaster: Hahahah.
23:16:52 <AnMaster> otherwise we would end up with stack stack but no stack
23:16:53 <fizzie> The underload interp seems to work with this compiler; haven't tested full fungot yet, there's a lack of fingerprints and such.
23:16:54 <fungot> fizzie: sarahbot eval ( map display ' ( 2 1 0
23:17:11 <AnMaster> ais523, well yes and you have no - and + for example
23:17:38 <AnMaster> I did think we figured out a way to get constants with y
23:18:00 <AnMaster> and then comparing stuff, you have w but not ` _ or |
23:18:53 <AnMaster> ais523, I think we concluded that befunge-98s is *probably* TC but unefunge-98s probably isn't
23:19:24 <AnMaster> ais523, you can grep the logs for this. I think me Deewiant and ehird were involved in the discussion
23:19:39 <AnMaster> last half of 2009 or during 2010
23:20:23 <AnMaster> ais523, to what? that he is gone?
23:21:22 -!- tombom has quit (Quit: Leaving).
23:22:02 <alise_> he'll be busy with work.
23:22:38 * AnMaster fixes the ignore to include the underscore version as well
23:24:12 <alise_> you know, calling me childish will stop working soon enough as you'll have definitively proved yourself to be even more childish than me.
23:24:23 -!- sebbu2 has joined.
23:24:38 <alise_> "don't fucking mention your ignores every time you can" is, like, rule #3 of not being a huge, annoying asshole on IRC
23:24:59 <alise_> "don't read logs to talk to someone you're ignoring while simultaneously reacting harshly when they evade your ignore to talk to you" is rule #4.
23:25:37 -!- sebbu has quit (Ping timeout: 240 seconds).
23:25:38 -!- sebbu2 has changed nick to sebbu.
23:31:23 -!- Oranjer has quit (Quit: Leaving.).
23:33:53 <ais523> Mathnerd314: you can do, say, "/ignore ais523"; then you wouldn't be able to see anything I said
23:34:14 <ais523> normally used against people who annoy you, or who are spamming a channel
23:34:51 <AnMaster> ais523, actually I need to tell it what type of ignore to apply. Just /ignore <nick> gives me syntax help
23:35:07 <ais523> depends on client, then
23:35:19 <AnMaster> I need to tell it something like "chan" or "priv" or "all" (there are a few more variants)
23:35:19 <pikhq> 17:24 < alise_> "don't fucking mention your ignores every time you can" is, like, rule #3 of not being a huge, annoying asshole on IRC
23:35:58 <AnMaster> ais523, there is also a "unignore" flag, to override other ignores for a more specific mask
23:36:02 <pikhq> BY THE WAY HAVE I MENTIONED THAT I HAVE AN IGNORE LIST
23:36:19 <AnMaster> ais523, like I ignore DCC from *!*@*, and then allow it from egobot
23:36:35 <alise_> HAVE I MENTIONED, I DISLIKE ALISE TO THE POINT THAT I WISH TO NOT SEE HIS MESSAGES TO THIS CHANNEL; ALTHOUGH I SHALL COMPLAIN ABOUT THE ADVERSE EFFECTS OF THIS, SUCH AS WHEN I ONLY SEE ONE HALF OF A CONVERSATION
23:36:57 <pikhq> Doomy doomy doom doom
23:37:21 <pikhq> That's the location.
23:39:48 <Mathnerd314> hmmm... what would /ignore Mathnerd314 do?
23:40:16 -!- oerjan has joined.
23:40:19 <AnMaster> Mathnerd314, depending on client, either filter out all the lines you said or give syntax help
23:40:44 <AnMaster> btw, http://llvm.org/pubs/ is quite an interesting list
23:41:15 <AnMaster> there are some truly fascinating things there
23:41:26 <Mathnerd314> AnMaster: how many channels are you on on freenode?
23:41:45 <Mathnerd314> just want to see if I've found them all :p
23:41:47 <oerjan> _all_ of them, obviously
23:42:11 <AnMaster> Mathnerd314, I doubt you found all
23:42:47 <oerjan> #catlicking is hard to find, after all
23:42:52 <AnMaster> Mathnerd314, how many did you find? /whois on you show three channels. If you like me have that "hide channel list" mode set then that is the subset we are both in
23:43:08 <AnMaster> oerjan, I wonder if you is there ;P
23:43:15 -!- alise_ has quit (Read error: Connection reset by peer).
23:43:30 <oerjan> alas, since it doesn't exist. at least on freenode.
23:44:02 <oerjan> or maybe it's so secret even i cannot find it
23:44:21 <AnMaster> a sure test to see if it is there is trying to join it
23:44:40 <AnMaster> another possibly less embarrassing way to check it is /mode #channelname
23:44:40 <oerjan> well that's what they want you to think
23:45:04 <AnMaster> oerjan, that won't list +s channels
23:45:14 -!- Oranjer has joined.
23:45:23 <oerjan> 00:42 #catlicking: No such nick/channel
23:45:57 <oerjan> oh? you mean the message would be fake?
23:46:17 -!- alise has joined.
23:46:22 <AnMaster> oerjan, from /mode? then it doesn't exist
23:46:42 <AnMaster> oerjan, well as I said, /list doesn't include +s channels
23:46:51 <oerjan> /mode gives a similar answer
23:46:53 <AnMaster> unless you are on those channel
23:47:03 <oerjan> it was /list #catlicking, of course
23:47:21 <AnMaster> oerjan, I think +s would be hidden from that too. At least on some IRCDs
23:47:47 <oerjan> ok, not sure if it makes sense to hide it from only _some_ commands
23:48:04 <AnMaster> oerjan, sure it does. You can't hide it from /join for example
23:48:39 <oerjan> well true, that would require a very fiendish deception
23:48:40 <AnMaster> oerjan, oh and +s also hides the channel from /whois, unless that person doing the /whois is also in that channel
23:48:52 <oerjan> not _impossible_, mind you
23:49:25 <AnMaster> oerjan, basically it hides it from everywhere where you wouldn't have to know about the channel already
23:49:26 <oerjan> well that's pretty obvious it has to hide that
23:49:47 <AnMaster> oerjan, and I guess special casing the "full match" variant of /list was too much work
23:49:56 <oerjan> AnMaster: yeah, but that still leaves /list with exact name as a dubious case
23:53:54 <zzo38> This channel is mode +cn
23:54:54 <AnMaster> oerjan, no message to channel without being in it
23:55:27 <AnMaster> I mean, it is the only sane variant
23:55:28 <zzo38> Enter HELP CMODE for help
23:55:35 <oerjan> presumably so you can turn it off
23:55:44 <AnMaster> zzo38, you mean /quote help cmode probably
23:56:04 <AnMaster> most clients have their own /help
23:56:08 <zzo38> This client doesn't do it that way
23:56:34 <AnMaster> oerjan, yes but I can't see why anyone would want to turn it off
23:56:50 <oerjan> zzo38: like when you said (iirc) that we had changed the 332 TOPIC - almost no one else would see the 332
23:56:52 <zzo38> This client has no /HELP or /QUOTE command, it just generates an error message "UNKNOWN SLASH COMMAND"
23:57:12 <zzo38> oerjan: Why not? Does someone turn it off?
23:57:16 <AnMaster> zzo38, so you need to type /msg or such for every line you write to irc?
23:57:34 <oerjan> zzo38: the client formats topics in their own way
23:57:35 <AnMaster> zzo38, are you intentionally being silly?
23:57:37 <zzo38> No, I just prefix it with the spacebar and it automatically types PRIVMSG and the current channel name and a colon
23:57:58 <zzo38> That's what happens in my client when I start a line with space, it will type in that command instead of a space.
23:58:13 <AnMaster> zzo38, isn't almost every line you type one starting with space?
23:58:29 <zzo38> About half of them are
23:58:42 <alise> zzo38: you are awesome
23:58:43 <oerjan> zzo38: like in irssi when i joined the channel, it said: 00:39 Topic for #esoteric: #esoteric, the international hub for esoteric programming language design and deployment - #esoteric is not associated with the joke language Perl, please visit www.perl.org - logs: http://tunes.org/~nef/logs/esoteric/?C=M;O=D
23:58:47 <AnMaster> zzo38, really? You do so many other things except chatting on irc?
23:59:04 -!- Azstal has joined.
23:59:12 <oerjan> irssi prepends the time to most things
23:59:26 <AnMaster> zzo38, wouldn't it make more sense to make message to the current channel the default?
23:59:37 <alise> Mathnerd314: his own
23:59:39 <zzo38> This client will also prepend the time to *all* things, but only if you type in /SET SHOWTIME +
23:59:43 <alise> rule of thumb; if zzo38 is using some software, he wrot it