00:01:18 I think the mirrors act like they do in Floyd's Bumpershot (a game I have read about somewhere; I haven't played). Adding the other pieces of that game and of Black Box game, can make it a generalized version of those game; I already said the computer tells you ahead of time how many mirrors, how many arrows, etc; you could also make the user configure the possible range of how many. Now it can make a superset of these games. 00:02:05 -!- doesthiswork has joined. 00:09:30 there's also the undead puzzle from tatham's collection that is a bit similar. 00:10:06 hm didn't doesthiswork say something in the logs i wanted to quibble about :P 00:10:16 yes? 00:10:27 i've just forgotten what it was 00:10:45 probably something about lambda calc fixed points 00:11:07 I am addicted to Listerine PocketPak strips 00:12:26 oh right. i think the others shot that down for me. what i wanted to say is that the fixed point theorem doesn't apply to _typed_ lambda calculus, because the types are usually specifically made to avoid nontermination (without explicit recursion), which is essential to construct the usual diagonal argument. 00:18:18 ok 00:19:22 or perhaps equivalently, the fixed point theorem is incompatible with types that give you a curry-howard isomorphism with a consistent logic. 00:20:09 which looked like what you were trying to look at 00:20:32 -!- yorick has quit (Remote host closed the connection). 00:21:26 What have people used the fixed point theorem to prove? 00:25:38 -!- copumpkin has quit (Ping timeout: 246 seconds). 00:25:46 that you can do arbitrary recursive computations? 00:26:14 -!- copumpkin has joined. 00:26:31 i am not aware of any more technical uses 00:27:45 i suppose it also destroyed church/curry's original attempts to do logic in lambda calculus/combinatory logic without any types 00:28:05 which may be what you have rediscovered 00:28:25 Yes, that is exactly the problem I was trying to understand 00:29:20 and it does this in a way that is similar to how russell's paradox destroyed naive set theory, i think. in fact they are both diagonal arguments. 00:29:55 as are godel's incompleteness theorem and turing's halting problem proof 00:29:59 *gödel 00:30:50 a great deal of rampage and destruction from just one basic proof idea, there. 00:31:03 yes, it is wonderful 00:31:20 there are also the complexity hierarchy theorems, which might not be considered destructive. 00:32:03 Is the typed lambda calculus basically like what Hofstadter called "rule of detachment" and "fantasy rule" (also, as it says, often called the "Modus Ponens" and "Deduction Theorem")? 00:33:52 zzo38: um there's the curry-howard isomorphism with intuitionistic propositional logic terms in -> , those would both be rules of that so i suppose they are included... 00:34:14 oh hm 00:34:23 Yes, of intuitionistic logic, I know, not of classical 00:34:33 you mean application is like modus ponens and lambda is like the deduction theorem? 00:34:43 when you look at what they do to types 00:34:45 Yes. 00:34:56 i suppose so, yes 00:37:59 -!- brainstorming has joined. 00:38:54 -!- brainstorming has left. 00:39:17 What would be the shortest possible sequent calculus which is Turing complete? 00:40:57 Do Wang tiles remain Turing complete when generalized to different geometries? 00:41:13 I would expect so 00:42:00 if you restricted them to a finite area they wouldn't 00:42:33 Yes, I know, I mean geometries which have infinite areas? 00:43:43 since you can embed 2d wang tiles in any such geometrty I would have to say yes they'd still be turing equivalent 00:45:44 But what if the tiles are triangular or something like that? 00:47:41 stick two triangles together and you have a parallelogram. Tile the plane with this shape 00:50:41 (I don't know how to embed 2 dimensions in a one dimensional line) 00:51:05 O, yes, you can make a parallelogram like that, if you add an extra color. 00:56:05 doesthiswork: i am pretty sure one-dimensional tiling is _not_ TC (should be a finite automaton, essentially) 00:58:14 Then I wonder what the minimum number of dimensions needed for a tiling to be TC. I think 1.5 is possible 01:02:20 i am not sure that fractal dimensions are compatible with tilings. 01:02:51 maybe they are, though 01:05:09 I think the serpinski triangle could host a TC wang tiles. 01:06:35 *take out the 'a' 01:06:54 **-a 01:07:54 thank you 01:16:02 -!- sacje has quit (Ping timeout: 246 seconds). 01:18:16 zzo38: are Wang tiles a sequent calculus? 01:18:55 And what does it mean for a sequent calculus to be TC? Does it mean that there's a such-and-such which maps Turing machines onto statements in the calculus such that the statement is provable if and only if the machine halts? 01:33:06 sounds like the obvious interpretation, anyway 01:34:06 tswett: I don't know, maybe it would be possible to make a sequent calculus of Wang tiles but I don't know 01:34:44 tswett: Yes, that is what I mean by a sequent calculus to be TC (and I have made a set of sequent calculus rules which implement a Turing machine). 01:37:56 I have also made up a way to interpret a sequent calculus as an asymmetric game (although the initial state isn't a part of these rules; it must be decided separately somehow). Put the initial state at the bottom, and follow the rules going up. The first player's job is to select a rule and substitutions in it. The second player's job is to select one of the sequents above the line in that rule. Whoever has no legal move loses. 01:41:02 (Because it is Turing-complete, it is possible to result in a draw, and there isn't necessarily any way to know it is a draw, although sometimes it is possible to tell.) 01:44:05 There is a game semantics for linear logic. 01:45:39 But I don't really know what its significance is. 01:46:47 a lot of things and logics have game semantics, where you have a goal and things which both help and hinder you from reaching that goal. 01:47:43 I think that is a different kind of game semantics though. 01:48:30 I like to call them 'adversarial models'. I think they're called that. 01:49:58 Gracenotes: now the question is, how do you make a program that will make qualifying and quantifying human knowledge into a logical framework that can be interpreted by computers as fun as a video game!?! 01:50:41 "trivial pursuit, forever" 01:52:09 you are right, you can never make programming a computer as fun as farmville.. 01:52:48 actually i take that back, farmville sucks. 01:52:57 programming is much better 01:53:05 I thought your first statement was sarcastic 01:53:22 its a pie in the sky idea 01:53:41 human knowledge isn't logical, and it can't be put into a logical framework 01:53:55 I have heard of people happily doing repetitive tasks over and over without the slightest thought of automation. 01:53:56 well you can create a mapping of the illogic 01:54:00 although perhaps you refer to the small subset of human knowledge that has explicit structural representations 01:54:44 Well, you can make some kinds of human knowledge into a logical framework, and some kinds of logical framework can be used for representing human knowledge, but actually it is different things, and their purposes can also vary a lot, and these also aren't the only two things. 01:55:43 neurplasticity is pretty remarkable 01:56:17 In any case, a lot of pieces of knowledge are not universally true; they come attached with probabilities. 01:56:29 with priors, both explicit and implicit 01:56:44 right thats true, but there is a lot of data out there that could be structured but isnt. 01:57:06 now the question is how do you make structuing that data appealing to a wide, non techinical audience? 01:57:14 I 'know' that this car 100ft ahead of me is going to change into my lane in front of the car in front of me within 5 seconds 01:57:16 even for vanities sake 01:57:18 for instance 01:58:12 (without a turn signal, in this case) 01:58:13 such as the relationship between all dongs which contain a particular four note riff 01:58:14 Well, if it helps (or is even the least bit relevant at all), I have made a sequent calculus for sokoban game. 01:58:28 as in structuing data about yourself, to create a "social media collage" of the unstructued data available on the internet. 01:58:32 stupid swype 01:58:42 dongs 01:58:49 s/dongs/songs/ 01:59:03 no, i like this one. 02:00:16 so although the collage may not have much structured data attached to it, it would be possible to publish this data structure and further integrate it with other structures that people have made. 02:00:45 in general, people assume universality a lot more than it actually exists 02:01:07 What do you do with the multiple incompatible strucctures obtainable from different social networks? 02:01:49 language (both natural and constructed/computer, actually) flattens it into communicable form. Very very restrictive. 02:01:51 well, so im trying to see if it is possible to have a semantic network of information slowly built by individual actors 02:02:31 so you could create a judgement that "obama is the president". although that would obviously have to have some sort of symbolic representation. 02:02:57 and that like i said earlier, it would even be open to vanity statements. such as "this is a picture of what i had for lunch" 02:03:22 so now you have all this associations that are only semi structured at this point 02:03:50 How do these "judgments" relate to intuitionistic type theory? Or the unstructured information ("intuitions")? 02:03:57 the interesting part comes from when a large amount of people agree on the symbolic representation that "obama is the president" 02:05:08 or even the minor unimportant details as affirming symbolically that your firend did indeed have what she said for lunch 02:05:23 thus adding more weight to the judgement, or proposition 02:06:35 any thoughts? 02:06:46 what is going on 02:06:54 lol, im talking about my crazy idea 02:07:19 i already asked questions :-( 02:08:11 stuff 02:08:16 right, ok so the most important part is the consensus on symbolic representation of our "common knoledge" in the world. the social media bit is essientially just a hook. 02:08:19 Bike: ^ 02:08:42 But that's where you have to get information from. And people deploy different "personae" on different networks. 02:09:09 * oerjan wonders if Cyc is still around 02:09:15 exactly. its not like a spider, but more of a knowledge base. 02:10:15 but what im trying to wrestle with is appeal to a general audience. 02:11:37 or more generally, how you would interact with the system. so would you be presented with information that affirms or refutes your collection of symbolic expressions. 02:12:54 so say you decide to claim that "obama is not the president". it would display the fact that you did, and the cout of times that that symbol has been affirmed and possibly a list of the people that publically affirm that symbol 02:13:38 so now you have the affirmation of the symbol that obama is NOT the president. so obviously there will be magnitued more people affirming that he is the president 02:14:18 so there is a shared truth value associated with him being the president. say 99% say he is and 1% say he isnt. 02:14:38 so thats boring 02:15:22 or well, it will be interesting what comes out of it, but in essence its just a massive collection of abstract representations of fact 02:15:42 so now how do you present this, or more specifically what? 02:16:48 obviously there are some simple things, like creating a profile of the user. and finding individuals that have said similar things, and then present things that these similar individuals have said 02:17:31 so essentially it would be similar to "collaborative filtering". 02:18:13 but the problem with systems like those is that you are only shown things that agree with your worldview. 02:20:01 anyway, like i was saying. this is kind of a pie in the sky idea.. 02:20:38 but i think its on a thread that we have been attempting to follow for a long time.. 02:21:02 i mean OWL, RDF and all those technologies failed hardcore 02:21:38 and i want to see how to make that an integral part of the general publics experience of the internet. 02:22:11 02:23:01 the best successes that have been had so far with human-like learning are neural nets 02:23:20 in particular, semisupervised deep learning architectures 02:24:24 yeah, ive heard similiar things too. i have some experience with NN, they are really interesting. sadly they like all models still suffer from the curse of dimensionality 02:24:49 have you heard about hierarchical temporal models? 02:25:04 they are really interesting for "streaming" sources of data 02:25:42 yes, that's mainly where unsupervised pretraining makes NNs amazing 02:25:42 and can pic out not just static patterns, but temporal ones as well. its very interesting. 02:25:54 regarding dimensionality curse 02:26:43 and I've seen interesting applications of NNs embedded in Bayes nets/fields 02:26:50 to represent temporal things 02:27:00 interesting 02:27:06 do you have any links? 02:27:39 http://www.youtube.com/watch?v=VdIURAu1-aU 02:28:08 hm, there might be an updated version of this recently released... /me will have to watch it 02:28:10 Oh! 02:28:15 ive see that video 02:28:26 hmm, its been a while though.. 02:28:31 ill have to rewatch it 02:28:49 yeah, i think the HTM is also mentioned in a google tech talk 02:29:13 in a talk? hm, do you know which one? 02:29:19 i guess not 02:29:20 http://youtu.be/48r-IeYOvG4 02:34:38 -!- oerjan has set topic: 22nd IOCCC opens August 1 http://ioccc.org/2013/rules.txt | jsvine is doing an esolang survey!: https://docs.google.com/forms/d/1OvEsdBioOFcXFAiscO34kctUWKs3dWQs5-ZouXdwy9Q/viewform | logs: http://codu.org/logs/_esoteric & http://tunes.org/~nef/logs/esoteric/. 02:34:53 -!- oerjan has set topic: 22nd IOCCC opens August 1: http://ioccc.org/2013/rules.txt | jsvine is doing an esolang survey!: https://docs.google.com/forms/d/1OvEsdBioOFcXFAiscO34kctUWKs3dWQs5-ZouXdwy9Q/viewform | logs: http://codu.org/logs/_esoteric & http://tunes.org/~nef/logs/esoteric/. 02:39:39 A description of the Unicode character set, written in the Georgian language, phonetically transcribed into mirror-reversed Devanagari script. Footnotes to the text are in Cree (phonetically transcribed in Kannada script), Occitan (transcribed in Pitman shorthand), Xhosa (transcribed into a variant of Braille normally used for Russian), Pennsylvania German (transcribed in Glagolitic script), Miqmaq hieroglyphs, an unidentified language transcr 02:40:13 an unidentified language transcr 02:41:30 i find it somewhat unlikely they could get together enough speakers to make that with any better than google translate quality 02:41:53 also, i doubt google translate does cree. 02:47:48 Bike: How are they going to do that? 02:48:10 who's they 02:49:06 I don't know; I hoped you know. 02:50:05 Bike: when i say say "an unidentified language transcr" it's suppose to be a hint to you that your message got cut off, hth 02:50:14 *supposed 02:51:24 I didn't think it was important, but "ibed into vertical Manchu script, and several unidentified scripts." 02:54:41 WELL HOW CAN WE KNOW IT'S UNIMPORTANT IF YOU DON'T PASTE IT HTH 02:55:23 You can't, but I can. 02:55:49 Or, at least, you can believe it to be unimportant to you. 02:56:27 THIS IS A FLAGRANT VIOLATION OF MY CONSTITUENT RIGHTS HTH 02:57:02 taking away your natural rights k 02:57:59 Gracenotes: that's just not right 02:58:51 help Amazon is recommending Hello Kitty things to me 02:59:10 and also College Living Essentials 02:59:33 are there Hello Kitty College Living Essentials 03:00:38 probably twin XL bedsheets 03:04:40 Gracenotes: Are you in college? 03:05:19 Do you know about Z-machine? The new version of my Z-machine assembler is now released. 03:06:14 Although I want to make up a SSA intermediate language for use with Z-machine, and some Haskell library for making Z-machine files. 03:29:56 -!- JesseH has joined. 03:32:15 if you add reflection does it become an S-machine? 03:34:32 * oerjan swats doesthiswork -----### 03:35:19 doesthiswork: I have never heard of such a thing. 03:38:17 zzo38: it was just a bad joke. When you look at Z in the mirror it looks like S 03:42:46 doesthiswork has this special curve-smoothing mirror 03:43:56 rip hexagons 03:44:03 hexagonal wang tiles would be cool tho 03:44:14 I am addicted to Listerine PocketPak strips 03:49:33 doesthiswork: nop 03:50:26 are you a girl from 13 to 48? 03:51:27 if not then I don't know why it suggests hello kitty college things. 03:51:51 because I was looking at tea spoons 03:52:08 did you know there are Hello Kitty spoon sets? 03:52:35 are they good? 03:53:01 maybe, check the reviews. 03:53:04 yes I did, there are hello kitty every thing. Sanrio milks their cash cow for all she's worth 03:53:15 cash kitten 03:53:25 everyone loves cat milk. 03:56:46 -!- mnoqy has quit (Quit: hello). 03:56:50 doesthiswork: It isn't quite "S". 04:03:01 -!- Bike has quit (Ping timeout: 276 seconds). 04:04:28 -!- Bike has joined. 04:08:01 kmc: Yes, see if you can make hexagonal wang tiles too. And other shapes. 04:11:10 Could ordinary wang tiles be made into just shapes (no colors) (like puzzle pieces)? Such as different shape for each color (according to the direction, too) and the shapes are made so it also won't fit if it is rotated or flipped. 04:13:08 yes 04:13:46 yep 04:14:08 sorry for the short answer but it takes longer to describe than to imagine 04:15:37 zzo38: one way is to code matchingness as having corresponding zigzag patterns on their bordering edges 04:16:32 you can encode 0 as /\ and 1 as __ say 04:17:08 and \/ for the matching one 04:18:14 and apart for the zigzag patterns the rest can still be squares and whatever 04:18:23 *from 04:22:02 oerjan: Yes those are the kind of things I was thinking of 04:22:46 Although you use a different set of patterns for each edge, such that the opposite edges will fit together though, I think. 04:24:14 well yes that's what i mean 04:25:14 it helps if you have asymmetrical teeth, but those are hard to show in text. 04:25:48 doesthiswork: Yes I thought of that too. 04:26:21 hm right you could do that, although i was thinking you could just fix the direction by having /\ on one end and __ on the other. oh hm __ may not be the best choice. 04:26:43 /\ and |^| perhaps 04:27:37 Yes, the nice thing about trinary is it has a direction 04:27:40 oh well that's a small detail. 04:28:29 Cut out the outline of "GREEN" along the edge 04:28:52 Brilliant in it's simplicity 04:29:04 And "TEAL" and "COSMIC LATTE" (you may need a fine craft knife for this one) 04:30:08 ...that _is_ brilliant :P 04:38:17 http://25.media.tumblr.com/a81cc3de8df6eab463ac666079105112/tumblr_mqmppwmOZA1qjr3c0o4_250.jpg 04:55:14 thx bookmarked 05:14:49 -!- CADD has quit (Read error: Connection reset by peer). 05:14:55 -!- CADD has joined. 05:21:44 -!- nooodl__ has joined. 05:22:03 -!- nooodl_ has quit (Read error: Connection reset by peer). 05:23:13 -!- zzo38 has quit (Disconnected by services). 05:23:18 -!- zzo38 has joined. 05:27:47 OK 05:27:53 ? 05:29:35 -!- nooodl__ has quit (Read error: Connection reset by peer). 05:35:47 I want to make a board game that exercises skill at organizing things the same way you have to do for a program. 05:36:14 How would such a thing be made? 05:37:22 I don't know, my best idea so far is some puzzle peices that each turn you have to use to make a structure that satisfies that rule 05:39:37 because jigsaw puzzles have the dynamic of organizing pieces 05:39:55 but I'm having trouble thinking of the right sort of rules 05:42:15 I don't know either. 05:48:45 but also the necessity of organizing a program is only learned when you have to keep modifying it to match the changed plans 05:49:03 so I think that would be a fun game too 05:50:16 -!- Bike has quit (Ping timeout: 276 seconds). 05:50:53 -!- Bike has joined. 05:52:29 -!- Bike_ has joined. 05:53:54 -!- oerjan has quit (Quit: ghint). 05:55:28 -!- Bike has quit (Ping timeout: 276 seconds). 06:05:05 Sometimes a program might be organized before it is put into the computer. 06:06:51 Note to self: What I have been considering to be "Moonlight Sonata" is just the first part of Moonlight Sonata 06:17:48 fyi that's true of like every "classical" piece of music you know 06:17:52 -!- Bike_ has changed nick to Bike. 06:18:36 Anything is true of every classical piece of music you know 06:19:35 Classical music often has multiple parts; in what I have seen, if there are three parts, the first and third parts are with the same key but the second part may be of a different key, and often shorter, too. 06:22:12 15 minutes is the whole thing right? 06:23:33 -!- CADD has quit (Ping timeout: 248 seconds). 06:26:45 -!- copumpkin has quit (Ping timeout: 248 seconds). 06:27:21 -!- copumpkin has joined. 06:30:32 -!- CADD has joined. 06:30:56 -!- CADD has changed nick to Guest97377. 06:31:10 -!- stuntaneous has quit (Read error: Connection reset by peer). 06:31:32 -!- stuntaneous has joined. 06:37:38 -!- Guest97377 has changed nick to CADD. 07:20:40 -!- conehead has quit (Quit: Computer has gone to sleep.). 07:34:04 -!- carado has joined. 07:34:22 Once somebody made up a global enchantment card (for Magic: the Gathering) called "Nirvana" with the text "Goblins cannot reach Nirvana." I made up a meaning for this card, although it would hardly ever actually do anything. 07:36:38 If the Magic: the Gathering cards programming language I had the idea of, would exist and would be able to treat "reach" as a verb, then if you enter it as "Goblin=s cannot reach ~" then it might be able to understand it, too. 07:47:58 -!- dessos_ has joined. 07:48:05 -!- dessos has quit (Read error: Connection reset by peer). 07:52:41 -!- epicmonkey has joined. 07:53:53 -!- douglass has quit (Ping timeout: 240 seconds). 07:58:50 -!- mnoqy has joined. 08:00:35 * Sgeo wonders what zzo38's opinion of Magic the Gathering Online is 08:11:06 -!- CADD has quit (Read error: Operation timed out). 08:19:19 -!- CADD has joined. 08:25:08 -!- Taneb has joined. 08:25:17 Morning! 08:26:23 -!- zzo38 has quit (Remote host closed the connection). 08:28:52 -!- epicmonkey has quit (Ping timeout: 276 seconds). 08:30:13 Taneb: Feeling bright and happy and sober there, I guess? 08:30:21 :D 08:30:25 Barely hung over at all 08:30:36 Good genes, I guess. 08:31:06 I think last night I assumed I'd have forgotten a lot more 08:31:29 So I left myself a bunch of notes 08:31:35 But I remember what I wrote on the notes 08:33:26 Also I met someone called Panda 08:45:28 -!- CADD has quit (Ping timeout: 264 seconds). 08:46:40 Sgeo: what about the Magic: The Gathering Online eXchange 08:47:14 -!- iamfishhead1 has joined. 08:47:29 `relcome iamfishhead1 08:47:31 -!- carado has quit (Ping timeout: 246 seconds). 08:47:35 ​iamfishhead1: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 08:47:57 Hi shachaf 08:48:16 hiamfishhead1 08:50:46 Me. myself and I 08:51:11 Taneb: good meowrning? 08:51:25 Better than I expected 08:52:32 You? 08:55:57 I fell asleep for a nap at 7 and then suddenly it was 2 09:03:16 -!- iamfishhead1 has quit (Quit: Leaving.). 09:04:13 :O 09:04:48 I think that means you had 5 more hours of sleep than me :( 09:05:20 aww :< 09:15:15 -!- Frooxius has quit (Read error: Connection reset by peer). 09:15:32 -!- Frooxius has joined. 09:17:23 glad you're feeling well Taneb :) 09:17:44 :) 09:18:05 hi kmc 09:18:09 hi shachaf 09:18:20 I hope my friends are all okay 09:21:27 * kmc → sleep 09:23:32 goodnight! 09:23:51 wow, apparently one of the categories for the UK censorship thing is "esoteric material" they're onto us ;_; 09:24:36 as long as hexham doesn't start censoring things too 09:26:28 -!- Frooxius_ has joined. 09:29:19 -!- Frooxius has quit (Ping timeout: 276 seconds). 09:29:24 Goodnight, kmc 09:30:19 -!- Frooxius_ has quit (Client Quit). 09:41:05 -!- sebbu2 has joined. 09:44:44 -!- sebbu has quit (Ping timeout: 260 seconds). 09:52:36 -!- MindlessDrone has joined. 10:07:13 -!- sacje has joined. 10:42:59 -!- epicmonkey has joined. 10:45:57 -!- doesthiswork has quit (Ping timeout: 248 seconds). 10:49:02 -!- carado has joined. 11:14:08 fizzie, clang-analyzer actually found a bug, if you used a mode less than zero or larger than 5 (invalid values) to FILE O it would access uninitialized memory when trying to clean up the already allocated file handle. Heh 11:14:59 fizzie, In total it found 11 items, one of them has a path length of 33 and is inside the genx library. Trying to figure out what is going on there now. 11:17:41 -!- carado has quit (Ping timeout: 246 seconds). 11:19:25 -!- carado has joined. 11:31:04 -!- carado_ has joined. 11:32:01 -!- carado has quit (Ping timeout: 246 seconds). 11:34:58 The analyzer always gives me a dozen "uninitialized argument value" errors that I don't care about :-/ 11:52:24 Fiora: did you see this quote about the "on-by-default" filters I pasted in here a few days ago? 11:52:27 "They have negotiated with the government and agreed on a system called "Active Choice +" in which customers opt in for filters [...] The leaked letter [...] suggests: "Without changing what you will be offering (ie active-choice +), the prime minister would like to be able to refer to your solutions [as] 'default-on'"." 11:52:39 pretty great 12:12:51 -!- epicmonkey has quit (Read error: Operation timed out). 12:14:43 Deewiant, hm, not much of that for me. I have two false positives in the funge space write-to-file-in-text-mode code, where the analyzer appears to simply fail at basic arithmetics. 12:16:14 Deewiant, and I have one real bug (but that doesn't affect me) in the getline-code I took from gnulib or glibc or some such, where it can leak memory if a realloc to grow a buffer fails. But that doesn't affect me since I always provide an already allocated buffer I believe 12:16:45 You can add an assert to make the analyzer shut up about stuff like that 12:16:58 Deewiant, tried, but no luck currently 12:17:10 #ifdef __clang_analyzer__ 12:17:10 1065assert(offset->x < maxx); 12:17:10 1066assert(lastspace == maxx - offset->x); 12:17:10 1067#endif 12:17:10 1068for (funge_cell x = offset->x; x < maxx; x++) { 12:17:11 ... 12:17:17 Even with that it doesn't see that loop as taken 12:17:20 I have no idea why 12:17:36 I meant for the realloc thing 12:17:43 Deewiant, oh that, right, possibly 12:18:23 Why #ifdef them out? 12:19:16 According to http://clang-analyzer.llvm.org/faq.html#use_assert that first assert should work for that but oh well 12:19:19 Deewiant, because those asserts are inside a loop, and since they were loop invariant I first put them outside the outermost loop, but since that didn't help I tried putting them inside instead 12:19:22 Not working either 12:19:38 and yes I agree, the first one should work 12:19:40 but doesn't 12:20:21 What does it matter if they're inside a loop, do you leave asserts in release builds or something 12:20:48 Deewiant, In RelWithDebInfo builds, but not in full Release no 12:20:55 anyway they didn't work for the analyzer anyway 12:21:10 So meh, giving up on trying to tell it about the false positives 12:21:26 I fixed all the real issues anyway, don't really care about there being 3 false positives in the code. 12:22:40 Deewiant, where did you get those uninit arg value errors from btw? 12:23:04 I mean, some sort of example code or such 12:23:04 In mushspace 12:23:15 They're not false positives, I just don't care about them 12:23:22 Example code: int x; f(x); :-P 12:23:30 And then f() doesn't read x 12:23:35 Well, that doesn't look well defined to me, unless f is a macro 12:23:55 AFAICT it shouldn't matter as long as f doesn't read it 12:24:12 Deewiant, pretty sure it isn't well defined to call with an uninitialized l-value, since the calling convention would end up reading it and putting it in a register or such 12:24:18 you could pass a pointer to x though 12:24:44 Deewiant, I'm not 100% certain though 12:24:58 It's possible, I haven't found anything specific in the standard though 12:25:03 Hm 12:25:17 oh geez 12:25:22 I just realised what I should write shiro 2 in! 12:25:23 rust 12:25:23 Deewiant, anyway why pass the argument if f doesn't need it anyway? 12:25:31 that way i can beat Deewiant and still be a hipster 12:25:37 elliott, how far did you get with shiro 1 anyway? 12:26:09 Vorpal: Basically to simplify the code since it needs it sometimes 12:26:15 Vorpal: um, it passed pure mycology except for like one annoying file IO technicality I didn't want to fix, and implemented like 15-20 fingerprints. 12:26:23 Deewiant, ah 12:26:24 with varying degrees of Mycology-passingness, but fairly good on the whole 12:26:32 it was missing a couple of fingerprints to run fungot iirc 12:26:32 elliott: " fnord", ou " fnord" seems to not parse them well. 12:26:37 elliott, fair enough 12:27:12 elliott, what about the stuff that mycology doesn't test? Like text mode for o. 12:27:15 Deewiant: is mushspace at the point where you don't really want to compete with it with a GC yet :p 12:27:23 Vorpal: that was probably broken 12:27:25 i/o are annoying 12:27:40 elliott, quite so, text mode o especially 12:27:50 since you need to strip trailing ws from the end of each line 12:28:07 elliott: Depends on your GC? I dunno :-P 12:28:43 Though I just thought of a more efficient way to do it... Except it will be even more complicated to write the code for. 12:29:59 What does a GC have to do with mushspace anyway? 12:31:27 Vorpal: well, pauses. 12:33:02 hm? 12:35:02 GCs tend to cause them. 12:35:33 Well yes 12:35:49 Deewiant, are you using a GC? 12:36:30 OK, I think foo x; f(x) is unspecified, but if x is a partially initialized struct I think it's still fine, hmm 12:36:32 Vorpal: No 12:36:49 Makes sense since you said you were aiming for performance iirc 12:36:50 -!- yorick has joined. 12:37:12 how does Vorpal understand how a GC could harm performance when talking to Deewiant but not when talking to me?????? 12:39:14 elliott, the initial cause was some parsing confusion on "want to compete with it with a GC". I first parsed that as him competing with it + a GC against something. 12:40:40 uh. okay :P 12:53:43 bbl 12:58:31 Deewiant: How do you make a partially initialized struct? 12:59:26 Uninitialized, and set a couple of members, I guess. 13:00:41 Or initialize it with { .foo = bar } 13:00:48 That's not partially initialized. 13:01:00 Well clang's analyzer claims it is 13:01:12 It's talking out of its ass, then. 13:01:15 "If there are fewer initializers in a brace-enclosed list than there are elements or members of an aggregate -- the remainder of the aggregate shall be initialized implicitly the same as objects that have static storage duration." 13:02:58 Oh whoops, it's actually referring to a struct member of the struct, my bad 13:05:03 Actually, I guess the version stating almost the same thing few paragraphs up, "-- all subobjects that are not initialized explicitly shall be initialized implicitly the same as --", is more relevant. 13:05:23 Good thing that's there, otherwise presumably struct { int a, b; } f = { .a = 42, .a = 69 }; would leave b uninitialized. 13:13:14 Actually this thing just seems to be confused 13:15:34 Also I concur with the foo x; f(x) being okay for a partially uninitialized struct -- "the value of struct or union object is never a trap representation, even though the value of a member of the structure or union may be a trap representation" -- and apparently so does the committee in DR222: http://std.dkuug.dk/jtc1/sc22/wg14/www/docs/dr_222.htm 13:16:33 Yes, I was reading C11 which has those DR222 changes 13:42:58 -!- FreeFull has quit (Quit: Rebooting). 13:57:39 -!- FreeFull has joined. 14:27:04 -!- pikhq_ has joined. 14:27:32 -!- pikhq has quit (Ping timeout: 260 seconds). 14:50:52 -!- nooodl has joined. 14:58:11 -!- copumpkin has quit (Quit: Computer has gone to sleep.). 15:01:11 what exactly is a trap representation? 15:01:48 Vorpal: "an object representation that need not represent a value of the object type" 15:04:26 Ah right 15:04:40 Deewiant, would null be considered one of those? 15:04:47 I think null is sort of a trap representation? 15:04:55 I wonder if NaN counts too. 15:05:17 No, null is a valid value that a pointer can have, and likewise NaN for floats 15:05:32 Deewiant, So on common systems there are no trap representations? 15:05:43 Certain object representations need not represent a value of the object type. If the stored value of an object has such a representation and is read by an lvalue expression that does not have character type, the behavior is undefined. If such a representation is produced by a side effect that modifies all or any part of the object by an lvalue expression that does not have character type, the behavior is 15:05:45 undefined. Such a representation is called a trap representation. 15:06:11 Vorpal: Not on x86 afaik 15:06:14 -!- aloril_ has quit (Ping timeout: 246 seconds). 15:06:36 Vorpal: You can set the FPU to trap on some stuff but I wouldn't consider that part of this 15:07:33 So what platforms do have it hm? 15:07:59 http://stackoverflow.com/questions/6725809/trap-representation oh, huh, this sems to explain some of it (?) 15:08:52 that's nasty 15:08:54 fake values 15:09:37 I guess one example might be "negative 0" in a ones' complement number format? 15:09:48 I'm not sure 15:10:45 yeah the SO answer gives that as an example 15:10:49 or, oh, the standard does 15:11:06 Evidently signalling NaNs remain undefined in C11 so those count 15:13:26 "Some combinations of padding bits might generate trap representations, for example, if one padding bit is a parity bit. Regardless, no arithmetic operation on valid values can generate a trap representation other than as part of an exceptional condition such as an overflow, and this cannot occur with unsigned types." 15:13:53 hm 15:18:31 "An integer may be converted to any pointer type. Except as previously specified, the result is implementation-defined, might not be correctly aligned, might not point to an entity of the referenced type, and might be a trap representation." 15:20:06 -!- aloril_ has joined. 15:54:18 -!- mnoqy has quit (Quit: hello). 15:55:18 -!- doesthiswork has joined. 15:55:52 good morning 16:03:11 -!- doesthiswork has quit (Remote host closed the connection). 16:09:28 -!- doesthiswork has joined. 16:09:43 -!- Lumpio- has quit (Ping timeout: 245 seconds). 16:09:44 -!- doesthiswork has quit (Client Quit). 16:10:06 -!- doesthiswork has joined. 16:13:35 -!- Lumpio- has joined. 16:23:02 -!- Taneb has quit (Ping timeout: 240 seconds). 16:28:41 -!- Taneb has joined. 16:35:15 -!- atriq has joined. 16:36:14 -!- Taneb has quit (Ping timeout: 240 seconds). 16:40:42 -!- Frooxius has joined. 16:44:47 good morning 16:52:57 -!- atriq has changed nick to Taneb. 17:06:03 -!- Phantom_Hoover has joined. 17:08:31 -!- zzo38 has joined. 17:34:30 -!- conehead has joined. 17:34:50 -!- doesthiswork has quit (Max SendQ exceeded). 17:35:10 -!- conehead has quit (Remote host closed the connection). 17:35:30 -!- Phantom_Hoover has quit (Ping timeout: 264 seconds). 17:35:36 -!- conehead has joined. 17:49:15 -!- doesthiswork has joined. 18:08:59 Hm. They make a distinction between undefined behavior and unspecified behavior. 18:09:20 I think "unspecified" means "something predictable happens, but it could be platform-dependent"? 18:09:26 So undefined behavior means "the implementation is allowed to do literally anything when this happens". 18:09:33 while undefined means "this should never happen, code is wrong if it does this, demons could shoot out your nose"? 18:09:44 so the latter is "the compiler can assume this doesn't happen"? 18:09:58 And unspecified behavior means "the implementation has some leeway in choosing what the result is when this happens". 18:10:05 yeah... 18:10:07 that sounds right. 18:13:23 There's undefined behaviour, unspecified behaviour, and implementation-defined behaviour 18:13:46 what's the difference between unspecified and implementation-defined? 18:14:28 Undefined = anything can happen; unspecified = there are many specified alternatives but which one happens at any given time can vary 18:15:36 "use of an unspecified value, or other behavior where this International Standard provides two or more possibilities and imposes no further requirements on which is chosen in any instance" 18:16:07 (unspecified value = "valid value of the relevant type where this International Standard imposes no requirements on which value is chosen in any instance") 18:16:21 (implementation-defined value = "unspecified value where each implementation documents how the choice is made") 18:17:10 So, my lazy expression reducer is pretty inefficient, I guess. 18:17:16 I see 18:17:28 so implementation-defined = unspecified but it has to be consistent within an implementation? 18:17:43 In that it can potentially traverse the entire expression every time a reduction step is performed. 18:17:53 unspecified by the standard, specified by the implementation 18:18:23 elliott: Depends on what you mean by consistent, I guess; it has to be documented 18:18:32 probably hard to enforce though :p 18:18:41 So it could still be e.g. selection by /dev/random 18:18:53 Deewiant: okay so it is just a documentation requirement and nothing more 18:19:12 "unspecified behavior where each implementation documents how the choice is made" 18:19:20 right 18:19:38 The intelligent way to do this would probably be to mark each sub-expression as to whether it's already been evaluated or not. 18:19:42 It's possible that there are further consistency requirements for specific things, I guess 18:19:44 http://www.jwz.org/images/gm.gif cow 18:21:18 That sure is a lot of agitation. 18:22:04 If that cow were real, would it really slosh that much? 18:22:36 I'm trying to figure out whether they did a good job with subsurface scattering or not. 18:23:41 Perfect cube tutorial http://i.imgur.com/fctEUfv.gif 18:29:02 http://www.kickstarter.com/projects/2010618696/dkss-reality-death-maze 18:30:52 someone pledged over $1,000 on that. 18:34:13 Could be the people funding their own kickstarter to make it look like it's supporte. 18:34:29 luckily they get their money back 18:35:00 Well, most of it. 18:35:28 "Help us support the Portal! Please fund DKS's Reality Death Maze to help us open our dimensional portal." er 18:36:05 Only most of it? 18:56:19 ion: I prefer twisted cubes 19:02:59 -!- MindlessDrone has quit (Quit: MindlessDrone). 19:04:02 Are all beginnings non-sequiturs? 19:04:44 sounds like a question for fungot 19:04:44 olsner: well there. fight about whether to play keen or watch demos. he didn't tell anything ( they don't) 19:16:15 Having written a basic proto-Hylisk interpreter, suddenly I have no desire to use it. 19:16:30 Oh hey Edward Kmett reads HPMOR 19:29:31 Harry Potter: Man on Rhea? 19:32:15 Harry Potter and the Methods of Rationality 19:32:18 I'm not such a fan of that story 19:34:10 because among other things genetics is a lot more interesting than presented there 19:35:50 -!- carado has joined. 19:35:53 -!- carado has quit (Read error: Connection reset by peer). 19:36:24 -!- carado has joined. 19:38:43 -!- carado_ has quit (Read error: Connection reset by peer). 19:43:04 -!- carado has quit (Ping timeout: 246 seconds). 20:17:30 -!- Bike has quit (Ping timeout: 264 seconds). 20:20:00 -!- ssue__ has quit (Ping timeout: 245 seconds). 20:20:35 -!- Guest18414 has quit (Ping timeout: 264 seconds). 20:20:53 -!- Guest18414 has joined. 20:25:37 -!- Bike has joined. 20:38:51 Tracking the #haskell tag on Tumblr may not have been the best idea 20:38:59 It's one of the most multi-purpose tags there is 20:39:22 And half of the stuff that is the programming language is just links to things I've already seen 20:40:09 Well. The UI is real clunky, the code may be buggy, half of the features are missing and the compositing is all wrong, but here it is anyway: http://zem.fi/ircvis/esoteric/people_presence.html 20:40:11 -!- Sgeo has quit (Read error: Connection reset by peer). 20:41:25 -!- Sgeo has joined. 20:41:37 interesting 20:41:56 kallisti's is unusual 20:42:12 it does show different things than the weekly and hourly graphs did 20:43:40 lambdabot doesn't have much of an hourly schedule either. 20:47:54 We can calculate the mutual information between two nicks to see how similar their sleep schedules are 20:48:46 -!- tertu has joined. 20:49:33 although kullback-divergance might be more fitting 20:49:47 fizzie: it seems I lost my sleep schedule in 2009. 20:50:25 FWIW, i also like git more. https://twitter.com/molovo/status/360346792602259456 20:51:01 -!- epicmonkey has joined. 20:51:20 I don't know offhand how to make SVG's simple alpha compositing do the operation I wanted, which was to blend colors with uniform weights where they overlap. The current scheme of setting layer opacities to 1, 1/2, 1/3, ... from bottom to top does the right thing if there's a pixel in all layers, but it dims the non-bottom layers where they composit with the black background. Filter effects ... 20:51:26 ... could probably do it, though. 20:53:23 kmc gained a sleep schedule mid 2012 20:54:04 I think I remember that! 20:54:57 MKRY on the list of nicks. :/ 20:54:59 taneb suddenly sprang into being in 2011 20:55:29 Yup 20:55:49 Actually, I've used the name "Taneb" since at least October 2007 20:55:51 Sleep schedule? What’s that? 20:56:04 I think I first used it July 2007 20:56:18 I suspect you are an irc bot ion 20:56:39 What makes you think you are an irc bot ion? 20:57:29 I seem to do a lot of breakfast irc between about 9 and 11 20:58:10 Note that there's a curious singular Taneb dot somewhere in September 2010. 20:58:23 that one is good iirc 20:58:25 if you pastelogs it 20:59:18 The weird thing is, I remember doing that, but I remember doing that in 2011 20:59:57 I can’t place p. much anything to a specific year, my sense of time is horrible. 21:01:17 http://codu.org/logs/log/_esoteric/2010-09-06#204051Taneb it seems that when Taneb appeared in 2010, I was... doing plots. 21:01:57 It definitely sounds like me 21:02:22 and then you didn't come back for a year? 21:02:52 Apparently! 21:03:01 Maybe it was a time-traveller impersonating me 21:03:06 But for what purpose? 21:03:17 Obviously, to save the space-time continuum! 21:03:20 fizzie: is Taneb and atriq merged in that graph? 21:04:14 olsner, I believe they are 21:04:17 Ngevd, too 21:04:27 are you ngevd too? 21:05:02 Yes 21:05:08 `rot13 atriq 21:05:12 ngevd 21:05:34 oh, I thought taneb was rot13 of atriq for some reason 21:05:42 My initials were ALMOST N. G. E. v. D 21:05:59 But my parents thought that was too long and dropped the E (which stood for Eliot) 21:06:01 olsner: Yes. 21:06:20 olsner: 'Taneb': ['Taneb', 'Ngevd', 'atriq'], 21:06:42 Shouldn't CakeProphet and kallisti be merged? Or am I misremembering? 21:08:01 Taneb: I think that was a merging I was supposed to do but couldn't be bothered rerunning the statistics-collection system on the entire logs. (Don't have a merging tool for them.) 21:08:39 I'll get it next time. 21:09:09 :) 21:09:18 Huh, I've been active in the channel for about as long as shachaf 21:12:09 And your schedules are pretty much complementary. Are you... are you shachaf? 21:12:33 What a twist! 21:12:54 And I read Homestuck and won't read OotS and he reads OotS and won't read Homestuck! 21:13:42 When comparing two things, thanks to the crummy blending, setting the first to red and the second (dimmed one) to turquoise seems to be a reasonably good pair. (I'll fix it properly at some point.) 21:15:04 (Though sadly the layers aren't always in the order specified.) 21:17:37 I can confirm that I am Taneb. 21:17:43 Totally called it 21:18:18 More evidence that shachaf and I are one and the same: 21:18:23 shachaf is not a rabbi 21:18:26 As far as I am aware 21:18:33 shachaf, are you a rabbi? 21:18:45 Have we ever been seen in the same IRC channel together? 21:18:57 I don't think so 21:18:58 Taneb: Nope. 21:19:04 Neither am I! 21:19:06 `? Taneb 21:19:08 Taneb is not elliott, no matter who you ask. He also isn't a rabbi although he has pretended in the past. He has at least two backup keyboards. (see also: d-modules) 21:19:25 `? d-modules 21:19:27 D-modules are just modules over the ring of differential operators. Taneb invented them. 21:19:36 -!- CADD has joined. 21:19:52 `? modules 21:19:53 modules? ¯\(°_o)/¯ 21:19:54 | 21:19:54 o/`¯º 21:19:57 `? ring 21:19:59 Addition, subtraction and multiplication have a certain ring to them. 21:20:07 `? differential operators 21:20:09 differential operators? ¯\(°_o)/¯ 21:20:10 | 21:20:10 º¯`\o 21:20:43 imo checkmate 21:30:04 -!- epicmonkey has quit (Read error: Operation timed out). 21:58:59 -!- Taneb has quit (Quit: Leaving). 22:02:05 * tswett ponders what a ~list is. 22:02:13 I.e., what's the comonad corresponding to the list monad? 22:03:17 Looks like it's... something that consumes an arbitrary number of items and then exits. 22:03:55 it's not a comonad in Hask 22:04:01 like shachaf said some days ago 22:04:09 -!- upgrayeddd has quit (Ping timeout: 246 seconds). 22:04:25 the comonad you get is in the "other category" of the adjunction that gives you a monad 22:04:42 Right, it's that other category. 22:04:43 State/Store is just a "happy coincidence" because the two functors involved are endofunctors on Hask 22:05:02 the comonad is in Mon 22:05:05 IIRC extract is fold 22:05:11 I forget what duplicate is but I recall it's boring 22:05:47 Mon must be one of those... closed symmetric what-have-yous. 22:06:24 Closed symmetric monoidal categories. 22:06:40 Mon has monoid homomorphisms as morphisms 22:06:46 and monoids as objects 22:08:18 So a monoidal category is one with a "tensor product" bifunctor which is associative with identity up to natural isomorphism. 22:08:52 And it seems like the "usual tensor product" is just the cartesian product or something? 22:09:18 also in particular, a ~list is just a list. 22:09:27 Is it now. 22:09:34 with a monoidal element type, if you insist. 22:09:58 So then now a closed monoidal category is one that has that currying thing. 22:10:39 And a *symmetric* monoidal category is, uh... 22:12:58 Apparently a braided monoidal category is one which is commutative and also satisfies some weird hexagon thing. 22:13:34 Mm, not quite commutative? 22:15:13 A symmetric monoidal category is one that actually is commutative? 22:16:47 Okay whatever. 22:17:45 Okay, so... yeah, what are the component functors of the list monad? 22:18:18 They take Set to Mon and back to Set, aye? So, the free functor (is... is that a thing?) followed by the forgetful functor? 22:19:39 hint: free monoid 22:19:52 and stuff. 22:19:57 I worked it out with shachaf once. 22:19:57 The free monoid functor? 22:20:01 unfortunately the comonad is boring. 22:20:21 but I don't remember the exact details... 22:20:34 Yeah, it looks like the comonad also pretty much makes lists, doesn't it? 22:20:57 A co-list of monoidal things is pretty much just a list of monoidal things. 22:22:40 "Extract" just multiplies all the elements together. And "extend", that's the w a -> w (w a) thing, right? 22:22:49 -!- copumpkin has joined. 22:23:01 -!- copumpkin has quit (Client Quit). 22:23:06 yeah 22:24:02 Oh, what's a monoid. How about the monoid of... things you can do with a pile of string. 22:24:04 That's a lovely monoid. 22:24:33 -!- copumpkin has joined. 22:24:42 So then a Colist StringThing is a list of things you can do with a pile of string. "extract"ing that concatenates all those things together. 22:24:51 I guess the things you can do with a pile of string actually form a category, not a monoid. 22:26:54 And "extend", what's that supposed to do? 22:28:44 Anyway, so far, this seems completely unrelated to the linear logic dual of List I've come up with. 22:29:00 Which is: ~List a = Bottom & (a -o ~List a) 22:31:30 -!- oerjan has joined. 22:32:19 Hum. In a closed monoidal category, must there exist a bifunctor & such that there's a natural transformation from A & B to A, and from A & B to B? 22:33:37 Rather, in a symmetric monoidal category, must there be such and such? 22:35:42 Rather, a closed symmetric monoidal category. 22:35:58 And, rather, must there exist product objects? 22:43:44 "wanted to ask u guys - Markov Chans with lotto Numbers...good idea?" 22:55:08 Hmm. The category of quantum state spaces. 22:55:59 Let's say this. Quantum state spaces where every state is required to be a mixture of finitely many pure states. 22:56:17 I'm not actually communicating right now, am I; I'm just talking to myself out loud. 22:58:26 Let's be fun and drop the mixture of finitely many whatever. 22:59:02 Nah, let's forget about the whole thing. 23:01:49 Oh, here's what a ~list is in linear typing. It's actually quite simple. 23:02:00 It's an object that, given an arbitrary length, gives you a list of that length. 23:05:44 Seems obvious in retrospect. 23:07:06 hey tswett, what's your favorite color? Does she know? 23:07:33 You don't seem to be giving me the context necessary to understand your questions. 23:08:44 64133,918181,262626,0194823,753957192719394739109375728,281917466 23:09:33 Oh, okay. 23:09:46 The answer is A. 23:11:24 That's not a color. 23:13:01 A is the answer to the greater surrounding question. 23:16:32 Though it's not meant to be a useful answer. It's more like a proof that all of the prerequisites for answering the greater surrounding question have been satisfied. 23:34:38 tswett: are you deep thought 23:43:12 oerjan: A 23:45:01 What candies exist that are as deliciously minty as Listerine strips? 23:48:44 mint candy flavor = the worst hth 23:53:40 -!- yorick has quit (Ping timeout: 256 seconds). 23:54:07 Listerine strips taste so good