00:02:53 but isn't the way board game players interact, taking turns to manipulate some state, game theoretical stuff 00:04:12 i guess not really 00:04:45 hmm 00:05:04 A|(B C) = (A|B) (A|C), obviously 00:05:15 but does A (B|C) = (A B)|(A C)? 00:05:23 where A B is common parts and A|B is combination 00:06:16 isn't the study of general properties of game trees an important part of game theory? at least the one book i've read talks about it a lot. 00:08:09 oklopol: winning theory could be your chance to include all the ridiculous ideas you've ever thought of into mathematics 00:08:23 so what's the symbol for A totally winning B? 00:08:31 i'm not sure how that maps to what category theory is to algebra though 00:08:42 Tw(A,B)? TW(A,B)? TwAB? A op B? 00:09:02 as always, A | B = A <==> A > B 00:09:13 or maybe more like >= 00:10:40 of course 00:10:43 but totally winning is about strategy 00:11:17 I think op is the best route as you know, operators are awesome and you can invent symbols for them 00:11:24 doesn't mean we should get too creative when defining the algebra of games 00:11:30 Whyever not. 00:11:38 indeedso iguess not. 00:11:48 or do i mean yes 00:11:55 Circled > would be nice. 00:12:02 i'm not really following any of these conversations 00:12:03 Might confuse with just >, but isn't that a good thing? 00:12:09 :| 00:12:14 yeah! 00:16:34 -!- alise has quit (Ping timeout: 252 seconds). 00:19:16 -!- Oranjer has joined. 00:30:42 -!- alise has joined. 00:30:55 what did i miss since what i last said? 00:32:05 beats me! 00:34:15 alise: < oklopol> yeah! 00:34:27 that is it? :P 00:35:25 well also "02:17… Oranjer has joined #esoteric" 00:35:26 that's sort of relevant to what Oranjer said 00:36:16 what is it with chess ais, you give them a huge amount of time because you don't wanna feel pressure and they just sit about doing nothing 00:36:27 you're a computer. you don't panic. stop wasting my time 00:37:50 chess is too hard anyway 00:38:23 what 00:38:37 lament: i don't care, it's entertaining 00:38:47 -!- Ilari has quit (Ping timeout: 268 seconds). 00:38:58 oh I think i may just have set up the ai wrongly 00:39:01 it just sat there and ran out of time 00:39:06 alise: AIs do use up time 00:39:22 coppro: yes but this one played fine with little time. also, as i said, it ended up not moving at all. 00:39:58 how does it end up not moving 00:40:19 lament: yeah i never learned how knights move 00:40:31 * alise tries a different type of clock 00:40:33 Oranjer: by not moving in the allocated time 00:40:42 I think they do the Kansas City Shuffle, oklopol 00:41:22 two steps this way and then one step this way oh and by the way YOU CAN FLY OVER OTHER PIECES, that's just insane 00:41:59 it's just a game after all 00:42:06 flying horses 00:42:25 -!- cal153 has quit. 00:42:47 Chess: the only playable Allegory of Islam 00:43:31 lament: your responses are really boring today, are you drunk on life? 00:43:54 i'm sober 00:44:00 Oranjer: you are way too postmodern 00:44:11 how so? 00:44:18 lament: 00:44:22 -!- Ilari has joined. 00:44:25 Muhammed flys somewhere on a flying ass 00:44:53 Muhammad, sorry 00:45:26 oklopol: empty string 00:49:24 -!- cal153 has joined. 00:57:20 -!- adu has joined. 01:00:10 -!- coppro has quit (Ping timeout: 245 seconds). 01:11:51 In which I play Chess extremely shittily: 01:11:52 1. b4 c6 {+0.17/8} 2. Nc3 Nf6 {+0.31/9} 3. Na4 d6 {+0.21/9} 4. c4 g6 {+0.06/8} 5. d4 Be6 {+0.14/8} 6. c5 Na6 {+0.06/9} 7. d5 Nxd5 {+0.79/8} 8. b5 cxb5 {+1.70/10} 9. e4 Qa5+ {+1.61/10} 10. Bd2 Qxa4 {+1.71/11} 11. Qxa4 bxa4 {+1.98/10} 12. exd5 Bxd5 {+2.00/10} 13. a3 Nxc5 {+3.09/9} 14. Ba5 Nb3 {+3.00/9} 15. Rb1 Bg7 {+3.82/10} 16. Bc7 Rc8 {+5.19/10} 17. Ba5 Nxa5 {+5.87/10} 18. g4 Bxh1 {+10.37/10} 19. Nf3 Bxf3 {+13.43/11} 20. Be2 Bxe2 01:12:06 23. Rb4 Rxa3 {+14.69/9} 24. Rb5 Rh3 {+14.96/8} 25. g5 a3 {+17.63/9} 26. f4 a2 {+22.11/9} 27. Rc5 bxc5 {+26.91/9} 28. f5 gxf5 {+27.85/9} 29. Ke1 Rxh2 {+79.98/28} 30. Kd1 a1=Q# {+79.99/28} 01:12:11 Admittedly a few mistakes were due to the mouse slipping. 01:12:27 That probably made the already ridiculous difference in skill vs the computer vastly worse 01:12:38 But hey, it was entertaining. I am awfully bad though. 01:13:48 how does one read this notation 01:13:48 can the computer give an estimate of how much you sucked? 01:16:16 Oranjer: ignore the bits in {}s 01:16:23 and then just google chess move notation 01:16:27 i'm white 01:16:29 obviously 01:16:30 hi 01:16:38 lament: probably, but i don't feel like hating myself that badly 01:17:34 alise 01:17:51 fax 01:18:00 hello 01:18:03 hello 01:18:18 I love finite calculus 01:18:27 ok zeilberger 01:18:34 ceil(burger) 01:18:38 failculus 01:18:47 it isn't really very calculusy tbh :p 01:19:04 it blows my mind that the are so many stiking similarities with the real calculus 01:20:05 it blows my mind that this blows your mind 01:20:23 given that calculus is obviously the limit of finite calculus 01:20:31 well 1 is basically the infinitesimal of the integers :P 01:20:47 finite calculus isn't calculus on integers 01:20:56 i know 01:21:09 i know you know, i just like saying it 01:21:11 it's catchy 01:21:18 ?? 01:21:22 it's not calculus on integers? 01:21:28 are you reading the same paper as me? :P 01:21:49 oh well it's calculus from integers 01:22:02 but the functions still go to R 01:22:11 fax: why not on booleans 01:22:12 mine are Z -> Z 01:22:17 boolean calculus, do it now 01:22:24 alise, I am actually reading George Booles paper on this right now 01:22:28 er book 01:22:39 haha man I'm laughing too much at the idea of boolean calculus 01:22:53 * fax frowns 01:23:00 fax: no you /must/ do it on Bool -> Bool where true : Bool, false : Bool and nothing else 01:23:03 well the reason the paper doesn't talk about Z -> R, i think, is that integers always sum to integers, so you can restrict it that way, unlike normal calculus 01:23:11 I guess I'm basically asking for calculus from naturals mod 2 01:23:13 so DO IT 01:23:16 >:3 01:23:34 -!- augur has quit (Ping timeout: 264 seconds). 01:24:01 well it could be Q -> Q also 01:24:03 but that's not as elegant 01:24:12 why are you talking 01:24:17 boolean calculus 01:24:17 now 01:24:28 alise, it's your idea, you do it! 01:24:41 i don't have a cock compiler 01:24:50 just s/Z/Bool/ in your code, job done 01:24:56 um :P that wont do it 01:25:02 i think it's very elegant from Z to R 01:25:06 hey I just realized Bool is a field 01:25:24 what's Bool? 01:25:27 oklopol, why is Z -> R better than Z -> Z? 01:26:05 gf 01:26:08 true/true = true 01:26:11 true/false = undefined 01:26:17 that's one fucking awesome field xD 01:26:19 "= undefined" *barf* 01:26:26 as in "is undefined" 01:26:27 because if we consider Z a measure space with cardinality as the measure, then sums are just integrals 01:26:29 false/true = false 01:26:32 false/false is undefined 01:26:40 *unbarf* 01:26:41 and with integration we usually have functions from our measure space to R. 01:26:42 so basically X/true = X anything else is undefined 01:27:04 oklopol, wait what 01:27:07 so the multiplicative inverse is 01:27:10 true^-1 = true 01:27:12 that's it 01:27:16 worst field ever 01:27:31 oklopol, ooh I wonder if there's a Z[i] calculus with all the nice harmonic, holomorphic stuff 01:27:31 then again multiplication is boring on booleans anyway 01:27:33 whoa 01:27:38 multiplication is division on booleans 01:27:43 wait no 01:27:49 except for half of it (/false) >_< 01:27:53 alise, unitary calculus!! 01:28:02 fax: the crazy dude's paper talked about discrete analytic functions 01:28:06 for all the cases where / is defined on bools it is identical to * 01:28:15 01:27 < alise> for all the cases where / is defined on bools it is identical to * 01:28:19 oops 01:28:24 oklopol: if you're using his notation you say R but you mean hZ_p 01:28:25 or mentioned them 01:28:26 looked neat 01:28:29 (where Z is a finite set) 01:28:37 do not pervert /our/ discourse :P 01:28:52 tbh addition on booleans is pretty nice, being xor 01:28:57 hmmmm 01:29:18 true - true = false; true - false = true; false - true = true; false - false = false; 01:29:19 heh - = + too 01:29:23 this is the best discovery I have made :)))))) 01:29:28 fax: what is 01:29:28 finding this finite calculus 01:29:36 dude it's just some addition and subtraction 01:30:48 hey fax DID YOU KNOW you also have exponentiation on booleans 01:30:54 x^true = x; otherwise undefined 01:31:04 lol 01:31:04 in fact, you can even use the ackermann function on them. 01:31:07 it's clear sums are integrals because every function is simple 01:31:07 from Z, with the usual measure 01:31:07 err wait what 01:31:07 that's bullshit, let me gather myself. 01:31:09 okay maybe it's not completely obvious 01:31:11 "Vladimir Arnold forcefully stated in one of his books that it is wrong to think about finite difference equations as approximations of differential equations. It is the differential equation which approximates finite difference laws of physics" 01:31:12 now you have INFINITE OPERATORS!!!!!!!!! 01:31:39 so fax is now the fifth ultrafinitist i gather 01:35:20 this pleases me 01:35:30 fax: I'll love you if you make a Coq module with ultrafinitist definitions of the following, paramaterised on the rational h and the prime p: Naturals, so that there is no prime greater than p; Integers, presumably with each half of the integers dedicated to a sign; Rationals, divided once more (h must fit into one of these); and Reals, defined as hZ_p. 01:35:48 Along with associated operations, the calculus he defines, and properties. 01:35:51 alise, I will help you do it :) 01:35:54 And by love you, I mean hate you love you. 01:36:06 fax: Well... I started writing it in my language but couldn't be bothered. 01:36:10 alise, I should implement (normal) construtive reals though 01:36:21 those are easy 01:36:30 following the sketch in my constructie functional analysis text 01:37:07 Sigma (f:Q+->Q), Forall (e1,e2:Q+), abs (f e1 - f e2) <= e1 + e2 01:37:08 boring 01:37:19 fax: now do it, ultrafinitistic peon 01:39:53 fax: Actually I suppose that all those sets don't neccessarily have to have the same size because they all coexist. 01:40:19 So having the integers be twice the size of the naturals (minus 1, because there's only one 0...) and having rationals be the size of the naturals plus the integers would be OK. 01:40:31 The reals have to be hZ_p by Order of Zeilberger. 01:42:30 The nice thing is that we don't need any pesky functions or anything to define these because there's a simple, finite number of cases. 01:46:53 p would be what? The largest known* mersenne prime (* known by http://coqprime.gforge.inria.fr/ ) 01:47:10 p and h are parameters to the module 01:47:43 they are universal constants like physical ones but we don't know what they are (zeilberger says that the True Value either p or h - i forget which - is unknowable so uh whatever) 01:47:50 so we just plug in values we like. 01:48:10 -!- augur has joined. 01:48:22 Time for a nick change. 01:48:39 -!- uorygl has changed nick to uorygl[hireMe]. 01:48:43 :P 01:48:45 fax: if you have an awful lot of cpu time on your hands the largest mersenne prime would be a good choice for p, yes. 01:49:03 h would be the result of pressing 0., holding down 0 for a long while, then pressing 1, probably. 01:49:23 shouldn't h come from a physical/science experiment 01:49:28 like the fine structure constant or something 01:49:43 Zeilberger claims they are separate to physical constraints and that he is a platonist. 01:50:01 Since we are following his school of ultrafinitism, not the usual physical-constraints one, that is not required. 01:50:14 1/p is a good value for h if you have that in your system. 01:50:26 What is hZ_p? 01:50:30 p is a natural and rationals = size of naturals + size of integers, so 01:50:36 1/p should always be acceptable 01:50:42 uorygl[hireMe]: Z is the integers 01:50:44 _p is subscript p 01:50:54 And h is an h? 01:50:57 Zeilberger, an ultrafinitist that believes no infinite sets exist, defines the reals as hZ_p 01:50:59 That explains so much. 01:51:06 where h is a very, very small number 01:51:09 and p is a very, very large prime 01:51:22 lol 01:51:24 01:50 < uorygl[hireMe]> That explains so much. 01:51:26 ^^^^ lol 01:51:39 So what does hZ_p mean? 01:51:50 It means hZ_p. :-P 01:52:04 That is not a definition! 01:52:23 Or, if it is a definition, then your mom is a perfectly good model of hZ_p. 01:52:27 Since your mom is your mom. 01:52:29 'Tis true 01:53:37 Z_p = Z/Zp I guess? 01:53:49 Galois field 01:53:51 Yeah, I figure Z_p is the integers modulo p. 01:53:57 I have no idea what the h is supposed to be. 01:54:13 F_p = Z/pZ 01:54:27 h is the fundamental mesh constant, it's smaller than 1 01:54:42 so hZ_p = {...-h,0,h,2h,3h,...} 01:54:56 h: It's Smaller Than One. 01:55:04 So you multiply each number by h? 01:56:08 lol 01:56:20 alise you should make slogans 01:56:22 so if h is the fundamental mesh constant, what's the cool name for p 01:56:39 uorygl this is my interpretation, but I am by no mean an expert on this 01:57:41 it doesn't actually do anything 01:57:42 Hmm, ultrafinitists don't even let you have a type of types. 01:57:54 After all, it's infinite. 01:58:00 Unless you have a finite number of sets, which would be cool. 01:58:03 oklopol: what doesn't? 02:00:01 I guess the best thing is to have the integers be of size p. 02:00:43 Which means that the naturals are of size (p+1)/2. 02:00:58 What does let you have a type of types? 02:01:05 So the rationals are of size p+((p+1)/2). 02:01:11 I know of... not many systems under which that's possible. 02:01:12 uorygl[hireMe]: Anything? 02:01:14 Nat : Set. 02:01:27 Yes, but Set !: Set. 02:01:38 Obviously. 02:01:43 But Set is still infinite. 02:02:08 So, the reals have the same size as the integers. 02:02:16 Which means that the reals are smaller than the rationals. 02:02:23 This Makes No Sense (not that ultrafinitism does); start over. 02:02:41 The naturals are of size (p+1)/2. 02:02:44 The integers are of size p. 02:02:52 your mom 02:02:52 The rationals are of size p. 02:03:06 Half negative, half positive. 02:03:11 also the h 02:03:19 So (p-1)/2 each. 02:03:26 Here's some ultrafinitism for you: take ZFC, remove the axiom of infinity, add an axiom of non-infinity. 02:03:52 fax: i don't know coq man I can't do this :( 02:06:34 alise, (p-1)/2 is valid Coq 02:07:09 yes it is 02:09:09 hmm 02:09:13 the size of the integers must be prime 02:09:41 that would make integers a field - weird 02:10:01 isn't that awesome not weird :) 02:10:14 see these are the possibilities ultrafinitism gives you dude 02:10:28 lol I will ttyl 02:10:37 I have to go 02:10:52 * Sgeo should have gotten an F on his history exam. Instead, I got a B+ 02:11:27 1234567890123456789012353 is a prime number 02:12:16 Sgeo: you've turned into a history person! 02:13:03 an historical personage 02:13:36 I got a 36/50 02:19:01 Things about the rationals: 1/p is a rational. 02:19:14 So, for every integer, there are p elements in the rationals for it. 02:19:26 p is the maximum size of a set. So, the rationals suck. 02:19:30 So, I must sacrifice something. 02:19:34 I sacrifice 1/p. 02:19:34 -!- Asztal has quit (Ping timeout: 265 seconds). 02:21:23 -!- fax has quit (Quit: 1234567890123456789012353). 02:38:14 -!- coppro has joined. 02:42:44 It would be interesting to see how varied an ultrafinitist system is. 02:42:45 My bet: Not at all. 02:47:07 -!- oklopol has quit (Ping timeout: 265 seconds). 02:51:54 http://sibeli.us/ 03:15:31 The best ultrafinitist system is a Galois field. 03:15:37 -!- uorygl[hireMe] has changed nick to uorygl. 03:16:01 what language lends itself to reflection the most? 03:16:20 BackFlip. :P 03:16:56 -!- alise has quit (Quit: Page closed). 03:16:58 not that kind of reflectiong 03:26:01 -!- werdan7 has quit (*.net *.split). 03:26:02 -!- rodgort has quit (*.net *.split). 03:26:02 -!- ttm has quit (*.net *.split). 03:28:18 Aura! 03:28:24 -!- ttm has joined. 03:28:26 jamaica! 03:28:35 Or whatever that's called. 03:29:03 -!- rodgort has joined. 03:40:39 -!- werdan7 has joined. 03:50:57 -!- Gracenotes has joined. 04:13:45 Gah, I'm so unclear sometimes. 04:17:52 I'm tempted to throw neutrons at you. 04:18:02 But that wouldn't really help. 04:18:29 -!- jcp has quit (Ping timeout: 260 seconds). 04:18:39 Sgisotype 04:43:28 -!- coppro has quit (Read error: Operation timed out). 04:59:52 -!- coppro has joined. 05:08:13 -!- coppro has quit (Ping timeout: 276 seconds). 05:24:30 Hm, smeta.na is available for the low low price of $4,000/yr 05:25:38 -!- coppro has joined. 05:34:19 -!- Oranjer has left (?). 05:39:42 * Sgeo is half tempted to use PSOX with Scheme 05:39:45 >:D 05:40:41 * Gregor three-quarters tempted to mock Sgeo's use of fractional temptation. 06:09:36 -!- skeeto has joined. 06:10:55 is it possible to write the identity function in Fractran? I don't think it's possible. 06:23:05 -!- skeeto has left (?). 06:33:24 So, what does PSOX look like? 06:33:44 One can not see PSOX. 06:33:50 One can only ... /experience/ PSOX. 06:33:56 * Sgeo decides that uorygl has been living in a bubble since the end of 2007 06:33:59 Does it provide the Unix standard library? 06:34:11 I don't think PSOX is famous. 06:34:33 It is infamous in these parts 06:35:11 It gives alise aneurysms 06:35:35 If it gives alise aneurysms, I'm almost bound to probably be slightly irritated by it. 06:45:05 -!- FireFly has joined. 06:49:15 -!- oerjan has joined. 06:56:10 Sgeo: Isn't PSOX about as well-maintained as PEBBLE these days? 06:56:27 pikhq, if PEBBLE was abandoned, yes 06:56:45 I've not touched it since, oh, 2007. 06:56:49 If people start showing interest, I may regain interest in maintaining PSOX 07:00:06 -!- kar8nga has joined. 07:06:43 -!- tombom has joined. 07:29:32 -!- oerjan has quit (Quit: leaving). 07:39:42 * Sgeo goes to try Smalltalk 07:51:44 -!- tombom has quit (Quit: Leaving). 07:52:53 -!- cheater2 has quit (Ping timeout: 246 seconds). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:02:50 -!- cheater2 has joined. 08:13:19 -!- FireFly has quit (Quit: Leaving). 08:15:54 -!- cheater3 has joined. 08:17:55 -!- coppro has quit (Quit: I am leaving. You are about to explode.). 08:19:53 -!- cheater2 has quit (Ping timeout: 256 seconds). 08:20:29 -!- zeotrope has quit (Ping timeout: 256 seconds). 08:21:04 -!- zeotrope has joined. 08:32:21 -!- OxE6 has quit (Ping timeout: 260 seconds). 08:33:24 -!- adu has quit (Quit: adu). 08:36:59 -!- adu has joined. 08:38:20 -!- MU has joined. 08:38:29 -!- MU has left (?). 08:52:01 -!- MizardX has joined. 09:15:03 -!- lament has quit (Ping timeout: 240 seconds). 09:15:10 -!- lament has joined. 10:16:32 -!- kar8nga has quit (Remote host closed the connection). 10:23:36 -!- oklopol has joined. 10:25:28 oerjan come quick 10:37:46 oklopol! :o 10:43:52 hi 10:44:28 do the types by any chance form a quasigroup in your a/b b\a type thingie? 10:45:23 what 10:46:12 i'll take that as a no 10:46:21 no no, dont take it as anything 10:46:26 i dont know what you're asking 10:46:30 oh okay 10:46:32 i'm talking about that 10:46:48 linguistics thing you tried to teach me and someone else and he was like whaaaaaa 10:47:06 (C)CG? 10:47:08 and you were like okay this is going nowhere i'm gonna go do something otherthing. 10:47:20 oh, right 10:47:32 lecomte and retore's minimalism 10:47:34 it was about semiconflabulent grammars 10:47:39 ah minimalist 10:48:00 i dont know if the types for a well defined structure. i doubt it 10:48:04 form** 10:49:31 hmm minimalism has (a/b)*b = a, but does it have (a*b)/b? i guess that makes no sense 10:50:07 well, * is an operation on lexical items that bear types 10:50:17 i just noticed a similarity when reading about quasigroups, but i haven't actually given it any thought 10:50:21 not a type constructor 10:50:25 right 10:50:33 so a*b isn't even defined in general 10:50:41 well, it is 10:50:44 therefore it can't form an algebra 10:50:45 oh? 10:50:47 its just not a type constructor 10:50:57 look at it like this 10:50:58 but is it defined no matter what the types of a and b are 10:51:07 thats correct 10:51:12 but / is a type constructor 10:51:15 * is not 10:51:29 so you cant do (a*b)/c 10:51:33 why? because a*b is not a type 10:51:43 so you cant use / on it 10:51:52 oh alright 10:51:58 think of it like haskell 10:52:04 a -> b is a type in haskell 10:52:11 a + b is not a type 10:52:17 so you cant have some type 10:52:19 (a + b) -> c 10:52:51 so i can't really say (A/B)*B = A either, i can say c*d : B if c : (A/B) and d : B? 10:53:33 pretty but. i mean, (A/B)*B would be seen as just an operation over the type objects 10:53:37 which is fine 10:53:42 its just not a type constructor 10:53:52 its an operation on types. 10:53:58 brb 10:54:11 but as an operation over type objects, isn't it partial? 10:55:01 say we just have the types A and B, how can A*B be defined if * isn't a type constructor 10:55:37 also how can it be defined on the objects or whatever, if a : A, b : B, what's the type of a*b? 10:56:53 it is indeed partial 10:57:31 A*B is undefined. only A/B * B and B * A\B are defined 10:57:43 for all types A and B 10:57:47 okay, so they do form an algebra, but it's partial 10:57:54 therefore it clearly can't be a quasigroup 10:57:55 its just function application dude 10:58:11 its literally beta reduction 10:58:17 on types instead of functions 10:58:27 and the types are directional 10:59:02 what's the difference between type constructors and type operators? both are operators that take types to other types 10:59:15 constructors are used to define the universe of types, yes, but i don't see how that's relevant 10:59:34 i probably shouldn't be looking at this quite this algebraically. 10:59:38 sure but a type constructor is, at least in this case, and i think in all cases, total 10:59:47 ah, well yes, okay 10:59:51 -> : T x T -> T 11:00:07 * : (T x T) x T -> T 11:01:14 theres also the tensor product thing that they had tho fight 11:01:27 they had a second type constructor, x 11:01:30 so (T, /, \) forms an algebra, but it doesn't really have any structure... so i guess you should just think of those as type constructors instead of an algebra 11:01:41 well, it DOES have structure 11:01:45 its just not a well known one 11:02:08 or rather, its not an interesting one 11:02:43 if you did math, for instance, + or * over the integers has all sorts of fun properties 11:02:49 well right, that's what i meant, it's the free algebra on two binary operations, sort of 11:02:51 like, sometimes you can get back what you gave it 11:02:58 or you can go in circles 11:03:03 etc 11:03:13 / and \ are not like that 11:03:30 yeah therefore free 11:03:47 which is to say, there are finite subsets of Z which are closed under + or * 11:04:03 there is no subset of T that is closed under / or \ 11:04:13 T as a whole is closed, but no subset of it is 11:04:24 that's not true 11:04:29 yes it is 11:04:35 the subalgebra generated by A/B is a subset 11:04:37 that's closed 11:04:43 what? 11:04:59 sorry, no finite subset 11:05:05 yeah that's true 11:05:13 obviously 11:05:33 but it's freeness that's the point 11:05:39 but there ARE finite subsets of Z which are closed under *, lets say 11:05:42 {1} for instance 11:05:54 or {0} or {0,1} 11:06:06 why are you telling me this? 11:06:13 im just saying 11:06:21 oh well i guess that's allowed 11:06:25 the structure of Z under + or * is more interesting than \ and / 11:06:40 simply because you can get substructures that are interesting like this 11:08:11 you can do all sorts of fun stuff with * and + that you cant do with / and \ simply because / and \ are, you might say, information preserving 11:08:26 yeah, you might even say it's free. 11:08:45 the result of addition is not something that has a uniquely identifiable origin 11:08:56 1 + 1 = 0 + 2 = -1 + 3 = ... 11:09:19 but A/B is just A/B. theres only one way to get A/B. 11:10:15 -!- Slereah has quit (Ping timeout: 240 seconds). 11:10:27 -!- comex has quit (Ping timeout: 276 seconds). 11:10:35 i don't really know the exact definition of freeness, but that's exactly what i mean by free in the case of an algebra that doesn't have any sort of identities. 11:11:43 there's a base and there's only one way to get everything from it. in the case of no identities, we have the stronger thing that every individual operation is completely reversible 11:12:24 anyway 11:12:57 if you let * be a type operator (which it technically isnt; it operators on things _with_ types, but we can pretend it can operate on just types for convenience) 11:13:15 then you get \ / and * forming some sort of "non-free" object, as you might say 11:13:18 identities being where the structure comes from, in the free monoid we can still have ab*c = a*bc even though it's free, where {a,b,c} is the base, because we have an identity that makes them the same, but if the operation satisfies no identities, then it's fully information preserving 11:13:52 they form a partial algebra, if that's the term 11:14:06 e.g. (A/B * B)/B, ((A/B)/B)*B, etc. 11:14:32 might still be free though 11:14:39 hmmhmm 11:14:49 maybe. im just saying that there you now get the non-uniqueness of histories. 11:14:59 trues 11:15:50 i'm actually literally atm reading a book that would completely explain the role of identities in universal algebra, if i just read like 20 pages ahead 11:16:00 :P 11:16:13 -!- Slereah has joined. 11:18:25 :) 11:20:40 -!- cal153 has quit (Ping timeout: 276 seconds). 11:22:02 (which also might be why i'm obsessing about the algebraic side of these things) 11:27:07 -!- cal153 has joined. 11:50:50 -!- cal153 has quit (Ping timeout: 248 seconds). 11:54:39 -!- cal153 has joined. 12:32:09 -!- fax has joined. 12:36:12 -!- alise has joined. 12:43:23 -!- oklopol has quit (Ping timeout: 245 seconds). 12:50:24 Gregor: I finished sibeli.us 12:50:43 Your score: 175822 / Points possible: 660500 / Grade: 26% (F) 12:50:50 I couldn't go any swbps because of my kb matrix 12:50:52 *do 12:51:00 alise is kool 12:52:40 augur: + /is/ an operation on types tyvm 12:52:40 it's (Either a b) in haskell syntax 12:53:14 a*b (same thing as cartesian product) = (a,b) 13:02:13 alise: oh, well ok. :P 13:02:30 i meant + as integer addition tho 13:02:40 thats all 13:04:22 -!- alise has quit (Ping timeout: 252 seconds). 13:04:36 -!- alise has joined. 13:04:39 o hai 13:04:42 Your score: 480612; Points possible: 660500; Grade: 72% (C-); this could do swbp (1234) most of the time, though I got some key-jammery there somewhere. I have to wonder if it would've been easier with the music, though. 13:05:20 Your score: 380183 Points possible: 660500 Grade: 57% (F) 13:05:33 1234 would have worked too? That'd have made it easier 13:05:47 "Use the keys '1', '2', '3' and '4' (or 's', 'w', 'b' and 'p') for strings, woodwinds, brass and percussion." 13:05:52 That's what it says on the front page. 13:05:54 Yeah, I missed that bit. 13:06:04 I just pressed "play" without reading the instructions. 13:06:14 Sounds exactly like the sort of thing you'd do! 13:06:53 swbp is highly inconvenient on Colemak; all left hand and in 2143 order 13:06:54 HA 13:06:54 Deewiant loses at something! 13:07:09 A first! 13:07:40 XD 13:07:41 But yeah, I started thinking ohh this is easy 13:07:41 And then it was all, like, SSSWSWSWISBWndhFoiDSJpKAFPAJDOIHWDSOIWJD 13:08:04 I dreaded the fast bits from the start :-P 13:08:05 fizzie: It's worse with the music, trust me 13:08:22 With a 100+-key keyboard, though, shouldn't you be controlling just about every instrument? 13:09:24 :D 13:09:24 Deewiant: I've heard the whole thing like... once before 13:09:54 And I, several 13:09:54 So a couple of times I thought "thank god, it's over" and then more shit popped up 13:10:44 Being .fi, it's sort-of required reading, I think. 13:11:00 Or listening. Anyway. 13:11:34 It's rubbish 13:11:34 You Finlanders suck :P 13:12:21 Deewiant: More automatic tweetery, though this is a bit Finnish-only: [2010-03-10 14:53:19] Tweeted: verikissanhiekka valtaa kanavia internetissä / akuutti rautaneito kuin laiteristiriita / laiminlyöty ja kukertava (runogen) 13:12:56 What. 13:13:03 heh 13:13:40 It's automagical poetry-generation; a rather old (10 years?) bit of code that I was suggested to make auto-tweet too. 13:15:57 1234 was a lot more comfortable if not easier: Your score: 418757 Points possible: 660500 Grade: 63% (D) 13:16:12 alise: I don't think my poetic skills are up to a faithful translation, but if you want a mostly literal one... "blood-cat-litter takes over channels on the Internet / the acute iron maiden like a device conflict / neglected and colorful". 13:16:25 Though "colorful" is a crappy word for "kukertava"; I don't really know what it should be. 13:16:35 fizzie: xD 13:16:48 Wiktionary's entry -- http://en.wiktionary.org/wiki/kukertaa#Finnish -- lacks a definition. 13:17:19 fizzie: flowery? 13:18:29 I'm not sure. Perhaps, though the connection to actual flowers is (at least to me) less there. 13:18:39 1. flowery -- (of or relating to or suggestive of flowers; "a flowery hat"; "flowery wine") 13:18:39 2. flowery, ornate -- (marked by elaborate rhetoric and elaborated with decorative details; "a flowery speech"; "ornate rhetoric taught out of the rule of Plato"-John Milton) 13:19:07 It's not sense #2, but it's maybe not exactly sense #1 either. 13:19:45 Interwebs say: "It's a Finnish word for a colour that isn't of any particular colour, I think." 13:20:08 xD 13:20:11 Right 13:20:21 Weird-ass word; to me it suggests flowers 13:20:50 Deewiant: Here's one poem I created earlier: "saatanan aarre ei ole valopuu / humanistien aurinko ymmärtää antaa kuin ruoska / kaipaus ei ole käytävä eikä brainfuck" 13:20:51 But evidently that's not what it means 13:21:07 fizzie: :-D 13:21:09 *word. 13:21:09 fizzie: translayt 13:21:21 -!- kar8nga has joined. 13:22:10 alise: "The treasure of Satan is not a light-tree / the sun of humanists knows to put out like a whip / longing is not a corridor, nor brainfuck". 13:22:31 "ymmärtää antaa" is another a bit difficult one. 13:22:34 fizzie: I'd've said "insinuates" 13:23:07 Deewiant: But that's "antaa ymmärtää", isn't it? 13:23:23 Yes, but with poetic license you can write it the other way around. 13:23:39 Oh, but it's not that, in fact; that thing there in the poem is the other half from the saying "antaa ymmärtää, muttei ymmärrä antaa". 13:23:39 I don't know, that just made more sense to me. 13:24:10 The translation used the "6. put out -- (be sexually active; "She is supposed to put out")" sense of "put out". 13:24:10 Then I'd just say "understands to give" 13:24:25 And to me, that wasn't implied :-P 13:25:13 Well, you'd have to know the guy whose irc behaviour was used as a model when constructing that particular wordlist. :p 13:25:14 those would make goodterrible lyrics 13:25:14 for a goodterribleterrible song 13:26:19 Deewiant: "ymmärtää antaa" is only in the "naula" wordset, c.f. http://www.pelulamu.net/naula/ 13:26:45 I learned long ago not to visit pelulamu.net 13:27:08 So yeah, okay. :-P 13:27:09 pelulamu.net? 13:27:40 Anyway, that generator is a handcrafted CFG, mostly not by me; there's four wordsets ("poetic", "gothy", "funny" and "naula") you can tell it to use. 13:28:01 If you do "-w goth", you get out stuff like: "sinä olet pääkallo / risti kylpee veressä / pikkutyttö kylpee veressä tulvillaan kipua sydänyöllä" 13:28:08 :-D 13:28:42 pelulamu.net? 13:28:42 also TRANSLATE :| 13:28:50 Do you have this available? I could put this in /etc/profile.d 13:29:16 alise: google.com/translate_t 13:29:43 Deewiant: Sowwy, but there's only a binary-only version available; I'm supposed to clean up the code before release; have been for the last ten years. 13:29:46 no :| 13:29:49 Deewiant: http://maija.irtie.org/runogen/ anyway. 13:30:23 specially as i'm going in ... 20 seconds? 13:30:23 but srsly what's pelulamu.net 13:30:23 like finnish rotten.com or sth? 13:30:28 alise: Well, the gothy one is approximately "you are a skull / a cross bathes in blood / a little girl bathes in blood full of pain at midnight". 13:30:45 fizzie: Can you hook me up with a 64-bit binary? 13:30:47 :D 13:30:54 Deewiant: Um, sure, I guess. 13:31:15 Deewiant: Don't you have any 32-bit compatibility libs, though?-) 13:31:21 No, I do not 13:31:26 -!- alise_ has joined. 13:31:28 I have a 32-bit chroot, which I'd rather avoid when possible 13:31:32 what was said since um sure i guess 13:31:48 Three lines that are available in the tunes.org clog log 13:32:05 well as i'm leaving right now 13:32:06 :p 13:32:16 Deewiant: It also generates the output in iso-8859-1; is that a problem, or can you pipe it through iconv or something manually? 13:32:31 well bye 13:32:48 Presumably something iconv-like is no problem 13:32:52 alise: Bye 13:33:40 http://zem.fi/~fis/runogen in that case -- the server will send it as text/plain, unfortunately. 13:34:24 Awesome 13:34:45 It seems something between the program and my screen even automatically understands the 8-bittiness 13:34:55 Cheers 13:35:10 -!- alise has quit (Ping timeout: 252 seconds). 13:37:00 -!- alise_ has quit (Ping timeout: 252 seconds). 13:37:10 Yes, it's a bit strange; the output looked just fine in rxvt-unicode when I ran it directly, but when I had the Python script print it out, it came up as the missing-character ? signs. I guess Python might do something there, though I was under the impression that if I just used os.popen and read() to get a 'str'-type 8-bit string and then print that, it shouldn't go and alter the bytes. 13:37:32 Though I had to manually utf-8ify it anyway for Twitter posting. 13:38:52 Unless I'm mistaken, there was also one undocumented (by -h) command line option, though I can't remember what it did. 13:39:32 Using "-v -v -v" will give you some printouts of the rule-parsing at least. :p 13:41:04 Written in C, presumably? 13:41:13 Written in very ugly C. 13:41:17 :-) 13:41:20 That's the main reason there's only binaries. 13:41:35 Gah, that thing's written in 2002; I'm ashamed of myself. 13:42:55 Deewiant: Here's a representative snippet of code quality: http://pastebin.com/XvpEJHVv 13:43:08 Looks good to me 13:43:25 Maybe I'm overly critical. 13:43:31 ;-) 13:43:53 alise is a girl 13:46:09 Deewiant: Well... the win32 gui code at least is a mess. :p 13:46:19 Ah, but it always is 13:48:10 Deewiant: http://pastebin.com/KMqHn2e6 13:48:20 Deewiant: There's even a manually implemented checkbox-listbox thing. 13:48:50 I like Outo virhe 1 and 2 13:49:41 Heh. I don't quite know what they mean. 13:49:42 And I wonder what's going on with the number 20000 in get_opts 13:50:02 Also, the loop: for (i = 20002; i < 20013; ++i) { if (i == 20012) break; ... } is nice 13:52:17 At least the messages are cheerful 13:53:28 I think the mapping there is that 20000+N (for N = 2 .. 10) means to generate a poem of N lines; and 20011 means that the length is taken from some textfield. 13:56:18 Deewiant: Nnngh. Look at this nonsense: mii.dwTypeData = strdup("&Muu pituus... (xxxxxxxxxxxxxx)"); sprintf(mii.dwTypeData, "&Muu pituus... (%d)", dw); 13:57:04 Nonsense? :-D 13:57:34 Makes sense to me; strdup is just a not very efficient way of doing it 13:58:40 (And of course it assumes a 32-bit DWORD but I guess everybody does) 13:59:41 I could've just used snprintf to calculate the length. Except that I guess MSVC calls that _snprintf and it doesn't actually return the number of bytes that were needed, so maybe not. 14:01:12 You should use the safer _snprintf_s! 14:01:54 -!- adu has quit (Quit: adu). 14:02:42 I don't think MSVC6 had the _s functions yet, in fact. 14:02:49 Probably not 14:39:36 -!- cpressey has joined. 15:07:18 -!- ais523 has joined. 15:27:22 http://dpaste.com/hold/170444/ 15:29:33 cpressey its very long :| 15:29:56 Yeah and it doesn't tell you much you didn't already know, either :) 15:30:08 I don't really get why don't you just use types to do this proof.. 15:30:37 But it helped me work out the system (so the comment is really the most valuable) 15:30:51 In short, because I don't want to be tied to any particular type system. 15:31:10 This method of (basically) pure rewriting lets you roll your own. 15:31:53 Hm, I guess I could have just done 'nand' to make it shorter. 15:32:20 -!- oerjan has joined. 15:34:07 oerjan come quick <-- er.. 15:37:45 * Sgeo should not have stayed up until 4 last night 15:38:20 Sgeo: now you'll _never_ catch up 15:43:44 cpressey what does tied to a particular type system mean? what I am suggesting is that a type system could be on you side, rather than against you 15:44:32 I guess there's no way to make a smalltalk system look like it's native? 15:53:44 wow alise is gonna love this http://www.paulkabay.com/#trivialism 15:57:23 -!- FireFly has joined. 15:57:34 -!- augur has quit (Ping timeout: 276 seconds). 16:02:53 fax: Well, people make up new type systems all the time, as research. I'd like to have something that supports that effort, rather than picking one type system and saying "That's all I got". 16:03:08 I gotta say, I love trivialism already. 16:03:10 bbiab. 16:03:13 -!- cpressey has left (?). 16:05:33 -!- cpressey has joined. 16:07:40 fax: To me, type systems are just a special case of abstract interpretation. 16:07:53 isn't that true in general? 16:08:20 Uh... yes? Not sure what you're referring to. 16:08:27 well you don't need to say "to me" 16:08:37 Oh, well 16:09:04 why don't you have an abstract interpretation module and use it to prove this boolean stuff in a much more effecient way? 16:09:53 That was kind of the plan, but I think it turned out that this proof construct thing *is* my abstract interpretation module... 16:10:19 Abstract interpretations can be mathematically modelled as Galois connections. 16:10:43 And these rewrite rules, with types going one way and evaluations going the other way, seem to be... close to that idea. 16:12:11 (I guess read my first statement as "Type systems are just a special case of abstract interpretation. Most people seem content to work inside the special case. But I want to design very general things.") 16:14:20 Galois connections?? 16:15:07 Oh, I barely understand it myself :/ 16:16:22 http://en.wikipedia.org/wiki/Galois_connection vs my shitty explanation http://catseye.tc/about/galois-connections.html 16:17:12 Also, my examples are wrong, and I think I say "element" where I mean "subset" in one place. 16:17:13 abstract values (such as {int, even, odd, power-of-two, prime, ... }). 16:17:20 ^ THIS AER TYPES!@! 16:17:35 Yes, I know. 16:20:09 And "turing-machines-that-always-halt" is a type, too... 16:21:04 Just, good luck proving that your function always evaluates to one. 16:23:58 aerotypes, just so much hot air? 16:26:28 -!- augur has joined. 16:27:16 Is !x -> x just as inconsistent as !x = x ? In the former, every statement has the same normal form, but there's only one normal form. In the latter, there are no normal forms. 16:28:59 -!- Gracenotes has quit (Quit: Leaving). 16:29:52 with intuitionistic logic otherwise, it is. 16:30:06 !false -> false, for example 16:31:04 or hm, x -> !!x is a theorem, so 16:31:17 x -> !!x -> !x follows 16:34:33 guess who's 24 today :D 16:34:53 oerjan: I agree it's ... on the same level, I just don't know if there is terminology to distinguish between the two. 16:34:56 augur 16:35:21 Hey, augur shares Chuck Norris's birthday. 16:35:31 cpressey: they're equivalent by my argument, in intuitionistic logic 16:36:48 oerjan: Well, maybe replace ! with @ to drop the connotation of "not" ... I'm just thinking symbolically. In both systems, you can pick any two arbitrary statements, like @@@@@x and @@x, and show they are equal. 16:37:19 without the connotation of "not" neither is inconsistent 16:37:25 Only diff is the first says they're equal because they're both equal to x. The second doesn't have to pass through x. 16:37:58 er, by "pass through" I mean "refer to x directly" 16:38:20 um neither has to pass through x 16:38:24 or wait 16:38:31 Oh, you're right. 16:38:33 Well, ... 16:38:48 :( 16:39:08 I still think they're inconsistent. 16:39:15 when you say !x -> x do you mean that there _exists_ an x for which this is true? in which case !x -> x is not inconsistent, just take x = true 16:39:55 oerjan: I mean, for all x, this is true. 16:40:06 Well, not "true" 16:40:28 cpressey: @x = x is not inconsistent if @ has nothing to do with "not" 16:40:32 x is a valid evaluation of !x. 16:40:54 oerjan: OK, then I totally don't understand formal logic. 16:40:58 * cpressey goes back to school 16:41:39 cpressey: and by nothing to do with "not", i mean that you throw away all the other axioms of ! 16:41:40 ?? 16:41:46 what's !x? 16:41:51 fax: not x 16:41:57 in a particular system? 16:42:02 (if so, which one) 16:42:18 fax: i don't think cpressey knows yet :D 16:42:22 maybe the problem is that the term "inconsistent" refers to logical systems and by discarding the "logical" meaning of the system, you can no longer use that term? 16:42:50 cpressey: if you have just @x = x, you cannot prove x = y for all x and y 16:43:10 one of them has to be a number of @'s applied to the other 16:43:44 (or to something common, but that happens to be the same thing in this case) 16:44:33 I think we need to clarify the universe, like what x and y can be 16:44:58 clarify the universe by melting it down and seiving it 16:45:08 mmmmmm 16:45:10 tasty. 16:45:11 cpressey: for example say that @x has the meaning !!x 16:45:36 then it is definitely consistent for @x = x to be true, because it's true in classical logic 16:46:05 although not necessary, since it is not always true in intuitionistic logic 16:46:16 If x and y elem {0, @0, @@0, ...} then we can prove x = y for any choice. 16:46:23 yeah 16:46:53 If you start picking them from {0, 1} or something, yeah, I see how you can't prove arbitrary things. 16:47:27 OK. Will mull this over. 16:50:56 -!- BeholdMyGlory has joined. 16:53:29 fax D: 16:53:30 :D 16:53:31 D: 16:53:33 :D 16:53:36 :D 16:53:41 * augur uses email instead 16:53:45 ? 16:53:58 so slow :| 16:58:51 OK, let me restate. In a system where there is only one value (call it 0), is @x -> x considered just as "inconsistent" as @x = x (which is just shorthand for {@x -> x, x -> @x}), or are there two different terms for "everything reduces to the same normal form, so we can prove any statement" vs. "there are no normal forms, so we can prove any statement"? 16:59:40 * cpressey 's jaw drops 16:59:44 my unit tests actually passed 17:00:24 cpressey: if there is only one value, then @x = x is obviously true 17:02:11 I might need to rethink again. 17:04:00 Like, what is a value. If we add another axiom #x = #x, then there are a bunch of irreducible terms #0, ##0, ###0, which are all distinct from 0, at least syntactically -- are they values? Is @@@0 not a value (well, it can't be distinguished from 0 or @0 or any other expression involving @, so maybe not?) 17:05:25 (Logic always was my least favourite esolang...) 17:06:08 -!- tombom has joined. 17:07:04 cpressey: also it is not a requirement of logics to be defined by reductions or have normal forms... 17:07:48 cpressey, oh I see what you mean, like adding a new 'function' as an axiom, without giving it reduction rules 17:07:48 oerjan: Yeah, I realize that. Kind of. 17:08:59 Kind of like saying it is not a requirement of graphs to be directed :D 17:09:26 Or to have degeneracies 17:11:04 -!- oklopol has joined. 17:11:07 how old am i? 17:11:17 i just turned either 21 or 20 a few weeks ago 17:11:24 argh 17:11:39 http://en.wikipedia.org/wiki/Anus_language 17:12:15 i'm almost sure it's 20 17:12:21 didn't i talk about this here? 17:12:29 i'm sure i've mentioned my age 17:12:38 fax: you'd think that page should have been protected... 17:13:01 oklopol: why donto you figure it out based on your date of birth 17:13:03 oklopol: well i recall you turning 20 i think, and it was more than a few weeks ago 17:13:11 okay, good 17:13:17 fax: sounds like a lot of work 17:13:29 as in, quite possibly a year and a few weeks ago 17:13:43 ... wtf. 17:13:49 also i think my memory problems are funny, which is also a reason to ask 17:14:20 * oklopol checks what year it is 17:14:35 okay so this year i turn 2010-1989 = 21 17:14:40 so in fact i just had to turn that. 17:15:14 oh right i had to be 20 and not 19 because of something alise said about 19 last year 17:15:27 i would remember if it'd applied to me 17:15:39 clearly oklopol is a being outside time and space 17:15:49 with troubles adapting 17:15:53 oklopol, quick, fetch a GPS! 17:16:07 Hmm 17:16:17 except that it depends on the location being on earth 17:16:23 which is a small subset of space 17:16:26 ._. 17:16:42 FireFly: you'd think it should be usable in low earth orbit too 17:17:00 I guess, but still just a small subset 17:21:54 lol my compositions from ~6 years ago are craaaazy 17:31:24 in theory, you could use GPS to determine your location anywhere in space 17:31:31 but it would be rather inaccurate far from the Earth 17:33:26 When you're far enough away that the Earth is basically a point, triangulating is hard :P 18:34:21 -!- augur has quit (Ping timeout: 260 seconds). 18:39:13 Quadrescence: success 18:39:41 lament: what is success 18:41:13 i mean failure 18:41:24 but you're unbanned in #Nm 18:41:37 n/m- 18:42:07 should i join it 18:42:45 of course not 18:42:57 you should take a stand 18:43:04 o 18:54:26 fizzie: I just got one starting with "lohikäärme on lohikäärme ja lohikäärme on lohikäärme"... maybe you should've enforced a bit of variety ;-) 18:54:57 Although I guess that's arguably validly poetic 18:55:04 `translate lohikäärme 18:55:12 dragon 18:55:16 dragon 19:00:14 -!- MizardX has quit (Ping timeout: 256 seconds). 19:02:00 -!- MizardX has joined. 19:06:23 Deewiant: I think there's supposed to be some sort of enforcement like that. 19:07:06 Deewiant: Apparently not for that rule, though. 19:13:06 Apparently :-P 19:23:05 -!- MizardX has quit (Read error: Connection reset by peer). 19:23:19 -!- MizardX has joined. 19:33:21 -!- oklopol has quit (Read error: No route to host). 19:33:44 -!- oklopol has joined. 19:42:11 -!- augur has joined. 19:47:21 fax: Actually I have other motivations for doing it this way, but they're... of questionable value 19:56:09 -!- kar8nga has quit (Remote host closed the connection). 20:12:48 -!- jcp has joined. 20:27:08 -!- Phantom_Hoover has joined. 20:27:30 Is there any need for a modern-day version of INTERCAL? 20:27:46 I don't think there's been any need for INTERCAL all along 20:27:51 it's still fun to work with, though 20:27:56 Is there any point, then? 20:28:08 there isn't a whole lot of point to much of what we do here 20:28:16 although, there's always the chance we might learn something about programming 20:28:17 Would it be interesting? 20:28:18 besides, it's fun 20:28:22 Or fun? 20:28:25 Phantom_Hoover: have you seen C-INTERCAL and CLC-INTERCAL? 20:28:30 Yes... 20:28:34 quite a lot of work has gone into modernising INTERCAL already 20:29:26 OK 20:29:28 -!- Phantom_Hoover has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838]). 20:29:35 that was strange 20:30:34 Yes. 20:33:53 -!- augur has quit (Ping timeout: 240 seconds). 20:38:35 Practical INTERCAL for the modern enterprise programmer 20:38:55 ais523: you just _know_ you need to write that book 20:39:08 not now, though 20:43:29 there's always the chance we might learn something about the deepest fantasies of wombats, as well. 20:43:35 it's just much, much smaller 20:43:49 ... probably 20:46:47 hey we'll need to do _some_ animal testing of our telepathic sensors before using them on humans, wombats should be excellent. 20:48:52 I just got back 20:48:54 and read the line 20:48:58 " there's always the chance we might learn something about the deepest fantasies of wombats, as well." 20:49:01 -!- augur has joined. 20:49:02 it was rather strange 20:49:07 * AnMaster tries to locate the context 20:49:25 i'm not entirely sure there was any 20:49:44 oerjan, that is rather worrying 20:49:54 AnMaster: yep, it was completely out of context 20:49:56 although, there's always the chance we might learn something about programming 20:49:57 which is why it was so strange 20:50:08 oerjan, and "INTERCAL for dummies"? 20:50:44 oh I get it now 20:51:18 well, sufficiently hyperintelligent dummies 20:51:48 or possibly crash test dummies. that might fit even better, actually. 20:52:15 :E 20:52:18 err 20:52:19 :D* 20:52:45 ...wherein AnMaster reveals himself as really being cthulhu. 20:52:50 hah 20:53:05 oerjan, or that I'm using qwerty 20:53:24 well i have no idea if they're close in dvorak or not 20:53:36 but that would be too simple of course 20:55:11 do crash test dummies dream of roadkill sheep? 20:58:10 Do people in #esoteric dream of inflatable sheep? 20:58:19 not normally, no 20:58:22 at least, I don't 20:58:35 mystery of the cube? 20:58:44 i cannot honestly say i'm sure i've ever done so 20:58:56 I haven't dreamt about that either 20:59:25 flying and cardinal sheeps possibly. But if so I must have forgot about them 20:59:38 what's a cardinal sheep? 20:59:53 oerjan, I believe that pun only works in Swedish 20:59:54 or rather 20:59:58 English/Swedish mix 21:00:11 what is the swedish 21:00:17 "karda" is a part of the process for making thread out of wool 21:00:25 I'm somewhat fuzzy on what exactly it involves 21:00:40 hm karde in norwegian 21:00:43 and the bits "kard" and "card" are produced the same in Swedish 21:00:47 well would be 21:00:53 we don't have the latter in any word afaik 21:02:37 inflatable sheep my be a cardinal sin 21:02:39 *may 21:03:30 (A sin often practiced by cardinals) 21:06:49 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 21:10:58 -!- jcp has joined. 21:20:09 -!- alise has joined. 21:24:30 -!- alise has quit (Ping timeout: 252 seconds). 21:26:55 -!- alise has joined. 21:26:58 05:41:13 Written in very ugly C. 21:27:01 the standard dialect of C 21:27:47 05:43:53 alise is a girl 21:27:48 inded. 21:27:48 *indeed 21:30:45 -!- ais523 has quit (Remote host closed the connection). 21:32:06 07:53:44 wow alise is gonna love this http://www.paulkabay.com/#trivialism 21:32:07 alise http://www.paulkabay.com/#trivialism 21:32:20 * cpressey applauds the psychic connection 21:32:20 Sorry, I'm already a preëventualist (http://viewsourcecode.org/why/preeventualist/; some links broken) 21:34:36 I'm a Stuckist, myself. 21:35:47 -!- pikhq has quit (Read error: Connection reset by peer). 21:36:03 /Philosophically/ I guess I cannot reject the proposition that all things are true. 21:36:15 -!- pikhq has joined. 21:36:16 But only because the question is a bit meaningless: from what frame of reference? 21:36:30 Even if you supply one, you must define the terms you use - and you cannot do that precisely. 21:36:39 So perhaps I actually believe that truth doesn't really exist, rather. 21:38:12 Nah, too easy. 21:38:21 Something exists, else why am I doing this? 21:38:31 And if it exists, might it not be true? It might. 21:39:03 alise philosophically 21:39:05 alise #philosophically 21:39:28 -!- alise_ has joined. 21:41:00 -!- alise has quit (Ping timeout: 252 seconds). 21:41:31 13:38:21 Something exists, else why am I doing this? 21:41:33 I don't know why you're doing this. 21:41:38 I gave (ack 4 1) half an hour, and it still didn't finish evaluating. It must hate me. 21:41:50 Also, the things that exist for you might differ from the things that exist for me. 21:42:04 Solipsism, while a ludicrously unlikely premise from inside our frame of reference, is still possible. 21:42:13 And philosophy is all about the possible yet unlikely. 21:42:27 But it's a sucky basis for action. 21:42:32 If I assumed cogito-ergo-sum, that wouldn't really be valid in philosophy, since it'd only be valid for me. 21:42:40 Solipsism, that is. 21:42:48 And philosophy shouldn't really only work for the author, otherwise it's ... not philosophy. 21:42:55 So objectively, nothing can be said to exist for certain; 21:42:57 *certain. 21:43:11 Truth is still ill-defined either way, though. 21:43:18 We have a rigorous definition of provability, but not truth. 21:43:27 We call things true if they seem to be true to us. 21:43:45 Oh, the Axiom of Choice is probably true. But that doesn't really mean anything, it's just human folly. 21:43:53 So, really, I guess I technically don't believe in anything. 21:44:11 In practice though, from this frame of reference, solipsism is bullshit, philosophical zombies don't exist, the universe is objective, and truth is a useful notion. 21:44:11 cpressey make ack doesn't terminated 21:44:59 A must confusing jumble of tenses, fax. 21:45:16 fax: ... I think I wrote it correctly, (ack 3 2) and such gave a result which corresponded with what I thought I saw when I had the impression I was looking at the Wikipedia page on the Ackermann function 21:48:30 or, what they *claim* is the Ackermann function 21:48:55 -!- Asztal has joined. 21:59:22 I should probably disappear from IRC for a while. 21:59:45 what, again? 22:00:30 Yes, again. 22:00:32 Bye! 22:00:34 -!- cpressey has left (?). 22:01:54 Bitchin' 22:02:00 *most 22:02:33 alise_: muphry's law in action 22:03:02 *Murhpy's 22:03:12 I just caused a stack overflow of the meta tower. 22:03:28 no, yes, wait, argh 22:04:48 bufuhukfbawf 22:05:00 -!- lament has quit (Ping timeout: 276 seconds). 22:05:26 fax: that's a very naughty word 22:05:35 my style is strictly ruude 22:05:38 aramakayhe 22:05:59 * alise_ wonders what's a better name for "data" that more strongly suggests induction and not just boring... data 22:06:06 "Inductive" is a bit too long. 22:06:14 -!- lament has joined. 22:17:59 -!- cheater2 has joined. 22:21:05 -!- cheater3 has quit (Ping timeout: 260 seconds). 22:30:29 -!- tombom has quit (Quit: Leaving). 22:46:12 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 23:02:45 doing classical logic in constructivist logic is fun 23:03:38 Try doing the non-contradiction theorem! 23:05:57 -!- oklopol has quit (Ping timeout: 260 seconds). 23:07:48 -!- oklopol has joined. 23:08:20 Slereah: What, not (p and not p)? 23:08:33 Yeah 23:08:35 That's in constructivist logic too :P 23:08:41 IS IT? 23:08:54 Or am I thinking of p or not p 23:08:55 Yes. 23:09:05 -!- coppro has joined. 23:09:07 We get rid of (p \/ ~p), not ~(p /\ ~p) 23:09:13 Ah yes 23:09:20 I often confuse them 23:09:21 The way to do classical logic in constructivist logic is to write everything as (p \/ ~p) -> ... 23:09:25 Contradiction and... 23:09:29 What's the other name 23:09:39 you can define classical P OR Q :<=> ~~(P \/ Q) 23:09:39 Law of the excluded middle. 23:09:42 and so on, 23:09:52 then you can prove classical tautologies 23:10:09 taut eulogies 23:10:10 http://pastie.org/864149.txt?key=efscdf3wmdhlbyfpnxqfdw 23:10:41 proof of (p->q) -> (~p->~q) -> q -> p classically 23:10:55 You have a taut body 23:10:56 I love the beauty of just letting LEM hand us a contradiction, at which point we simply take its word and prove the thing we want to prove, whatever it is, from it. 23:11:00 I can tell from your taut pants 23:11:23 Trivial system ~ 23:11:25 -!- oklopol has quit (Read error: Connection reset by peer). 23:11:29 Everything is true! 23:11:56 -!- oklopol has joined. 23:12:34 There are no trivial mathematics, just trivial mathematicians 23:12:56 -!- FireFly has quit (Quit: Leaving). 23:12:59 shut up 23:13:15 -!- BeholdMyGlory has quit (Read error: Connection reset by peer). 23:13:16 lament feels singled out there 23:13:51 -!- alise__ has joined. 23:14:10 * alise__ realises he redefined modus tollendo ponens in that proof 23:14:50 Well, almost. 23:15:14 -!- alise_ has quit (Ping timeout: 252 seconds). 23:17:27 modus penis 23:18:38 alise__: are the implications left-associative or right-associative? 23:19:15 right-associative. Obviously. As they're also the function arrows. 23:19:39 oh. wait what? 23:19:55 Curry-Howard isomorphism. Types = statements in constructivist logic. 23:20:03 Values = proofs. 23:20:03 (In a dependently-typed language.) 23:20:04 * coppro explodes 23:20:08 It's the future, mon. See: Agda, Coq, Epigram. 23:20:23 future 23:20:26 FUTURE 23:20:37 I'll believe you when I see it in .NET :P 23:20:46 .NET: The Future 23:20:47 non-dependently typed too. just you only get propositional logic then, or thereabouts. 23:21:03 .NET is looking to be the future, regrettably 23:21:32 oerjan: propositional logic is for butts 23:22:13 i see an obvious pun but i'll leave it for Slereah 23:23:48 nice of you to throw him some scraps of meat that you can't be bothered to pick from the bones 23:24:59 it's more like it seems more his style 23:25:07 (see above) 23:28:10 metastruct will be so cool :| 23:28:49 does anyone know a program that will simply ask X to clean up any temporary resources it has hanging around? 23:29:00 i n *hit by falling anvil* 23:29:01 so that I don't have to write one myself 23:29:28 yes 23:29:38 foo : (ProgDescription -> Prog) -> Prog 23:29:47 shutdown -r 23:29:53 foo p = englishDescr "ask X to clean up any temporary resources it has hanging around" 23:29:56 erm 23:30:01 foo p = p (englishDescr "ask X to clean up any temporary resources it has hanging around") 23:30:13 the program is (foo _) 23:30:15 where _ is obvious. 23:33:21 -!- augur has quit (Ping timeout: 252 seconds). 23:38:13 -!- oklopol has quit (Ping timeout: 240 seconds). 23:56:33 -!- oerjan has quit (Quit: Good night). 23:57:05 -!- oklopol has joined. 23:57:26 coppro: kill -9 23:57:36 (note: all resources considered temporary) 23:57:47 haha 23:58:39 Resources should totally include their extents.