←2018-02-17 2018-02-18 2018-02-19→ ↑2018 ↑all
00:00:56 -!- oerjan has joined.
00:13:43 <boily> bonsϿirjan.
00:16:02 <int-e> `"
00:16:03 <HackEgo> 10) <fungot> GregorR-L: i bet only you can prevent forest fires. basically, you know. \ 144) <fungot> ais523: my nose feels like a bad heuristic
00:16:38 <int-e> dang, 144 made me laugh
00:20:46 <oerjan> bood evenily.
00:22:32 -!- staffehn has quit (Ping timeout: 276 seconds).
00:26:11 <FireFly> ´"
00:26:13 <FireFly> er
00:26:15 <FireFly> `"
00:26:16 <HackEgo> 837) <kmc> so i guess my root of trust for Arch Linux is...typedef int f(float); \ 1138) <Taneb> Well, get him <Phantom_Hoover> her! <Taneb> Well, get her <Taneb> Hang on <Taneb> Since when is Liam Neeson a "her"/ <Phantom_Hoover> oh i thought you meant my dad's godmother
00:26:27 <FireFly> `'
00:26:27 <HackEgo> 460) <Phantom_Hoover> On further reflection, I think I did manage to miss winter and spring altogether. <Phantom_Hoover> This does explain the goblin siege I had in autumn.
00:26:30 <FireFly> cute
00:29:31 <boily> `’
00:29:31 <HackEgo> ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: ’: not found
00:33:39 <fizzie> fungot: Is your mouth a good heuristic?
00:33:39 <fungot> fizzie: i've seen it
00:37:21 -!- staffehn has joined.
00:39:14 -!- jaboja has joined.
00:43:09 <boily> fungot, the Heuristical Holistic Sentient Fungot.
00:43:10 <fungot> boily: yes i believe in your letrec example, a third is very close to normal scheme. maybe i'm missing a way to cast a lot of programming concepts which are not
01:19:26 -!- staffehn has quit (Ping timeout: 265 seconds).
01:30:52 -!- staffehn has joined.
02:22:43 -!- erkin has quit (Quit: Ouch! Got SIGABRT, dying...).
02:24:05 -!- Melvar has quit (Ping timeout: 240 seconds).
02:25:33 <moony> fungot's mouth is a good PRNG seed
02:25:34 <fungot> moony: are therer any good scheme should be " rube on conveyor belts
02:37:30 -!- Melvar has joined.
02:52:15 -!- mniip has joined.
02:55:06 -!- boily has quit (Quit: DISC CHICKEN).
03:02:41 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
03:08:41 -!- variable has quit (Quit: Found 1 in /dev/zero).
03:10:24 -!- jaboja has quit (Quit: Leaving).
03:10:35 -!- jaboja has joined.
03:47:48 -!- jaboja has quit (Remote host closed the connection).
05:21:43 -!- variable has joined.
05:23:37 -!- dingbat has joined.
05:53:00 -!- oerjan has quit (Quit: Nite).
06:31:18 -!- variable has quit (Quit: /dev/null is full).
06:56:09 -!- aeyxa has joined.
07:01:25 -!- Naergon has quit (Remote host closed the connection).
07:04:32 -!- laerling has joined.
07:07:46 -!- variable has joined.
07:33:02 -!- TakeYourFreedom has joined.
07:54:18 -!- sleffy has quit (Ping timeout: 240 seconds).
08:05:57 -!- aeyxa has quit (Quit: Page closed).
08:06:51 -!- aeyxa has joined.
08:14:01 -!- TakeYourFreedom has quit (Remote host closed the connection).
08:25:38 -!- wob_jonas has joined.
08:25:52 <wob_jonas> monocular o => https://www.smbc-comics.com/comic/process
08:31:02 -!- zzo38 has quit (Disconnected by services).
08:31:08 -!- zzo38 has joined.
08:33:39 -!- variable has quit (Quit: Found 1 in /dev/zero).
08:38:18 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client).
09:03:57 -!- Melvar has quit (Ping timeout: 256 seconds).
09:16:35 -!- Melvar has joined.
10:11:37 -!- LKoen has joined.
10:48:08 -!- danieljabailey_ has quit (Ping timeout: 255 seconds).
10:58:10 -!- Melvar` has joined.
11:01:15 -!- Melvar has quit (Ping timeout: 256 seconds).
11:16:48 -!- AnotherTest has joined.
11:26:25 -!- Melvar` has quit (Ping timeout: 248 seconds).
11:30:49 -!- aeyxa has quit (Ping timeout: 260 seconds).
11:39:27 -!- Melvar` has joined.
11:43:25 -!- aeyxa has joined.
12:07:09 -!- Melvar` has quit (Ping timeout: 260 seconds).
12:07:38 -!- Melvar` has joined.
13:04:10 -!- boily has joined.
13:17:15 -!- Melvar` has quit (Ping timeout: 256 seconds).
13:29:47 -!- Melvar` has joined.
13:37:02 <boily> `5 w
13:37:10 <HackEgo> 1/2:amortized//An amortized word is a word that oerjan can never remember. \ wob_jonas//wob_jonas is b_jonas in disguise, so that he can do magic tricks. \ functor//Functors are morphisms in the category of small categories. \ twitter//Twitter is Taneb's bird collection (presumably). \ shamtag//A shamtag is something that you durch in ord
13:37:12 <boily> `n
13:37:12 <HackEgo> 2/2:er to make it flome.
14:24:13 <int-e> `dowg shamtag
14:24:21 <HackEgo> 8211:2016-05-30 <tsweẗt> learn A shamtag is something that you durch in order to make it flome.
14:27:36 <int-e> Well, I /guess/ tswett was training a letter based language model for english.
14:30:59 <int-e> Ah, confirmed. It was a neural network. http://esolangs.org/logs/2016-05-29.txt has a discussion in the morning.
14:52:59 -!- xkapastel has quit (Quit: Connection closed for inactivity).
15:14:00 -!- variable has joined.
15:46:20 -!- wob_jonas has joined.
15:47:06 <wob_jonas> int-e: yeah, that was nice. I also trained a letter-based statistical model (no neural net) once, on Hungarian text, and quoted in this channel a few lines it output at some point.
15:59:57 -!- Melvar` has quit (Ping timeout: 240 seconds).
16:00:10 -!- Naergon has joined.
16:06:00 -!- erkin has joined.
16:08:23 -!- boily has quit (Ping timeout: 255 seconds).
16:13:31 -!- Melvar` has joined.
17:00:00 <int-e> . o O ( fingernails evolved so that people won't cut their fingers all the time )
17:01:56 <wob_jonas> int-e: no way. there haven't been enough time since we've been washing sharp steel knives hidden by soap bubbles in a kitchen sink for that to matter for evolution.
17:03:31 <int-e> wob_jonas: there's no way to be sure!
17:04:02 <int-e> (alternatively, then this is proof for Intelligent Design)
17:04:11 <wob_jonas> int-e: there sure is. metal items like kitchen sinks and knife blades would be preserved well enough that we'd find archaeological evidence
17:04:33 <wob_jonas> If such things existed for more than twelve thousand years, we'd know about it.
17:06:08 <wob_jonas> You could argue that the fingernails have some role in stopping papercuts, and that people have had paper for much longer than we know, but all the old paper have decomposed and eaten by fungi.
17:06:49 <int-e> wob_jonas: You know, the "the world was created 4000 years ago" world view is quite consistent.
17:07:22 <wob_jonas> int-e: no, we do have archaeological evidence that civilization is more than 4000 years old
17:07:47 <wob_jonas> but not more than 12000 years old, give or take a few thousand years, and depending on how exactly you define civilization
17:08:18 <wob_jonas> Unless you believe the legends of an old magical civilization erasing its existance from the very time stream in a huge magical accident of course.
17:08:36 <int-e> The only thing that is stopping me from actually believing it is that I don't think that anybody would actually go through all the trouble of painstakingly faking all this evidence.
17:17:53 -!- Melvar` has quit (Ping timeout: 248 seconds).
17:31:29 -!- Melvar` has joined.
17:34:44 -!- variable has quit (Quit: Found 1 in /dev/zero).
17:35:24 -!- aeyxa has quit (Ping timeout: 260 seconds).
17:51:07 <int-e> Ah so it's not just me who wonders how people actually train their (deep) neural networks. Even the experts don't know: http://www.sciencemag.org/news/2018/02/missing-data-hinder-replication-artificial-intelligence-studies
17:57:06 -!- xkapastel has joined.
18:03:03 -!- variable has joined.
18:08:59 <int-e> Yay, I now have actual undecidability (and recursive inseparability) results for Minsky machines formalized in Isabelle :)
18:09:19 <APic> yay
18:09:43 <wob_jonas> int-e: oh, I think you had mentioned you were working on it
18:09:58 <wob_jonas> int-e: how did you prove that they're undecidable?
18:10:12 <wob_jonas> did you write a self-interprter?
18:10:34 <wob_jonas> or an interpreter of an, um, simpler undecidable language?
18:10:47 <APic> =6.9=
18:10:51 <APic> *purrrrrr* 😸
18:11:06 <APic> Both Spirals lead to epic Success, probably. ☺
18:17:12 -!- variable has quit (Quit: Found 1 in /dev/zero).
18:19:19 <int-e> wob_jonas: I didn't have to write any interpreter myself. I basically showed that every r.e. set is recognized by a Minsky machine; I'm building on top of a formalization that has a universal function for r.e. sets. http://downthetypehole.de/paste/jCpbJsVP has some hilights (incomplete and no proofs)
18:19:29 <APic> yay
18:20:44 -!- sleffy has joined.
18:20:45 <wob_jonas> int-e: I see. so it's the latter, you write an interpreter for some other language, the one used to define recursive enumarable sets in that formalization?
18:21:25 <APic> Hi sleffy
18:21:31 <int-e> wob_jonas: Of course there is an interpreter in there, namely a Minsky machine that recognizes (some preimage of) that universal r.e. set. But I have no clue what it looks like, it's not a constructive proof.
18:22:36 <int-e> (it's also clear how to make this constructive *in* principle, but Isabelle/HOL is a classical logic)
18:22:36 <wob_jonas> int-e: oh wait, you're right, it needn't be an interpreter written in Minsky, but only a compiler from the other language to Minsky, the compiler itself implemented in Isabelle
18:23:29 <sleffy> APic, hello!
18:23:34 <APic> Me-ow!
18:23:44 <sleffy> Hel-lo!
18:24:14 <APic> Yoooooo-hooo!
18:24:15 <wob_jonas> hello
18:25:58 <int-e> wob_jonas: so what I'm saying is that this "compiler" from the other language (r.e. sets) to Minksy doesn't actually have to be constructive.
18:26:13 <wob_jonas> int-e: ok
18:26:19 <wob_jonas> I'm not sure what "constructive" means there
18:26:37 <wob_jonas> or more like have a hard time imagining a non-constructive implementation
18:26:50 <APic> https://www.youtube.com/watch?v=qnTINa7818c
18:26:56 <int-e> no choice, no law of excluded middle.
18:27:12 <wob_jonas> hmm
18:27:12 <int-e> wob_jonas: Well I have a ton of lemmas stating "there exists a Minsky machine M such that..."
18:30:18 <wob_jonas> int-e: ok, now I'm thinking of the ending of the Smullyan mockingbird book, musing about whether there's a bird that can solve the halting problem
18:30:43 <int-e> wob_jonas: and while if you looked at the proofs you'd find that they're all constructive, there is no direct way of getting at a compilation function.
18:31:39 <wob_jonas> int-e: is there an evaluator function, one that can also recognize invalid programs, for the original language?
18:32:43 <int-e> yes. there's a nat_to_ce_set :: nat => nat set. (I suppose invalid programs become the empty set? I haven't checked.)
18:33:00 <int-e> ("ce" = computably enumerable = recursively enumerable)
18:33:18 <wob_jonas> int-e: ok
18:35:30 <int-e> (Recursive inseparability is a 1953 innovation that I learned about two years ago... I really wonder why it isn't taught in every computability theory course.)
18:36:29 <APic> Probably because Morse-Code is not taught in Schools.
18:36:32 <APic> ;=P
18:37:20 <wob_jonas> what
18:37:37 <int-e> Prime example: (assuming consistency) The set of provable formulas and the set of disprovable formulas in Peano Arithmetic are recursively inseparable: there is no decidable set that contains all the provable formulas and none of the disprovable ones. The beauty is that this doesn't say anything about the formulas that are neither provable or disprovable...
18:37:43 <wob_jonas> fungot, can you solve the halting problem?
18:37:43 <fungot> wob_jonas: well, when you define cond, that is.))
18:38:18 <wob_jonas> int-e: yeah, I think I heard that theorem
18:39:31 <int-e> A more useful example are Turing Machines that can accept or reject, or run forever; the set of TM configurations that halt in an accept stated, and the set of TM configurations that halt in a reject state, are recursively inseparable.
18:39:47 <int-e> s/stated/state/
18:40:03 <APic> 😸
18:40:33 <wob_jonas> int-e: yeah, that's more or less equivalent
18:42:34 <int-e> A less obvious example are PCP problems that have a finite solution, and PCP problems that have no infinite solution. (For example, (1,11) has the infinite solution (1*,1*) arising from appending (1,11) to itself over and over again)
18:45:16 <wob_jonas> Hmm.
18:47:49 <APic> Yes?
18:48:01 <APic> Good old Infinity. ☺
18:48:45 <int-e> Incidentally, that is what I really want to have...
18:49:16 <APic> ,o0(Toeoeoe-roeoeoeoe)
18:49:35 <int-e> And Minsky machines are my intermediate model of computation.
18:49:35 <APic> All those Coincidents...
18:49:40 <APic> Good old Marv
18:49:44 <int-e> `coins
18:49:48 <HackEgo> poridgecoin s17057034167130coin landcoin contumcoin ointecoin audacoin idecoin ]coin gruptorcoin xxvcoin jumpcoin deltapecoin hevnarylangtheonchurchwaynomialcoin xivcoin spielcoin whittlecoin akcrcoin angcoin atheteembertyscraftermdcoin itfcoin
18:50:34 <APic> lol
18:50:50 <int-e> APic: you spoke of coin-cidents?
18:50:58 <APic> Dunno
18:51:19 <int-e> `coins
18:51:20 <HackEgo> wikipwritoncoin gubacoin nhiucoin obfecoin aheuiculus'scoin obftecoin minlinksencoin bolcoin chologifruincoin parcoin archwaycoin brocarmcoin musicontroncoin madncoin eningcoin persetcoin autcoin surangcoin unbocoin turingcoin
18:51:28 <APic> yay
18:51:35 <int-e> I think those are better.
18:51:49 <APic> Seems so.
18:51:55 <wob_jonas> turingcoin, archwaycoin
18:52:06 <APic> B-)
18:52:16 <int-e> `words
18:52:18 <HackEgo> keili
18:56:41 <APic> Kewl
19:11:52 -!- sleffy has quit (Ping timeout: 256 seconds).
19:25:49 -!- sleffy has joined.
19:35:09 -!- sleffy has quit (Ping timeout: 260 seconds).
19:39:51 -!- Melvar` has quit (Ping timeout: 268 seconds).
19:50:57 -!- LKoen has quit (Remote host closed the connection).
19:52:37 -!- Melvar` has joined.
20:31:19 -!- erkin has quit (Read error: Connection reset by peer).
20:35:06 -!- erkin has joined.
20:43:53 -!- augur has joined.
20:46:17 -!- LKoen has joined.
21:03:06 <zzo38> So far I have programs reading three vector formats: Fuun RNA, Janome Embroidery Format, and DRAWX vector format. I did not write the program that can convert a raster picture into such format, because I do not know much about cross-stitch (or about embroidery in general) to do so. Do you know?
21:07:57 <wob_jonas> zzo38: I don't, but I think some teams have effectively developped a raster image to Fuun DNA compiler to solve the contest.
21:08:32 <wob_jonas> It's tricky because it's a deliberately esoteric vector format.
21:09:52 <zzo38> Yes, although in that case you don't need any stitches, at least. Still, it is perhaps something to be seen; I have not seen such a thing
21:15:58 -!- moei has joined.
21:42:16 -!- augur has quit (Remote host closed the connection).
21:42:58 -!- erkin has quit (Read error: Connection reset by peer).
21:44:52 -!- erkin has joined.
22:03:04 -!- aeyxa has joined.
22:03:47 -!- jaboja has joined.
22:03:47 -!- Naergon has quit (Ping timeout: 260 seconds).
22:19:13 -!- clog has quit (Ping timeout: 248 seconds).
22:26:46 <zzo38> Do you like the GLOGG container format I made up? It is similar to Ogg format, although the header is normally only 22 bytes long (but can vary), and there is a few other functions included (all optional, though), and it uses a different mechanism to identify codecs (they are identified by a UUID, given as part of the control data, although the control data is optional anyways). Converting Ogg->GLOGG should not be difficult; any existing file shou
22:27:36 -!- boily has joined.
22:33:13 <zzo38> So, any codec suitable for Ogg will be suitable with this new format too, although it will help to define the UUID for each such codec.
22:49:39 -!- laerling has quit (Quit: Leaving).
22:50:11 <int-e> zzo38: how many of your file format extensions have, you know, become standards?
22:52:15 <shachaf> i,i how may of your oil companies have, you know, become Standard?
22:56:34 <zzo38> int-e: None as far as I know. I don't know about future, though; things in future is difficult to predict.
22:56:59 <shachaf> That's why I predict things in the past.
23:01:31 <zzo38> Did you read the document? (I have recently added a "primary bit" to the control flags. Like the rest of the control data, it is optional.)
23:02:21 <int-e> . o O ( of course not? )
23:03:43 <zzo38> The document is: http://zzo38computer.org/textfile/miscellaneous/glogg
23:03:59 <zzo38> Afterward, I can make up another file with the description of the caption codec.
23:04:16 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
23:05:42 <zzo38> Now you can mention your complaint about anything I may have made a mistake, or other kind of complaints or questions.
23:07:35 <shachaf> int-e does not like this
23:09:15 <int-e> I've skimmed the document. The only motivation I see is that a person naming themselves zzo38 "don't like the way [OGG] uses to determine codecs."... presumably GLOGG improves on this.
23:09:40 <int-e> My bet is that nobody will care. For now I can give one example.
23:10:06 <int-e> (Sorry, I mean nobody besides the author, I'll give zzo38 that much credit.)
23:13:16 <zzo38> O, OK.
23:15:54 <zzo38> However, it does do some other stuff too; it does not only provide an alternative way to determine codecs. You can also specify relation of streams, and index marks, and a few of the things from Ogg Skeleton (although some are omitted because they should properly belong in separate metadata streams).
23:16:18 -!- AnotherTest has quit (Ping timeout: 240 seconds).
23:18:59 <int-e> zzo38: I think that you should present the problems you're perceiving with the state of the art (say, the Ogg format) up front. It takes time to try to reverse engineer the problem from the solution (which tends to also require understanding the original), and I for one am not willing to invest that time in order to figure out whether I even care about the problem at all. OTOH, if you manage to...
23:19:05 <int-e> ...convince me that there *is* a problem worth solving, then I'd be much happier to try to understand the proposed solution.
23:19:40 <zzo38> OK
23:19:48 -!- augur has joined.
23:22:10 <zzo38> One problem is that they fail to specify how multiple streams are related to each other. Sometimes this isn't important, but sometimes it will be relevant. That's why it is an optional feature.
23:22:54 -!- sprocklem has joined.
23:25:16 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=54148&oldid=54143 * Alcofrisbas * (+216) /* Introductions */
23:26:07 <int-e> shachaf: I experience heightened levels of indifference :P
23:26:25 <shachaf> Higher than your usual?
23:26:35 <int-e> who cares?
23:26:52 <shachaf> `? int-e
23:26:53 <HackEgo> int-e är inte svensk. Hen kommer att spränga solen. Hen står för sig själv. Hen gillar inte färger, men han gillar dissonans. Er hat ein Hipster-Spiel gekauft.
23:29:00 <int-e> hmm hipster game, was that Braid or the Witless?
23:29:29 <int-e> I guess I don't care about that either.
23:29:52 <shachaf> That sentence doesn't look very Swedish...
23:30:02 <shachaf> `dowg int-e
23:30:10 <HackEgo> 10861:2017-05-03 <shachäf> le//rn_append int-e//Er hat ein Hipster-Spiel gekauft. \ 10125:2017-01-12 <oerjän> slwd int-e//s;.$;, men han gillar dissonans.; \ 9127:2016-09-30 <oerjän> learn_append int-e Hen gillar inte f\xc3\xa4rger. \ 7535:2016-04-25 <oerjän> learn_append int-e Hen st\xc3\xa5r f\xc3\xb6r sig sj\xc3\xa4lv. \ 7232:2016-03-14
23:30:19 <shachaf> ?!
23:30:44 <shachaf> It was SSR.
23:30:48 <int-e> Oh.
23:31:00 <shachaf> 10:22:36 <int-e> http://int-e.eu/~bf3/tmp/ssr.png <-- oh nein, ich habe schon wieder ein Hipster-Spiel gekauft. (aber nicht zum Vollpreis, gibt grad ein humble bundle)
23:31:19 <int-e> but note the "schon wieder"
23:31:44 <int-e> ("yet again", I guess)
23:32:52 <shachaf> Did you kauft any Hipster-Spielen since then?
23:34:21 <zzo38> Multimedia container formats other than Ogg do exist, but most of them are too complicated it look like.
23:37:39 -!- contrapumpkin has joined.
23:42:34 <int-e> shachaf: Well tbqh I don't even know what a "hipster game" is... I've seen the label in a couple of game reviews. I think I had found some top-ten of hipster games somewhere just before I wrote that...
23:43:29 <int-e> To me it sounds like "is being recommended on linkedin" ;-)
23:44:21 <int-e> Regardless, bedtime.
23:46:22 <zzo38> Now I added a few other functions too, such as reverse relations (useful for captions), and passthrough mode (useful for playing back stereovision videos on non-stereovision implementations without causing additional problems), although these are not the only uses of these functions; they may be used for whatever you find them useful for.
23:47:57 <int-e> shachaf: But if you want to know about games I regretted buying recently, I'd name "What remains of Edith Finch" and "Oxenfree".
23:48:14 <shachaf> Wwhy did you regret buying them?
23:48:35 <shachaf> Maybe you would like this song: https://www.youtube.com/watch?v=oFlG7KN6OqY
23:50:42 <int-e> Both are essentially linear (the former more so than the latter)... the latter is ultimately about relationships among a bunch of teenagers, otherwise it's just running around finding various spots on a map.
23:51:23 <int-e> Did I say bedtime? I think I said bedtime. It is bedtime. Good night.
←2018-02-17 2018-02-18 2018-02-19→ ↑2018 ↑all