←2010-03-13 2010-03-14 2010-03-15→ ↑2010 ↑all
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:12:54 <alise_> I prefer the latter
00:13:35 <oerjan> happy pi day!
00:16:21 <fax> bapfhj
00:16:44 <oerjan> gnörp schnibble
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:05 <oerjan> Z?
00:21:33 <pikhq> "Zulu". Notes the time zone as being UTC.
00:22:19 <oerjan> wright
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:35:58 <fax> ;(
00:36:07 <alise_> fax: why
00:36:16 <alise_> pikhq: because it tastes nothing like salt or vinegar
00:36:17 <fax> I can't handle people
00:36:30 <alise_> fax: bah
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:13 <pikhq> Deliciousness.
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:05 <fax> hi
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:04:24 <alise_> !
01:05:28 <fax> :D
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:16:31 <alise_> so pretty
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:33:31 <augur> SUP BITCHES
01:34:22 <oerjan> INF ANTS
01:35:07 -!- Oranjer has joined.
01:35:15 <augur> :O
01:35:22 <Oranjer> what!
01:36:35 <oerjan> LIM ERICKS
01:38:20 <Oranjer> oh
01:38:22 <Oranjer> cool
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:47:51 <Sgeo> 76360k
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:44 <alise_> fax: no i mean like 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:28:49 <fax> what 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:03 <comex> like what? 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:27:16 <nooga> helloh 03:27:25 <coppro> helloh 03:27:41 <pikhq> holleh 03:28:22 <nooga> don't you people sleep? 03:28:58 <coppro> no 03:28:59 <coppro> nevar 03:29:52 <oklopol> well it's only 5:30 here 03:29:53 <Gregor> Sleep is for the weak. 03:30:03 <nooga> 4:30 here 03:31:12 <nooga> oklopol: finland? 03:32:23 <Gregor> http://sibeli.us/ ! 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:32:48 <pikhq> Sgeo: 見たくない。 03:33:01 * Sgeo can't read Japanese 03:33:02 <pikhq> nooga: Only 21:32 here. 03:33:07 <oklopol> finland 03:33:10 <pikhq> Sgeo: Don't wanna. 03:33:20 <Sgeo> lol 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:25 <nooga> blargh 03:37:33 <nooga> japanese romances 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:39:36 <nooga> sounds awesome 03:39:44 <nooga> no, really 03:39:50 <Sgeo> It is 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:40:35 <Sgeo> *point 03:40:49 <nooga> :3 03:41:04 <Sgeo> Sorry if that was too spoilery 03:43:00 <nooga> nah 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:17:10 * mibygl shrugs. 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:26 <mibygl> Perhaps. 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:40:53 <mibygl> I have not. 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:41:38 <kwertii> yep, that's the one 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:28 <pikhq> Also, filesystem? 06:00:29 <pikhq> Bah. 06:00:32 <mibygl> Smalltalk, except it's the entire Internet! 06:00:40 <pikhq> So. Smalltalk. 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:04:59 <mibygl> The Croquet Project? 06:05:50 <pikhq> Erm. That. 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:15:45 <Gregor> ... 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:17:59 <Gregor> Bravo, sir. 06:18:17 <pikhq> Not my joke. Is Douglas Adams. 06:18:26 <Gregor> Aha, didn't know. 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:18:41 <Gregor> This galaxy, in fact. 06:18:44 <pikhq> Ah. 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:14 <alise> *mathematica 15:43:55 <fax> hi alise!! 15:45:58 <alise> hi there 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:42 <alise> and coyotos died 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:01:39 <alise> <3 16:13:43 -!- nooga has joined. 16:23:20 <nooga> .... 16:34:37 <alise> maxima is rubbish 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:30 <alise> Well... yes. 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:12 <alise> ISBOOL := \x f. f 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:45 <alise> Erm. 17:58:46 <alise> In C. 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:39 <alise> */1+?y$2 18:28:39 <alise> ) 18:28:54 <alise> Then (pow2 n) produces a value in the range 1 to 2^n, inclusive. 18:29:36 <fax> ??? 18:29:41 <alise> What? 18:30:09 <alise> Hmm, actually, it's in the range 1 to 2^(n-1). 18:30:12 <alise> fax: what's ??? ? 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:32 <fax> yndpaf 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:33:42 <alise> why 18:33:44 <alise> cold or hot? 18:33:50 <fax> neither 18:34:20 <alise> then what 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 <alise> I love J 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:00 <alise> Recursion in C: 18:50:01 <alise> LC *lcalloc(void) 18:50:02 <alise> { 18:50:02 <alise> return malloc(sizeof lcalloc()); 18:50:02 <alise> } 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:01 <alise> Nope! 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:08 <pikhq> alise: Beautiful. 18:56:10 <alise> [Window Title] 18:56:19 <alise> superstrict.exe 18:56:19 <alise> [Main Instruction] 18:56:19 <alise> superstrict.exe has stopped working 18:56:19 <alise> [Content] 18:56:19 <alise> Windows is checking for a solution to the problem... 18:56:20 <alise> [Cancel] 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:35 <Gregor> ... okidokie. 18:56:35 <alise> *Wait, what? 18:56:43 <pikhq> I woke up. 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:00 <Gregor> IT IS NOT PERMISSIBLE 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:00:20 <alise> *was 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:14:53 <alise> u (y+1) - u y 19:14:53 <alise> ) 19:15:03 <alise> id deriv 3 19:15:04 <alise> 1 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:17 <alise> % deriv i. 10x 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:24 <alise> (%x is 1/x) 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:33 <alise> inded it is 19:18:35 <alise> *indeed it is 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:20:02 <alise> oh the humanity! 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:18 <alise> id deriv 19:22:19 <alise> +----------------------+ 19:22:19 <alise> id+-----------------+ 19:22:19 <alise> 1:u (y+1) - u y 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:23:37 <alise> _99 19:24:27 <alise> fax: that's deriv on f : [int] -> [int] 19:24:28 <alise> well 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:25:35 <alise> :p 19:25:59 <fax> heh 19:26:02 <alise> huh j also has limits 19:26:07 <alise> cute syntax ^:_ 19:26:08 <alise> i.e. 19:26:13 <alise> f^\infty(x) 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:04 <alise> plot x;sin x 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> ) 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:00 <Sgeo> Ah 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:40:34 <alise> works perfectly 19:41:11 <fax> show me :( 19:41:28 <alise> like what, a screenshot? 19:41:32 <fax> yeah 19:43:54 <alise> fax: uploading 19:44:45 <alise> fax: http://i.imgur.com/bg46u.png 19:45:06 <alise> that steps 1 100 19:45:10 <alise> *100 100 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:46:11 <alise> %x is 1%x 19:46:12 <alise> which is 19:46:14 <alise> 1 19:46:14 <alise> - 19:46:14 <alise> x 19:47:10 <alise> fax: so % deriv x is almost but not quite %x... 19:47:12 <alise> % deriv 100 19:47:12 <alise> 0.00990197 19:47:13 <alise> %100 19:47:13 <alise> 0.01 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:27 <alise> % deriv 100x 19:47:27 <alise> 100r10099 19:47:27 <alise> %100x 19:47:27 <alise> 1r100 19:47:32 <alise> well using rationals /didn't/ help 19:47:39 <alise> :-D 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:08 <oerjan> yes 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:51:52 <alise> naturally 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:58:54 <oerjan> heh 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:17 <alise> er 20:03:19 <alise> n > 2 20:03:44 <fax> :| 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:04:32 <oerjan> or triang(x+y) + y 20:04:51 <oerjan> Q.E.D., practically 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:06:36 <oerjan> very basic formula 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:25 <wareya> hi 20:08:29 -!- wareya has changed nick to Wareya. 20:08:31 <oerjan> hi Wareya 20:09:00 <Wareya> what's up? 20:09:10 <oerjan> something math 20:09:13 <Wareya> k 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:12:52 <oerjan> ok 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:14:59 <fax> oh my god 20:15:13 <oerjan> fax: hm? 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:00 <alise> hahaha 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:36 <alise> yes 20:22:47 <alise> fax: where did you define integral 20:22:57 <pikhq> alise: That site concludes that I am English. 20:23:04 <alise> oh you did. 20:28:40 <fax> what is oerjan's synchronicity? 20:29:26 <alise> oerjan believes in synchronicity 20:29:59 <fax> me too 20:30:00 <fax> what is it? 20:30:07 <oerjan> XD 20:30:21 <oerjan> google synchronicity 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:54 <fax> hmmmm 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:33:41 <fax> ?hm 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:42 <fax> ooh 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:16 <oerjan> oh 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:29:32 <oerjan> grmbl
21:29:52 <fax> daskelab
21:29:53 <HackEgo> No output.
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:01 <oerjan> oh
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:35:50 <oerjan> it is 21:36:43 <oerjan> it's reconstructing x^2 from its iterated differences 21:36:53 <oerjan> (at 0) 21:38:40 <fax> Hmmmm 21:38:43 <fax> this is finite calculus 21:38:45 <fax> ? 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:38:58 <oerjan> yep
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:25 <oerjan> i'm recalling it
21:39:34 <oerjan> there was some playing around on #haskell
21:39:39 <oerjan> long ago
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:01 <oerjan> *facepalm*
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:41:52 <fax> hm
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:08 <oerjan> *the nth
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:17 <fax> mm
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:45:17 <augur> hey guys
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:48:44 <augur> magic
21:48:46 <augur> fax!
21:48:49 <fax> hi augur!
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:26 <augur> twin peaks huh
21:49:27 <fax> isn't it comb 3 3 = 1?
21:49:30 <fax> oh
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:14 <augur> indeed 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:53:54 <oerjan> fax: yep 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:45 <oerjan> heh
21:54:46 <fax> 72 isn't prime :|
21:54:56 <oerjan> indeed
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:55:56 <augur> ok brb
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:21 <oerjan> well not aloud anyway
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:00 <oerjan> hm wait
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:25 <oerjan> so that shows it
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:39 <oerjan> oh
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:07:45 <fax> ;S
22:07:55 <oerjan> huh?
22:08:02 <fax> p(x) can be prime
22:08:14 <oerjan> *cannot always
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:09:58 <fax> mm
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:11:51 <songhead95> Based on Super Mario Bros.
22:12:24 <Oranjer> oh really now?
22:12:31 * oerjan carefully scuttles away from the madman :D
22:12:31 <Oranjer> expound please
22:12:38 <songhead95> you go down tubes to enter programs
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:13:36 <songhead95> the keyboard is two NES controllers
22:13:42 <songhead95> or something
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:17:50 <fax> oh right!
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:09 <fax> hm
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:19:43 <oerjan> i doubt it
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:21:08 <oerjan> x^m y^n - x^n y^m say
22:21:11 <fax> yeah
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:01 <augur> O HAI
22:25:15 <oerjan> so by induction we can make it nonzero (in fact as large as we wish)
22:25:25 <fax> wow
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:26:14 <oerjan> *possibly large
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:28:12 <songhead95> k kool
22:28:26 <oerjan> yeah
22:28:33 <songhead95> seen, and contributed
22:28:43 <oerjan> oh right
22:29:01 <songhead95> have my own language :]
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:12 <augur> so fax
22:31:16 <augur> lets try to work on this :o
22:31:29 <songhead95> whatcha talkin bout?
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:16 <augur> tho oerjan
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:42 <fax> I was
22:32:48 <augur> is a class of formal languages that can be compactedly expressed in a regular expression like form
22:32:53 <songhead95> well ok then...
22:34:12 <oerjan> augur: and you joined after songhead95 so i was assuming you weren't referring to his project
22:34:25 <augur> :P
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:32 <oerjan> linear time, you said
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:36:56 <fax> ?
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:25 <augur> ok
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:12 <augur> ok.
22:39:25 <augur> anyway
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:36 <oerjan> yeah
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:47 <augur> probably not.
22:41:58 <fax> (I think that is the compliment of primes?)
22:42:04 <fax> unary
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:28 <augur> (a^m b^m)^n
22:44:40 <oerjan> augur: make it (a^m)^n a^m a^n a
22:44:45 <augur> or that
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:26 <augur> lets see
22:46:38 <fax> huh
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:35 <augur> is linear time
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:32 <augur> or is it?
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:51:32 <augur> to what now?
22:51:38 <oerjan> to _that_
22:51:45 <augur> i dont follow
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:00 <augur> oh, right
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:22 <augur> right
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:55:33 <augur> probably.
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 <augur> a^n b^n
22:58:50 <fax> is that like variables numbers only
22:58:57 <fax> mm okay
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:51 <augur> no
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:19 <augur> :p
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 <oerjan> oh food ->
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:04 <augur> etc
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:01 <oerjan> oh hm
23:19:19 <oerjan> if you have multiple stacks then you can copy them
23:19:40 <oerjan> {-x}{+y}{+y}
23:20:53 <oerjan> i have a suspicion that might give you a minsky machine - something TC, definitely not linear
23:21:21 <augur> mm i dont know
23:21:38 <oerjan> er
23:21:57 <oerjan> * {a-x}{b+x}{c+x}
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:28 <augur> no backtracking
23:22:46 <augur> deterministic processes
23:22:57 <augur> maybe. i dont know. :p
23:23:02 <fax> ;D
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:23:47 <augur> hm
23:23:56 <augur> ok
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:25:34 <augur> right
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:35 <augur> state* 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:33:56 <augur> thats ok
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:14 <augur> perhaps!
23:35:14 <augur> but
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:44 <fax> hm
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:13 <fax> *nod*
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:40:14 <augur> maybe?
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:42:46 <augur> example?
23:43:43 <oerjan> a^{x+y} b^{2y+3z} c^{y+z}
23:44:27 <oerjan> er wait
23:44:35 <oerjan> * a^{x+y} b^{2y+3z} c^{x+z}
23:44:38 <oerjan> sheesh
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:16 <oerjan> or nonnegative
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:16 <fax> :D
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:35 <augur> it doesnt matter
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:53:57 <augur> bye alise ::hug::
23:54:09 <alise> <3
23:54:26 <oerjan> alise: take care
23:54:33 <augur> oerjan: sure there is, because it contains a free variable (w), c{7z + 11w} is c*
23:54:37 <fax> see you
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:00 <augur> i think.
23:55:10 <oerjan> augur: c is not a string parsed by my original form, that's the _point_
23:55:17 <augur> what
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:56:51 <augur> er
23:57:00 * oerjan cackles evilly
23:57:05 <augur> lets see
23:57:09 <augur> to get c
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:28 <alise> hahaha
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:58:49 <fax> oerjan,
23:58:52 <augur> you'd get c^(11n)
23:59:02 <augur> for n in Z
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
23:59:49 <augur> ;)
23:59:56 * augur diophants alise
←2010-03-13 2010-03-14 2010-03-15→ ↑2010 ↑all