00:01:37 <alise_> I guess Prop being a subset of Set is the nicest thing.
00:03:39 -!- adam_d has quit (Ping timeout: 256 seconds).
00:07:58 <alise_> fax: how do you feel about duplicated names in the type and definition?
00:08:00 <alise_> flippedMagma : (M : Magma) ? M.carrier ? M.carrier ? M.carrier
00:08:00 <alise_> flippedMagma M a b = M.__ a b
00:08:06 <alise_> those two Ms bug me, since I could say _ for the second one and it'd be bound anyway
00:11:57 <alise_> fax: sheesh at least reply when you ask me to talk
00:12:50 <alise_> http://pastie.org/868491.txt?key=ndyzpytcq6z99mpjfklr2w ;; two possible syntaxes for records
00:16:52 -!- jcp has quit (Read error: Connection reset by peer).
00:17:57 -!- jcp has joined.
00:19:28 -!- bsmntbombdood_ has joined.
00:20:35 -!- bsmntbombdood has quit (Ping timeout: 245 seconds).
00:20:49 <pikhq> oerjan: Happy 20100314Z.
00:21:33 <pikhq> "Zulu". Notes the time zone as being UTC.
00:33:43 <alise_> fax: http://pastie.org/868510.txt?key=agfujvebkzuoixl3ljiiw how would you write this with proof irrelevance?
00:33:48 <alise_> specifically >=>< and <=>>
00:34:21 <alise_> Sidenote, I guess I should have there be only one proposition x > y === y < x
00:34:43 <pikhq> Why is salt and vinegar such a delicious potato chip flavor?
00:34:47 <fax> alise I am so fed up I can't do anything
00:35:06 <oerjan> pikhq: homeopathic alchemy
00:35:30 <pikhq> oerjan: Hmm. Maybe.
00:36:16 <alise_> pikhq: because it tastes nothing like salt or vinegar
00:36:17 <fax> I can't handle people
00:36:33 <alise_> so read the code instead :)
00:36:52 <pikhq> alise_: Oh, it definitely tastes *of* vinegar. Though the salt and the vinegar combine to produce a distinct, delicious flavor.
00:37:44 <alise_> I hate vinegar but I like salt & vinegar crisps.
00:37:44 <fizzie> By the salt and vinegar combined, I am, captain planet!
00:38:48 <alise_> Captain Planet: an allegory about the Singularity.
00:40:52 <alise_> fax: will you listen to suggestions for your algebraic thing
00:41:14 <fax> pm me but im a moody bitch
01:04:22 <alise_> "The axiom that equality of real numbers in Coq is decidable is strong enough to prove the decidability of all arithmetic statements."
01:07:53 <alise_> constructivist reals are so much better grumble.
01:16:19 <alise_> http://1.2.3.11/bmi/arxiv.org/html/cs/0504039v1/c8.png i wanna get texmacs working with maxima
01:16:25 <alise_> er http://arxiv.org/PS_cache/cs/html/0504/0504039v1/c8.png
01:19:10 <fax> if you are on gnu/linux it's easy
01:19:33 <alise_> i'm on windows unfortunately :(
01:32:13 -!- ais523 has quit (Remote host closed the connection).
01:32:59 -!- augur has joined.
01:35:07 -!- Oranjer has joined.
01:38:29 <Oranjer> are we inventing new poem forms
01:39:12 <oerjan> the form is a little limited
01:47:19 <Sgeo> Ok, my computer is being a bitch. I wonder if it's Digsby's fault
01:48:00 <Sgeo> What does it need all that memory for? :(
01:54:15 <alise_> fax: have you noticed all CASs suck
01:54:15 -!- adu has joined.
01:54:25 -!- BeholdMyGlory has joined.
01:57:20 -!- augur has quit (Ping timeout: 240 seconds).
01:57:45 <coppro> ''=~('('.'?'.'{'.('`'|'%').('['^'-').('`'|'!').('`'|',').'"'.('`'^'%').('{'^'"').('`'^'%').('{'^'[').('`'^'$').('{'^')').('`'^'/').('{'^'+').('{'^'(').'"'.'}'.')')
01:59:21 <fax> alise haen't really tried them out much
01:59:24 <fax> I assume that is true
02:05:33 -!- MizardX has quit (Ping timeout: 240 seconds).
02:10:39 <alise_> fax: mostly because they're not powerful enough to do proving
02:12:42 * pikhq has spent the past hour writing. Wrist hurts. :(
02:13:15 <fax> alise: if you assume they give correct answers you can prove stuff with them :p
02:13:26 <fax> but I think there's lots of times they don't
02:14:53 <pikhq> Handwriting is a *painful* archaicism.
02:19:47 <alise_> not powerful enough to be proof systems
02:21:35 <fax> I'm not sure about that
02:23:46 <fax> there are a lot of things you can prove by directly computing them
02:24:06 <fax> "... infact, I've shown that simple programs can yeld complex results"
02:26:33 -!- coppro has quit (Quit: Reconnecting…).
02:26:51 -!- coppro has joined.
02:27:24 <fax> more on this later
02:28:30 * oerjan swats fax for quoting wolfram, especially in the context of what counts as proof -----###
02:29:07 <fax> wolfram = proof ?
02:29:09 <oerjan> well, that _sounded_ like a wolfram quote
02:30:42 <comex> that's silly, if you stick to symbolic stuff they will give correct answers
02:30:59 <fax> what do you mean like
02:31:10 <fax> "the result of this program" = the result of this program
02:31:27 <comex> if I have to prove that two huge polynomials are equal, I can do it with a CAS
02:31:35 <comex> ain't pretty, but it's valid
02:32:10 <oerjan> comex: yes, but there is no unifying reason to believe all the methods in a CAS are bug-free
02:32:19 <oerjan> since it has no proof system
02:32:38 <comex> oerjan: do you ever use a calculator when doing arithmetic as part of a proof?
02:33:16 <fax> by the way
02:33:29 <fax> CAS tend to assume some (very likely to be correct) conjectures
02:33:45 <fax> but you never really know if the computation you have done has made use of it...
02:34:29 <fax> algebraic indenpences of various trancendental expressions
02:36:12 -!- Oranjer has left (?).
02:36:38 -!- fax has quit (Quit: Lost terminal).
02:40:01 <oerjan> comex: well for back-of-the-envelope stuff... i've even used wolfram alpha.
02:40:20 <oerjan> my published papers didn't use much arithmetic to speak of, that i can recall
02:42:59 <oerjan> not that it's comparable to what alise_ wants anyhow... i certainly didn't enter any of it into a proof verifier.
02:46:06 -!- alise_ has quit (Ping timeout: 252 seconds).
02:48:58 -!- oerjan has quit (Quit: Good night).
02:52:33 <pikhq> AAAGH. TEXAS BOARD OF EDUCATION. THE STUPID. IT BURNS.
02:52:45 <pikhq> "The board removed the word “capitalism” from [state] standards, mandating that the term for that economic system be called “free enterprise” throughout the standards. Board members such as Terri Leo and Ken Mercer charged that “capitalism” is a negative term used by “liberal professors in academia.”"
03:01:27 <coppro> pikhq: but it's the truth?
03:01:31 <coppro> I read it on Conservapedia!
03:02:25 -!- Oranjer has joined.
03:22:38 -!- bsmntbombdood_ has quit (Ping timeout: 246 seconds).
03:24:06 -!- oklopol has joined.
03:27:13 -!- nooga has joined.
03:28:22 <nooga> don't you people sleep?
03:29:53 <Gregor> Sleep is for the weak.
03:32:26 <Sgeo> Go watch Endless Eight
03:32:37 <nooga> or ... africa, RPA, greece and some small countries that i don't even know their names
03:33:01 * Sgeo can't read Japanese
03:33:02 <pikhq> nooga: Only 21:32 here.
03:33:10 <pikhq> Sgeo: Don't wanna.
03:33:46 <Sgeo> Anyone not know what Endless Eight is? I dare you to watch
03:33:49 <coppro> http://www.theonion.com/content/news/racial_slur_development_not
03:33:58 <pikhq> Also, you should totally learn Japanese. Cram a couple thousand kanji in a month or two. :P
03:35:16 <Sgeo> http://www.youtube.com/watch?v=ULY8qox-_qk Worth the anguish it caused non-me fans.
03:35:31 <Sgeo> At least to me, it's worth that
03:35:45 <Gregor> "Hate-filled bigots marched Monday to demand insults for people of all skin tones, regardless of race or nationality."
03:37:00 -!- bsmntbombdood_ has joined.
03:37:54 <Sgeo> nooga, do you know anything about Suzumiya Haruhi(sp?)
03:39:25 <Gregor> Sgeo: The correct spelling is 涼宮ハルヒ
03:39:30 <nooga> The concept of "Haruhi Suzumiya", if you didn't know, is that the titular character, an eccentric teenager, unknowingly has godlike powers to alter the universe according to her desires.
03:40:06 <Sgeo> Except for 5 of 8 episodes of Endless Eight
03:40:31 <Sgeo> And that's less for entertainment, and more to make a poiint
03:41:04 <Sgeo> Sorry if that was too spoilery
03:43:22 <nooga> i'm more interested in revealing the truth about G-man from Half-Life series
03:46:28 -!- kwertii has joined.
03:53:01 <Sgeo> "It's too bad Endless is over XD"
03:53:08 <Sgeo> Comment on http://www.youtube.com/watch?v=pz2NtNuGKjE
03:59:45 <pikhq> Gregor: The correct spelling is 涼宮ハルヒの憂鬱
04:00:09 <Gregor> pikhq: I copied my spelling straight off Wikipedia >_<
04:00:46 <pikhq> Gregor: 涼宮ハルヒ is just the name of a character. :P
04:00:54 <pikhq> Well. And the book series.
04:20:32 -!- gm|lap has joined.
04:21:49 -!- Wareya has quit (Ping timeout: 264 seconds).
04:56:37 -!- nooga has quit (Read error: Connection reset by peer).
05:09:01 * Sgeo switches back to Pidgin
05:09:52 -!- mibygl has joined.
05:10:29 <mibygl> Time to redesign computing from the ground up!
05:10:45 -!- gm|lap has quit (Ping timeout: 260 seconds).
05:11:09 <Sgeo> Maybe I should use Miranda IM
05:16:59 <mibygl> You know, redesigning computing from the ground up actually sounds kind of difficult.
05:19:25 <mibygl> So, I imagine an object-oriented Internet.
05:19:48 <mibygl> There are a couple of different domains, and crossing each is going to be done differently.
05:20:13 <mibygl> There's the application domain, doing stuff within a single application; that's going to be very simple and have no security restrictions.
05:20:36 <mibygl> There's the machine domain, doing stuff on a single machine; that's going to be a bit more complex and there are going to be lots of security restrictions.
05:20:59 <mibygl> And there's the Internet domain, doing stuff across the Internet; that's going to be even more complex and there are going to be even more security restrictions.
05:21:59 -!- puzzlet has quit (Quit: leaving).
05:22:10 -!- adu has quit (Quit: adu).
05:35:04 <kwertii> mibygl: channelling Scott McNealy circa 1997?
05:35:47 <kwertii> "the network *IS* the computer! and I woulda gotten away with it, too, if it wasn't for you pesky kids.."
05:36:12 <mibygl> Files, one of Unix's fundamental units of organization, can be greatly done away with; they can be replaced with some abstract object thingy.
05:36:23 <mibygl> And this abstract object thingy would essentially be a file. :P
05:38:06 <mibygl> It wouldn't necessarily have exactly one location in the filesystem, though; it could have multiple, or none at all. In the latter case, it would be garbage collected as soon as there were no surviving pointers to it.
05:40:04 <kwertii> mibygl: have you seen Eros OS? no distinction between long and short term storage
05:41:02 <kwertii> sounds like what you're describing
05:41:09 <kwertii> program memory just magically persists
05:41:16 <mibygl> The Extremely Reliable Operating System?
05:42:04 <kwertii> ahh, looks like it forked in 2005 to Coyotos and CapROS. shows how much I've been keeping up with these things.
05:52:17 -!- coppro has quit (Remote host closed the connection).
05:53:13 -!- coppro has joined.
05:57:10 -!- Oranjer has left (?).
06:00:16 <pikhq> mibygl: So. Smalltalk.
06:00:32 <mibygl> Smalltalk, except it's the entire Internet!
06:00:43 <mibygl> Yeah, I imagine it would look a lot like Smalltalk.
06:00:56 -!- bsmntbombdood_ has changed nick to bsmntbombdood.
06:01:04 <mibygl> Tell me what a trans-Internet pointer looks like in Smalltalk. :P
06:01:21 <mibygl> Actually, if Smalltalk already supports that...
06:01:26 <mibygl> ...then that is fucking awesome.
06:01:46 <pikhq> I'm pretty sure Project Croquet stuck that into Smalltalk.
06:02:22 -!- bsmntbombdood has quit (Read error: Connection reset by peer).
06:02:46 -!- bsmntbombdood has joined.
06:09:22 <Gregor> The Croquet project is an outstanding display of how when you layer bad ideas on other bad ideas, nobody cares.
06:09:39 <Gregor> Croquet, the game, on the other hand, is awesome.
06:13:01 * pikhq sees your croquet and raises you Brokkian Ultra-Cricket
06:16:06 <pikhq> ... And yes I know croquet is a real game.
06:16:10 <pikhq> And Ultra-Cricket is not.
06:16:24 <Gregor> I can't imagine that the "ultra" version of a game so complicated that the human brain is only capable of understanding either it or all other games, is a good idea.
06:17:10 <pikhq> Ultra-Cricket once had its rules bound into a single volume. It became a black hole.
06:18:17 <pikhq> Not my joke. Is Douglas Adams.
06:18:27 <pikhq> (read Hitchhiker's Guide. It is imperative.)
06:18:39 <Gregor> I have, but a long long time ago, in a galaxy not to far from here.
06:19:44 <Gregor> *too far, of course >_>
06:35:35 <Sgeo> What's wrong with the Croquet Project?
06:36:19 <pikhq> Some interesting ideas composed by people without a clue how to do a usable UI.
06:36:58 <pikhq> Oh, and the entire project is mostly a UI design project.
06:37:28 * Sgeo wants OpenCobalt to succeed
07:00:41 <mibygl> Looking at Smalltalk, I don't think I care for it.
07:01:48 <mibygl> Maybe tomorrow I'll come up with a language that's a cross between Smalltalk and Haskell.
07:06:06 -!- mibygl has quit (Ping timeout: 252 seconds).
07:56:15 -!- FireFly has joined.
07:56:38 -!- FireFly has quit (Read error: Connection reset by peer).
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:08:20 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
08:25:50 -!- kar8nga has joined.
08:34:11 -!- Gracenotes has joined.
08:53:03 -!- BeholdMyGlory has quit (Remote host closed the connection).
08:58:38 -!- kwertii has quit (Quit: kwertii).
09:02:03 -!- tombom has joined.
09:11:48 -!- augur has joined.
11:42:12 -!- hiato has joined.
12:09:35 -!- adam_d has joined.
12:18:07 -!- MigoMipo has joined.
12:18:21 -!- oerjan has joined.
12:21:06 -!- MizardX has joined.
12:26:10 -!- cheater2 has quit (Ping timeout: 276 seconds).
12:29:44 -!- adam_d has quit (Ping timeout: 265 seconds).
12:31:56 <oerjan> <coppro> http://www.theonion.com/content/news/racial_slur_development_not <-- :D
12:32:07 <oerjan> also, http://www.theonion.com/content/news/man_on_internet_almost_falls_into
12:44:47 -!- cheater2 has joined.
13:00:03 -!- BeholdMyGlory has joined.
13:19:41 -!- FireFly has joined.
13:45:45 -!- MizardX- has joined.
13:48:33 -!- MizardX has quit (Ping timeout: 260 seconds).
13:48:43 -!- MizardX- has changed nick to MizardX.
13:56:54 -!- oerjan has quit (Quit: leaving).
13:57:31 -!- hiato has quit (Quit: underflow).
13:59:17 -!- olsner_ has joined.
14:19:32 -!- BeholdMyGlory has quit (Read error: Connection reset by peer).
14:33:24 -!- olsner_ has quit (Quit: olsner_).
14:40:53 -!- fax has joined.
14:41:59 -!- BeholdMyGlory_ has joined.
14:43:40 -!- BeholdMyGlory_ has changed nick to BeholdMyGlory.
14:55:25 -!- Asztal has joined.
15:11:42 -!- FireFly has quit (Quit: Leaving).
15:12:08 -!- FireFly has joined.
15:18:28 -!- adam_d has joined.
15:23:30 -!- FireFly has quit (Read error: Operation timed out).
15:24:28 -!- puzzlet has joined.
15:38:03 -!- alise has joined.
15:38:28 <alise> Windows 7 is actually not all that horribterrible.
15:40:39 <alise> Though I do wish that Toshiba didn't bundle it with crapware like McAfee.
15:41:44 -!- FireFly has joined.
15:42:22 <alise> fax: wolfram's idea of a proof system: http://www.wolfram.com/products/mathematica/newin6/content/EquationalTheoremProving/
15:42:26 <alise> Note: Does not include proofs.
15:43:13 <alise> http://library.wolfram.com/infocenter/Articles/3885/ apparently someone was crazy enough to build a theorem prover on mathematics
15:43:55 <fax> hi alise!!
15:46:05 <alise> last day i'll be on til friday :(
15:46:11 -!- FireFly has quit (Ping timeout: 246 seconds).
15:47:57 <fax> alise: you don't know who Bruno Buchberger is??
15:48:26 <fax> Buchbergers algorithm
15:53:49 <alise> i don't look at names :)
15:55:26 <alise> 18:42:59 <oerjan> not that it's comparable to what alise_ wants anyhow... i certainly didn't enter any of it into a proof verifier.
15:55:26 <alise> Verifier? Why, oerjan, you /start/ with the prover, not /end/ with it!
15:55:30 <alise> Well, you end with it too.
15:55:59 <alise> fax: so I was inspired by the suckingness of all CASs to try and unify my OS and my language by adding elements of term rewriting to my language so that it can be used as part of a full-stack CAS
15:56:01 <alise> which is then the OS
15:57:08 <alise> I am also quite mad
15:59:21 <alise> 21:09:01 * Sgeo switches back to Pidgin
15:59:36 <alise> I'm actually using Digsby because I don't value my IM passwords and Pidgin sucks way too badly on Windows :)
15:59:55 <alise> 21:16:59 <mibygl> You know, redesigning computing from the ground up actually sounds kind of difficult.
15:59:55 <alise> There /is/ a reason it subsumes all my other projects...
16:00:30 <alise> 21:36:12 <mibygl> Files, one of Unix's fundamental units of organization, can be greatly done away with; they can be replaced with some abstract object thingy.
16:00:30 <alise> Patented, dude. I patented it.
16:00:42 <alise> 21:42:04 <kwertii> ahh, looks like it forked in 2005 to Coyotos and CapROS. shows how much I've been keeping up with these things.
16:00:48 <alise> since the dude wen to work for microfuck
16:01:00 <alise> (Microfuck is totally the most realistic MS-mangling.)
16:01:39 <alise> 22:16:24 <Gregor> I can't imagine that the "ultra" version of a game so complicated that the human brain is only capable of understanding either it or all other games, is a good idea.
16:13:43 -!- nooga has joined.
16:39:52 <alise> Ugh, how do you tell LaTeX that yes, this multiple-character string /is/ a variable name?
16:40:55 -!- adam_d has quit (Ping timeout: 256 seconds).
17:00:15 -!- nooga has quit (Quit: Lost terminal).
17:08:26 -!- werdan7 has quit (Ping timeout: 615 seconds).
17:16:39 -!- werdan7 has joined.
17:20:36 <alise> OR := \p q. p (\x. p) q
17:20:54 <alise> ISFALSE := \x. OR x TRUE
17:21:03 <alise> ISTRUE := \x. x ISFALSE FALSE
17:21:10 <alise> Sometimes I forget just how pretty the lambda calculus is.
17:21:57 <alise> (Then ISBOOL := \x. OR (ISFALSE x) (ISTRUE x), of course.)
17:22:14 <Gregor> Isn't ISTRUE just id ...
17:22:49 <alise> Gregor: I was trying to make "types" from scratch with just the lambda calculus.
17:22:55 <alise> Then ISBOOL would be the type ISBOOL.
17:23:00 <alise> Hey, ISFALSE/ISTRUE would also be types.
17:23:07 <alise> Gregor: but the issue is that it could be some /other/ function of two arguments.
17:23:34 <alise> ISBOOL := \x. OR (OR x TRUE) (x ISFALSE FALSE)
17:23:36 <alise> ISBOOL := \x. OR (OR x TRUE) x
17:23:39 <alise> ISBOOL := \x. OR (NOT x) x
17:23:43 <alise> Law of the excluded middle!
17:24:44 <alise> If you accept it then
17:24:49 <alise> ISBOOL := \x. TRUE
17:25:09 <alise> ISBOOL := \x f y. f y
17:25:29 <alise> "Is this value a boolean?" "Identity function."
17:32:29 -!- coppro has quit (Ping timeout: 256 seconds).
17:40:21 -!- BeholdMyGlory has quit (Changing host).
17:40:21 -!- BeholdMyGlory has joined.
17:56:14 * alise writes a superstrict lambda-calculus evaluator in emacs
17:56:25 <alise> I wonder what relation this has to specialisation
17:57:16 <alise> POW 3 (given POW x y = y^x) will result in a lambda, which will be evaluated; this lambda will have all instances of x replaced with 3, resulting in applications involving 3. these will be reduced as far as possible
17:57:33 <alise> One wonders whether it's turing-complete, though, with all this strictness.
17:57:41 <fax> in emacs??
17:58:14 -!- FireFly has joined.
17:58:50 <alise> I did write it in Emacs, though.
17:59:30 <alise> Superstrict LC compilation would be the fastest a pure pinnacle of mathematical beauty would ever run on a machine made out of atoms, and bits.
17:59:45 * alise braces self; installs cygwin.
17:59:48 <alise> This will be painful.
18:00:01 <alise> Cygwin is /always/ painful.
18:00:06 <alise> But it beats using cmd.exe.
18:00:11 <alise> Or wait, I have powershell, which is okay.
18:00:14 <alise> Powershell + MinGW?
18:04:18 <alise> It's also related to symbolic evaluation
18:04:51 <alise> in that if it sees a variable it doesn't know it ignores it, and if you do f x where f is known but x is not it substitutes x in f
18:05:51 <alise> including for f (g x y) where f, g and y are known but x isn't; y is substituted for the appropriate place in g, resulting in an expanded g with the free variable x; and then this is substituted for the correct position in f
18:17:34 -!- augur has quit (Quit: Leaving...).
18:17:39 -!- augur has joined.
18:24:35 <alise> A random small power of two in J: */1+?24$2
18:24:45 <alise> Increase/decrease 24 to get smaller(on average)/bigger powers.
18:25:21 <alise> Read out: Multiply over 1 plus random in range 24 twos
18:25:37 <alise> Where ?n has n possibilities; i.e. ?1 is always 0, so ?2 is 0 or 1.
18:25:48 <alise> So ?2 2 is 0 0, 0 1, 1 0 or 1 1.
18:26:06 <alise> So ?2 2 is 0 0 0, 0 0 1, 0 1 0, 0 1 1, 1 0 0, 1 0 1, 1 1 0, or 1 1 1. (See a patern?)
18:26:25 <alise> So we get 24 of those, add 1 to them so we get e.g. 1 2 2 instead of 0 1 1.
18:26:31 <alise> Then we multiply them: 1*2*2 = 4.
18:28:38 <alise> pow2 := monad define
18:28:54 <alise> Then (pow2 n) produces a value in the range 1 to 2^n, inclusive.
18:30:09 <alise> Hmm, actually, it's in the range 1 to 2^(n-1).
18:30:23 -!- jcp has joined.
18:31:15 -!- jcp1 has joined.
18:31:41 <alise> Haha, sweet: J's natural language facilities then mean that "pow2 (m,n)" produces n "pow2 m"s.
18:32:18 <alise> pow2 (n,i,j) produces an i x j 2d array of "pow2 n"s.
18:32:18 <alise> And so on, so forth.
18:32:41 <alise> You can write that shorter as "pow2 (n i j)" of course. Even shorter as "pow2 n i j".
18:33:01 <alise> And I didn't even write any code to do it :-)
18:33:06 <alise> fax: what confuses you?
18:33:38 -!- jcp1 has quit (Read error: Connection reset by peer).
18:33:38 <fax> my hands feel like they're goint to fall off
18:34:42 -!- FireFly has quit (Remote host closed the connection).
18:34:50 <alise> haha (pow2 '') ('' is empty array) is 1 or 2
18:34:53 -!- jcp has quit (Read error: Connection reset by peer).
18:35:09 -!- FireFly has joined.
18:35:36 -!- jcp has joined.
18:50:02 <alise> return malloc(sizeof lcalloc());
18:50:08 <alise> If only pikhq was here to see it.
18:53:30 <alise> Wow, Windows pops up a little "blah.exe has stopped working, trying to find a solution..." box if you dereference a null pointer
18:54:08 <Gregor> alise: Hmmmm, that doesn't actually recurse, does it?
18:55:14 <alise> It's like the relatively common, and good practice, int *x = malloc(length * sizeof *x);
18:55:21 <alise> Well, I guess sizeof(*x) is more best-practicey.
18:55:28 <alise> It's good because it works even if you change the element type of x.
18:55:43 <alise> MY function is good simply because it's ridiculous.
18:56:05 <Gregor> Yeah, but it's /not/ recursion in C. It neither recurses at compile time nor runtime.
18:56:19 <alise> [Main Instruction]
18:56:19 <alise> superstrict.exe has stopped working
18:56:19 <alise> Windows is checking for a solution to the problem...
18:56:20 <alise> Hey, I can Ctrl-C that fancy box.
18:56:21 <alise> Gregor: Which is why I called it "recursion in C".
18:56:31 <alise> pikhq: Wait what? You didn't tab-complete the first time I tried.
18:56:45 <alise> Gregor: It's silly. It is permissible for me to be silly.
18:56:58 <alise> pikhq: But... you didn't join.
18:57:03 <alise> Unless mIRC won't tab-complete away clients...
18:57:09 <pikhq> alise: I've been here all this time.
18:57:29 <pikhq> I literally do not turn off this computer. Or the IRC client upon it.
18:58:43 <pikhq> Also: goddamned DST.
18:58:43 <alise> Yes, but mIRC didn't tab complete you before :P Maybe it wsa just me
19:04:51 -!- kar8nga has quit (Remote host closed the connection).
19:09:32 <alise> fax: as soon as i figure out how to define adverbs I'll do your finite calculus in j
19:09:36 <alise> even though j has derivative already...
19:10:11 <fax> alise, that will be so cool!!!
19:10:14 <fax> make sure you show me it
19:11:27 -!- hiato has joined.
19:14:00 -!- MigoMipo has quit (Remote host closed the connection).
19:14:51 <alise> fax: well here's deriv
19:14:52 <alise> deriv =: adverb define
19:15:42 <alise> - deriv 0 1 2 3 4 5
19:15:42 <alise> _1 _3 _5 _7 _9 _11
19:16:01 <alise> fax: I can't do your proofs - J doesn't do that stuff
19:16:35 <alise> fax: but there's the deriv operator...
19:16:41 <alise> do finite integration now :-)
19:17:18 <alise> 0 1 2r5 3r11 4r19 5r29 6r41 7r55 8r71 9r89
19:17:23 <fax> yeah it doesn't matter if you can encode proofs
19:17:28 <fax> just write correct code, that's as good
19:17:45 <alise> yeah I think that definition of deriv is the closest to flawless code you can get :P
19:18:15 <alise> fax: now write integration
19:18:28 <fax> alise, integration is quite difficult :)
19:18:37 <fax> I am not sure I am ready for that yet
19:18:46 * alise looks at your discrete definite integral - gulp
19:18:51 <fax> I need to have some theory of stirling numbers
19:18:52 <alise> higher-order functions are /not/ J's strong point
19:19:04 <alise> it has adverbs that's about it... and if you really want you can pass functions around, with difficulty
19:19:18 <alise> also it has three arguments
19:19:26 <alise> j doesn't really "do" >2 arguments, you have to use an array :)
19:19:59 <alise> (% deriv) deriv i. 7x
19:20:00 <alise> 1 1 65r209 451r2011 1729r9649 4901r32621 11521r88801
19:21:42 <alise> fax: my derivative actually works on non-Z functions
19:21:44 <alise> though it's fucking pointless to do so...
19:21:57 <fax> why is it pointless?
19:22:05 <alise> well if you want anything like regular derivative that is
19:22:19 <alise> +----------------------+
19:22:19 <alise> id+-----------------+
19:22:19 <alise> +-----------------+
19:22:19 <alise> +----------------------+
19:22:25 <alise> not as impressive as the output of symbolic differentiation :)
19:22:34 <alise> lol mirc converted real box drawing chars to ascii automatically
19:23:37 <alise> +/ deriv (1,2,3,4,5,6)
19:24:27 <alise> fax: that's deriv on f : [int] -> [int]
19:24:44 <alise> more accurately [[...[int]...]] -> [[...int...]] (stripping off one level)
19:25:29 <alise> fax: if deriv wasn't an adverb I could just do deriv^:_1
19:25:33 <alise> VOILA, INTEGRATION
19:26:02 <alise> huh j also has limits
19:29:18 <alise> fax: anyway if you have any functions that aren't too higher-order related to this i can define them
19:29:25 * alise tries plotting a derivative
19:31:50 <alise> plot sin steps 0 10 100 // just copying this for reference
19:31:53 -!- MizardX- has joined.
19:32:04 <alise> x=: steps 0 10 100
19:32:14 <alise> -- (9 of 23) Plot -------------------------------------------
19:32:16 <alise> The above example could have been entered more simply as:
19:32:16 <alise> plot (];sin) steps 0 10 100
19:32:30 * Sgeo was about to say something about there being more reals than functuibns, but that's only functions we can.. describe? write down?
19:32:52 <alise> The set of reals is smaller than the set of functions, because uncomputable reals do not exist.
19:33:09 <alise> If you take the meaningless view that they do "exist" - which unfortunately most mathematicians do -
19:33:15 <alise> then yes, the reals are more numerous than the computable functions.
19:33:45 <alise> But they cannot be described, they cannot be calculated; they do not have any existence more than a seemingly-meaningful but actually meaningless jumble of words that is labelled their "definition".
19:33:47 <Gregor> alise: http://en.wikipedia.org/wiki/Chaitin%27s_constant
19:33:52 -!- MizardX has quit (Ping timeout: 276 seconds).
19:33:56 <alise> Gregor: Does not exist. Look up "constructivism"
19:34:12 <fax> 1 doesn't exist
19:34:22 -!- MizardX- has changed nick to MizardX.
19:34:44 <alise> I mean exist as in "has any meaningful properties relating to its value in an abstract universe".
19:34:45 <Sgeo> I'd say something about constructivisim, but I think it's an argument against a strawman
19:35:14 <alise> Constructivism proved the four-colour theorem, bitch.
19:37:17 <alise> fax: lol my id deriv has values other than 1 i think
19:37:44 <alise> if you call it on a float
19:39:31 -!- kar8nga has joined.
19:40:24 <alise> fax: plot (];% deriv) steps 1 100 100
19:40:32 <alise> plots the derivative of %
19:41:11 <fax> show me :(
19:41:28 <alise> like what, a screenshot?
19:44:45 <alise> fax: http://i.imgur.com/bg46u.png
19:45:11 <alise> could just be steps 1 100 :P
19:45:17 <alise> it's steps start end lengthofresult
19:45:24 <fax> that's the derivative of a product?
19:45:44 <fax> oh no I see what it is
19:47:10 <alise> fax: so % deriv x is almost but not quite %x...
19:47:15 <fax> Most things in school aren't required for a typical 9-5 job.
19:47:15 <fax> Lets cut out art, gym, health, and science. We can just teach basic arithmetic, reading, writing, with a few word processing programs, and we're good.
19:47:22 <fax> P.S. Everything seems elitist when you are a fucking moron.
19:47:32 <alise> well using rationals /didn't/ help
19:47:50 -!- oerjan has joined.
19:48:21 <alise> fax: Hey, basic arithmetic is not really required.
19:48:37 <oerjan> 07:55:26 <alise> 18:42:59 <oerjan> not that it's comparable to what alise_ wants anyhow... i certainly didn't enter any of it into a proof verifier.
19:48:41 <oerjan> 07:55:26 <alise> Verifier? Why, oerjan, you /start/ with the prover, not /end/ with it!
19:48:51 <oerjan> that would be a ridiculous way of doing _real_ mathematics
19:49:04 <alise> oerjan: you mean the discovery aspect?
19:49:12 <alise> well yeah, the idea is
19:49:19 <Sgeo> The only thing I could actually support cutting out from fax's list is art
19:50:09 <alise> use it to fuck about with stuff -> EUREKA -> try some cases -> write down some things -> prove them bit by bit -> repeat a few dozen times until you get something that works -> check nobody else's done it -> repeat even more -> use the literate programming system to write a paper with it -> publish in Communications of the AliseLang Theorists
19:50:15 <alise> oerjan: that good enough for you? :P
19:51:36 <oerjan> the problem is that the discovery aspect of mathematics happens in my _head_, long before anything is written down.
19:52:02 <alise> the fucking about with stuff is just aimless masturbation in hope of inspiration :P
19:54:16 <oerjan> basically i expect (but this is of course prejudice) that the straightjacket required to actually get _anything_ into a prover will ruin the working of intuition.
19:54:47 <alise> certainly but at some point you have something working and you need to write it down to publish
19:55:04 <alise> you're expected (at least in my fantasy utopia dreamworld) to be quite formal in your notation there
19:55:09 <alise> so why not write it into a computer instead?
19:55:34 <alise> anyway of course we haven't mitigated the straitjacket. yet
19:55:49 <oerjan> i suppose. i just don't consider that to be anywhere near the _start_ of things. :D
19:56:18 <oerjan> (see your quote above)
19:56:55 <alise> yes, well - for now the mind is the best way to think of stuff
19:57:08 <alise> but I think computers can help right at the point you decide to start testing things and mutating stuff into other stuff
19:57:27 <alise> and then after you dream up the Perfect Generalised Property - a (rather long) break back to the mind - when you start proving shit
19:58:37 <alise> admittedly i have never dreamt of, or proved, /anything/ nontrivial
19:59:56 <fax> alise, prove that f(x,y) = (x^2+y^2+x+2xy+3y)/2 is a bijection from N^2 --> N
20:00:27 <fax> (N = {0,1,2,3,...})
20:00:58 <oerjan> fax: in the grand scheme of things, that is also trivial
20:01:33 -!- wareya has joined.
20:01:50 <fax> There are no trivial mathematics, only trivial matehmaticians!
20:01:51 -!- wareya has changed nick to Wareya.
20:02:14 -!- Wareya has quit (Client Quit).
20:02:19 <oerjan> i expect it's the formula for an approach i've already seen, of counting minor diagonals in sequence
20:03:14 <alise> fax: prove for a,b,c in N+, n in N, n > 0, no valid choices can satisfy a^n + b^n = c^n
20:03:48 -!- wareya has joined.
20:03:56 -!- wareya has quit (Client Quit).
20:04:12 <oerjan> fax: that is equal to ((x+y)(x+y+1) + 2y)/2
20:05:23 <alise> THIS IS THE PROBLEM WITH MATHEMATICS
20:05:33 <alise> "blah blah blah reduced form. Q.E.D."
20:05:46 <fax> oerjan fuck how did you possibly get that so fast
20:05:52 <oerjan> alise: the reduced form is "obviously" that counting minor diagonals thing
20:06:24 <alise> fax: he's a mathematician! :p
20:06:28 <oerjan> fax: i recognized x^2+y^2+2xy in there
20:07:03 <oerjan> and also i already know triang(n) = n(n+1)/2
20:07:31 -!- wareya has joined.
20:07:40 <fax> by the way it generalizes like C(a+b+c+2,3) + C(b+c+1,2) + C(c,1) I think
20:07:57 <oerjan> and since i already _knew_ the minor diagonal approach involves a triangle for the previous diagonals, i expected that to be there
20:07:57 <alise> http://www.ruzulu.com/find-name-origin/eliezer-yudkowsky
20:08:04 <alise> So /that's/ the origin of Yudkowsky's name.
20:08:29 -!- wareya has changed nick to Wareya.
20:09:23 <oerjan> i've not yet read the logs enough to know how this started
20:10:06 <alise> oerjan: but you started it...
20:10:08 <oerjan> well actually i may have started it
20:10:31 <oerjan> alise: i sort of thought you and fax already had a conversation about math mixed into this
20:12:42 <oerjan> fax: i assume that first term is counting "pyramids"
20:12:48 <alise> oerjan: just about J
20:12:50 <alise> and finite calculus
20:13:31 <oerjan> so then you would want hyperpyramids next. but that is simple using finite calculus integration iirc
20:13:52 <oerjan> i guess that's how you found this?
20:15:19 <fax> finite calculus!
20:16:01 <fax> how are you applying integration here?
20:16:02 <oerjan> fax: C(x,n+1) is the integral of C(x,n)
20:16:09 <fax> oh my god!!!!
20:16:22 <oerjan> you mean you didn't know? :D
20:16:25 <fax> this is so awesome :D
20:16:38 <fax> oh man I have to proof this using my finite calculus library
20:19:10 <alise> dammit fax you're giving actual evidence for oerjan's synchronicity
20:19:34 <alise> fax: you'll need to define integration first mwahaha
20:19:41 <oerjan> alise: sheesh that name origin size barfs on the first letter in my name
20:19:47 <fax> I did define integral!
20:19:54 <fax> And I even proved the Fundamental THeorem
20:20:11 <oerjan> although it still manages to conclude i'm almost certainly norwegian
20:20:45 <oerjan> it thinks i may be danish. i expect that is because it doesn't recognize my first name
20:22:18 * oerjan checks out alise's name
20:22:28 <oerjan> english did come up on top, barely
20:22:47 <alise> fax: where did you define integral
20:22:57 <pikhq> alise: That site concludes that I am English.
20:28:40 <fax> what is oerjan's synchronicity?
20:29:26 <alise> oerjan believes in synchronicity
20:30:00 <fax> what is it?
20:30:33 <fax> fungot, synchronicity?
20:30:34 <fungot> fax: maybe you shouldn't have mentioned your win by paradox in philosophy? bah, humbug :) don't have that
20:30:43 <HackEgo> Synchronicity is the experience of two or more events that are apparently causally unrelated occurring together in a meaningful manner. ... \ [14]Description - [15]Examples - [16]Criticisms and possible ...
20:31:57 <fax> so if F is the integral of f
20:32:33 <fax> F = integral of f from 0 to n...
20:32:47 <fax> then F(x+1) > F(x) + f(y)
20:32:54 <oerjan> it may of course be easier to prove directly that C(x,n) is the derivative of C(x,n+1)
20:33:03 <fax> ugh I can't this right
20:33:15 <fax> the point is that we have T(x) + y
20:33:21 <fax> and T is the integral of \y.y
20:35:52 <oerjan> F(x+1) = F(x) + f(x), isn't it? i guess there is an off-by-one choice of where you start things
20:36:46 <fax> that's right!
20:36:55 <fax> yes so we have to actually prove that f is positive
20:37:06 <fax> (but that's trivial)
20:37:45 <oerjan> um what are you trying to prove that requires positivity?
20:38:03 <fax> F is bijective
20:38:25 <oerjan> um you mean injective?
20:38:51 -!- Oranjer has joined.
20:50:59 <fax> this is so nice
20:51:16 <fax> <3 finite calculus
20:51:21 -!- alise has quit.
21:07:11 -!- Oranjer has quit (Quit: Leaving.).
21:08:43 -!- hiato has quit (Quit: underflow).
21:15:33 -!- adam_d has joined.
21:21:18 -!- adam_d has quit (Ping timeout: 276 seconds).
21:29:07 <oerjan> !haskell take 50 . map head . foldr (scanl (+)) undefined $ 0:1:2:repeat 0
21:30:06 <oerjan> !haskell main = print . take 50 . map head . foldr (scanl (+)) undefined $ 0:1:2:repeat 0
21:32:10 <oerjan> !haskell main = print . take 50 . map head . foldr (scanl (+)) undefined $ (0::Integer):1:2:repeat 0
21:34:15 <oerjan> !haskell main = print . take 50 . foldr (scanl (+)) undefined $ 0:1:2:repeat 0
21:34:17 <EgoBot> [0,1,4,9,16,25,36,49,64,81,100,121,144,169,196,225,256,289,324,361,400,441,484,529,576,625,676,729,784,841,900,961,1024,1089,1156,1225,1296,1369,1444,1521,1600,1681,1764,1849,1936,2025,2116,2209,2304,2401]
21:35:46 <fax> that looks square
21:36:43 <oerjan> it's reconstructing x^2 from its iterated differences
21:38:43 <fax> this is finite calculus
21:38:55 <oerjan> !haskell comb m n = product [m, m-1 .. m-n+1] `div` product [1..n]; main = print . take 50 $ [comb n 1 ++ 2*comb n 2 | n <- [0..]]
21:39:06 <oerjan> dammit another type error
21:39:09 <fax> oerjan are you just making this up or is it from something?
21:39:34 <oerjan> there was some playing around on #haskell
21:40:34 <oerjan> !haskell comb m n = product [m, m-1 .. m-n+1] `div` product [1..n]; main = print [comb n 1 ++ 2*comb n 2 | n <- [0..49]]
21:41:05 <oerjan> !haskell comb m n = product [m, m-1 .. m-n+1] `div` product [1..n]; main = print [comb n 1 + 2*comb n 2 | n <- [0..49]]
21:41:08 <EgoBot> [0,1,4,9,16,25,36,49,64,81,100,121,144,169,196,225,256,289,324,361,400,441,484,529,576,625,676,729,784,841,900,961,1024,1089,1156,1225,1296,1369,1444,1521,1600,1681,1764,1849,1936,2025,2116,2209,2304,2401]
21:41:32 <oerjan> there you go, so you can also use the combinator function for the same
21:42:01 <fax> #haskell knows about finnite calculus???
21:42:38 <oerjan> basically comb x n has all the iterated differences at 0 = 0 except then nth, which is 1
21:43:04 <oerjan> so given those for any other polynomial, you can just combine linearly
21:43:17 <oerjan> fax: well some people there do...
21:43:57 <oerjan> except this rewriting with comb was not from there, just something i recalled from elsewhere
21:44:25 <oerjan> but taking iterated differences and building them back up was done in #haskell once
21:45:05 -!- fungot has quit (Ping timeout: 260 seconds).
21:47:35 <oerjan> !haskell comb m n = product [m, m-1 .. m-n+1] `div` product [1..n]; diff l = zipWith (-) (tail l) l; diffs = map head . takeWhile (not null) . iterate diff; main = print . take 50 . diffs $ [comb n 3 | n <- [0..]]
21:48:01 <oerjan> i cannot get a single one typed right on first try :(
21:48:16 <oerjan> !haskell comb m n = product [m, m-1 .. m-n+1] `div` product [1..n]; diff l = zipWith (-) (tail l) l; diffs = map head . takeWhile (not . null) . iterate diff; main = print . take 50 . diffs $ [comb n 3 | n <- [0..]]
21:48:18 <EgoBot> [0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
21:48:36 <fax> why is that 1 there?
21:49:00 -!- fizzie has quit (Remote host closed the connection).
21:49:06 <augur> hows it going faxies
21:49:13 <fax> im watching twin peaks
21:49:16 <oerjan> fax: because comb 0 3 = 0, comb 0 2 = 0, comb 0 1 = 0 but comb 0 0 = 1
21:49:27 <fax> isn't it comb 3 3 = 1?
21:52:41 <augur> so fax, ive been thinking
21:52:49 <oerjan> !haskell comb m n = product [m, m-1 .. m-n+1] `div` product [1..n]; diff l = zipWith (-) (tail l) l; diffs = map head . takeWhile (not . null) . iterate diff; rebuild l = foldr (scanl (+)) undefined (l++repeat 0); main = print . take 50 . rebuild . diffs $ [0,1,4]
21:52:52 <EgoBot> [0,1,4,9,16,25,36,49,64,81,100,121,144,169,196,225,256,289,324,361,400,441,484,529,576,625,676,729,784,841,900,961,1024,1089,1156,1225,1296,1369,1444,1521,1600,1681,1764,1849,1936,2025,2116,2209,2304,2401]
21:52:56 <augur> i think there's an interesting class of formal languages worth investigating
21:53:05 <fax> yes the linear time parsible ones?
21:53:16 <augur> but more importantly
21:53:24 <oerjan> fax: see you can use it to guess which polynomial you have from the first few terms
21:53:48 <fax> oerjan, wait it figures out a polynomial from a finte portion of the sequence?
21:53:52 <augur> the ones that are transparently representable in simple linear format
21:54:06 <oerjan> as long as you have more terms than the degree of the polynomial, it works
21:54:22 <fax> !haskell comb m n = product [m, m-1 .. m-n+1] `div` product [1..n]; diff l = zipWith (-) (tail l) l; diffs = map head . takeWhile (not . null) . iterate diff; rebuild l = foldr (scanl (+)) undefined (l++repeat 0); main = print . take 50 . rebuild . diffs $
21:54:30 <oerjan> rebuild could also be written using comb, naturally
21:54:34 <fax> !haskell comb m n = product [m, m-1 .. m-n+1] `div` product [1..n]; diff l = zipWith (-) (tail l) l; diffs = map head . takeWhile (not . null) . iterate diff; rebuild l = foldr (scanl (+)) undefined (l++repeat 0); main = print . take 50 . rebuild . diffs $ [2,3,5,7,11,13,17]
21:54:37 <EgoBot> [2,3,5,7,11,13,17,72,332,1139,3129,7361,15469,29837,53797,91850,149910,235571,358397,530235,765551,1081789,1499753,2044012,2743328,3631107,4745873,6131765,7839057,9924701,12452893,15495662,19133482,23455907,28562229,34562159,41576531,49738029,59191937,70096912,82625780,96966355,113322281,131913897,152979125,176774381,203575509,233678738,267401662,305084243]
21:54:46 <fax> 72 isn't prime :|
21:55:09 <oerjan> and it is well known that no polynomial can give only primes
21:55:26 -!- fizzie has joined.
21:55:55 <fax> oerjan, even if you count -2, -3 etc as primes -- but I don't know how to prove it
21:56:15 <oerjan> that is presumably the sixth degree polynomial that starts with the given primes first
21:56:45 <fax> there IS a polynomial which gives the set of primes + a bunch of random negative integers
21:57:06 <oerjan> yeah. it is not a polynomial in one variable, though, iirc.
21:57:33 <fax> there is a proof in my book (about the not giving only primes thing) but I have been trying to figure it out myself
21:57:51 <oerjan> ok i'll not think about it then :)
21:58:09 <fax> you wont??
21:58:16 -!- Oranjer has joined.
21:58:28 <fax> oh feel free :)
21:58:36 <fax> I have been on it two days and not got it
21:58:39 <oerjan> it's actually quite trivial
21:59:18 <oerjan> if p(x) = a_n*x^n + a_(n-1)*x^(n-1) + ... + a_1*x + a_0 is your polynomial
22:00:24 <oerjan> choosing x a product of a_0 isn't quite guaranteed
22:01:04 <oerjan> oh, except if it's _large_ enough, it has to be different from a_0 itself
22:01:41 <oerjan> if a_0 is 0, just choose x to be any non-prime
22:01:58 -!- augur has quit (Read error: Connection reset by peer).
22:03:27 * fax doesn't undersatnd :/
22:03:35 <oerjan> as x -> infinity, so does the polynomial
22:03:35 <fax> but it's meant to be for multivariate ones too
22:03:53 <fax> but there are infinite primes
22:04:01 <oerjan> well i'm not sure of that proof
22:04:38 <oerjan> fax: if you choose x divisible by a_0, then p(x) is divisible by a_0, so not a prime unless it is equal to a_0. if x is large enough that cannot happen.
22:04:50 <fax> when I give up on proofs they are always SO OBVIOUS it makes me annoyed
22:05:18 <fax> oerjan, oh that is clever!
22:05:33 -!- augur has joined.
22:05:41 <oerjan> i would guess something similar works for multivariate polynomials too, they can still have only one constant term after all
22:05:59 <fax> but I don't really understand it
22:06:19 <oerjan> (choose _all_ the variables divisible by the constant term)
22:06:21 <fax> because there is a (26 variable) polynomial whos positive values are all primes
22:06:44 <oerjan> fax: yeah but i've not proved that p(x) cannot be negative
22:07:07 <oerjan> only that it cannot be a positive prime
22:08:02 <fax> p(x) can be prime
22:08:42 <fax> but oerjan doesn't that contradict the 26-var polynomial?
22:09:46 <fax> the thing is you can have negative coefficents too
22:09:48 <oerjan> no! if you choose all variables divisible by the constant term, you probably force the polynomial to be negative
22:10:46 -!- songhead95 has joined.
22:11:17 -!- augur has quit (Quit: Leaving...).
22:11:31 <songhead95> Hello, if I knew a better place to discuss this I would, but this seems like a good place.
22:11:41 <songhead95> I was thinking of designing an esoteric operating system.
22:12:31 * oerjan carefully scuttles away from the madman :D
22:13:24 <songhead95> on another part of the screen is another mario, in an array of blocks with different QWERTY keyboard keys on them, and when you hit a block, the keystroke is injected
22:14:20 <fax> oerjan, what if the constant is prime?
22:17:11 <oerjan> fax: that's why you need to make the other variables large enough that the polynomial cannot be that value
22:17:34 <oerjan> only something divisible by it
22:18:15 <Oranjer> so a physically transversable OS environment
22:18:45 <oerjan> i suppose if you have more than one variable you need to take care somehow that their largeness doesn't cancel out
22:19:31 <fax> can you make a nonzero multivariate polynomial whos absolute value is always below some constant
22:19:36 <fax> nonconstant*
22:20:34 <oerjan> first, you only need to look at the terms of largest degree (the others will vanish in comparison in the limit)
22:20:55 <oerjan> but if there is more than one such term they might cancel
22:22:06 <oerjan> actually, you can start by looking at the variable with largest term alone
22:22:20 <oerjan> x^n * something in the other variables
22:22:35 <oerjan> if that something is not 0, then you only need to blow up x
22:24:24 <oerjan> oh right and we can use induction to choose the other variables such that it is not zero :D
22:24:54 -!- augur has joined.
22:24:56 <oerjan> that something is after all a polynomial in the remaining variables, one variable less
22:25:15 <oerjan> so by induction we can make it nonzero (in fact as large as we wish)
22:25:59 <oerjan> and after we've done that the other variables are fixed, even if large, so we can blow up x even more
22:27:18 <songhead95> is there any sites dedicated to esoteric operating systems?
22:27:47 <oerjan> songhead95: afaik there is only one community for all things esoteric, and you are there
22:29:16 <fax> I wish I was better at this myself :D
22:29:25 <oerjan> there might be some other sites for specific things (lolcode?) with "mass appeal"
22:29:47 <oerjan> (note lolcode is considered too vanilla here, or something :) )
22:30:34 <oerjan> and of course there are sites of individual esolangers.
22:31:16 <augur> lets try to work on this :o
22:31:53 <oerjan> i don't know what augur is talking about
22:32:11 <augur> i wasnt talkting to oerjan so it doesnt matter :D
22:32:19 <augur> what im talking about
22:32:27 <fax> augur what exactly
22:32:34 <oerjan> i thought fax was talking to me, so i don't understand what "this" you would be referring to
22:32:48 <augur> is a class of formal languages that can be compactedly expressed in a regular expression like form
22:34:12 <oerjan> augur: and you joined after songhead95 so i was assuming you weren't referring to his project
22:35:51 <oerjan> augur: oh that more than CF thing i briefly saw you mention?
22:36:17 <augur> sort of. there seems to be a class of languages which cut across various levels
22:36:42 <augur> which can be parsed in linear time and which have the convenient property of being describably in compact, Regex-like form
22:36:43 <fax> I don't know what you are talking about augur
22:36:51 <oerjan> so, they are all context sensitive, since that includes everything linear _space_
22:36:53 <fax> point free
22:37:22 <augur> oerjan: i dont know if they're all CS
22:37:39 <augur> i dont know much about them, i dont think they're a previously investigated class
22:38:16 <oerjan> augur: i vaguely recall somewhere reading that there aren't any concrete examples (at least not naturally occuring) of CF languages not parsable in linear time if you can walk around in the string, or something like that
22:38:49 <oerjan> augur: it's just an observation from the known fact that CS languages == languages parsable in linear space
22:39:00 <oerjan> and linear time is a subset of linear space
22:39:45 <augur> the language a^n b^n c^n is classically non-CF but its lineartime and obviously regexlike
22:40:10 <augur> since you could just use that like the regex. or using standardish notation, a{n}b{n}c{n}
22:40:15 <augur> and thats completely linear time
22:40:22 -!- songhead95 has left (?).
22:40:27 <augur> infact, a{n}b{n}c{n}d{n}... etc
22:40:43 <fax> REGEX + numbers?
22:40:44 <augur> infact, for _arbitrary different powers, in _arbitrary_ orders
22:40:50 <fax> exponentiation
22:40:57 <augur> not just exponentiation
22:41:04 <augur> linked exponentiation
22:41:24 <augur> even classically hard linguistic phenomena like cross-serial dependencies are possible
22:41:36 <augur> e.g. a^m b^n c^m d^n
22:41:37 <fax> surely you can't parse stuff like (a{n}){m} in linear time?
22:41:58 <fax> (I think that is the compliment of primes?)
22:42:12 <augur> well, (a^m)^n might be. it depends on your interpretation of that, right
22:42:34 <augur> i mean, you could interpret that the following two ways
22:42:48 <oerjan> fax: hm you'd have to be able to do a prime check on mn in time O(mn), that sounds doable
22:43:02 <augur> thats either a^(m*n), so just a^m
22:43:47 <augur> OR you could interpret that as a^(m_0) a^(m_1) ... a^(m_n) for different m's each time
22:43:50 <oerjan> oh right you need m,n>=2. but i assume that's easy to rephrase.
22:43:58 <augur> which is i suppose also just a^m
22:44:21 <augur> you need multiple symbols to get intrigue
22:44:40 <oerjan> augur: make it (a^m)^n a^m a^n a
22:44:46 -!- werdan7 has quit (Ping timeout: 619 seconds).
22:44:56 <augur> i dont know if those are linear time
22:45:16 <augur> but importantly, they're conveniently trivial to represent
22:45:24 <oerjan> augur: i think they are. you can store the numbers you've counted in binary, after all
22:45:39 <oerjan> so arithmetic is likely much _less_ than linear in the whole thing
22:45:48 <augur> actually, i think a^(m*n) a^m a^n a is probably not complicated
22:45:52 <augur> it might even be CF
22:46:13 <oerjan> augur: it's a^((m+1)*(n+1))
22:46:40 <oerjan> ok if m, n can be zero we've still got nowhere
22:46:47 <fax> we can put arbitrary polynomials like this?
22:46:52 <fax> a^(P(x,y,z,w))
22:47:06 <augur> well but see then the question is whether or not P is valid in that, right
22:47:08 <fax> then it can be unary representation of any recursive set :P
22:47:26 <augur> because arguably, { p(w) : w in {a,b}* }
22:47:28 <oerjan> fax: if we can nest (a^m)^n it's just a matter of expanding the polynomial back using the distributive law
22:47:31 <augur> where p is the permute function
22:47:46 <augur> the language is just the Bach/MIX language
22:48:19 <augur> but permutation seems to be a valid thing to have in such a simple notation
22:48:51 <augur> i mean, this is what im not sure about.
22:49:38 <augur> even _if_ such a thing were accepted, tho, i dont think the grammar for, say, simple math expressions, would be expressable.
22:50:14 <augur> e.g. exp -> 0 | ... | 9 | (exp op exp) ; op -> + | - | * | /
22:50:30 <oerjan> augur: i just said that polynomials can be expanded. a^(p(...)+q(...)) = a^p(...) a^q(...) etc.
22:50:31 -!- werdan7 has joined.
22:50:54 <augur> im pretty sure that thats not possible to describe with the sort of transparent stuff we're talking about, so.
22:51:22 <oerjan> augur: if you have (a^m)^n, then you have all you need to expand things
22:52:41 <oerjan> e.g. a^(m^2 + m*n + 2*n) = (a^m)^m (a^m)^n a^n a^n
22:53:13 <augur> but the question was wheat power is required for the (a^m)^n part
22:54:09 <oerjan> augur: well i'm pretty sure (a^m)^n _alone_ can be parsed in linear time, even with m, n >= 2 restriction. whether it can be combined with other things is another matter.
22:54:44 <oerjan> in fact given we just mentioned that 26-variable polynomial giving the primes, we might have some trouble :D
22:55:06 <oerjan> otoh that has negative coefficients. those might be trouble in themselves.
22:56:19 <augur> im curious tho precisely what the computational class of these things are
22:56:24 <augur> because theyre not the CS languages
22:56:29 <fax> augur of what?
22:57:29 <oerjan> yeah we haven't got the precise definition yet
22:58:06 <augur> lets say of languages describable using just the regular processes (e.g. |, ?, +, *, concateenation, subtraction)
22:58:15 <augur> plus coindexed exponentiation, say
22:58:44 <fax> coindexed? :(
22:58:50 <fax> is that like variables numbers only
22:59:08 <oerjan> augur: and that is the class you've heard is linear time?
22:59:10 <augur> where you share the exponent
22:59:23 <augur> oerjan: that is the class that im interested in, which i suspect might be linear time
22:59:27 <oerjan> exponents can be just single variables, then?
22:59:41 <augur> because it seems to be a trivial addition to regular expressions that let them handle INCREDIBLY non-regular languages
22:59:45 <oerjan> augur: oh i thought this was some known class you were referring to?
22:59:57 <augur> thats why im interested in them
23:00:03 <augur> im fairly certain theyre _not_ known
23:00:11 <fax> well this language AUG is equivalent to having {n+3} type indices, because you can just expand them out
23:00:28 <augur> theres also another class you might imagine
23:00:31 <fax> you can also multiply them, because (X{a}){b} = X{a*b}
23:00:38 <augur> regular languages + stack operations
23:00:57 <oerjan> ok. i am now suspecting things might get hairy (possibly nonlinear) if you allow exponents to nest
23:01:05 <augur> e.g. if you had a global stack, you can push and pop to the stack each time you read something of a certain nature
23:01:16 <oerjan> because of having all those polynomials
23:01:21 * fax doesn't lik stacks :(
23:01:53 <augur> e.g. lets say that {+x} means push x, and {-x} means pop x, then a{+x}*b{-x}* i think would generate a^n b^n
23:02:24 <augur> so thats basically a*b* but each time you read an a you push an x to the stack, and each time you read a b you pop an x from the stack
23:03:02 <augur> and the language is recognized if the whole string is consumed, the stack ends up empty, and at no point do you fail to be able to pop a symbol
23:03:07 <augur> if you need to pop it.
23:04:30 -!- kar8nga has quit (Remote host closed the connection).
23:05:56 <augur> i think that would generate a similar class of languages but not the _same_ class
23:06:07 <augur> like, if you had named stacks, you could do
23:06:47 <augur> a{a+x}*b{b+x}*c{a-x}*d{b-x}*
23:07:03 <augur> where a{a+x} pushes an x to the stack named a
23:07:52 <augur> and that would generate the language a^m b^n c^m d^n but using that you couldnt get one extra exponent to m at the end
23:07:56 <augur> because the a stack would be empty
23:08:04 <augur> but if you could push to multiple stacks who knows!
23:09:03 <augur> a{a+x,b+x}*b{a-x}*c{b-x} which i think would generate a^m a^n b^n c^m
23:09:08 <augur> which is trivially CF
23:09:23 <augur> but you could use that interestingly
23:14:33 -!- tombom has quit (Quit: Leaving).
23:17:23 -!- kwertii has joined.
23:18:25 <oerjan> well that stack thing is at least in NP... since you can always guess
23:19:19 <oerjan> if you have multiple stacks then you can copy them
23:20:53 <oerjan> i have a suspicion that might give you a minsky machine - something TC, definitely not linear
23:21:59 <augur> i mean, look, ignoring the time it takes to do stack operations, which is roughly constant because you're at most pushing or popping form all stacks
23:22:10 <augur> each symbol takes constant time to recognize
23:22:22 <fax> but backtracking
23:22:46 <augur> deterministic processes
23:22:57 <augur> maybe. i dont know. :p
23:23:19 <augur> i mean, this is sort of where the extras fuck you up, right
23:23:20 <oerjan> augur: oh this minsky machine thing is not about symbols at all. you could do TC computation without reading a single symbol, once you have filled the stacks from your input
23:24:31 <augur> so i guess the real question is, what is an interesting subset of these languages
23:24:43 <augur> if you can only use a single global stack, is that interesting?
23:24:58 <augur> what about a global stack with only one symbol, eg its an integer register?
23:25:08 <augur> what about multiple integer registers? etc.
23:25:28 <oerjan> multiple integer registers no, since that's all you use for minsky machines anyway
23:26:26 <augur> my implementation for the exponent language just has integer registers which necessarily reset to their fullest just prior to transitioning to a symbol that pops from it.
23:26:36 <oerjan> two global stacks, um now we are dangerously close to a brainfuck tape...
23:26:55 <augur> e.g. a^n b^n c^n pushes n times, then transitions to another stack, pops n times, then resets, and transitions and pops n times again
23:27:14 <augur> but i think the crucial thing is that theres some transparency between the symbols and the string, right
23:27:40 <oerjan> augur: you said something about determinism, that's rather different from regexes...
23:27:53 <augur> i was maaaaybe saying you have deterministic processes
23:28:20 <augur> you can do the majority of regexes deterministically, modulo the non-regular processes
23:28:41 <augur> i dont know if you could do this deterministically. probably not.
23:29:09 <augur> because a^m a^n b^m c^n will i think be potentially problematic
23:29:21 <augur> e.g. aaabbc vs aaabcc
23:29:40 <oerjan> well you'll need some arithmetic at least, not just a stack machine
23:29:56 <augur> well no, you dont need arithmetic
23:30:16 <oerjan> i mean to parse in linear time
23:30:18 <augur> you'd just need backtracking to branch off when you change from incrementing m to incrementing n
23:30:26 <augur> so that probably isnt linear time
23:30:48 <oerjan> a^m a^n b^m c^n pretty obviously can be parsed in linear time
23:31:04 <augur> well, it IS just a^n a^m b^m c^n
23:31:09 <augur> so its a simple CF language
23:31:17 <augur> so i guess it is indeed linear time
23:31:24 <fax> oerjan, it CAN but actually doing it in a general way seems like a difficult problem to me
23:31:27 <augur> but getting a linear time stack machine
23:31:42 <fax> oerjan, I mean you just parse a^x then b^m and then c^(x-m)
23:31:49 <fax> but figuring that out in linear time ?
23:31:52 <oerjan> if you don't allow nested exponents, then maybe it is possible. would require some integer linear equations i think
23:31:54 <augur> right, if you could do the arithmetic then sure.
23:32:12 <fax> also... I wonder if this way, we might introduce subtraction :))))
23:32:17 <augur> then again, you'd build state machines for each thing, right
23:32:20 <fax> then reach full recursive sets
23:32:32 <augur> so you'd be given the expression /a{m}a{n}b{m}c{n}/
23:33:22 <augur> and you'd just do some arithmomagic internally to turn that into /a{x}b{x-n}c{x-m}/ where the second exponents are calculated once you transition away form the last a
23:33:38 <augur> so yeah that would do it, you're right
23:33:46 <fax> yeah but remember we have multiplication and addition of constants
23:33:52 <fax> so this is getting a bit wild
23:34:07 <augur> i dont think having simple math is a problem
23:34:20 <oerjan> i'm much more doubtful if we have multiplication
23:34:24 <augur> /a{n}b{2*n}/ should be a valid expression
23:34:28 <fax> simle math? :)))
23:34:37 <fax> augur diophantine equations are recursive
23:34:38 <augur> as should /a{m}b{n}c{m*n}/
23:34:43 <oerjan> although i'm not sure even with linear stuff
23:34:44 <fax> hilberts 10th
23:35:15 <oerjan> fax: there is a limitation in that we have a finite string to parse
23:35:38 <oerjan> so we cannot get arbitrarily large numbers for parsing a given string
23:35:54 <augur> it depends on what simplicity we allow. is there a way to get /a{x}b{some recursive equation dependent on x}/?
23:35:59 <fax> yeah you are right, that puts a strong limitation on it
23:36:55 <augur> i mean, sure, diophantine equations are recursive
23:37:03 <augur> but do we need to _solve_ them or just compute a value with one
23:37:57 <augur> because if we have, say, /a{x}b{y}c{3x + 5y}/ you have, _roughly_, a diophantine equation. or at least part of one
23:37:57 <oerjan> in principle we could just go through all possible values of the exponents and test each combination in turn. i don't think that gives linear time though :D
23:38:03 -!- BeholdMyGlory has quit (Read error: Connection reset by peer).
23:38:04 <augur> but you're not solving for x and y, you're _given_ x and y
23:38:05 -!- FireFly has quit (Quit: Leaving).
23:38:13 <augur> so all you need to so is compute 3x + 5y
23:38:16 <fax> that proves it's subturing
23:38:49 <augur> i mean, maybe there ARE cases where we'd need to solve for it, i dont know
23:39:08 <augur> somewhere with like /...a{x}...b{y}.../
23:39:26 <augur> where x and y are determined according to a diophantine equation
23:40:06 <augur> /a{3x + 2y}b{x}c{y}/
23:41:39 <augur> but surely not, because thats refactorable. /a{z}b{z - 2y}c{y}/ => /a{z}b{w}c{z/2 + w/2}/
23:41:56 <augur> i dont think we'd ever have to _solve_ diphantines.
23:42:40 <augur> or whatever. i think i did that wrong.
23:42:40 <oerjan> hm... actually i think we must, but not necessarily hard ones
23:43:43 <oerjan> a^{x+y} b^{2y+3z} c^{y+z}
23:44:35 <oerjan> * a^{x+y} b^{2y+3z} c^{x+z}
23:46:08 <oerjan> * /a{x+y}b{2y+3z}c{x+z}/
23:46:33 <augur> a^(x+y) b^(2y+3x) c^(x+z) = a^w b^(2w + x) c^(x+z) = a^w b^q c^(q - 2w + z)
23:47:01 <augur> = a^w b^q c^(q - 2w) c*
23:47:34 <augur> so you dont have to _solve_ a diophantine equation
23:48:03 <oerjan> note that you have to check that the original x,y, and z become positive integers
23:48:29 <augur> no, you just calculate q - 2w on the fly
23:48:33 <augur> and if its negative you fail
23:48:43 <augur> actually no, you dont, right
23:48:46 <oerjan> my example was, however, too simple
23:49:04 <augur> because if its negative, since you have + z, q - 2w + z can be any number
23:49:23 <augur> so this is technically the language a*b*c*!
23:50:04 <oerjan> /a{2x+3y}b{5y+2z}c{7z+11w}/
23:50:18 <oerjan> _now_ you're bloody going to have to solve something
23:50:55 <fax> aa{x}aaa{y}bbbbb{y}bb{z}ccccccc{z}ccccccccccc{w}
23:51:14 <oerjan> i forgot that for awkward linear integer equations, you need more variables than equations
23:52:21 <augur> = a{w}b{w/3-2x/3}c{7z+11w} = a{w}b{q}c{7z+33q+6x}}
23:53:11 <augur> = a{w}b{q}c{33q + n} = a{w}b{q}c{n} = a*b*c*
23:53:19 -!- alise has joined.
23:53:30 <oerjan> augur: and are you _really_ sure all of those correspond to x,y,z,w nonnegative originally?
23:53:46 <alise> Remember to update the alise sighting counter over the next week...
23:53:55 <alise> Oh, wait, most of you guys don't know. Unit again... yeah.
23:53:56 <oerjan> augur: _false_. there is no way you can get c, say
23:54:33 <augur> oerjan: sure there is, because it contains a free variable (w), c{7z + 11w} is c*
23:54:47 <alise> oerjan: I can't take care of myself, I'm dysfunctional! That's why I'm there! ;-)
23:54:55 <augur> well, not in the form you give it, but in the equivalent form it does
23:55:10 <oerjan> augur: c is not a string parsed by my original form, that's the _point_
23:55:37 <augur> what do you mean its not a string parsed by your original form
23:55:59 <oerjan> c is not a member of the language /a{2x+3y}b{5y+2z}c{7z+11w}/
23:56:17 <oerjan> because you damn well cannot get 1 = 7z+11w for nonnegative z,w
23:56:19 <augur> oh ok. ok then lets see
23:57:22 <augur> x = 0, y = 0, z = 0
23:57:27 <alise> 12:30:34 <fungot> fax: maybe you shouldn't have mentioned your win by paradox in philosophy? bah, humbug :) don't have that
23:57:34 <augur> because a{2x + 3y} = a{0}
23:57:43 <augur> and b{5y + 2z} = 0
23:57:43 <oerjan> um, augur, it's _obvious_ you cannot get c
23:57:53 <alise> win by paradox /is/ pretty philosophically dodgy
23:58:11 <oerjan> you cannot get anything strictly between 0 and 7
23:58:11 <augur> therefore you'd have to generate c{11w} = c
23:58:21 <augur> so yes. indeed you are correct.
23:59:29 <augur> but again, oerjan, i dont think this would be an issue
23:59:37 <augur> since it doesnt involve _solving_ a diophanting
23:59:37 <alise> 12:51:16 <fax> <3 finite calculus
23:59:37 <alise> it's like arithmetic but cooler!
23:59:42 <fax> in my book is says assume P(x1,...,xm) only takes prime values, then let p = |P(1,...,1)| and consider Q(y1,...,ym)=P(py1+1,...pym+1)
23:59:46 <alise> diophanting sounds like an awesome sexual act