00:00:04 1::2::3::nil is represented as <3, {yes->1;no->2;maybe->3}> 00:00:24 r::q::p::::snil is represented as <4, {north->1;south->2;east->3;west->4}> 00:00:27 oops 00:00:35 r::q::p::s::nil is represented as <4, {north->r;south->q;east->p;west->s}> 00:00:40 aha 00:00:43 gotcha! 00:00:48 ok, so what's the induction for T'? 00:00:58 why don't you write it 00:01:03 ill tell you if you get it right :) 00:01:07 look at O for inspiration 00:02:15 Pr 00:02:27 Ordinarily I'd love to, but - I really should have left many minutes ago. 00:02:49 You could save the dialogue for later, I'd love to participate, and just show me the induction schema for mu now for me to mull over. 00:02:57 Or you could wait for both. Your choice. 00:05:14 there is no way you can possibly understand the scheme for Muu 00:05:29 Likely. 00:05:29 You have to first understand T 00:05:35 But I'm interested in it regardless. 00:05:47 it will be very simple and clear once if you just approach it step by step 00:06:25 Yes, but I /really really/ have to go. Surely, there is no harm in telling me it? 00:06:35 well I don't know how to write it out either 00:06:47 we need to establish some new notation together first 00:07:05 just use any existing language :P 00:07:09 or are they not appropriate? 00:07:31 P(L') -> (forall n, forall f, (forall i, P(f i)) -> P(B' f)) -> forall t', P(t') 00:07:38 that's the scheme for T' I wish you had got it 00:08:03 i probably would have if i tried 00:08:08 but /i/ /have/ /to/ /go/ 00:08:11 please try and understand 00:08:13 bye, anyway 00:08:17 so for T, P(L) -> (forall l, [] P l -> P(B l)) -> forall t, P(t) 00:08:28 [] is a new notation we have invented 00:08:43 [] P (a::b::c::d::nil) = P a /\ P b /\ P c /\ P d 00:09:09 [] is defined for any strictly positive functor 00:09:20 (proof of this is in some paper I can show you later) 00:09:27 this is enough to define induction on Mu 00:11:07 It's the end of days for There. 00:12:17 "•DSL/Cable modem: 25 minutes" 00:12:23 for a 47MB download 00:12:44 -!- alise_ has quit (Ping timeout: 252 seconds). 00:17:37 -!- FireFly has quit (Remote host closed the connection). 00:22:37 -!- coppro has joined. 00:32:03 -!- BeholdMyGlory has quit (Remote host closed the connection). 00:48:18 * Sgeo wants to play on FICS against someone he knows 01:01:47 * pikhq has been futzing a tiny bit with TinyGC... 01:01:59 ... It appears to work, and appears to be slow. 01:02:00 Yeah. 01:02:42 Sgeo: what's your rating? 01:03:03 coppro, um, it's been years since I was last on FICS 01:03:05 How do I get that? 01:03:12 Sgeo: oh, ok 01:03:15 then I'll play you 01:03:17 Found it 01:03:29 I just didn't want to play against someone way better than me 01:03:31 Um, rating for Blitz or Standard or Lightning? 01:03:40 coppro, I'm probably not better than you 01:03:40 don't really care 01:03:45 It's been years since I played chess 01:06:23 Sgeo: what time controls do you want? 01:06:32 *shrug* 01:06:55 Regular, I guess 01:07:37 Sgeo: it says you're examining a game 01:07:42 What? 01:07:56 there we go 01:12:14 * Sgeo clearly has no clue what he's doing 01:12:56 I only have a little more than you 01:13:15 I can give you some pointers afterward, if you'd like 01:15:29 Sure 01:17:06 -!- MissPiggy has quit (Quit: Lost terminal). 01:17:18 * Sgeo isn't really thinking anything through that much 01:20:21 You went downhill around move 16 01:30:26 I've lost, haven't I? 01:31:33 :(:(:( 01:32:33 mostly 01:34:21 [In case anyone cares, I just lost] 01:34:26 coppro, what client do you use? 01:34:34 eboard 01:34:45 it's not great, but it's not terrible 01:34:46 * Sgeo is using BabasChess 01:34:54 Used to use Chess Machine and love it 01:37:22 -!- lament has quit (*.net *.split). 01:37:22 -!- HackEgo has quit (*.net *.split). 01:38:45 -!- lament has joined. 01:39:59 -!- HackEgo has joined. 01:42:24 http://i.imgur.com/qlrHy.jpg 01:44:13 bsmntbombdood: OK, I'm putting that on sibeli.us for the moment. 01:46:00 i don't get it 01:47:34 http://sibeli.us/ 01:48:17 who the hell is Jean Sibelius 01:48:31 X_X 01:48:34 God I hate people. 02:08:55 Anyone want to see the game between coppro and I? 02:10:25 ??? 02:10:32 Oh, chess game. 02:10:35 I am so suck at chess. 02:17:45 Gregor, bet you're better than me 02:17:54 I haven't played in YEARS 02:18:00 And when I had, I barely paid attention 02:18:36 I know the mechanics, just no strategy 02:18:52 Sgoe: you were pretty good for the first half 02:18:57 but then your moves just became random 02:19:15 although you missed some opportunities to develop; getting pieces out and involved is key 02:20:34 -!- oerjan has joined. 02:22:46 hm... FAUST "Functional AUdio STream"... What are the chances of that name NOT being designed to fit the acronym? 02:23:12 exceedingly tiny i'd say, since if they didn't know about faust, FAST would have been closer 02:23:42 -!- coppro has quit (Quit: I am leaving. You are about to explode.). 02:24:10 -!- coppro has joined. 02:26:54 -!- gm|lap has joined. 03:02:04 oerjan: Awesome catch :P 03:02:53 So, what person who's totally not me wants to get out the sheet music for Finlandia and record the event sequence for my Generic Music Idol Band Star Game. 03:02:58 With a "?" there 03:07:13 http://ficsgames.com/cgi-bin/show.cgi?ID=243952855;action=show 03:09:39 -!- adu has joined. 03:10:22 -!- Asztal has quit (Ping timeout: 264 seconds). 03:36:18 -!- oerjan has quit (Quit: leaving). 03:38:57 -!- gm|lap has quit (Quit: HydraIRC is a child molester -> http://silverex.net/news <- i couldn't change my quit message). 03:39:09 -!- GreaseMonkey has joined. 03:43:57 GreaseMonkey: Generic Music Idol Band Star Game? 03:43:58 Erm. 03:44:02 Gregor: Generic Music Idol Band Star Game? 03:44:17 Clearly, something *that* generic should have the sequence generated from the sheet music! 03:44:36 Impossible, the recording, being of non-shitty music, doesn't have a constant tempo. 03:44:40 ... And by sheet music, I mean a convenient, easy-to-parse subset! 03:45:25 * pikhq tries to think of non-shitty music with a constant tempo... 03:45:30 * pikhq is having severe difficulty. 03:46:13 Okay, I'm having trouble thinking of *shitty* music with a constant tempo now. :P 03:47:43 4'33". 03:47:46 * pikhq vejnas! 03:50:13 * Gregor plays zee5.ogg 03:50:16 ;P 04:00:51 Oh, I never really answered your question. 04:01:20 Generic Music Idol Band Star Game is a generalization of DDR, Guitar Hero, Rock Band, and all the other identically dull games out there. 04:01:58 Currently it's roughly equivalent to DDR, for the others I would need non-instant events, but that's a trivial addition really. 04:02:19 And of course the horrendous karaoke part that should earn the death sentence to all who play it is excluded. 04:05:21 Hey, DDR started it and was unique... 04:05:31 ... And then came more bemani from Konami... 04:05:31 DDR did not start it. 04:05:34 And it was not unique. 04:05:39 Parappa the Rapper started it. 04:05:54 DDR merely introduced a non-gamepad controller to the equation. 04:05:59 ... And then they started releasing games with just the music changed... 04:06:24 And then Guitar Hero and Rock Band came around. 04:06:43 Well after the genre had been beaten into a bloody, homogenous pulp. 04:07:28 Regardless, DDR didn't start it, they were just the first ones clever enough to get people to pay for an alternate controller that is only useful for one game. 04:07:53 Rock Band did the best in that regards of course, getting people to pay for FOUR alternate controllers that are only useful for one game, and are in fact interchangeable except for layout. 04:07:54 DDR's the home version of an arcade game. 04:08:32 Well fine, they were the first ones clever enough to devise an alternate control mechanism, which they used initially in arcade :P 04:09:06 Anyway, the whole genre is stupid rubbish that has the unfortunate tendency of making people think they have a viable skill when they have none. 04:09:40 But it's also an amusing thing to parody with Finlandia :P 04:09:44 DDR is quite enjoyable. But... Yeah, the whole genre is ridiculously repetitive. 04:09:57 "Oooh, let's make a new game, but with *different songs*!" 04:10:01 Also, http://upload.wikimedia.org/wikipedia/en/4/4f/Inch_converter.jpg is the most horrifying thing I've ever seen. 04:10:16 "Hey, I got something better! Let's change the brand name and *have a different controller*!" 04:11:08 And of course, no useful skill involved. Just a useless one. 04:13:18 I suppose the basic agility encouraged by DDR is arguably a more viable skill than the ability to thumb something that's such a poor approximation of a guitar that it literally has no relevance were you to actually want to learn the guitar. 04:13:32 Actually, hahahah, y'know what really started the genre? 04:13:36 Miracle Piano Teaching System 04:13:51 Also of note: DDR functions as a form of exercise. Everything else... Is about as useful as playing air guitar. 04:14:45 But Miracle Piano Teaching System is, of course, far too difficult for the average GMIBSGer, and besides it actually teaches a skill that borders on useful. 04:15:14 Indeed. 04:15:50 At the least, you're more likely to impress a female with being able to play piano than being able to do Paranoia Survivor Max on challenge. 04:16:04 And that is why all males do anything, right? :P 04:17:05 It's worked out well for me! >_> 04:17:16 Hahah. 04:18:08 The karaoke-thing on Rock Band, tangentially, is damn near impossible if you can sing. 04:18:31 You're not allowed to use vibrato, yes? 04:18:39 Yes. 04:18:41 Or rather, you'll be penalized for it. 04:18:44 Or... Anything else. 04:18:59 And God help you if you're not used to singing the melody. :P 04:19:06 Heh 04:19:20 This is Rock BAND, not Rock CHOIR 04:19:51 Although a choral GMIBSG would be ... impossible for the neanderthals that play that kind of game to figure out *shrugs* 04:19:56 Feh, that was offensive. 04:20:03 Neanderthals aren't so bad, really. 04:20:11 They're our cousins. 04:20:31 Let's say ... australopithecus. 04:20:38 Eh, most people play it as an excuse to be with friends. 04:20:46 Kinda silly to need an excuse, but hey. 04:21:07 I MIGHT have negative opinions about this genre of game :P 04:21:45 I have negative opinions about most of the genre simply because it's been beaten in the ground more than even freaking sports games. 04:22:44 Oh, and the choice of music for them usually *sucks*. 04:23:06 Of course, they need the most constant and dull music possible to make the game possible. 04:23:16 Aside from the fact that if it was good, royalties would be too expensive. 04:23:38 DDR tends to commission music. 04:23:51 And Guitar Hero commissions... Covers. 04:23:59 lol 04:24:02 Very annoyingly poor covers, too. 04:24:14 The whole concept of covers amuses me a lot, btw. 04:24:34 It is kind of amusing, yes. 04:24:36 I want to convince my cellist friend to say he's doing a cover of Shostakovich some time :P 04:25:16 All because of the singer-songwriter thing that started getting common in the 50s... 04:26:12 * pikhq got reminded of that terrible Kansas cover again. 04:26:17 But what's really hilarious is that I'm sure that the majority of singer-songwriters nowadays are not, in fact songwriters, but the actual songwriters are grunts who get no recognition. 04:26:39 Gregor: The majority of *popular* ones, perhaps. 04:26:48 Naturally that's what I'm referring to, yes. 04:26:58 The popular singer-songwriters today aren't even singers. They're boobs with autotuners. 04:26:59 When you get outside the realm of popular musical shovelware, then you start seeing talent. 04:27:25 Heck, just get outside the past couple decades or so and you start seeing talented people that are popular. 04:27:50 So, you're saying that music continues its steady slide into the abyss :P 04:27:51 Freaking autotune. 04:28:11 -!- Oranjer has joined. 04:28:20 Nah, just the stuff that gets shoved down people's throats that I'm not sure how anybody can like. 04:28:30 what what 04:28:39 Awesome timing for Oranjer to waltz in :P 04:29:09 I'm guessing it's...religion? 04:29:26 No. 04:29:32 Not particularly close. 04:29:32 darn 04:29:35 Could be farther though. 04:29:36 I give up 04:29:48 There are logs, y'know :P 04:29:53 hmph 04:29:53 Music. Specifically, manufactured music produced by the RIAA. 04:30:02 oh 04:30:23 Examples include Celine Dion and Nickleback. 04:30:25 (effin' Canada!) 04:30:35 Celine Dion is a national treasure 04:30:50 Boobs with an autotuner. 04:31:04 boobs with an autotuner is a national treasure 04:31:12 I beg to differ. 04:31:13 Y'know, if they built the autotuner right into the breast implants, they could save a lot of trouble. 04:31:22 boobs with an autotuner is national treasure 04:31:32 (alt title) 04:32:10 in soviet russia, blah blah... 04:32:57 http://pubacc.wilcox-tech.com/~greaser/mods/dootman.it if you're lacking somewhat interesting music 04:33:04 You want a national treasure? *Jimi Hendrix* is a national treasure. 04:33:39 I agree 04:42:07 jimi hendrix is dead. 04:42:14 he can't be a national treasure. 04:42:25 augur: WE WORSHIP HIS BONES. 04:42:28 don't you get it, augur? 04:42:34 his bones have gone missing 04:42:36 oic 04:42:43 we have to go on a quest to find them 04:42:46 well, ofcourse his bones have gone missing 04:42:54 he's been resurrected 04:43:45 As a ZOMBIE 04:44:21 National Treasure 3: Zombie Hendrix would be, literally, the best movie conceivable 04:45:08 Why 3? 04:45:11 Ohwait 04:45:19 hahahaha 04:45:21 There were some movies called "National Treasure", weren't there? 04:45:27 yep 04:45:29 Yeah. 04:45:38 Clearly not movies I ever saw :P 04:49:47 They weren't... Notable. 04:52:37 o.O at coppro's record on ficsgames.com 04:52:42 Although it's better than mine 04:53:41 the first info I see on that site is entirely opaque 04:53:47 what is FICS? 04:54:24 hey! alright! 04:54:30 Free Internet Chess Server [ freechess.org ] 04:54:30 does this handle variants? 04:54:51 Some 04:54:53 Yes. 04:54:56 >:( 04:55:01 some does not mean any 04:55:05 Oranjer finds a Chess server, and his first thought is "let's NOT play the game that we've been playing for thousands of years" 04:55:08 which means you can't define your own 04:55:22 well, that's my first thought with anything ever, so yay! 04:55:26 (OK, not thousands ;) ) 04:56:06 Well, there's some ability to define your own starting positions I think 04:56:25 Sgeo: don't look there :P 04:56:28 hmph 04:58:33 It'd be nice if it did shogi... 04:58:55 AND GO 04:58:59 And Poker 04:59:04 And Checkers 04:59:04 isn't there a program out there that lets you play any chess variant? 04:59:11 including chess and go, I think 04:59:15 1,000...something, I think 04:59:57 Gregor: Shogi is a chess-family game. 05:00:29 damn, I finally found the program 05:00:37 but it costs money 05:00:47 http://www.zillions-of-games.com/ 05:00:59 pikhq: I was being intentionally stupid :P 05:01:22 http://www.chessvariants.org/programs.dir/zillions/ 05:01:26 -!- Gracenotes has joined. 05:01:38 Gregor: Mmkay. 05:09:22 * Sgeo should probably do something that will give him nutrition 05:24:03 FICS has a number of popular variants, but nothing like new pieces 05:24:43 I reluctantly admit, after much time using Firefox, that Chrome is a far more reliable browser >_> 05:24:52 The client-server model makes that difficult 05:25:03 yeah, Firefox gets major slops for reliability 05:25:12 Why is it that flash stalls out and shits out Firefox, but in Chrome it doesn't? How does the process separation stop Flash from stalling? 05:26:13 that question seems obvious to me--but I fear that in asking it, you suggest a deeper answer? 05:26:50 Yes, I do :P 05:27:04 oh 05:27:16 Gregor: When Flash stalls in Firefox, Firefox shits itself. 05:27:26 When Flash stalls in Chrome, Chrome kills the process. 05:27:49 I'm not referring to halting or crashing, just momentary stalls. 05:27:56 Ah. 05:28:16 That's just because Firefox's implementation of the NSAPI sucks. 05:28:18 e.g. Hulu plays seamlessly in Chrome, but is gappy and shitty in Firefox. 05:29:32 * pikhq tries installing Chromiumn 05:32:09 Chromeyfox 05:34:11 I love Chrome 05:34:40 I just trust Google's intentions less and less recently ... 05:34:59 shh! don't let them hear you! 05:35:11 Google IRC? well then 05:35:32 You can always download SRWare Iron 05:35:42 >.> 05:35:54 -!- oklokok has quit (Ping timeout: 248 seconds). 05:36:24 there is a popup 05:36:27 I can't trust it boo 05:42:36 Gregor: Chromium is probably in your package manager. 05:42:50 Yes, yes it is. 05:42:56 There. 05:43:04 That would be how I installed it. 05:43:15 Why that's not Chrome. 05:43:19 Has none of the nasty bits. 05:43:26 ??? 05:43:45 I thought Chromium was the devel name 05:44:33 -!- oklokok has joined. 05:44:41 OKLOCOCK 05:48:45 * Sgeo has a chair! 05:54:26 -!- oklokok has quit (Ping timeout: 265 seconds). 06:05:52 -!- oklokok has joined. 06:14:49 Chrome takes ages to compile. 06:20:20 g++ chrome.cc -lages -o chrome 06:25:30 * Gregor looks for a theme for Chrome called something along the lines of "Not being wildly different from the OS for the sole purpose of being wildly different from the OS, with no UI benefit" 06:29:04 Now I'm waiting on the code going into /usr/src/debug. Hooray. 06:29:25 (... So I like the ability to use gdb when something segfaults...) 06:34:53 -!- sebbu2 has quit (Ping timeout: 260 seconds). 06:34:54 -!- sebbu has joined. 06:34:55 hi all 06:35:16 hello 06:40:37 -!- MizardX has quit (Read error: Connection reset by peer). 06:46:32 How does http://www.geocities.com/lifemasteraj/beginner1.html still exist? 06:47:50 What universe do these people come from? http://www.mywot.com/en/scorecard/geocities.com 06:48:04 Sgeo, this is mind boggling 06:48:23 The WOT stuff, or the continued presense of the geocities site> 06:48:24 ? 06:48:37 latter 06:52:17 Good lord, it's so Geocities too X-D 06:53:32 Maybe e's paying for hosting? 07:04:29 -!- tombom has joined. 07:10:14 -!- Oranjer has left (?). 07:48:44 -!- tombom has quit (Quit: Leaving). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:16:24 -!- GreaseMonkey has quit (Quit: HydraIRC -> http://www.hydrairc.org <- Nobody cares enough to cybersquat it). 08:38:17 -!- cmeme has quit (Ping timeout: 265 seconds). 08:46:13 -!- sebbu has quit (Ping timeout: 258 seconds). 08:47:21 -!- cheater2 has quit (Ping timeout: 248 seconds). 08:48:33 -!- cheater2 has joined. 08:50:28 -!- sebbu has joined. 08:57:50 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 09:11:25 -!- adu has quit (Quit: adu). 09:50:53 -!- FireFly has joined. 09:52:09 -!- ais523 has joined. 10:17:15 -!- MizardX has joined. 10:41:01 -!- ais523 has quit (Remote host closed the connection). 10:50:25 -!- ais523 has joined. 12:26:30 -!- BeholdMyGlory has joined. 12:30:07 -!- alise has joined. 12:30:10 16:08:17 so for T, P(L) -> (forall l, [] P l -> P(B l)) -> forall t, P(t) 12:30:16 sorry, had already left at that point 12:32:28 I'll play anyone at chess! Extremely badly! 12:35:06 alise: hmm, I used to be OK at chess, but haven't practiced in years 12:35:22 major issue for me would be finding a chessboard that doesn't automatically suggest moves for me 12:35:33 I've been beaten by a non-prodigy twelve year old. 12:35:35 So... yeah. 12:35:54 tell you what, I think my really awful chess AI still runs in DOSBox 12:36:06 ais523: there are billions of clients for FICS 12:36:13 I know 12:36:14 Sgeo and coppro played yesterday, see logs for what clients they used 12:36:37 oh, I just assumed each player would use their own board and you'd send moves over IRC 12:38:10 -!- MigoMipo has joined. 12:38:17 ah; i have no chessboard at all here 12:38:29 chess sux 12:38:30 ugh, it seems that although it runs in DOSbox, it captures both the keyboard and mouse 12:38:42 and, also, I'm so bad it'd take me ages to figure out how to express the moves I make :-) 12:38:44 thus making it impossible to switch windows, or otherwise communicate with people 12:38:45 maybe I could use a program and you could use a real board 12:38:59 alise: I meant, setting something like GNU chess to 2-player mode to use it as a board 12:39:07 heh 12:39:17 or we could just sign up for fics :P 12:39:34 and have my horrible failure recorded for all eternity 12:39:46 hmm, almost works in wineconsole 12:39:54 only issue is that it sizes the screen incorrectly 12:40:10 fixme:int:DOSVM_Int10Handler Load ROM 8x8 Double Dot Patterns - Not Supported 12:40:35 hmm, and that one shouldn't even be hard, you can simply implement it by doubling the vertical height of the screen 12:40:44 (virtual screen, that is) 12:40:46 in fact, i'm sure someone must have made a java applet client for fics 12:40:57 yeah but wine is shit :P 12:41:14 let's get crysis 5 working! who cares about the rest of the api 12:41:29 we want to support the gaymen community :| 12:41:38 meh, running a program and only 2 fixmes, that's not bad 12:41:51 besides, I've run stuff in WINE that I really needed to be able to run in order to get projects done 12:42:13 it works just fine on MPLAB C30, except that it makes MPLAB spout a few warnings when it loads 12:42:17 alise: http://i.imgur.com/pDiHb.jpg 12:45:32 A-anyway. 12:48:47 ais523: fics or manual? I have the fics regpage up here 12:49:05 manual, because playing games over a work connection is hard to explain 12:49:33 but I'm assuming attempting to keep track of everything said on IRC would be a fool's errand 12:50:15 Just make a +m channel for it 12:50:26 you're disrupting one of my essential tactics! (decide what to do instinctively so that every move takes about a second) :-P 12:50:29 Or did you mean the lack of even a local chessboard 12:50:52 ais523: also, the irc bytes sent and the chess bytes sent will be pretty much identical, you know 12:50:59 in fact, the chess bytes may be binary and thus more obscure 12:51:15 alise: the chess bytes will have headers 12:51:28 and won't go through at all if they're on a nonstandard port 12:51:34 you can automatically see where the bytes are sent 12:52:15 * alise googles for chess over irc out of curiosity; maybe there's something that'll automate it for me 12:52:35 If you have irssi there is 12:52:42 Don't know about other clients 12:52:57 (And I haven't tried the irssi one either, I just know about it) 12:53:56 yeah i saw that but i meant a chessboard program that actually sends and recvs the moves itself 12:53:57 ah well 13:00:10 I can play if you want 13:02:27 -!- oerjan has joined. 13:03:20 Deewiant: I can't decide whether you'd be better or worse than ais523 13:03:52 well, I have no idea how good Deewiant is at chess; I'm formerly-decent-but-out-of-practice 13:04:03 maybe in the top 2 or 3 in the school while I was at secondary school 13:04:08 I'm rather surprised how little this stock Windows 7 is annoying me 13:04:11 even IE8 13:04:24 I'm formerly-not-entirely-shit-but-out-of-practice 13:04:28 I mean, sure, it sucks, but.. 13:04:38 Load, you fucking downloa page! 13:04:38 IE8 is so much better than IE6, that's why it feels so good 13:04:39 *download 13:04:42 I want my chess client. 13:04:52 ais523: I know, but I keep forgetting I'm actually using IE as opposed to, say, Firefox 13:05:26 and I actually really like using the taskbar to switch tab 13:05:27 s 13:05:27 without extensions, there aren't many user-visible differences between even IE7 and Firefox 13:05:37 *tabs 13:05:39 also, taskbar to switch tabs would be a nightmare the way I use tabs 13:06:18 but the thing is, I use alt-tab to switch windows mostly 13:06:22 so it's actually quite nice 13:07:10 * alise tries to figure out how to get winboard to do two-player 13:07:34 Our secondary school -equivalent had folks who got silver in some Scandinavian chess championship; at least one of the guys had an ELO near 2000 13:08:21 Probably all the active chess club people there (maybe 10-20 of them?) could beat me without too much trouble 13:08:37 This seems to not do two-player offline. Sigh. 13:08:50 Just use FICS :-P 13:08:57 Winboard works offline 13:08:57 you could probably have written a chess client yourself by now 13:09:11 Deewiant: ais523 refuses to because of work connection 13:09:15 I used to write them for practice when I was younger; I think I wrote one in Excel 13:09:19 also it does, but only one-player-against-engine 13:09:20 -!- Asztal has joined. 13:09:27 alise: Yes, but if you want to play me instead ;-) 13:09:36 alise: And no, there's mode -> edit game 13:09:43 ais523: Last chance before I cruelly cast you aside in favour of a real man 13:09:48 Which is basically equivalent to two-player one-machine 13:09:56 alise: last chance to what? 13:10:01 Except that it doesn't have timing 13:10:02 I don't mind not playing if it's too hard to set up 13:10:16 Deewiant: "edit game", what a ridiculous name for it! 13:10:20 Well, use FICS or I cast you aside for now :P 13:10:30 ais523: Well, it's not really a two-player mode. 13:10:54 Deewiant: do I need to register for fickz? 13:10:55 It's just that: allowing you to edit what move is taken at a given point. Something you'd typically do when viewing an already played game. 13:11:05 alise: I don't know how it works. :-P 13:11:11 That could make future moves impossible, surely? 13:11:14 Deewiant: >_< 13:11:28 Well, surely it deletes the history from that point forward. 13:11:32 If you are not a registered player, enter guest or a unique ID. 13:11:55 "alise" is not a registered name. You may use this name to play unrated games. 13:11:57 Right. 13:11:59 Deewiant: Well, connect. 13:12:08 I am connected, I even registered. 13:12:19 could we have the moves posted in-channel somewhere so I can watch? 13:12:27 maybe not this channel, though 13:12:35 Easy enough 13:12:36 Okay. 13:12:44 #deewiant-alise-champ-2010 13:12:48 heh 13:18:41 -!- alise_ has joined. 13:20:42 -!- alise has quit (Ping timeout: 252 seconds). 13:28:33 -!- oerjan has quit (Quit: leaving). 13:50:02 -!- alise_ has quit (Ping timeout: 252 seconds). 15:01:58 -!- cpressey has joined. 15:41:33 -!- alise has joined. 15:41:55 Name for a Reversi-playing program: Infersi 15:43:52 -!- coppro has quit (Quit: I am leaving. You are about to explode.). 15:44:25 coppro's quit message has been false every time so far 15:44:32 I'm starting to suspect he doesn't actually mean it 15:44:44 either that, or it isn't targeted at me, in which case some context would be helpful 15:45:17 I've exploded several times when he's left 15:45:31 Quite painful 15:47:37 I wonder what the most practical Haskelly thing is for making a GUI 15:47:57 I have no idea, but deep-down I hope it indirectly involves Befunge 15:49:01 Write Befunge code that uses WIND and then system "rcfunge tmp.b98" ? 15:49:43 No 15:49:44 something like that, but with more tight binding on the Haskell 15:49:51 maybe you could go via INTERCAL 15:49:51 Also, that's Windows-only 15:50:04 if INTERCAL doesn't have Haskell bindings yet, it probably should do 15:50:21 mostly to annoy Haskell advocates 15:50:32 alise: What's Windows-only? WIND is only implemented using X 15:50:55 I would prefer something written in pure Befunge that uses ANSI control codes to make a ncurses-y user interface 15:50:55 Or at least, RC/Funge-98 only implements it with X, and I don't know of any other interpreter that implements it at all 15:50:57 Okay. 15:50:57 Oh, really? 15:51:28 RC/Funge-98 is very non-Windows-only 15:51:34 Quite the opposite 15:51:40 it would be funnier if the software only worked using X on Windows 15:52:03 hi 15:52:04 cpressey: yep, and that sort of thing's entirely possible; I just don't think anyone's tried yet 15:52:21 I would prefer something written in pure Befunge that uses ANSI control codes to make a ncurses-y user interface <-- anything wrong with NCRS? 15:52:33 for a start "something written in befunge" tends to be very non-reusable 15:52:45 -!- alise_ has joined. 15:52:59 due to the complete lack of something that works for emulating functions. And even with SUBR it is somewhat messy 15:54:29 Don't forget MACR 15:55:26 -!- alise has quit (Ping timeout: 252 seconds). 15:56:34 hmm, is there any Befunge extension that works Modular SNUSP-style? 15:57:09 Depends on what that style is 15:58:11 basically, it has commands for subroutine call and return 15:58:21 that work like setjmp/longjmp on an explicit stack 15:59:50 I don't think there's anything quite like that, no 16:00:46 it makes subroutining very easy 16:00:53 or ofc you could just use IFFI and do subroutines that way 16:01:57 -!- MissPiggy has joined. 16:02:07 Deewiant, hm... 16:02:20 -!- MissPiggy has changed nick to fax. 16:02:36 ais523, you need to port IFFI to work without depending on ick 16:02:48 At one point I wanted to have "pages" that the IP could travel between (kind of like 2.5 dimensions I guess), but there was a lot of resistance (too machine-y, I guess.) 16:02:49 that would be "rewrite", not "port" 16:02:52 of course, since you replace mainloop that would be painful 16:02:53 but it's a useful project 16:03:06 ais523, also, it must work with t 16:03:10 unlike IFFI currently 16:03:10 the replacing the mainloop is actually not an issue, it's a trivial wrapper 16:03:29 the real issue is that it's tightly hooked to ick's control logic, on the basis that the entire purpose of CFFI is to do that 16:03:43 cpressey, I think I joked about a two letter fingerprint NX. That works like the page permissions on hardware 16:03:52 -!- alise_ has quit (Ping timeout: 252 seconds). 16:03:53 read, write, execute flags 16:04:03 I'm not sure what a write only area would be useful for 16:04:15 logging? 16:04:27 ais523, would be easy to overwrite what you logged though 16:04:27 you could read it in a debugger, but not make a security leak 16:04:39 ais523, I'm not sure that makes sense 16:04:45 since other threads could still read the data 16:04:46 Something more elegant would be some kind of "memory switch" that remembers which direction you turned (i.e. which branch you took), and lets you reverse it / backtrack... that captures the idea of call/return but in a kind of spatial way. 16:05:03 cpressey: MODE has switchmode which is essentially that. 16:05:20 cpressey: sounds worryingly like TRDS 16:05:37 which could also be very usable for subroutine call/return, if it wasn't for the essential complexity of the whole thing 16:05:38 Although of course it doesn't work with multiple threads. 16:06:00 Since it only remembers the latest branch ever, not the latest branch per IP. 16:06:57 huh 16:08:45 Switchmode is close, but it would need to be more elegant, combining in the functionality of w, perhaps. 16:09:34 What to do with a w that passed through? 16:09:38 I.e. compared equal 16:09:48 Otoh, pretty dispatcher structures are one of the things that make Befunge fun, so why try to make it easy? 16:09:57 For the other cases, you can single-usely turn it into [] 16:10:35 Deewiant: You could turn the w into one of three instructions that reverses the decision and then turns itself back to w for the next use. 16:10:54 But what does reversing == mean 16:11:01 Since it distinguishes between < and > ordinarily 16:11:07 You'd have to pick one arbitrarily? 16:11:28 Reversing the path chosen. == chooses the straight line, reversing the straight line still is the straight line. 16:12:01 I suppose so 16:20:09 Speaking of "practicality" in esolangs I always liked the idea of an "esoteric OS adapter" (Easel/PESOIX/PSOX) much better than language-specific facilities like fingerprints. But it seems so much harder to get such a project off the ground. 16:21:20 -!- ais523 has quit (Remote host closed the connection). 16:21:46 I think it's somewhat of an excuse to limit the capabilities of your esolang 16:22:52 I mean, all you need now is putchar and getchar and you're done; language-specific ways of talking to the OS/doing other things like that can be more interesting, IMO. 16:23:30 They can be, true. 16:36:52 -!- oerjan has joined. 16:38:02 07:43:52 --- quit: coppro (Quit: I am leaving. You are about to explode.) 16:38:03 07:44:25 coppro's quit message has been false every time so far 16:38:18 well in the long run, if the Big Rip hypothesis is true... 16:46:17 I mean, PSOX is in no way a replacement for Befunge fingerprints, because those can affect the language, not just the OS. But there are just so many esolangs out there that just can't be reasonably expected to grow their own OS features. (Not that PSOX would necessarily be able to help all of those, either, though) 16:48:01 I think the big barriers to adoption are 1) the spec isn't simple/abstract enough and 2) there is no proof of concept implementation 16:48:12 (Isn't that always the story, though?) 16:49:33 I would like to stand corrected about there not being an implementation 16:50:04 Sgeo does seem to have an implementation of it in Python? 16:50:32 The file I/O stuff needs some work 16:50:46 And the spec for the File I/O stuff is probably iffy 16:55:48 Also, it's untested on Windows 16:56:07 Although was a major spec change just due to projected issues with Windows 16:59:07 -!- kar8nga has joined. 17:00:40 Having it be a pipeline (and only a pipeline) is definitely the right design, I think. 17:01:18 I haven't unravelled the spec sufficiently to know what I think about the details yet... 17:32:31 -!- tombom has joined. 17:35:58 -!- hiato has joined. 17:38:52 -!- hiato has changed nick to sudobus. 17:39:44 -!- sudobus has changed nick to aqualoqua. 17:39:55 -!- aqualoqua has changed nick to sudobus. 17:40:34 -!- sudobus has left (?). 17:45:17 -!- hiato has joined. 17:45:23 -!- hiato has changed nick to sudobus. 18:01:34 -!- alise has joined. 18:02:17 Chromium is the devel name 18:02:22 and all the nasty stuff has options to disab;e 18:02:23 so there 18:03:43 Gregor: You can set chromium to use OS colours 18:03:50 in options 18:04:03 -!- lament has quit (Ping timeout: 240 seconds). 18:04:28 -!- lament has joined. 18:06:14 -!- alise_ has joined. 18:06:19 21:35:32 You can always download SRWare Iron 18:06:23 You could, but you'd be retarded: 18:06:40 http://neugierig.org/software/chromium/notes/2009/12/iron.html 18:08:10 -!- alise has quit (Ping timeout: 252 seconds). 18:08:50 ... He was expecting *money* from that? 18:08:50 Dear God. The money in FLOSS is... Support. 18:09:09 fax: you're a fax machine again? 18:09:23 pikhq: he got it - see all the publicity 18:09:31 I especially like how he removed an entirely innocuous class 18:10:24 alise_: So. Dumb. 18:10:41 If he wanted a real privacy-based browser, he'd do... Something smarter. 18:10:52 Default to incognito, integrate Tor, etc. 18:10:54 Best thing to do is just to turn off all the settings in main Chrome. 18:11:06 Yuh. 18:11:14 They're settings for a reason, after all. 18:11:17 Google Updater automatic installation. 18:11:22 automatic updates = privacy violation 18:11:30 Bug tracking system, sends information about crashes or errors. 18:11:36 bug reporting = privacy violation 18:11:46 DNS pre-fetching. 18:11:49 dun dun DUNNNN 18:11:56 A timestamp of when the browser was installed. 18:12:00 Oh now /that/ is just insidious 18:12:30 I'm just surprised how candid he was about his real goal 18:12:36 ;) 18:12:37 DNS pre-fetching was even *called* insidious? 18:12:40 ;);););) 18:12:46 pikhq: oh the lines that aren't factual are my mocking 18:12:52 the guy clearly has no idea what he's doing 18:13:13 I submit that he knows exactly what he is doing 18:13:17 i read the full log he doesn't understand why people aren't nice to him :-) 18:13:18 He's marketing 18:13:19 cpressey: i mean code-wise 18:13:31 Ah. Well there, he barely needs to 18:13:40 Also: what means rotful? 18:13:53 Only needs an understanding of what will scare sufficiently paranoid people 18:13:59 We haven't had a super-shitty #esoteric meme in ages, and we need one. 18:14:17 rotful 18:14:18 hi 18:14:26 fax: yo 18:14:42 fax: wow, my brain has completely different heuristic clauses for MissPiggy and fax 18:14:59 fax: so I actually read that "hi" completely differently than if you said it before changing your nick back 18:15:13 apparently my brain infers huge gobs of meaning into "hi" purely based on who says it 18:15:19 :) 18:15:46 permanent nick change or not? 18:16:31 alise_: ... Mine too, oddly enough. 18:17:07 hmm... i guess it will take some time for the heuristics to migrate 18:17:19 unless you're going to start acting like fax acted too, in which case you'll be two entirely different people 18:18:38 cpressey: The issue with PSOX was basically that Sgeo didn't know what he was doing, so it was in fact rather heavily Brainfuck-oriented. 18:19:37 (and Linux) 18:19:51 cpressey: Obviously the solution is to have it communicate with /its own/ esolang that just does IO stuff. 18:20:02 PSOX seems mostly alright. There are definitely some things that need clarification, and some that I would want to change. 18:20:10 *disable (typo from way back) 18:20:29 cpressey: Well, it only works with languages that do unrestricted byte-by-byte two-way synchronised binary IO. 18:20:31 Which is ludicrous. 18:20:36 | | | 18:20:36 +-+ * | 18:20:36 | | | * 18:21:22 wat 18:21:26 alise_: But that's common. If your language communicates with smoke signals, anything like PSOX isn't going to be much help anyway. 18:21:43 cpressey: Well, printable ASCII would be a good subset to use... 18:21:48 It looks line-oriented, actually. 18:21:56 It's still heavily binary. 18:22:01 Also, it's abandoned. I forget why. 18:22:18 Printable ASCII I could live with, but I don't know of any langs that are really crippled from binary I/O? 18:22:32 That's more of an OS issue. 18:22:36 Thank you, MS-DOS. 18:22:36 If I were going to spec an IO esolang, I would have it use little particles of data being catapulted off to data sinks (forts), and "enemy" cannons (input sources) shooting out particles. 18:22:46 So you place forts and cannons in the right place to aim, and coordinate their firings. 18:22:55 cpressey: INTERCAL-72 can only do roman numerals 18:22:59 alise_: OS /colors/ are not the issue. OS /style/ is the issue. 18:23:18 so perhaps INTERCAL-72 roman numeral format without over/underlines (so only small numbers) is the lowest common denominator 18:23:26 Gregor: Well, you can get the title bar. And it uses GTK widgets inside the page. 18:23:53 Gregor: If that isn't acceptable, don't use Chrome :P 18:23:56 alise_: It could look for the first two symbols output, consider them '0' and '1' in binary, and build the rest on that. 18:23:58 If it uses GTK widgets, then why even with "use GTK+ theme" (whatever that means) enabled does it look like friggin' Windows >_< 18:24:10 Use GTK+ theme = use its colours 18:24:17 And because you don't have a GTK+ theme set up, presumably. 18:24:20 So it's using Raleigh. 18:24:24 Which looks uber-ugly. 18:24:27 I use XFCE. 18:24:34 So I most certainly have a GTK+ theme set up. 18:24:39 Then it's because you touch yourself at night. 18:24:54 More seriously, it's because it's using your title bar colour for a big bit, I imagine. 18:24:54 I touch myself in broad daylight, thank you very much. 18:24:59 You could try and edit the settings manually. 18:25:05 If the 3rd character output is different from the first two, it could assume you have printable characters available... if it's non-printable, it could assume you have 0-255. 18:25:46 cpressey: you might want it to use the first two _lines_ output 18:25:50 cpressey: I think that for most esolangs, fancy programs are /boring/. 18:26:02 An IRC client in SNUSP. Whoopdedo, 18:26:07 *Whoopdedoo, that's mostly glue. 18:26:18 For those where it can be interesting, it's because of an aspect of the language. 18:26:22 So you want it part of the language. 18:29:44 That's along the lines of what I was thinking when I said PSOX makes stuff less interesting 18:30:45 yeah 18:30:55 * cpressey shrugs 18:30:57 OK 18:31:58 I'm certainly not looking to write a webserver in Hargfak. 18:32:35 I was more thinking of it as a tool to allow esolangs to be more easily passed off as "real". 18:32:46 i.e. 18:32:48 Marketing. 18:33:21 But if it makes things less interesting, n/m 18:34:46 But on that note, I don't see why most Befunge fingerprints are interesting. 18:37:08 They aren't. 18:37:16 In fact, Befunge is relatively uninteresting past its abstract core. 18:37:24 Concurrency adds a large gob of fun. 18:37:36 Time travel and multiverses add more large gobs. 18:37:37 Beyond that, meh. 18:38:22 s/interesting/a popular topic of conversation/, then. 18:38:50 fax: Bad news! 18:38:53 "Let me repeat that. By allowing the judgmental equality to identify these two closed extensionally equal values, we collapse the judgmental equality on terms under a false hypothesis. Bye bye typechecker." 18:38:59 http://www.e-pig.org/epilogue/?p=324 18:39:12 cpressey: Because the hoi polloi suck at identifying the novel. 18:39:29 In fact all the fun in -98 is pretty much the huge sack of implementation woes. 18:39:30 that post is quite confusing, I don't understand why this doesn't mean epigram is broken 18:39:39 fax: it is 18:39:44 they're having to replace W-types with something else 18:39:58 otherwise they're fucked 18:40:27 what confuses me is, whatever they replace W types with: Can't you just implement W with /that/? 18:40:45 obviously they have to replace it with something less powerful/abstract 18:40:54 http://muaddibspace.blogspot.com/2010/03/algebra-system.html you didn't tell me you had a blog :| 18:41:42 alise_: In that case, Befunge-111 should probably not exist. A clear, unambiguous spec would only ruin the fun. 18:41:49 because it's embarassing :P 18:41:59 fax: lawl 18:42:09 cpressey: Well... yeah. Isn't that obvious? 18:42:19 You need to introduce a bag of craziness to make it fun, which is why I've been pushing my idiocy. 18:42:27 No, not to me. 18:42:44 fax: hmm... I agree that ZFC is probably inconsistent, yet I'm having some sort of knee-jerk AARGH NO reaction to its statement 18:42:53 Help? 18:43:05 lol 18:43:49 fax: I think I've read a post on your blog before and it was ridiculously overcomplicated for something 18:44:18 mm? 18:44:19 What's this about ZFC being inconsistent? 18:44:35 -!- MizardX has quit (Read error: Connection reset by peer). 18:44:40 uorygl: it probably is 18:45:23 That would be News. 18:45:23 http://r6.ca/blog/20091101T231201Z.html 18:45:28 well, not probably 18:45:31 -!- MizardX has joined. 18:45:42 but if you belong to general dependent-type constructivist cabal, then yeah probably :P 18:45:54 fax: of course you forgot to add "for the same reasons that Coq is probably inconsistent". 18:45:59 alise: Today I just picked up "Constructive Functional Analysis" 18:46:33 "Can we really believe in the consistency of any system whose ordinal strength we do not have a notation for?" 18:46:35 ... 18:46:49 * fax can't interpret that '...' 18:46:49 ...... 18:46:55 nor that 18:47:06 Probably "That's ridiculous, either p or not p" 18:47:15 (Note: Above sentence is merely mocking the mocking of the classicalists.) 18:48:13 "..." was shorthand for "..." 18:48:14 fax: Ah yes, I think it was your thing on halving numbers 18:48:27 I thought it might be that 18:48:35 cpressey: Inner meaning? 18:48:57 Maybe I'll eventually figure out the words for the thought, but don't expect it soon. 18:50:07 cpressey: Fundamental thought, generalised, is "I agree", "I disagree" or ""? 18:50:42 Honestly, my inclination was to respond with "Please, won't somebody think of the children??!?!" 18:50:48 I don't think whether a person belongs to a general dependent-type constructivist cabal or not has any bearing on whether ZFC is probably inconsistent or not. 18:50:58 fax: you object to insulting wolfram? :| 18:51:05 But I am sensitive to overusing Simpsons quotes. 18:51:13 stop stalking me!! 18:51:17 uorygl: Oh yes it does! 18:51:21 fax: I CAN'T HELP IT 18:52:28 hey gloss is exactly what i need for my othello program i think 18:52:33 can it do mouseclicks, I wonder 18:53:15 I'm reading about finite calculus right now, though 18:53:41 the discrete derivative of f at x is defined as f(x+1)-f(x) 18:53:54 What would it mean for ZFC to be inconsistent? In practical terms, I mean. 18:54:34 It would mean that in ZFC, it's possible to prove anything at all, making all theorems proved in ZFC meaningless. 18:55:04 Exactly. 18:55:31 It's probably easy to modify the axioms to make it consistent if it isn't, but you'd lose tons and tons of results. 18:55:31 I was thinking more like, another refinement would be layered onto it to plug the hole, like ZFC itself was layered onto naive set theory. 18:55:42 alise you know I have a soft spot for people like wolfram 18:55:54 fax: I don't actually. 18:56:00 oh 18:56:19 I do. It's a beanbag chair in a dungeon. 18:56:27 fax: Personally, the way he reacted to ais523's solving of the Wolfram prize gives it a slightly personal edge to me. 18:57:01 "Oh, how wonderful! A kid has proved what I always suspected. This has wide-reaching implications and provides an important bit of evidence for MY unifying theory of everything. When I first wrote about it ..." 18:58:40 did he mistreat ais in some way? 19:00:28 He did him a great intellectual disservice by making only passing mention to his achievement in his post on it, and spending 99% of the large tome talking about how good he was for thinking of it. 19:01:34 Even before I knew that, he rankled me immensely. 19:03:40 Of course. I especially enjoyed the Usenet post where he, as a teenager, belittled someone with far more experience than him because he had a pile of books with which to learn more than him. 19:04:17 Number of references to the body of computability research in "New Kind of Science": ... well, he mentions the name "Turing" a couple of times. In the phrase "Turing machine". 19:04:18 link? 19:04:28 fax: I'll find it; sec. 19:05:00 fax: For now, he's Feynman writing to Wolfram (warning: surrounded with wolframlove by the transcriber) http://elzr.com/posts/wolfram-feynman 19:05:03 *here's 19:07:06 If ZFC was inconsistent, there would be chains of reasoning in it which did not terminate, correct? 19:07:16 cpressey: You are thinking in computational terms. 19:07:23 Inconsistency means that you can prove a falsehood. 19:07:32 This is a contradiction. 19:07:33 alise_: As is my perogative, I thought. 19:07:37 i.e.: p & ~p. 19:07:47 From this, you can prove anything. 19:08:15 You can prove that false is 42, that 43+1 = -99 and -99 is also a horse of size 98 that behaves as a monoidal functor when applied to itself. 19:08:16 If you can prove anything, you can prove the premises, therefore there are chains of reasoning which do not terminate. 19:08:22 See http://xkcd.com/704/ for an example 19:08:43 Deewiant: I liked that xkcd - incredibly rare for me as of late. 19:09:09 xkcdsucks had a really stupid rebuttal saying that a piece of data isn't true or false, it's a piece of data, but obviously you'd just do "Your mom's phone number is 923487958" and prove that 19:09:10 then use that 19:09:18 lol 19:10:08 cpressey: In the dependent-types view, we hvae 19:10:11 *have 19:10:15 Types :: statements 19:10:17 Values :: proofs 19:10:29 If you prove a falsehood, your value doesn't terminate when evaluated. 19:10:38 alise_: The most recent xkcd was REALLY bad. 19:10:41 So, yes, in a way you are right. 19:10:42 I'm not convinced of the converse, though (If there are chains of reasoning which don't terminate in ZFC, then it's inconsistent) 19:10:46 So bad I may remove it from my RSS reader. 19:10:47 But "termination" doesn't make any sense in logic. 19:10:51 I don't read xkcd. 19:10:56 Deewiant: Yeah, that was an enjoyable xkcd. 19:10:59 Infinite chains of reasoning, perhaps, but there is no computation, so there is no termination. 19:11:09 cpressey: I used to. 19:11:14 But it became shitty. 19:11:34 alise_: You have a computational view of "termination", I think. 19:11:34 I read xkcd still because *following* a hit-and-miss comic takes very little time. 19:11:45 cpressey: Right you are. 19:11:50 Once I've started following a comic, it takes a severe facepalm moment for me to stop. 19:11:55 ... Or just severe apathy. 19:11:57 oklokok, hi 19:12:21 pikhq: Yeah, but this latest one was terrible, even for XKCD. 19:12:26 Like, ow, my brain hurts terrible. 19:13:53 cpressey: what do you mean by "chain of reasoning"? 19:14:04 Gregor: True. It did quite suck. 19:14:13 This looks like a non-terminating chain of reasoning to me: 1 = 1; therefore, 2 = 2; therefore, 3 = 3; therefore, 4 = 4; therefore, . . . 19:14:29 -!- alise has joined. 19:14:44 Or just "1 = 1 therefore 1 = 1 therefore ..." 19:14:57 pikhq: did you /see/ the xkcd where the whole joke was "Here are some cartoon female genitals. Here are stick people that cannot possibly possess them. LOL, TGI FRIDAYS" 19:15:23 alise: ... I think I scrubbed it from my memory. 19:15:38 uorygl: AFAICT that's what I mean. 19:15:57 hey I've hated xkcd for years 19:15:59 cpressey: okay, so I just showed you a non-terminating chain of reasoning. So does that mean ZFC is consistent? 19:16:00 -!- alise_ has quit (Ping timeout: 252 seconds). 19:16:02 how come you guys are only just catching up now 19:16:02 cpressey: imo proofs aren't actually part of zfc's truth space 19:16:14 fax: it started sucking around maybe 2007-2008 imo. 19:16:21 You have axioms and rules for deriving theorems from those axioms. 19:16:25 cpressey: as in they're just a tool for us to reason about, and verify things 19:16:35 but they're totally orthogonal to any issue actually related to the set of truths we call zfc 19:16:36 fax: Because it's gone from overrated but amusing to overrated and sucking most of the time. 19:16:42 ah 19:17:19 * sudobus liked it better when the convo was about stuff he knew about, like the cocio-economic effects of a potential utube cencorship, or cats 19:17:41 uorygl: No, that's the converse that I said I wasn't convinced of, isn't it? 19:17:54 "utube" ;_; 19:18:09 fax: (: 19:18:13 sudobus: you do realise this is a progrmaming channel :) 19:18:16 *programming 19:18:22 I'm not convinced of the converse, though (If there are chains of reasoning which don't terminate in ZFC, then it's inconsistent) 19:18:33 cpressey: so now are you convinced that the existence of a non-terminating chain of reasoning doesn't imply that it's inconsistent? 19:18:49 alise: sudobus == hiato 19:18:54 uorygl: Other way 'round. If it's inconsistent, then etc 19:18:59 sudobus: Spelling. Improve it. 19:19:00 ah 19:19:13 pikhq: he's south african he can do what the hell he likes because he's interesting 19:19:17 sudobus: I know what a catbus is, but what's a sudobus? 19:19:20 IRC has just enough people who spell things correctly to make it really depressing when someone comes out with shit like "cong@l8" 19:19:36 pikhq: Srue tihng man 19:19:45 rotful 19:19:46 fax: here's wolfram being a complete idiot http://groups.google.com/group/comp.lang.lisp/msg/f3b93140c2f2e922?dmode=source&output=gplain&pli=1 19:20:06 I think you mean "çocio-economic" and "cençorship". 19:20:20 alise: it's what you get when you take a and rest it perpendicularly on a piece of paper that says "sudo" just right tos that the o's overlap 19:20:24 Most people are complete idiots at least a couple of times in their lives 19:20:34 I think he meant イエユイノボメノ. 19:20:37 uorygl: sorry, my bad 19:20:39 (note -- not actual Japanese) 19:20:40 alise, ah this is KMP -- I have read this 19:20:45 Deewiant: Yes, it takes a very special sort of person to make a career out of it. 19:20:57 fax: kmp? 19:21:00 oh pitman 19:21:35 Indeed 19:22:07 Deewiant: It shows that Wolfram has a huge attitude problem & ego that has lasted til today. 19:22:10 He then said "I'm going to read these and then I'll know as much as you." 19:22:14 hehe 19:22:26 alise: I just realised I left out at least a word from my previous reply. Note: rest a mirror ... just right so that the .. 19:23:35 I actually am going to read these, and then I actually will know as much as you! 19:24:25 I should carry about a stack of books just incase I want to insult someone 19:25:40 including "the compiler book with the dragon on it" 19:25:49 cpressey: AAAH. 19:26:09 Tangentially, I should read the Dragon Book sometime. 19:26:16 why? it's outdated 19:26:23 you would only read if you like history 19:26:30 What's not outdated? 19:26:38 Appels book 19:26:39 ... Outdated books can be enjoyable. 19:27:02 Or at least enlightening. 19:27:26 fax: The latest edition of the dragon book is newer than Appel's 19:27:39 By about 10 years 19:27:40 Oh, and there have been 2 later editions. 19:27:43 Most recent was in 2006. 19:27:56 Of course, most people think of the *first*, but still. 19:28:08 ah that's interesting 19:28:20 they have republished it, I have not seen the new version 19:28:21 The first is out of print :-P 19:28:28 I've heard the recent editions are not much more than reprints of the originals? 19:28:31 Deewiant: Yeah, yeah. 19:28:36 there aren't any compiler books from a functional perspective 19:28:37 hmph 19:28:53 alise: "Modern Compiler Design" explains a bit of how Haskell is compiled 19:28:58 alise: "Modern Compier Design"... yeah 19:29:04 no, I mean 19:29:08 structuring compilers functionally 19:29:12 alise, Calculating Compilers 19:29:12 MCD's coverage is not very good though 19:29:24 (PhD thesis, but it's a good read anyway) 19:29:27 fax: well... foo to you 19:29:30 cpressey: True, unfortunately 19:29:31 alise: The Implementation of Functional Programming Languages, by SPJ? 19:29:36 foo ?? 19:29:56 Part of me wonders why you even need a book on it :/ 19:29:57 alise, http://www.reddit.com/r/squiggol/ 19:30:06 cpressey: Sexy purposes 19:31:12 alise??? 19:31:14 Gah 19:31:20 http://www.uni-koblenz.de/~laemmel/expression/long.pdf cool, material on the expression problem! 19:31:23 Proving compilers correct is useless. 19:31:33 cpressey, hahahahah 19:31:33 Prove the generated code is correct. 19:31:40 cpressey: That's... what you do. 19:32:08 cpressey: ... That's not the only reason to write a compiler functionally... 19:32:14 Or write anything functionally... 19:32:15 A correct compiler will take an incorrect program and produce another incorrect program. 19:32:17 You prove that the canonical semantics of the input (syntax tree) are equivalent to the canonical semantics of the output. 19:32:19 "Proving compilers correct is useless." -- I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a remark. 19:32:25 And... That's... What people do... 19:32:25 -!- sudobus has quit (Quit: leaving). 19:32:43 fax: Some of it is overstatement. But not all of it. 19:32:45 cpressey: Why yes. Yes it will. 19:32:54 Adapted from Babbage - On two occasions I have been asked, 'Pray, Mr. Babbage, if you put into the machine wrong figures, will the right answers come out?' I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question. 19:33:05 cpressey: And I would expect nothing more of a correct compiler. 19:33:20 Well. I also want correct code to produce correct output. 19:33:43 So, dependently-typed combinator calculus. 19:33:53 ... 19:33:57 Specifically: a language with only combinators that has dependent types and is total (but not powerless). 19:34:01 (No lambda abstractions.) 19:34:03 alise answer me! 19:34:04 A compiler is code. Proving a compiler correct is a subset of proving code is correct. Why people concentrate on that one subclass eludes me. 19:34:04 Commence. 19:34:08 fax: answer WHAT 19:34:12 s/sub*/subcase/. 19:34:22 alise from earlier 19:34:25 cpressey: Uh? 19:34:32 fax: what 19:35:12 cpressey: It's fairly simple -- when your compiler is *incorrect*, you cannot rely on the compiler to generate correct code. 19:35:21 ugh alise why are you so mean 19:35:30 fax: I'm not, I just don't know what the fuck you want me to do 19:35:50 Please stop assuming you're the center of the universe and that I follow what you say above all others, I like you but please just repeat what you want me to reply to 19:36:39 cpressey: Proving a compiler correct is proving a function (Lang -> Lang) correct. Call it f. What you're saying is "Prove that semantics (f x) = semantics x". But if we wanted to prove f correct, we have to express the intended semantics. "Given the input x and the output x', prove that semantics x' = semantics x". 19:36:46 pikhq: Right, so proving programs correct is important. I get that. 19:36:51 So proving the compiler correct /is/ proving the compiler's output correct. 19:37:03 What I don't get is why this *special case* is so friggin' popular, esp. in theses. 19:37:29 because it's hard. 19:37:30 and important 19:37:32 alise, you just seem to sort of phase out when I link you stuff 19:37:35 see e.g. Reflections on Trusting Trust 19:37:43 cpressey: Because it's more important than most other cases. 19:37:45 fax: no I just don't respond to links that I am unable to interpret the context of; also, I did respond 19:37:49 I linked to an article linked to in that subreddit 19:37:53 Since almost everything is compiled. 19:38:01 alise, no there's a compilers book in there 19:38:15 fax: i didn't see 19:38:21 ah 19:38:24 Yet ultimately, everything is interpreted. 19:38:43 We should probably be proving our text editors correct, too. 19:40:32 Do you have any idea how much verification goes into making an x86 CPU? 19:40:33 cpressey, http://jaguar.it.miami.edu/~chris/formal_methods_in_the_movies/TheWizardOfOz.html 19:41:17 -!- alise_ has joined. 19:41:24 alise: Issues still slip on through on occasion, though. 19:41:35 Though the only such case I can think of is the FDIV bug on the Pentiums... 19:41:48 cpressey: We do not prove our editors correct because it is incredibly trivial to verify that they produce the correct results with a so-simple-there-cannot-be-any-bugs utility such as cat. 19:42:01 pikhq: Which is basically the reason WHY they do formal verification nowadays. 19:42:09 Indeed. 19:42:26 cpressey: For compilers, Reflections on Trusting Trust shows that it is pretty much /unknowable/ whether a compiler is correct. 19:42:45 Even if the compiler is not malicious, such errors could happen. And verifying that a huge program was compiled correctly? Good luck. 19:42:53 So we attack the problem at the source, and prove our compiler correct. 19:43:19 how does one get a degree sign in LaTeX? 19:43:30 in an equation that is 19:43:40 alise_: If you prove that the generated code is incorrect, you've caught a bug *regardless* of whether it was in the compiler or in the code being compiled. 19:43:54 * AnMaster looks at fizzie 19:44:23 cpressey: You don't understand - given a black-box compiler proving that your code was compiled correctly is almost impossible. 19:44:23 AnMaster: \circ or something 19:44:24 Consider: 19:44:33 AnMaster: See also http://detexify.kirelabs.org/classify.html 19:44:39 AnMaster: ^\circ, I think 19:44:48 When we prove the compiler correct, we do it by meticulously analysing every case it uses to compile constructs; we have direct access, we prove the atomic compilations correct, and their compositions. 19:44:51 Deewiant, hm okay 19:44:53 Voila, the compiler is Always Right. 19:44:55 well that works 19:44:58 -!- alise has quit (Ping timeout: 252 seconds). 19:45:01 I think I saw ^\circ used somewhere, yes. 19:45:02 cpressey: If we just have the input, and the output... where do you start? 19:45:03 AnMaster: I.e. raise it to the power of one circle :-P 19:45:09 You have to model how it was compiled first - basically, write your own compiler. 19:45:12 Deewiant, hah 19:45:15 "we do it by meticulously analysing every case it uses to compile constructs" -- *sigh* 19:45:18 Then you have to verify that each compilation is equal to how your model would compile it. 19:45:30 cpressey: But then we have to verify our now-very-real model compiler is correct, or it's useless. 19:45:34 alise_: You have the semantics of the program, and you have the semantics of the target language. That's where you start. 19:45:50 have you every actually done a formal correctness proof for a non-trivial compiler? 19:45:55 ever* 19:46:12 http://anthony.liekens.net/index.php/LaTeX/DegreesNotation -- that suggests either ^\circ (possibly with your own \newcommand) or the existing \degree from \usepackage{gensymb}. 19:46:20 fax: Would you prefer I went into the nitty-gritty when the abstarct principles are all that matter here? 19:46:26 fax: Me? No. But (as should be obvious) I have reasons for that. 19:46:36 cpressey, not you, alise :p 19:46:36 fizzie: I was thinking ^\circ. Thought it'd be too silly to say. 19:46:52 It's less silly than just ^o at the very least. :p 19:47:16 fax: For trivial compilers, the problem seems not too difficult, maybe even enjoyable if the compiler is written a certain way 19:48:27 * fax needs alise to get into the trenches 19:49:40 fax: But my ivory tower is so comfortable... 19:49:56 Besides, I refuse to do any serious work in anyone ELSE's language. They have cooties. 19:50:18 :P 19:54:51 Actually (to get back to the previous topic) the problem seems trivial if you construct your compiler compositionally (though I realize full well almost all production compilers aren't, but we were talking about functional languages.) If a->b is correct, and b->c is correct, then a->b->c = a->c is correct. 19:55:29 If a->b is correct, and c->d is correct, (a,c)->(b,d) is correct, assuming sane composition 19:56:26 cpressey: Now add full-program optimisations. 19:56:44 Oh yes. The problem AS USUAL is that someone wants it to GO FAST. 19:57:30 :-D 20:00:46 :( 20:00:57 this is not accurate 20:01:50 -!- alise_ has quit (Ping timeout: 252 seconds). 20:02:25 -!- alise has joined. 20:02:35 cpressey: Mind you, I don't plan on including a clever compiler in my OS. 20:02:46 It's near-the-metal, and cpus are really fast. So... 20:04:09 -!- lament has quit (Ping timeout: 260 seconds). 20:06:38 I'm simply disregarding all considerations of efficiency. 20:07:00 Waste of time to worry about wasting time. 20:07:20 -!- lament has joined. 20:07:59 cpressey: ah, words of truth 20:09:15 At the same time, I will continue to complain about web sites that are slow to load. I have a hypocrisy quota to reach, you see. 20:11:00 http://dadgum.com/james/performance.html 20:14:44 ping 20:15:39 alise: Why are you writing an Othello in Haskell? 20:15:49 Felt like it. :-) 20:21:23 Argh! 20:21:24 I need type-level functions. 20:21:29 :D 20:21:41 ...because I'm implementing a dependently-typed language. :-) 20:21:50 (But not for /that/ reason.) 20:23:09 othello and its rich internal type system... 20:23:45 <3 20:24:03 * alise steps back, examines his general structure. 20:24:04 Happy happy joy joy joy 20:24:14 Lam :: (Id a -> LC b) -> LC (a :-> b) was so nice, too. Sigh. 20:24:29 so you Lam-ent its loss? 20:24:32 You could even Show it. 20:24:40 Types: 20:24:53 pi (x:T). r 20:24:53 * 20:25:03 I don't believe in ZFC, I don't see why I should believe in dependent types. 20:25:03 in pi, T:* 20:25:11 hehe 20:25:21 Values: 20:25:26 ztheist 20:25:28 * cpressey proves himself 20:25:47 \(x:T).(e:R) : pi (x:T). R 20:26:08 alise why don't you write it in Coq (type functions!) then extract it to haskell 20:26:12 (f : pi (x:T). r) v : r[x=v] 20:26:16 if you do that it'll be a really sweet hack 20:26:26 fax: mm maybe 20:29:17 use monads ! 20:30:23 everything's better with monads! 20:30:58 sem' xs (App f x) = (sem xs f) (sem xs x) 20:31:00 not allowed :( 20:31:07 with 20:31:07 App :: LC (a –> b) -> LC a -> LC b 20:31:23 I guess I need to specifically specify f must be a Lam 20:31:37 whats xs? 20:31:38 how lame 20:31:47 fax: de bruijn housekeeping 20:32:02 actually I think it needs to be a function... maybe 20:32:14 wait, no 20:32:42 against inferred type `[(.) (forall a1) (LC a1)]' 20:32:44 lol 20:32:45 (.) 20:37:40 fax: sem' :: (Id t -> t) -> LC a -> a 20:37:44 sem' v (Var i@(Id n :: Id t)) = v i :: t 20:37:46 why doesn't this work :( 20:39:02 something to do with needing to enable a bunch of extensions that should really be the default? 20:39:39 already done 20:39:45 Couldn't match expected type `t' against inferred type `a' 20:39:47 :/ 20:40:16 do sem' :: (Id a -> a) -> LC a -> a :D 20:40:17 ohh 20:40:18 I just needed 20:40:22 (forall t. Id t -> t) 20:40:23 to be the type 20:40:25 duh 20:40:30 how can that be the right type? 20:40:34 what's Id t? 20:40:39 oh I see 20:41:07 can you implement (in a pure and safe way) STRefs this way? 20:43:43 -!- alise_ has joined. 20:44:44 -!- alise has quit (Ping timeout: 252 seconds). 20:53:01 -!- oerjan has quit (Quit: Good night). 20:54:07 othello is more fun than this 20:54:35 fax: I assume there's some hyper-monoidal structure for game boards :-P 20:58:12 fax: Reifying without _|_: 20:58:13 instance (TNat n) => TNat (S n) where reify _ = 1 + ((reify :: (n -> n) -> Integer) id) 20:58:15 Clever, huh? 20:58:38 In fact, you could even have reify :: Dummy n -> Integer where (data Dummy t = Dumb) 20:59:09 Dummy is basically values indexing on types :P 20:59:45 Well, sort of 21:13:42 Press Ctrl-# to continue! 21:17:12 wat 21:17:34 fax: is there any dependent language that lets you elide most of the obvious proofs and the like... I feel like I'm writing tons of obvious proofs except in haskell atm :) 21:17:58 coq 21:19:11 fax: you sure? 21:19:26 well I am interpreting 'elide' in a special way 21:21:46 that means "specify"? 21:23:15 yeah and prove them 21:23:19 lol 21:24:27 fax: http://www.reddit.com/r/dependent_types/comments/baf7g/wtypes_good_news_and_bad_news_laquo_epilogue/ why epigram 2 isn't broken 21:24:33 i think 21:25:04 from the murky depths http://sneezy.cs.nott.ac.uk/darcs/RDTP/2ndmeeting/ctm-3.JPG ... 21:27:21 fax: btw I think I understood your thing about induction from the logs 21:27:29 so what is mu-elim's actual type, I'm curious? 21:27:38 admittedly this is the rough kind of understanding, not the deep kind 21:28:20 huh 21:28:25 what the heck is going on 21:28:26 somehow 21:28:35 every X process ended up as STOPPed 21:28:48 killall -CONT seems to have helped *somewhat* 21:30:07 except I can't resume that dbus crap 21:30:16 it causes everything else to SIGSTOP again 21:30:21 Smells like cat food. 21:32:19 I should really devise a way to isomorph the pure data types with an efficient implementaiton. 21:32:21 *implementation 21:32:48 lol :D 21:33:16 what 21:33:39 I once read a PhD thesis were 70% of the ~200 pages was a transcript of a session with an interactive proof system. 21:33:44 *where 21:35:12 what the hell is going on 21:35:22 it all started when inkscape crashed 21:35:31 it seems that resulted in dbus crashing or something 21:35:52 ooh nice, gconfd is eating 100% CPU 21:38:39 -!- MigoMipo has quit. 21:39:11 * fax snooze 21:39:13 No! Sleep! 'Til Brooklyn! 21:39:39 cpressey: Formalised proofs are the future! 21:39:44 Although a transcript is probably not the best form. 21:39:45 brb 21:40:02 formal math is so difficult 21:40:24 but it's different than proving stuff on paper, and it's a bit different than programming too 21:40:34 it's a bit perverse 21:40:44 Can you say "thesis padding"? 21:40:51 heh 21:48:36 I'm probably going to try to include a proof checker in the language I'm working on. Not a prover though, that's just way too much work. But a proof checker is pretty simple. 21:48:54 how do you prevent LaTeX from including a date on the title page? 21:49:56 proof checker = type checker 21:50:33 proof checker is simple? :) 21:50:37 yes that is true 21:50:43 but it is hard to write proofs :P 21:50:45 = derivation checker 21:51:10 AnMaster: Use \date{} -- though it might be suboptimally spaced. 21:51:38 fizzie, hm spacing is important since I don't use a separate title page 21:52:37 Try it and see. If it's not good, you'll probably have to just do the titles manually; the usual \maketitle is not very customizable. 21:52:50 It's possible that it's clever enough to detect and special-case an empty date. 21:53:36 someone (fax) gimme the interpretation brackets 21:53:50 [[ ]] 21:53:59 qwrtuc6ybpoi;ytrweaqstr4jy;poin0[;qwo'm[pn;iqw;p0oi[ie3ye3wdrty;piyuhtw2qwqaretshygu,-';juytdrtuh0poesr48#'[p0oiyhtdryk]=' 21:54:02 fax: >:| 21:54:06 :p 21:54:16 hands in the air 21:54:16 you dirty qwerty user! 21:54:27 yeah 21:56:53 -!- Oranjer has joined. 21:57:45 coq proofs don't look nearly enough like real mathematical proofs 21:57:47 imo 21:58:00 coq? 21:58:04 kazonk; whup f; bop; ligxs 21:58:09 Oranjer: Coq. 21:58:13 Theorem prover, programming language. 21:58:19 ooh, okay 21:59:43 alise they shouldn't look like what you find in textbooks 21:59:59 Trivial example of what I have in mind: http://dpaste.com/169655/ 22:00:20 alise, well it has been pointed out by Freek that these proof assistants do look very much like Euclids Elements in style 22:00:30 but I mean on paper stuff is a different world 22:00:44 yeah but it shouldn't be a different world! 22:00:55 paper can't compute (yet!) :P 22:01:13 imo we should all be using dependent formal proofs everywhere 22:01:28 and with say coq proofs that is .. not practical 22:02:05 :| 22:02:10 more of your bullshit 22:02:31 "dependent formal" 22:02:33 what 22:03:15 fax: you can just not listen to me, you know 22:04:10 but ignoring people is the center that all totaltarianism revolves around! 22:04:20 Dude, we're still grappling with sophisticated SE concepts like "comments" and "tests" 22:07:28 I am currently trying to add a feature to a swath of our code that another engineer accurately described as an "accretion" 22:07:57 I would LOVE to be able to prove some simple properties about this code, if only to figure out what the variable names should REALLY be called instead of "ctx" and "data" 22:08:03 cpressey: :-D 22:08:50 But it is written in a mainstream programming language, which means, who KNOWS what the semantics of this code REALLY are? How do you even begin to write a proof when your axioms are based on "well, it's implemented this way, on this os, on this cpu" 22:08:53 ? 22:09:43 Programming is a shithole/ 22:09:45 *shithole. 22:10:03 * AnMaster gives up on this 22:10:17 yay 22:10:24 * AnMaster uses a -1.5 em vertical spacer and then violently hits LaTeX with it 22:10:33 that seems to work 22:11:34 it is is an extremely hackish way to get two minipages beside each other. One containing a circuit diagram, the other containing values for components in an eqnarray environment 22:11:35 We don't even have debuggers that aren't crap. (Where did this value come from? Tell me. No, you can't, can you.) 22:11:50 fizzie, wonderfully hackish in factr 22:11:53 fact* 22:13:49 cpressey: Indeed. 22:14:03 I tend to often end up with some negative spaces here and there too, though I always feel I'm doing something wrong. 22:14:05 Actually you've made me think: perhaps debuggers are isomorphic to proof assistants. 22:14:14 (Except you never get around to proving anything.) 22:14:32 alise_: They're certainly related. 22:14:41 It's all about tracing. 22:16:01 You need to visualize the innards to see why the end result is not what you expected. 22:16:30 * fax visualize your innards 22:16:35 Eww 22:16:50 fizzie, actually that wasn't just a negative space. it was a -6 em vertical spacer at the top of a mini page 22:17:00 to "fake" it being at level with the other one 22:17:31 somehow the display style equation in that mini page caused it to fill out the whole page when it came to vertical placement 22:19:21 Chrome's search feature is a suckfest ... and not the good kind. 22:20:04 Gregor: Howso? 22:20:12 Just type in what you want and press enter. ...Hooray. 22:20:29 Or if you're going to search for something that looks like a URL, ?poop://lol. 22:20:39 I think there's even a shortcut for Ctrl-L + ? 22:20:41 Nonono, search on a page, its "find" feature 22:20:54 Whatever you want to call it. 22:22:24 Oh 22:22:25 Why? 22:23:18 1) What was wrong with '/' and type? 2) The most common use of find on a page for me is getting to a link to click it. But when I hit 'enter', it goes on to the next effing match, it doesn't click the link >_< 22:25:19 does it support regex? 22:28:19 Gregor: (1) Oh, Ctrl-F, how horrible. (2) Okay. 22:28:28 AnMaster: No. Because it's meant for people to use. Quickly. 22:28:35 And I can't even fall back to print statements without pulling my hair out because the values have magical stringification so they throw an exception when I try to print them. 22:28:40 Ctrl is a lot farther from the home row than / is, if searching is common then it's annoying. 22:28:46 cpressey: :-D 22:28:48 -!- tombom has quit (Quit: Leaving). 22:28:58 But that's a minor issue, it's the no-click thing that annoys me, surely I don't need to tab to the right link ... 22:29:15 Gregor: Chrome is a bit mouse-based. There's an extension that lets you do /foo and the like. 22:29:54 http://github.com/philc/vimium 22:31:07 alise_, you know, I quite often use egrep as a quick way to search 22:31:15 AnMaster: you are not technicaly human though. 22:31:25 alise_, neither are you if you know any regex 22:31:51 Gregor: Ctrl is *on* the home row. 22:32:05 pikhq: Screw you Unixy Solaris keyboard 22:32:20 pikhq, picture 22:32:28 AnMaster: I just xmodmap'd. 22:32:39 axiom interact : Interaction p f t -> World s -> {p s} -> (t, World (f s)) -- this, but with some sort of way to mark the previous world as invalid 22:32:49 (I'm trying to formulate all IO as one single interaction axiom.) 22:32:51 pikhq, ah 22:32:57 pikhq, to caps lock? 22:33:06 AnMaster: Yeah. 22:33:43 alise_: Uniqueness type? 22:33:56 pikhq: Thanks for complicating up my theory :P 22:34:01 Heheh. 22:34:25 basically, (World s) represents a world with conditions s 22:34:44 (Interaction p f t) is an interaction on worlds; p is Conditions -> Prop 22:34:52 meaning "is this interaction acceptable under these conditions?" 22:35:05 for instance, a read-from-stream interaction would have a p representing that the buffer must be open in the world 22:35:11 f is Conditions -> Conditions 22:35:17 representing the effect it has on the conditions of the world 22:35:28 a close-stream interaction would require that the stream be open in p, and make it closed in f 22:35:35 and t is the type of the result it returns 22:35:50 dependent types would mean that closing an already-closed file would actually be a type error. 22:36:41 yes 22:36:51 conor mcbride did some sort of thing on this i know 22:37:21 and idris 22:37:51 heh i'm actualy reading idris stuff now 22:37:55 hmm 22:37:57 maybe the issue is World 22:38:28 dunno 22:40:18 fax: how does idris do it? 22:41:47 theres papers on it 22:42:01 -!- kar8nga has quit (Remote host closed the connection). 22:42:02 yeah but i can't find them 22:42:32 http://www.cs.st-andrews.ac.uk/~eb/drafts/tfp08.pdf 22:42:35 http://www.cs.st-andrews.ac.uk/~eb/drafts/ngna2009-dsl.pdf 22:42:51 Make a dependent type system where trying to unserialize a corrupt string is a type error! 22:45:00 cpressey: Possible but a bit useless since you have to prove it. 22:45:13 So you'll basically do if corrupt x then fail else yay (long proof) 22:45:26 Better to have the serialiser return, say, Maybe DeserialisedType 22:45:41 "Better", sure. 22:46:44 dependent types would mean that closing an already-closed file would actually be a type error. <-- anything wrong with that? 22:46:46 fax: Just to confirm. http://www.cs.st-andrews.ac.uk/~eb/drafts/tfp08.pdf is not about interaction, yes? 22:46:53 I skimmed it and didn't see anything related. 22:46:58 AnMaster: It's a good thing. Duh. 22:47:07 alise_, what I thought 22:47:48 What about failing to close a file? 22:48:18 I mean, from a practical perspective, a single guard on "oops, this file handle is already closed" is nothing. But leaking file descriptors is a real problem. 22:49:08 cpressey: Actually, yeah, you could. 22:49:25 Make interact continuation-y and require that the world yielded by the continuation satisfies another bit of the Interaction. 22:49:26 cpressey, also closing a file could fail 22:49:36 open-file would have as its ever-ever-postcondition that the file is closed. 22:49:56 cpressey, isn't fclose() in C allowed to fail if data is buffered but there is no space to write it? 22:50:21 Yes, fclose() can fail. 22:50:34 so, well you could have to propagate some such errors to your high level language 22:50:39 cpressey: i think 22:51:29 Scylla and Charybdis 22:51:50 Indeed. 22:52:20 -!- oklokok has quit (Read error: Connection reset by peer). 22:52:38 Scylla and Charybdis <-- ? 22:52:46 the latter means "ircd software" to me 22:53:01 (the one freenode uses nowdays is based on charybdis) 22:54:05 Gogle it. 22:54:08 *Google 22:54:31 alise_, greek mythology? 22:54:45 No, the other Scylla and Charybdis. 22:55:37 alise_, [The phrase "between Scylla and Charybdis" has come to mean being in a state where one is between two dangers and moving away from one will cause you to come closer to the other.]? 22:56:27 No, the other Scylla and Charybdis. 22:56:58 alise_, I only get idiom and mythology hits on my first two results pages 22:57:12 haven't checked further 22:57:22 alise_, so what the heck are you talking about 22:57:49 The other Scylla and Charybdis. 22:57:58 alise_, there is no such hit for me 22:58:02 so please explain 22:58:07 The other Scylla and Charybdis. 22:58:50 okay, now you are just trolling 23:00:00 It's not my fault you're an idiot. 23:00:35 for not figuring out you were trolling sooner? perhaps 23:00:59 I had a hard time imaging you were trolling at first. 23:01:01 For convenience, this function may accept either a string, a list, a dictionary, or a file. 23:01:28 Yes, very convenient. 23:01:53 -!- madbr has joined. 23:02:16 cpressey: Ouch. 23:02:54 cpressey: Ever considered just becoming a hermit? 23:02:57 A hermit with internet access. 23:04:31 Well yes, if it wasn't for the whole property-tax thing. 23:05:09 cpressey: Caves. They have none. 23:05:37 Then there's that whole evading-park-rangers thing. 23:06:39 cpressey: Beats 9-5, right? 23:07:21 Totally. I should have gone to Hermit School when I had the chance... 23:08:15 I'm basically banking on becoming a tenured professor because of my sheer genius without trying at some point. 23:09:02 Well, then practise backstabbing now, is my advice. 23:09:10 heh 23:09:12 You'll need it in grad school. 23:10:29 Remember when I said sheer genius? 23:10:33 I'll do it and NOT EVEN REALISE IT. 23:10:43 Set myself to auto-pilot, baby. 23:12:28 -!- oklokok has joined. 23:12:32 ho oklokok 23:12:44 alise tenured how? 23:13:12 the badass kind that means I can do nothing and never get fired 23:13:17 (note: I do not actually believe any of this0 23:13:23 *this) 23:13:29 like Zeilberger 23:14:21 "Academic tenure is primarily intended to guarantee the right to academic freedom: it protects teachers and researchers when they dissent from prevailing opinion, openly disagree with authorities of any sort, or spend time on unfashionable topics" 23:14:33 "Zeilberger considers himself an ultrafinitist." Wow, they actually exist?? 23:14:46 yeah so I do 23:14:58 * cpressey is impressed 23:15:00 ultrafinitist? what does that even mean? 23:15:04 I don't beleive that a^b terminates 23:15:45 Like other strict finitists, ultrafinitists deny the existence of the infinite set N of natural numbers, on the grounds that it can never be completed. In addition, ultrafinitists are concerned with our own physical restrictions in constructing (even finite) mathematical objects. Thus some ultrafinitists will deny the existence of, for example, the floor of the first Skewes' number, which is a huge number defined using the expone 23:15:46 XD 23:15:56 It's like argument by lack of imagination 23:16:12 Argument by well our current computers can't do it/well our current understanding of physics means we can't do it 23:16:15 Or by vagary in definition of "exists" 23:16:20 fax: surely you don't consider yourself such. 23:16:45 I can in fact produce an object that is of some arbitrary numerical length. By defining the units appropriately. 23:16:47 So ultrafinitists believe there to be a largest number. I wonder what it is :) 23:17:01 I wonder what it is _today_. 23:17:07 :-D 23:17:13 For instance, I have a meter stick that is roughly G 1/G-meters. 23:17:17 yeah that's kooky 23:17:24 I'm not completely alien to their ideas, but I don't think I am one 23:17:27 Who pinged me? 23:17:44 alise_: the largest number is 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875897 23:17:57 lament: 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875898 23:17:59 lament: 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875898 23:18:02 Suck it. 23:18:03 haha 23:18:10 that's not a number 23:18:15 just a meaningless string of digits 23:18:21 oh lament is a 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875897-finitist 23:18:22 it is a number 23:18:29 you could argue that numbers larger than X don't have any practical use, that's kinda dumb 23:18:33 It's the successor of the largest number you proclaimed. 23:18:36 it doesn't mean anything. Numbers can't be that large. 23:18:39 it's not a number 23:18:47 lament: Define number. 23:18:50 no u 23:18:52 I'm a 2^16-finitist 23:19:16 fax: lament thinks such a finitism doesn't exist 23:19:17 so there 23:19:17 data Number = Zero | Succ Number 23:19:48 pikhq, fix Succ -- where is your arithmetic now? 23:19:51 math isn't haskell 23:19:55 Nat := Mu (Unit &) 23:19:58 lament, ask #haskell :x 23:20:09 Succ it. 23:20:09 why? I'm more qualified than #haskell 23:20:12 fax: Congrats, you just defined infinity. 23:20:15 why doesn't oklocorpse talk to me :( 23:20:17 i've a math degree, most people in #haskell don't. 23:20:21 oklokok oklokok oklokok 23:20:24 pikhq: ugh, no 23:20:33 _|_Nat is not infinity 23:20:59 alise_: Fine, fine. He's defined _|_ :: Number. 23:21:10 lament: hey did you specialize? 23:21:15 at some point 23:21:16 no 23:21:18 why doesn't oklocorpse talk to me :( <-- I guess he got tried of saying BRAAAINS? 23:22:27 lament :( 23:22:53 -!- oklokok has quit (Ping timeout: 260 seconds). 23:23:45 -!- oklokok has joined. 23:24:00 damn postmodernists 23:24:10 postpostmodernism 23:25:39 oklokok? 23:26:00 ω exists because I can describe it (I can describe Atlantis too) 23:30:08 ω is shorthand for some definition in some system of axioms. in those, it is presumably a coherent concept 23:30:22 the problem is that you want Atlantis to be a concept of this world. and we don't control /our/ axioms. 23:30:48 God no, I don't want that. They would cream us with their nuclear laser missiles! 23:31:05 :D 23:31:21 * fax sighs there are so many things I want to do that I am unable to do any of them 23:31:42 I love how the Halting Problem is equivalent to the Entscheidungsproblem. 23:32:04 yeah that's a good one 23:33:46 meeee 23:33:48 s/things/women 23:34:27 decide : (∀a. Prog a → Bool) → (P : Prog (Nat → Bool)) → Bool 23:34:28 decide H P = ¬(H 《i := 0. Do: If ¬(P i), break. i := i + 1. Loop. 》) 23:34:35 Or thereabouts. 23:35:55 hi oklookpaoufpadda 23:36:02 I got something to show you 23:36:14 www.stanford.edu/~dgleich/publications/finite-calculus.pdf ! 23:36:24 you said you didn't like analysis because it wasn't finite enough 23:38:09 well i'm not sure that's exactly that i said :D 23:38:12 but i'll check 23:38:12 http://i43.tinypic.com/2v8s9w8.png 23:38:15 whoope 23:38:16 I see fax doesn't like my proof :( 23:38:19 oklokok this stuff is so cool though! 23:38:20 Scientist: Yeah, the expansion of the universe is accelerating and there seems to be stuff that seems to to exert negative gravity and that stuff is dark energy 23:38:22 seriously I have to master it 23:38:23 Dude: and what is that, what is it made of? 23:38:24 sorry spam 23:38:26 Scientist: Really we have no fucking clue, we hoped you'd stop asking after hearing "dark energy" 23:38:30 bye 23:38:35 alise: I just assumed it was correct 23:38:39 Wareya: yawn 23:38:52 yet another lol-they-call-it-dark-it-must-just-be-made-up bullshit story 23:38:59 be ignorant elsewhere :| 23:39:35 decide on the reals is interesting btw 23:39:36 who said I agree? 23:39:39 it's just funny 23:39:39 nested halting-checking 23:39:40 byer 23:40:09 I can describe black holes 23:40:47 [Note to the editor: Insert a "your mom" joke here.] 23:40:51 [No. -Ed] 23:42:21 alise_, that's what she said! 23:42:25 night → 23:46:29 http://en.wikipedia.org/wiki/Clifford_Stoll The acme klein bottle guy is also the caught Markus Hess guy and also thought interwebs would never catch on 23:50:34 oklopkoupuo i think this is a precursor to Umbral Calculus 23:50:52 not entirely sure 23:53:11 oklokok btw I have not done OR yet :( 23:53:28 actually I was going to try and code that stuff into epigram just for fun but it was too hard 23:53:43 (I couldn't even define a tree type) 23:53:54 alise_, what did you think of my proof? 23:53:58 you can ask for hints if you want 23:54:15 cpressey: which proof? 23:54:16 oklokok, well if you had an intermediate problem between AND and OR that would be good :p 23:54:28 http://dpaste.com/169655/ 23:54:48 It's wrong. The last thing on the 3rd line should be "Stack'" 23:55:05 cpressey: You've neglected to specify what you're proving, for starters. 23:55:18 Looks more like an evaluation to me, 23:55:19 *me. 23:55:43 Theorem is always: first line and last line of "proof" section are equal. 23:55:46 well the thing is 23:55:55 cpressey: That's a rubbish proof system 23:55:56 What is a proof if not an evaluation? 23:55:56 Gian-Carlo Rota began his career as a functional analyst, but changed directions and became a distinguished combinatorialist. -- he helped develop this umbral calculus 23:55:59 for most things that are in the middle, you'll need to have OR already 23:56:02 cpressey: A proof is a value 23:56:02 i mean most things i know 23:56:18 fax: link to that book that had tons of proofs in i think coq 23:56:18 Well, sure, everything is a value 23:56:18 if you can live with using OR before knowing how to compile it, then yeah i have a few 23:56:21 supposedly from the future 23:56:27 cpressey: No, quite literally 23:56:34 p : P where P : Prop = p is a proof of P 23:57:01 oklokok oh, I was thinking about AxB = BxA, it seems to only have solutions like A = (mnux)^n(mnu), B = ..^m... 23:57:02 there's a reason proof assistants are all dependent and whatnot, it's because this is the way things make sense in computing 23:57:27 alise, I don't know what you are referring to 23:57:38 not all proof assistants work on dependent type theory 23:57:53 but dependent type theory is really an excellent way to do it imo 23:58:13 if |A|>|B|, then TxB = xBT, which gives you all the solutions 23:58:23 fax: well yeah 23:58:31 oklokok huh?? 23:58:33 there are a few basic techniques that get you through most things 23:58:37 not all-are dependent 23:58:41 but are all-dependent-and-whatnot 23:58:50 fax: i just substituted A = BT because |A| > |B| 23:58:59 there's a symmetric case for B > A 23:59:05 hm 23:59:12 ah! 23:59:17 oh and after that you already have all the solutions 23:59:25 if you don't see it... see fundamental theorem 23:59:29 ;) 23:59:35 alise_: To be clear, it's not a proof finder, it's only a way to write out proofs so that they can be checked. 23:59:43 cpressey: Of course. 23:59:46 we should probably be doing this in pm, i'm not sure it's as entertaining to others 23:59:49 And since a proof is a series of derivations, I don't see anything wrong with this. 23:59:54 well actually 23:59:59 we should be doing this tomorrow