00:02:12 -!- augur has quit (Remote host closed the connection). 00:06:06 -!- madbr has joined. 00:07:37 -!- ^v has quit (Read error: Connection reset by peer). 00:08:25 -!- ^v has joined. 00:19:38 -!- ^v has quit (Read error: Connection reset by peer). 00:20:03 -!- ^v has joined. 00:20:46 -!- atslash has quit (Quit: This computer has gone to sleep). 00:29:34 -!- oerjan has quit (Quit: Nite). 00:34:02 -!- shikhin has joined. 00:37:38 every world we reach is fungot 00:37:38 kmc: ( i'm saying this as a cgi. use mod_lisp.) and can be left off. 00:37:48 fungot: are you a full-time internet? 00:37:48 kmc: that's a macro. i thought that was fnord 00:42:06 p. sure fungot is computer-generated imagery 00:42:07 shachaf: what use would a variable? 00:42:12 -!- Tod-Autojoined has joined. 00:45:38 -!- TodPunk has quit (Ping timeout: 240 seconds). 00:50:58 -!- ineiros_ has quit (Ping timeout: 240 seconds). 00:51:04 -!- douglass_ has quit (Ping timeout: 240 seconds). 00:52:55 -!- boily has joined. 00:52:56 -!- douglass1 has joined. 00:52:56 -!- ineiros has joined. 00:52:57 -!- boily has quit (Client Quit). 01:01:49 -!- Tod-Autojoined has changed nick to TodPunk. 01:12:31 -!- edwardk has quit (Read error: Connection reset by peer). 01:19:29 -!- shikhout has joined. 01:19:45 -!- Phantom_Hoover has joined. 01:23:05 -!- shikhin has quit (Ping timeout: 264 seconds). 01:31:16 -!- augur has joined. 01:31:29 -!- shikhout has quit (Remote host closed the connection). 01:47:34 -!- Tod-Autojoined has joined. 01:48:07 -!- nycs has joined. 01:51:19 -!- jconn has quit (Ping timeout: 240 seconds). 01:51:20 -!- TodPunk has quit (Ping timeout: 240 seconds). 01:51:21 -!- fowl has quit (Ping timeout: 240 seconds). 01:52:30 -!- Taneb has quit (Ping timeout: 276 seconds). 01:52:33 -!- `^_^v has quit (Ping timeout: 276 seconds). 01:55:04 -!- Zerker has joined. 01:55:57 -!- Taneb has joined. 02:04:35 -!- fowl has joined. 02:05:27 -!- Tod-Autojoined has changed nick to TodPunk. 02:06:53 -!- FreeFull has quit. 02:09:42 -!- Zerker has quit (Quit: Colloquy for iPad - Timeout (10 minutes)). 02:12:24 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif). 02:14:08 -!- Ghoul_ has quit (Quit: Connection closed for inactivity). 02:36:00 -!- Phantom_Hoover has quit (Remote host closed the connection). 02:48:42 -!- kwertii has joined. 02:49:28 -!- kwertii has quit (Client Quit). 03:09:35 -!- tertu has quit (Disconnected by services). 03:09:35 -!- ter2 has joined. 03:15:17 -!- hk3380 has quit (Ping timeout: 264 seconds). 03:28:34 -!- copumpkin has changed nick to ubiquipumpkin. 03:32:01 -!- Sorella has quit (Quit: It is tiem!). 03:39:58 -!- conehead has quit (Quit: Computer has gone to sleep). 03:48:08 http://dumb.domains/ 03:49:41 thank you for making this all possible, ICANN 03:51:08 boobies.cool 03:52:57 is there a list of all the crazy TLDs that have appeared? 03:53:16 http://en.wikipedia.org/wiki/List_of_Internet_top-level_domains 03:53:18 nevermind :) 03:54:25 hark, a pumpkin 03:55:55 alas, pumpkin is not a tld :( 03:57:39 ubiquipumpkin: surely you could make it one 03:57:57 I guess the requirements are significantly lower :P 03:58:48 there might not be .pumpkin but at least there's .bike 03:59:46 thank god 03:59:48 pumpkin.co 03:59:57 what's with dnssec anyway 04:00:08 kmc: omg if I were publishing jvm packages I'd be all set 04:00:27 yes 04:01:38 Name: .red 04:01:47 Entity: those who like the color red 04:01:49 -!- ubiquipumpkin has changed nick to copumpkin. 04:02:00 it's a high bar, copumpkin 04:03:16 -!- tertu has joined. 04:03:55 bo.red 04:04:56 upholste.red 04:05:50 -!- ter2 has quit (Ping timeout: 265 seconds). 04:06:25 hat.red? 04:06:29 -!- hk3380 has joined. 04:10:31 -!- EgoBot has quit (Remote host closed the connection). 04:11:27 -!- EgoBot has joined. 04:12:19 -!- FireFly has quit (Ping timeout: 240 seconds). 04:13:29 -!- tromp has quit (Ping timeout: 252 seconds). 04:14:14 -!- tromp has joined. 04:14:44 -!- Gregor has quit (Ping timeout: 240 seconds). 04:16:00 -!- EgoBot has quit (Ping timeout: 265 seconds). 04:18:07 -!- FireFly has joined. 04:18:55 -!- Gregor has joined. 04:31:00 -!- Sprocklem has joined. 04:43:44 -!- hk3380 has quit (Ping timeout: 252 seconds). 04:49:59 -!- Vorpal has quit (Quit: ZNC - http://znc.sourceforge.net). 04:59:54 -!- ^v has joined. 05:04:31 -!- Slereah has joined. 05:05:11 -!- Slereah_ has quit (Ping timeout: 252 seconds). 05:08:07 -!- password2 has joined. 05:34:58 -!- Sprocklem has quit (Ping timeout: 245 seconds). 05:45:52 -!- edwardk has joined. 05:48:40 -!- madbr has quit (Quit: Rouringu de hajikunda!). 05:51:07 -!- tromp has quit (Ping timeout: 252 seconds). 05:59:04 -!- password2 has quit (Ping timeout: 276 seconds). 06:02:54 FireFly: You can check for whether a cell belongs to you or the enemy 06:03:23 You can scan the memory and bomb every location not belonging to you 06:07:22 -!- jconn has joined. 06:09:57 and I see the 'C' instruction isn't documented 06:10:08 It was intented to allow one to copy itself 06:22:46 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif). 06:36:53 -!- augur has quit (Ping timeout: 258 seconds). 06:52:14 -!- conehead has joined. 07:09:00 -!- augur has joined. 07:12:43 -!- edwardk has quit (Ping timeout: 240 seconds). 07:12:45 oerjan: what's with the weird bolding in https://en.wikipedia.org/wiki/Booth_encoding 07:13:14 looks like it took three edits to mess it up 07:23:11 -!- MindlessDrone has joined. 07:29:10 -!- slereah_ has joined. 07:29:17 Hello is this where we learn about the magic 07:34:48 -!- KingOfKarlsruhe has joined. 08:06:54 -!- edwardk has joined. 08:17:01 https://www.google.com/patents/US20030083544?dq=finding+love&hl=en&sa=X&ei=VqxuU52KKKLjsASNloCwBA&ved=0CDUQ6AEwAA 08:27:05 -!- Patashu has joined. 08:39:45 -!- oerjan has joined. 08:42:18 -!- Bike has quit (Ping timeout: 265 seconds). 08:51:23 -!- drdanmaku has quit (Quit: Connection closed for inactivity). 08:51:48 -!- atslash has joined. 09:08:34 -!- TodPunk has quit (Ping timeout: 240 seconds). 09:15:39 shachaf: someone was too bold while editing hth 09:46:12 -!- shikhin has joined. 09:59:37 if spammers were to pay 1 cent to charity for every spam mail they send 09:59:41 what a world we would live in... 10:01:26 so far 10/10 agreed on re-return EOF and unbounded memory to the right 10:04:04 -!- mhi^ has joined. 10:06:36 But spam is charity! 10:06:43 So many are from poor countries 10:07:02 http://en.wikipedia.org/wiki/Spammer#Geographical_origins 10:20:37 -!- shikhin has quit (Ping timeout: 252 seconds). 10:24:02 -!- hk3380 has joined. 10:28:51 -!- KingOfKarlsruhe has quit (Read error: Connection timed out). 10:36:14 -!- edwardk_ has joined. 10:37:55 -!- edwardk has quit (Ping timeout: 276 seconds). 10:51:47 -!- Phantom_Hoover has joined. 10:56:11 -!- hk3380 has quit (Ping timeout: 255 seconds). 11:12:40 -!- Patashu has quit (Disconnected by services). 11:12:40 -!- Patashu_ has joined. 11:36:59 -!- TodPunk has joined. 11:39:32 -!- TodPunk has quit (Read error: No route to host). 11:39:39 -!- TodPunk has joined. 11:42:09 -!- Tod-Autojoined has joined. 11:44:52 -!- TodPunk has quit (Ping timeout: 276 seconds). 11:45:05 -!- edwardk_ has quit (Ping timeout: 258 seconds). 11:47:27 -!- shikhin has joined. 11:47:35 -!- Sgeo has quit (Read error: Connection reset by peer). 11:51:48 -!- yorick has joined. 11:52:07 -!- shikhin has quit (Ping timeout: 250 seconds). 11:59:41 -!- edwardk has joined. 12:08:53 -!- conehead has quit (Quit: Computer has gone to sleep). 12:15:19 -!- nucular has joined. 12:15:19 -!- nucular has quit (Changing host). 12:15:19 -!- nucular has joined. 12:21:37 -!- mhi^ has quit (Quit: Lost terminal). 12:23:39 -!- mhi^ has joined. 12:23:41 -!- mhi^ has quit (Changing host). 12:23:42 -!- mhi^ has joined. 12:46:23 -!- Sorella has joined. 12:49:29 -!- edwardk has quit (Ping timeout: 264 seconds). 12:50:34 -!- tromp has joined. 13:21:11 -!- mhi^ has quit (Quit: Lost terminal). 13:44:22 -!- nycs has changed nick to `^_^v. 13:44:23 -!- Patashu_ has quit (Ping timeout: 265 seconds). 14:00:03 -!- Phantom__Hoover has joined. 14:00:54 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds). 14:17:16 -!- hk3380 has joined. 14:17:32 -!- shikhin has joined. 14:22:25 -!- conehead has joined. 14:29:14 -!- oerjan has quit (Quit: leaving). 14:29:19 -!- password2 has joined. 14:30:18 -!- g2` has joined. 14:30:44 -!- g2` has left. 14:41:58 -!- password2 has quit (Read error: Connection reset by peer). 14:47:29 -!- Sprocklem has joined. 14:55:09 -!- adu has joined. 15:01:29 -!- slereah_ has quit (Ping timeout: 264 seconds). 15:02:23 -!- slereah_ has joined. 15:04:01 -!- nooodl has joined. 15:04:19 -!- mhi^ has joined. 15:07:36 -!- MindlessDrone has quit (Read error: Connection reset by peer). 15:10:35 -!- FreeFull has joined. 15:17:50 -!- nucular has quit (Ping timeout: 258 seconds). 15:22:30 -!- nucular has joined. 15:27:54 -!- ^v has joined. 15:28:52 -!- ^v has quit (Client Quit). 15:37:19 oerjan: thx for fixing tdh 15:40:33 exercise: write non-recursive factorial for Church numerals 15:41:53 exercise: write non-recursive ackermann function for Chuch numerals 15:42:29 you sure that's possible? 15:43:04 it's possible for it to be an exercise 15:43:06 at least factorial is possible 15:44:00 the ackermann thing is instructive. 15:44:37 I have a typographical hint: instead of ack(n,m), write ack_n(m). 15:45:15 There's a slightly (very) cheaty way of doing this... 15:46:03 int-e: good point. now it looks not only possible, but straightforward:) 15:51:37 my best factorial is 78 bits 15:54:05 the single-argument ackermann function is usually \n -> ack(n,n) 15:57:55 -!- tertu has quit (Ping timeout: 240 seconds). 15:58:28 so 54 bits for \n m -> Ack(n,m); 58 for \n -> Ack(n,n) 15:59:03 -!- copumpkin has quit (Remote host closed the connection). 15:59:31 What language? 15:59:36 blc 15:59:38 binary lambda calculus 15:59:46 OK 16:00:42 -!- slereah_ has quit (Quit: Leaving). 16:02:19 hmm, i even have something about goodstein and ackerman on my home page at http://homepages.cwi.nl/~tromp/pearls.html#goodstein 16:05:05 -!- Sprocklem has quit (Ping timeout: 264 seconds). 16:05:14 -!- MindlessDrone has joined. 16:06:46 i,i frebled tromp 16:11:22 47 bits for the Ackerman-like g i define there 16:12:04 is all this still non-recursive 16:12:18 yes 16:12:54 but i doubt if the goodstein function can avoid recursion 16:14:58 57 for factorial. 16:15:11 cool 16:16:43 -!- Sprocklem has joined. 16:17:23 mine is based on F cont succn facn = cont (succ succn) (succn * facn) 16:17:30 what's yours based on? 16:19:44 it's \n\f. n (\f\n. n (f (succ n))) (\_. f) 1 ... it operates on f^k, where k is 1, n, n*(n-1), n*(n-1)*(n-2) etc. 16:21:20 oh.. 16:21:29 -!- Bike has joined. 16:21:36 At this point you might as well brute force it 16:22:38 -!- Sprocklem has quit (Ping timeout: 240 seconds). 16:25:14 C++ good link 16:25:58 -!- adu has quit (Ping timeout: 240 seconds). 16:34:19 "Writing a BLC8 interpreter in Brainfuck, which would provide a matching upper bound in the other direction, is left as an exercise for die-hard Brainfuck programmers." ince 16:34:22 nice* even 16:35:14 i dont expect anyone to ever take up that challenge:) 16:36:03 it's gonna be so horridly slow that you'd have trouble checking that it works 16:36:37 at least the direction i took is pretty efficient 16:37:25 c2bf might be only a few patches away from being up to the task 16:38:08 C is nearly as bad at memory management as brainfuck, however 16:38:49 at least it has pointers 16:39:28 In fact I disagree completely with that statement. 16:40:21 In Brainfuck you find yourself playing Hilbert's Hotel games all the time. That doesn't really happen in C. 16:41:46 By C I mean the subset of C implemented by c2bf. 16:41:48 ("Oh I will put this data on cells divisible by 3, that data on cells with remainder 1 modulo 3, and the cells with remainder 2 modulo 3 will be mostly zero except for one or two bookmarks to guide my code") 16:42:04 hmm 16:42:31 maybe you should call it c2bf-C 16:44:39 Apparently, c2bf has a "heap" stride but there is no malloc. It'll probably need to be implemented using inline assembly manipulating the heap. 16:45:17 -!- AnotherTest has joined. 16:47:27 you can view the tape as 2-dimensional, with the ith row being cells 1*2^i,3*2^i,5*2^i ... 16:48:08 i demand a hilbert space tapej 16:48:12 each successive row being twice as spread out 16:56:59 I demand a bf like language where +-,. are illegal on cells where |index| isn't prime . 16:58:34 why a bf derivative? 16:58:50 Everything is a bf derivative . 16:59:20 nortti: Doesn't have to be brainfuck 16:59:28 but I'd wonder whether you could find your way to the next cell 17:01:14 The number of reachable cells is limited by the size of the program 17:02:04 hm? 17:03:30 Not if you find an algorithm that searches for the next valid cell 17:03:52 but how do you get there if +-,. are illegal? 17:04:03 It cannot, because it cannot mark the cells on the way to the next valid cell 17:04:19 isn't three-cell brainfuck turing-complete? so just use 235 for everything. 17:04:32 Bike: that assumes unbounded cells 17:06:17 @oeis 2,3,7,23,89,113 17:06:18 Increasing gaps between primes (lower end): primes p(k) where p(k+1)-p(k) ex... 17:07:42 it's easy to prove that arbitrary long gaps in the sequence of primes exist, just use the CRT to find some n such that n, n+1, ..., n+k are divisible by the first k+1 primes, respectively. 17:10:50 sexy primes 17:11:39 -!- Sprocklem has joined. 17:14:29 > fix (\f ((p,g):ps) -> (p,g) : f (filter ((>g).snd) ps)) $ zipWith ((.)<$>(,)<*>subtract) <*> tail $ nubBy (((>1).).gcd) [2..] 17:14:33 mueval-core: Time limit exceeded 17:15:00 > take 10 $ fix (\f ((p,g):ps) -> (p,g) : f (filter ((>g).snd) ps)) $ zipWith ((.)<$>(,)<*>subtract) <*> tail $ nubBy (((>1).).gcd) [2..] 17:15:04 mueval-core: Time limit exceeded 17:15:26 > take 10 $ fix (\f ((p,g):ps) -> (p,g) : f (filter ((>g).snd) ps)) $ zipWith ((.)<$>(,)<*>subtract) <*> tail $ nubBy (((>1).).gcd) [2..] 17:15:28 [(2,1),(3,2),(7,4),(23,6),(89,8),(113,14),(523,18),(887,20),(1129,22),(1327,... 17:18:24 > map (text . printf "%.3f") $ zipWith (flip (/)) <*> tail $ [2,3,7,23,89,113,523,887,1129,1327,9551,15683,19609,31397,155921] 17:18:26 [1.500,2.333,3.286,3.870,1.270,4.628,1.696,1.273,1.175,7.197,1.642,1.250,1.6... 17:20:16 `coins 17:20:17 ​cercoin yourchiewucoin smocoin cottscoin oisorcoin ncommecoin apfcoin cutercoin petropricoin musissivcoin brazhdcoin varspncumercoin bisc-x86coin kitcoin bradablecoin wordfuctusioncoin ihaxcoin glassendseemeditegrofrcoin kirstecoin skullacoin 17:20:25 @oeis 1,2,3,4,5,23 17:20:27 Concatenation of the prime power factors (with maximal exponent) of n; a(1) ... 17:20:33 really 17:20:41 @oeis 1,2,3,4,5,32 17:20:43 Numbers that are the sum of at most 5 positive 5-th powers.[0,1,2,3,4,5,32,3... 17:20:44 hahaha 17:20:49 ._. 17:21:00 @oeis 1,2,3,4,5,35 17:21:02 Every base 6 digit of n is a base 10 digit of n.[1,2,3,4,5,35,123,154,215,33... 17:21:18 This is almost silly 17:21:37 this is the reason why people complain about "find the next number" puzzles 17:21:55 @oeis 3,1,3,3,7 17:22:00 2^A000120(n)-1.[0,1,1,3,1,3,3,7,1,3,3,7,3,7,7,15,1,3,3,7,3,7,7,15,3,7,7,15,7... 17:22:19 "1, 2, 3, 4, 5, x" "x = 6!" "don't be silly, x = 35" 17:22:27 Wow very much 1337 17:22:33 Yeah, why would x be 720? 17:22:38 @oeis 1,2,3,4,5,720 17:22:39 Sequence not found. 17:22:43 phew. 17:22:52 @oeis 8,6,7,5,3,0,9 17:22:53 Decimal expansion of (7^(e - 1/e) - 9)*Pi^2, also known as Jenny's constant.... 17:22:55 let's invent a sequence 17:23:54 @oeis 14,23,28,33,42,51,59,68,77,86,96,103,110,116,125 17:23:55 Numbered stops in Manhattan on the Lexington Avenue subway.[8,14,23,28,33,42... 17:23:57 -!- conehead has quit (Ping timeout: 258 seconds). 17:24:05 -!- conehead_ has joined. 17:24:08 wait, what 17:24:09 Good sequence 17:24:12 @oeis 3,6,9,21,24,27,30,33,36,42 17:24:13 Numbers n such that 2*n^2 + 1 is prime.[1,3,6,9,21,24,27,30,33,36,42,45,66,7... 17:25:19 -!- conehead_ has changed nick to conehead. 17:25:31 > map ord "Za" 17:25:33 [90,97] 17:25:44 @oeis 88,89,90,97,98,99 17:25:44 Sequence not found. 17:25:56 :O 17:26:30 I'm actually surprised there isn't a sequence for [A-Za-z] 17:27:47 @oeis 53,54,55,57,58,63,64 17:27:48 Sequence not found. 17:27:51 :O 17:28:13 maybe it only lists infinite sequences 17:28:14 @oeis 14,18,23,28,34,42 17:28:14 Local stops on New York City Broadway line (IRT #1) subway.[14,18,23,28,34,4... 17:28:33 the lexington avenue subway does not have an infinite number of stops 17:28:33 wait, that does kind of contradicts the subway stuff 17:28:34 I hope "Numbered stops in Manhattan on Lexington Avenue subway" isn't infinite 17:28:42 space-filling subway 17:28:44 :D 17:29:28 It's a long ride, as they say 17:30:16 There are also the sequences that may or may not be infinite 17:30:32 https://www.youtube.com/watch?v=aP1bvY7IqZY 17:31:43 @oeis 2,3,5,7,13 17:31:46 Mersenne exponents: primes p such that 2^p - 1 is prime. Then 2^p - 1 is cal... 17:33:04 @oeis 1,4,9,15 17:33:06 Triangle of Mahonian numbers T(n,k): coefficients in expansion of Product_{i... 17:34:15 @oeis 2,6,7,8,22,23,28,37 17:34:16 Sequence not found. 17:34:20 @oeis 2,5,7,8,22,23,28,37 17:34:22 Numbers n such that 2*n^2 + 3 is prime.[0,1,2,5,7,8,22,23,28,37,40,43,47,50,... 17:34:38 they must have a really large database 17:34:59 well, yeah, it's been running for like a billion years too 17:35:24 "over 220000 sequences" 17:35:26 hmm. my brute force blc search only goes up to 38 bits (doing up to 1000 reductions on each term) 17:36:10 (38 is as far as it gets within an hour) 17:36:32 -!- Sprocklem has quit (Quit: leaving). 17:37:13 Free time on the local cluster? 17:37:16 the predecessor function (with 0 -> 0) is another hard one. 17:37:27 -!- drdanmaku has joined. 17:38:00 (my best is 43 bits) 17:38:54 yes, i got 43 bits as well 17:39:40 i now got pictures of both pred and fac on my office wall 17:40:38 what are you talking about 17:41:09 about lambda diagrams http://homepages.cwi.nl/~tromp/cl/diagrams.html 17:41:14 binary lambda calculus. again. still. I don't know. 17:44:19 @oeis 7,11,14,20,21,30,31 17:44:20 Sequence not found. 17:45:16 -!- Tod-Autojoined has quit (Quit: This is me, signing off. Probably rebooting or something.). 17:45:30 -!- TodPunk has joined. 17:46:58 i don't get the K example 17:46:58 Wait, how many 38-bit blc programs are there? 17:47:19 Somewhere up to 2^32 17:47:50 Oh, I thought int-e tested 2^38 programs in one hour. 17:48:01 *38 17:48:47 I'd imagine a lot of them are invalid or don't terminate in a nasty way 17:48:48 @oeis 0, 0, 0, 0, 1, 0, 1, 1, 2, 1, 6, 5, 13, 14, 37, 44, 101, 134, 298, 431, 883 17:48:48 The number of closed lambda calculus terms of size n, where size(lambda x.M)... 17:49:08 https://oeis.org/A114852 17:49:33 38071898 of size exactly 38 17:49:45 See, less than 2^32 17:49:58 MUCH less 17:50:44 okay, i start getting it 17:50:55 hmmm, https://oeis.org/search?q=brainfuck&sort=&language=&go=Search 17:54:33 right. 82811806 total. 17:54:33 Hmm, I do have free time on a cluster 17:54:59 waste of resources, one should first write a faster evaluator. 17:55:46 -!- shikhout has joined. 17:57:41 the ultimate blc challenge is finding more bits of the halting probability omega 17:57:52 i've only managed the first 4 bits 17:58:10 it requires deciding halting behaviour of many programs 17:58:44 -!- shikhin has quit (Ping timeout: 255 seconds). 17:58:53 only a finite number of omgae bits can ever be proven 17:59:11 in a fixed, consistent logic 17:59:36 yes, more can be proven in inconsistent logic:) 17:59:54 in fact such logic proves they're all 17:59:56 in fact such logic proves they're all 0 18:00:09 and also all 1 18:00:17 tromp_: ooh 18:00:22 I remember when that was posted to /r/haskell 18:03:09 can you say more about why only a finite number of bits can be proven? 18:03:40 by a close analog of berry's paradox 18:04:11 let's say you can enumerate theorems of the form K(x) >= n 18:04:37 that give lower bounds on Kolmogorov complexity of finite strings 18:04:53 hmm. I wonder which is the "best" memo library on hackage. (I'm using memotrie but only because that's the first usable one I found) 18:04:58 i.e. there is no blc program less than n bits that outputs x 18:05:41 then you can write a short program that enumerates such theorems until it finds one with n >= N, and outputs the corresponding x 18:06:42 this would show K(x) < logN + O(1), a contradition for large enough N 18:07:10 ah! neat 18:07:10 so any consistent theory can only prove finitely many theorems of that form 18:07:50 the argument for bits of omega is a little more technical 18:08:20 but basically, if you have the first n bits of omega, you can identify all x with K(x) <=n 18:08:36 and thus also an x with K() > n 18:11:11 i like Data.MemoCombinators 18:13:08 in fact i used that for the OEIS entry: https://oeis.org/A114852/a114852.hs.txt 18:14:14 but also for April 2014's Ponder This problem, where i needed to memoize a function on a bounded list of Integers 18:14:30 eh, referring to memoization and dynamic programming asthe same thing... 18:15:33 i'm disappointed that Memo.integral means integers and not, somehow, integration 18:17:08 newest band name: Gigabit Bonghit 18:17:33 http://gigabit.bonghit 18:18:38 i clicked that, thinking it would lead somewhere 18:18:43 thanks again, ICANN 18:18:47 you can't tell anymore 18:18:48 yeah 18:18:58 ICANN has cheezburger 18:20:16 Bike: Yes that confusion happens a lot. To be fair, memoization is a very common implementation strategy for dynamic programming. 18:21:29 oh sure 18:22:03 unrelatedly, does anyone else think it's funny when fib is used as an example for recursion and memoization, since you can do it way better with linalg 18:22:37 tromp_: what I like about memotrie (possibly because I came up with the same design at some point) is the split memo = untrie . trie, where 'trie' and 'untrie' give you access to the actual data structure used for memoization. 18:23:10 tromp_: (personally I call 'trie' 'populate' and 'untrie' 'loopkup', but that's just colors of a bikeshed) 18:23:17 int-e: everyone came up with the same design at the same time, or so i hear 18:23:19 *lookup 18:23:20 i prefer salmon 18:23:51 shachaf: not everyone; plenty of memoization libraries revolve around 'memo'. 18:24:27 conal and luqui released their memoization libraries within hours of each other or something 18:25:11 `run words --eng-1M 1000 | grep -o '\w*b' | sed 's/$/ong/' | sort | uniq | /usr/bin/paste -sd\ | head -n 20 18:25:12 bong hbong subong 18:25:33 `run words --esolangs 1000 | grep -o '\w*b' | sed 's/$/ong/' | sort | uniq | head -n 20 | /usr/bin/paste -sd\ | rainwords 18:25:34 ​bong 18:25:38 Bike: I think it's a fine exemple for introducing the memoization concept. You want people to think about the structure of the computation rather than the actual computed values. 18:26:01 yeah sure 18:26:12 just for my understanding: in the K lambda diagram, one could have left out the upper half of the vertical bar? 18:26:26 erm 18:26:29 nvmd 18:26:35 it's a good example for recursion too, i just imagine a million programmers using these implementations in actual programs 18:27:03 Bike: fortunately fibonacci numbers aren't all that useful in practice ;-) 18:27:21 how rude! i have to simulate fuckbunnies all the time 18:27:24 especially the larger ones where the linear algebra starts to pay off. 18:27:34 But memofib is such algebraic, much compositional 18:29:05 unlike linear algebra 18:35:30 ) mp 18:35:31 FireFly: |value error: mp 18:36:53 > fix ((0:) . scanl (+) 1) 18:36:54 [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377,610,987,1597,2584,4181,6765,10946,... 18:36:56 -!- ^v has joined. 18:37:53 what the hell is fix 18:38:04 a fixed point combinator 18:38:12 ah 18:38:13 :t fix 18:38:13 (a -> a) -> a 18:38:34 > fix error 18:38:36 "*Exception: *Exception: *Exception: *Exception: *Exception: *Exception: *Ex... 18:39:19 (Sorry, that one is getting old.) 18:40:30 > fix unsafeCoerce :: Int 18:40:32 Not in scope: ‘unsafeCoerce’ 18:40:56 ) mp =. +/ . * 18:40:56 FireFly: |ok 18:41:04 ) <"2 mp^:(<10)~ 0 1,.1 1 18:41:05 FireFly: +---+---+---+---+---+----+-----+-----+-----+-----+ 18:41:05 FireFly: |0 1|1 1|1 2|2 3|3 5|5 8| 8 13|13 21|21 34|34 55| 18:41:05 FireFly: |1 1|1 2|2 3|3 5|5 8|8 13|13 21|21 34|34 55|55 89| 18:41:05 FireFly: +---+---+---+---+---+----+-----+-----+-----+-----+ 18:41:21 J <3 18:42:30 oh of course j, the language whose linenoisiness is only beated by teco 18:42:53 at least it's ASCII 18:42:59 what is teco? it sounds like i want to learn it 18:42:59 unlike APL 18:43:02 can you really say that in the land of haskell oneliners........... 18:43:07 teco is the editor emacs is based on, or something 18:43:12 emacs = editor macros (for teco) 18:43:19 ew 18:43:31 teco is like the esotericest esolang ever 18:43:44 teco actually does not resemble emacs in normal use at all 18:43:45 I understand that it (emacs) wasn't based on Lisp at that time. 18:43:55 and people used it seriously! 18:44:05 I used ed seriously 18:44:16 That's not as weird 18:44:19 int-e: yep, it was basically a screen editor written in a scripting language for another editor 18:44:42 (ok. a clone that was implemented in lpmud) 18:45:09 -!- shikhout has changed nick to shikhin. 18:46:07 Actually that's about the fragment of vi that I know to use. I use emacs for larger edits. 18:46:28 so, emacs was written with an editor that was written in a language for a third editor? 18:46:37 (where s/vi/vim/ because I use the cursor keys) 18:47:18 myname: no, it run on the teco editor's scripting language 18:47:29 and how did we end up discussing text editors anyway ... such a loaded topic is best avoided on programming channels. :) 18:48:11 there are things to avoid. politics, religion and text editors (or is that part of the second one?) 18:48:24 or maybe the former 18:48:27 or both 18:48:45 yes. 18:49:05 it came up because nortti mentioned it, like, five minutes ago 18:49:19 7 mins, actually 18:49:47 /like/ 18:49:59 no, I do not 18:50:06 So, uh, thoughts on Unity? 18:50:15 the DE? 18:50:17 * FireFly attempts to divert the channel to a less controversial topic 18:50:28 yes 18:50:44 terrible. literally the antichrist, foretold in the holy texts 18:50:57 last I used it (12.04?) it was still kinda buggy but I could see how they could make it usable 18:51:17 then again, I could more easily see how they could fuck it up completely 18:51:31 I have not yet had the displeasure of using Unity, and I have no plans to change that. 18:51:42 usability doesn't matter. it's perfect and it's evil 18:51:53 why is it evil? 18:52:02 once its market share has increased the goat shall release the third seal 18:53:29 yay, DDG ranks the game engine before the desktop environment. 18:55:27 probably ranks gnomes before gnome as well 18:56:06 nope, gnome.org is the highest 18:59:46 I am somewhat worried that I haven’t seen a serious project to provide a waylandish xmonad-alike yet. 19:00:02 what, is xmonad that tied to x 19:00:22 uh, in wayland the wm itself also does display server 19:00:32 I think most WMs are 19:00:41 What nortti said. 19:01:42 * nortti wonders into how small space can be a complete wayland impl be fitted into 19:02:05 I'm a bit worried about that too.. I've been meaning to try out wayland, but I've gotten too used to tiling window managers to be comfortable with weston 19:06:06 -!- tertu has joined. 19:13:22 fungot: g'evening 19:13:22 FireFly: i didn't mention that. i think there's my name in for a bit more 19:15:36 this is also why i'd have a hard time switching to OS X 19:15:40 that and the dismal state of package management 19:18:59 what is why? because fungot didn't mention that? 19:18:59 Bike: eck, not for efficient programming :) 19:19:04 yeah 19:20:08 -!- conehead_ has joined. 19:22:22 perhaps fungot will fix my makefile 19:22:22 kmc: i'm building off of esr's pronouncements is highly questionable. 19:23:05 -!- conehead has quit (Ping timeout: 264 seconds). 19:24:01 it is 19:24:27 confirm 19:34:52 they put quantum::superpositions in perl6 lol 19:35:09 -!- ^v has quit (Read error: Connection reset by peer). 19:35:14 -!- AnotherTest has quit (Ping timeout: 240 seconds). 19:35:21 Is that for the & and | (or whatever it was) operators? 19:35:30 yea 19:35:37 -!- ^v has joined. 19:36:03 I never really understood them 19:37:02 were those the ones detailed in the talk about perl and physics? 19:39:35 I don't know, but they're explained in http://en.wikipedia.org/wiki/Perl6#Junctions 19:47:43 -!- mhi^ has quit (Quit: Lost terminal). 19:48:29 -!- ^v has quit (Ping timeout: 252 seconds). 19:49:57 -!- ^v has joined. 19:56:35 -!- mhi^ has joined. 19:59:07 -!- Sprocklem has joined. 20:04:41 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif). 20:07:31 -!- tertu has quit (Ping timeout: 240 seconds). 20:16:16 -!- tertu has joined. 20:21:50 -!- quintopia has quit (Ping timeout: 255 seconds). 20:26:11 -!- tertu has quit (Disconnected by services). 20:26:11 -!- ter2 has joined. 20:31:27 -!- nucular has quit (Quit: Excess Food). 20:35:14 -!- Bike has quit (Ping timeout: 258 seconds). 20:36:51 -!- Bike has joined. 20:49:01 -!- tertu3 has joined. 20:49:14 tromp_: would 0000101110110 = \\(0 2 1) ==> U(p,z) = <2,z> contribute to the halting probability or is it limited to closed terms? 20:50:58 -!- oerjan has joined. 20:51:27 impl<'sink, In, Out, Hold: TreeHandle, Sink: TreeSink> TreeBuilder<'sink, Sink> { 20:51:29 hmm. 20:51:30 B| 20:52:21 kmc: what is that? 20:52:41 a mess. 20:52:49 -!- ter2 has quit (Ping timeout: 276 seconds). 20:52:58 is kmc making an esolang 20:53:17 Yeah, I think it's called "rust" 20:53:23 that depends, is HTML parsing turing complete? 20:53:26 i'm not making Rust 20:53:28 just using it 20:53:38 well I have a few patches in rust 20:53:47 See 20:53:54 Contributing to an esolang, then :P 20:53:58 :D 20:54:03 it's less eso than C++ 20:54:06 tromp_: Oh. I see you're "only" requring the <_,z> context to be in normal form. that also answers my question then. 20:55:01 hm I have 10 commits in rust, that's more than I thought 20:55:17 several of them are in code that no longer exists 20:55:18 my wild guess is that standard html parsing is not tc but that html-that's-actually-used parsing is. 20:55:23 two of them are fixing the same thing that broke twice 20:55:31 oerjan: the idea of HTML5 is to unify those two things 20:56:19 good, good. 20:56:28 so probably uncomputable, then. 20:56:49 it's a precise spec for how to handle even very broken content, so that all browsers will do it the same way 20:57:02 as a result it's stupifyingly complicated 20:59:42 The spec is really just taking the crazy way in which browsers have already been parsing broken HTML and formalizing it so that you can continue to write the same broken HTML in perpetuity. 21:00:05 well, yes and no 21:00:06 shachaf: yw 21:00:14 it specifies which constructs are considered broken 21:00:23 conformance checkers will reject them, but their meaning is still specified 21:01:01 int-e: yeah, the halting prob. definition is subtle. i believe the normal form requirement is necessary to allow identifying all programs that contribute to an omega prefix 21:01:18 -!- MindlessDrone has quit (Quit: MindlessDrone). 21:01:37 Yeah, but that's not really different than how it's been previously. The upshot is that it still renders. 21:02:47 IE6 somehow manages to parse tag-soup mess into where an element could have a child whose parent isn't the first element 21:03:00 s/into where/so that/ 21:03:12 i don't want to have U(p:z) = in there either 21:04:41 -!- Patashu has joined. 21:05:00 The non-tree DOM, right? Looking at the graphs for those was "fun." 21:05:26 tromp_: Actually, why not? As long as it reaches that point without looking at the 'z' part ... hmm. Tricky. 21:06:01 monotone: yeah, Hixie has some fun diagrams in an old blog post: http://ln.hixie.ch/?start=1037910467&count=1 21:06:33 tromp_: Anyway it looks to me like you have no unique definition of \Omega. The BLC.pdf draft does not mention a normal form property at all, stating that you might just as well not have it. 21:06:42 but i doubt if the goodstein function can avoid recursion <-- i wonder if the functions expressible in system F are the same as those that can be proved total in peano arithmetic, or something like that. 21:07:24 i want to be able to prove the famous symmetry of information thm 21:07:27 oerjan: that excludes fix? 21:07:37 int-e: yes 21:07:47 for this purpose, at least 21:08:00 that paper has an obsolete definition:( 21:08:06 which i shld update 21:08:33 non-tree DOM? :( 21:08:44 this is why we can't have nice things 21:09:09 I wonder how the HTML5 algorithm would parse that example.. 21:09:17 -!- Sprocklem has quit (Quit: Watching rugby). 21:09:23 int-e: but importantly, it includes church numerals. 21:09:29 to prove symmetry of information, you must be able to take any halting computation and see if the output is a pair starting with some given x 21:09:41 (forall a. (a -> a) -> a -> a) 21:10:07 tromp_: anyway, as I read it, 'z' would be a symbolic variable (to prevent the program from inspecting the input beyond the "consumed" part), but then z is also a normal form, so U(p:z) = would be allowed. 21:12:54 no, z is not in NF 21:13:19 oh hm no system F is stronger than that https://en.wikipedia.org/wiki/Second-order_arithmetic#Definable_functions_of_second-order_arithmetic 21:13:20 NF should be closed terms 21:14:30 that works. 21:15:25 FireFly: http://www.whatwg.org/specs/web-apps/current-work/multipage/the-end.html#misnested-tags:-b-i-/b-/i 21:15:43 i've been meaning to rewrite that paper for ages:( always other stuff getting in the way 21:16:02 right now i'm preoccupied both with cuckoo cycle and 8x8 connect-4 :( 21:16:17 what are you doing with connect 4? 21:16:24 (is that standard? in first order term rewriting, free variables are everywhere (there's no way to bind them...)) 21:16:29 trying to solve it 21:17:01 so variables as normal forms are also everywhere. 21:17:04 as in which player wins with optimal play? 21:17:21 yes, kmc 21:17:26 width 8 ... oh that would upset my intuition about the game a lot. 21:17:36 how are you going about it? 21:17:47 i should edit that article to make explicit what that i mean closed normal forms, int-e 21:18:36 kmc: hm, that seems to match the Mozilla behaviour from 2002 21:18:46 well, i have a solver that works some dozen plies into the game 21:18:57 kmc: you should see http://homepages.cwi.nl/~tromp/c4/c4.html 21:18:58 the element cloning is a bit bizarre, but it's invalid to begin with so I guess it doesn't matter too much 21:19:03 now i need to play lots of games and build an opening library 21:19:55 tromp_: the last link + the first parentheses in https://en.wikipedia.org/wiki/Goodstein%27s_theorem would seem to imply that the goodstein function _can_ be expressed in system F. 21:20:07 *that last link 21:22:34 you mean "The Power of a Detour via Infinity", oerjan? 21:22:57 no, i mean _my_ last link https://en.wikipedia.org/wiki/Second-order_arithmetic#Definable_functions_of_second-order_arithmetic 21:23:58 i realized my sentence was ambiguous and that's why i changed to "that" 21:24:42 hmm, how does definability in system F related to definability without recursion? is that equivalent? 21:24:55 system F has no recursion 21:25:12 it's rank-N typed lambda calculus 21:26:39 ic. so i should be able to redefine my function g without using haskell's recursion 21:27:06 but it may not be pretty:-( 21:27:25 -!- Patashu has quit (Ping timeout: 265 seconds). 21:27:56 tromp_: the church numeral thing should JUST WORK, if you give church numerals the right type (forall a. (a -> a) -> a -> a) 21:28:04 i'd sort of expect you'd need to represent ordinals. 21:28:40 yes, another property of system F is that you can _define_ church numerals as the terms of that type 21:29:21 this also works for church representations of many other data types 21:31:30 e.g. the only system F terms of type forall a. a -> a -> a are the church booleans 21:32:47 system F is the original system with parametricity, and unlike haskell's version there are no subtle caveats for when it applies. 21:33:22 which subtle caveats 21:33:27 bottoms and seq 21:33:58 @let scow = seq 21:34:00 Defined. 21:37:29 http://s.cow 21:37:45 https://cow 21:38:12 tromp_: btw if the implementation of g in system F depends heavily on higher rank types, then it's likely you may need explicit type annotations to make it compile as haskell. 21:38:29 -!- augur has quit (Ping timeout: 258 seconds). 21:38:34 (with ghc's rank-n extension) 21:39:17 -!- Bike has quit (Ping timeout: 264 seconds). 21:39:44 because haskell's type inference only infers rank-2 types with all foralls outermost. 21:39:56 um 21:40:27 i'm not sure if that is considered rank-2 21:41:02 -!- Bike has joined. 21:41:08 ghc doesn't infer rankine types hth 21:42:23 `frink 100 rankine -> kelvin 21:42:28 Warning: undefined symbol "rankine". \ Warning: undefined symbol "rankine". \ Unconvertable expression: \ 100 rankine (undefined symbol) -> 1 K (temperature) 21:42:38 darn 21:43:00 apparently frink doesn't support them at all 21:43:05 even with explicit annotations 21:43:10 shocking 21:44:29 -!- Phantom__Hoover has quit (Ping timeout: 250 seconds). 21:52:28 I didn't even know about it. Is it actually used for anything? 21:52:34 It seems like a terrible scale 21:54:05 I think a lot of engineering in the US is still done with ye olde units 21:54:45 * kmc wonders if BART gauge is 1676 mm or 5'6" 21:56:42 a difference of 400 microns 21:57:20 100 microns sounds much smaller than 0.1 mm 21:57:25 Isn't that less than the error caused by heat fluctuations? 21:57:26 -!- Phantom__Hoover has joined. 21:57:31 Taneb: probably 21:57:57 it's easy to prove that arbitrary long gaps in the sequence of primes exist, just use the CRT [...] <-- n! + i, i = 2..n hth 22:03:10 true 22:06:53 Taneb: hm, no, I think it's about an order of magnitude larger 22:07:30 :( 22:07:37 steel expands by a factor of 13e-6 / °C; record temperature range in SF is 43 °C 22:08:04 What's really scary is the age of my university is of the same order of magnitude as my age 22:08:16 top of a rail is about 7 cm 22:08:23 -!- HackEgo has quit (Remote host closed the connection). 22:08:33 -!- HackEgo has joined. 22:08:38 which comes out to about 40 microns 22:08:44 > 7 * 43 * 13e-6 22:08:45 3.913e-3 22:08:53 > 0.01 * 7 * 43 * 13e-6 22:08:55 3.913e-5 22:10:04 > 3.913e+1 22:10:06 mueval-core: L.hs: removeLink: does not exist (No such file or directory) 22:10:10 Yeah 22:11:43 hmm. 22:11:58 Munkkikorppikotka. 22:12:33 (this reminds me that I don't know for certain why this happens. mueval copies that file to /tmp, but can several muevals run concurrently?) 22:13:57 hmm, it copies L.hs to /tmp/L.hs? 22:14:51 http://en.wikipedia.org/wiki/Thermal_expansion#Examples_and_applications "Thermal expansion of long continuous sections of rail tracks is the driving force for rail buckling. This phenomenon resulted in 190 train derailments during 1998–2002 in the US alone." 22:15:16 i think that's buckling because it gets longer, not thicker 22:15:21 olsner: sadly, yes. that's where it puts the temporary haskell file to be loaded, and it doesn't set an include path in ghci 22:15:40 where by ghci I mean ghc-as-a-library. 22:18:16 then I assume/hope that only one evaluation can be running at a time? 22:18:55 is it lambdabot that copies the file and runs mueval on it, or is that in mueval? 22:18:57 00:10:06 mueval-core: L.hs: removeLink: does not exist (No such file or directory) <-- this is evidence to the contrary 22:19:04 it's mueval 22:19:51 which should probably create a temprary subdirectory in /tmp each time instead. 22:20:12 just to avoid this problem. oh well. 22:21:53 -!- impomatic has quit (Ping timeout: 264 seconds). 22:26:43 -!- tertu3 has quit (Ping timeout: 240 seconds). 22:35:49 -!- impomatic has joined. 22:36:19 via agora http://www.loweringthebar.net/2014/05/sign-installer-cited.html 22:44:03 -!- Eritzap has joined. 22:45:46 -!- Sgeo has joined. 22:48:05 -!- Eritzap has quit (Client Quit). 22:52:06 Who's kumool 22:52:15 Maybe not part of here 22:52:58 `coins 22:53:00 ​papacoin flumpezzycoin vergenigmationcoin dupcoin earenamcoin percoin regxcoin fullcoin adedcoin andomcoin carcoin closuricoin inctcoin funandcoin voltacoin bearecoin ozakcoin numpcoin brbcoin acrcoin 22:53:13 I think we've seen dupcoin before. 22:53:40 Sgeo: wat? 22:53:45 -!- nooodl has quit (Ping timeout: 252 seconds). 22:54:00 kmc: might be a duplicate. 22:54:30 i also have a hunch we'll see brbcoin again 22:55:00 oerjan: someone in tcl said 22:55:10 "wow Sgeo i find an interesting language and you are already in channel" 22:59:11 -!- augur has joined. 22:59:25 spoooky 22:59:54 Sgeo: are you in all the language channels twh 23:00:19 No, but I'm in a lot of them 23:01:44 -!- yorick has quit (Read error: Connection reset by peer). 23:02:19 -!- mhi^ has quit (Quit: Lost terminal). 23:02:28 Java, Prolog... actually, seem to be banned from ##prolog :(, Ada, Agda, Atomo, Atomy, Chicken, Clojure, Concatenative (Factor etc.), Dylan, Elixir, Erlang, Guile, Haskell and some associated channels, Idris, Lisp (CL), Pharo, Smalltalk, Racket, Red-lang, Retro, Scala, Scheme, Self-lang, sgeolang, Tcl 23:02:51 how did you get banned from ##prolog 23:02:52 haha how do you get banned 23:03:05 was the ban message "No."? 23:03:37 kmc: nah they just cut him off 23:03:44 -_- 23:10:45 * impomatic notes that Sgeo isn't in Forth, Oberon or Pascal :-P 23:11:46 whoa, a language channel that banned Sgeo? 23:11:56 i must investigate this 23:12:14 ##prolog: ban *!*@*.dyn.optonline.net 23:12:25 oh. 23:12:27 boring. 23:12:38 [wiki] [[Special:Log/delete]] delete * Ehird * deleted "[[Sngscsv]]": content was: "todo" (and the only contributor was "[[Special:Contributions/Dggh|Dggh]]"); possibly spam? feel free to recreate when there's more content 23:12:43 yes 23:13:21 Why block an entire ISP? :( 23:14:07 internet scow provider 23:16:24 Sgeo: if there's an ip-changing troll from there... 23:16:59 (also, i hear cloaks exist.) 23:17:24 actually, do they help against that... 23:18:04 yes 23:28:25 -!- tertu3 has joined. 23:31:57 -!- ter2 has joined. 23:35:24 -!- tertu3 has quit (Ping timeout: 258 seconds). 23:49:27 -!- ter2 has quit (Read error: Connection reset by peer). 23:49:49 -!- ter2 has joined. 23:55:58 (ok. a clone that was implemented in lpmud) <-- ooh me to 23:56:09 also i learned lpc before real c 23:56:24 -!- shikhout has joined. 23:56:57 that lpmud ed may be the reason i ended up a vim user 23:59:40 -!- shikhin has quit (Ping timeout: 265 seconds).