00:13:54 -!- imode has quit (Ping timeout: 256 seconds). 00:23:33 -!- 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.”). 00:23:44 int-e: what have you poke them with? 00:26:30 pointy letters and rount letters 00:26:35 round even 00:30:54 -!- arseniiv has quit (Ping timeout: 256 seconds). 00:32:46 The web thing's been a little flaky occasionally. I was meant to debug it, but haven't managed to. 00:33:29 Should be back now. 00:33:42 ...or maybe not. 00:33:45 -!- FreeFull has quit. 00:34:44 Well, at least it's started to hang up kind of consistently. 00:35:44 I think chances are there's some bug in the websocket-based stalker mode that manages to hang up the regular request processing, even though it's not supposed to. 00:36:00 -!- MTGBusyBeaver42 has joined. 00:36:30 When I restart it, it works for a bit, until there's a new stalker mode connection, and then it stops working again. 00:39:07 Might have something to do with there being two active stalkers at the same time, that's probably not something I actually tested. 00:52:25 ais523: looking at your WiP proof for 10 waterclocks, I'm not familiar with the language you are implementing, but it looks like the idea is to use that language to implement a cyclic tag system and prove TC that way, 00:53:05 2-tag, but yes 00:53:44 the eso wiki says not all variants of high rise are TC, what makes this implementation one of the TC ones? 00:54:33 it's pretty easy to implement High Rise variants in The Waterfall Model, the hard part is to aim for a TC variant 00:54:45 I erred on the side of implementing a more powerful variant to make almost certain that it's TC 00:55:04 (you can implement a simpler variant that /might/ be TC with 8 waterclocks, I added two extra here to more or less totally make sure) 00:55:19 -!- Lord_of_Life has quit (Ping timeout: 255 seconds). 00:55:35 to prove this particular Waterfall machine TC, you have to do two things, prove it implements that particular High Rise variant, and prove the variant TC 00:56:01 it's only a WIP proof because I haven't done either half yet, I'm currently working on the second half (when I'm working on something that isn't my day job) 00:56:50 yeah, it looks like implementing it in TWM isnt asking for anything TWM has a hard time doing 00:57:17 it's the use of the E' waterclock that makes it almost certainly TC, its purpose is to outright skip every second 2 in the High Rise data string 00:57:45 that gives us the one bit of state that you need to add to 1-tag to make it TC, so the only remaining hurdle is to prove that the rest of the language can implement 1-tag 00:58:44 I may as well write my thoughts on that up here, too: the only thing that determines where new 2s are added in the data string is the distance between two (non-ignored) 2s scrolling off the data string 00:59:18 the basic idea is to use two sorts of distances, small distances which also happen to be odd numbers, and large distances which also happen to be even numbers 00:59:40 then small distances push the corresponding large distances onto the data string, large distances push a string of small distances onto the data string 01:00:17 for the latter, you have a block of 1s in one half of the data string that matches up to the pattern you want (made of 1s) in the other half 01:00:52 for the former, you have a sequence 101010101010101… in one half of the data string against a 1 in the other that adds up to a 2 only if you have a small (thus odd) distance 01:01:17 and a few sporadic 1s in both halves which match up only when using a specific small distance 01:01:40 err, I don't mean one half of the data string, I mean one half of the geometric sequence 01:01:52 the ratio between successive elements is a very large power of 3 01:02:01 and the two halves are around 3^n and 3^(n+1) 01:02:11 actually this proof uses 9 rather than 3 but it's the same principle 01:02:33 I probably haven't explained this very well, it'll probably be better to write it up as an actual proof, or else write a compiler 01:02:36 to make it more formal 01:03:13 thanks, this did actually help, high-rise is wierd 01:04:44 it's funny, in the early history of esolangs, people made things like INTERCAL and Malbolge which were weird on purpose, for the sake of weirdness 01:05:04 -!- Lord_of_Life has joined. 01:05:07 and nowadays, when we look into the simplest, most fundamental available tarpits, we get just as much weirdness but it's naturally occurring 01:05:54 Yeah I actually was looking at 3-star programmer randomly like a year ago 01:06:47 there's a High Rise language in base 2, with carries allowed, which uses a blank sequence for 0 and a geometric (not interleaved-geometric) sequence for 1 which I'm genuinely not sure whether it's TC or not, it seems so close to being TC but I can't quite make it work 01:06:49 so wierd for operations like that to be TC 01:08:26 it gets easier once you realise that you can set things up so that some of the addresses are constants that always point to the same place, that effectively lets you get rid of stars when you don't want them 01:08:50 it doesn't seem that ridiculous to me that a program based on ++*k, ++**k, ++***k can be TC for constant k 01:09:27 only having increments available for writing and only having dereferences available for reading is painful, but by keeping regimented control over the whole of memory, it's not /that/ bad 01:11:35 yeah, it is still bizarre to think about, more common operations like XOR are a lot easier to understand why. 01:12:18 actually I think the hardest part with Three Star Programmer (and with the I/D machine) is that every statement has to increment /something/ so you need to find a lot of useless variables to throw your increments away in 01:13:12 the TC proof for the I/D machine goes to the effort of setting up a queue that's never read from, just so that it can write to it the same way that it writes to the queue that it does use, thus vastly reducing the number of writes that need to be special-cased to sometimes write to somewhere useless 01:13:51 this is a common trick in esoprogramming, I think, creating a dummy data structure that's just like your real, useful data structure so that you can throw away unwanted writes without using a conditional 01:14:02 it was invented by Donald Knuth when he was programming in INTERCAL 01:15:16 yeah I've definitely seen it before. 01:15:54 anyway back to TWM->high-rise -> 2-tag -> TM 01:16:31 what approximate ratio do we need in TWM to get an X state TM? 01:16:49 let's see: a TWM program is defined by zeroing triggers and initial values 01:16:54 and number of waterclocks 01:16:57 the number of waterclocks is fixed 01:17:14 the initial values could be small because 2-tag is good at bootstrapping itself 01:17:42 (by "small" I mean in the 1000-10000 range, although you could add an additional waterclock if you needed them smaller) 01:18:06 the zeroing triggers are mostly small but a few of them will be enormous, encoding the High Rise program that encodes the 2-tag program that encodes the TM 01:18:11 Initial values are the same cost as the transitions 01:18:19 right, that doesn't surprise me 01:19:34 the size of the zeroing triggers will be a small multiple of the ratio of the High Rise geometric series times the base of High Rise geometric series, as a number 01:19:45 but the 2-tag translation sees it as a string of digits 01:19:51 which we'll be converting into a number using base 9 01:20:51 the length of the string, I suspect is roughly quadratic in the number of colors of the 2-tag system (the length of the productions obviously also matters but it's only linear in those, so the number of colors probably dominates) 01:21:21 so we have a number of the form 9^(2^colors) 01:21:34 this is larger than most reasonable one-arrow numbers, but smaller than almost all two-arrow numbers 01:21:46 wait, no 01:21:58 it's 9^(colors^2 * constant) which is much smaller 01:22:21 it's large as one-arrow numbers go, but perhaps in reach, and thus easily dominated by two-arrow numbers 01:22:47 the question is, how large of a 2-tag system do you need to implement a UTM 01:23:13 and I don't know that part because the 2-tag-from-UTM translation isn't one that I've personally worked on 01:23:49 Well there are some pretty small UTMs 01:24:34 there's a paper covering this but it isn't publicly available 01:24:53 so I can't just look up the complexity 01:25:07 ofc, the simpler the UTM, the larger the encoding of its input you typically need 01:26:43 so the busy beaver function for a given UTM will grow more slowly the simpler the UTM is (although not much more slowly because busy beaver functions grow faster than anything computable, so they're all pretty fast) 01:26:44 wait we dont need a UTM, we can encode the TM busy beaver as the 2-tag program 01:27:22 right; and in fact you could encode a Waterfall Model busy beaver which would probably be busier (it would have to be at least as busy) 01:27:50 Yeah once we iterate the conversion doesn't particularly matter 01:27:57 it's an interesting problem because you need to show that the UTM exists in order to prove that the busy beaver function grows quickly, but the busiest beaver probably won't use one at all 01:28:40 hmm, or maybe it will? that's an interesting question in its own right 01:29:05 (and one that's very hard to answer because finding busy beavers is almost impossible even for very small machines) 01:29:51 hey, #esoteric regulars: if you have a language that is sub-TC, does that imply that finding busy beavers for it is computable? or can a language be sub-TC and yet have an uncomputable halting problem? 01:30:02 Yeah, though how to define the size of a TWM busy beaver something like (Clocks, Max size) 01:30:23 "number of Plant tokens required to set it up" 01:30:31 yes 01:33:01 if Flooding Waterfall Machines have real busy beavers then we can have a lot more freedom in the setup and probably get an extra layer of iterations too 01:33:50 well, 10 waterclocks + a number of flooding clocks is going to give you much busier beavers, because you can write a UTM using the 10 waterclocks, and use the flooding clocks as additional storage that naturally tends to explode 01:34:11 if all your waterclocks are flooding, I'm still unsure what happens 01:34:53 I think the best way to think about the flooding version of the language is that the zeroing triggers actually run every cycle, but their effects don't become visible until their clock zeroes 01:35:22 but that way of thinking about it hasn't helped me much with actually programming in the language :-D 01:37:57 yeah, either way of thinking about it, there's not really a good way to encode the values, due to combining multiplication and addition/subtraction 02:30:58 -!- ais523 has quit (Quit: quit). 02:36:09 -!- ais523 has joined. 02:37:07 MTGBusyBeaver42: you should point out to the thread that Battletide Alchemist doesn't work if there's any way to have it on the field when setting up a double-Arcbond (even among your own creatures); you can use the optional damage prevention to make the loop run for a set, unlimited number of iterations 02:38:11 like, the idea is that you make the opponent gain loop each iteration but don't use it yourself, set up a trivial infinite loop, run yourself out of life via choosing not to use Battletide Alchemist after a chosen number of iterations in order to deal a chosen amount of damage to the opponent 02:39:28 although, I think it isn't being used anyway in the current versions 02:39:29 -!- ais523 has quit (Client Quit). 02:42:20 "There's a reason the comprehensive rules and errata for Magic: The Gathering is hundreds of pages long and reads like a federal tax code" I don't think so; the tax code is much more confusing. 03:15:20 Well the score is actually how negative their life goes, not the total dealt. 03:16:49 is the federal tax code TC? 03:19:12 [[Lightlang]] https://esolangs.org/w/index.php?diff=70265&oldid=68026 * Felixcesar15 * (-2131) New instruction set 03:20:50 [[Lightlang]] M https://esolangs.org/w/index.php?diff=70266&oldid=70265 * Felixcesar15 * (-49) 03:25:43 I don't know, but that is independent. 04:17:41 -!- oerjan has quit (Quit: Nite). 04:26:47 -!- MTGBusyBeaver42 has quit (Remote host closed the connection). 05:05:11 -!- imode has joined. 05:25:46 -!- Sgeo has quit (Ping timeout: 258 seconds). 06:04:56 -!- kritixilithos has joined. 06:21:53 -!- Sgeo has joined. 06:38:49 -!- myname has quit (Quit: Lost terminal). 06:56:52 -!- imode has quit (Ping timeout: 265 seconds). 07:12:10 -!- myname has joined. 08:20:03 -!- xelxebar_ has quit (Ping timeout: 240 seconds). 08:42:49 ais523: "can a language be sub-TC and yet have an uncomputable halting problem?" => certainly. just take a language that is like a normal TC language but the programs are encrypted with a random function that is very uncomputable in both directions. basically just take a random language that has no rules to it. 08:44:10 like, the encryption isn't uncomputable because of some fancy complexity theory reason, only because by cardinality reasons most functions are uncomputable. 08:51:51 -!- b_jonas has quit (Quit: leaving). 08:58:52 -!- xelxebar has joined. 09:45:05 Can an actually-implementable language be sub-TC and have an uncomputable halting problem? 09:45:59 It seems likely to me 09:46:38 Just saying "this thing has an uncomputable halting problem" doesn't feel like it should get you Turing completeness for free. 09:47:19 A program p in Language P does no computation and halts if and only if p doesn't halt 09:48:23 Haha 09:49:25 That sounds more like a description of a language with no correct implementation. 09:49:42 But I can see what you're trying to do :) 09:53:09 Maybe just take a single Turing machine whose halting already can't be decided... say it searches for a proof of a contradiction in our metatheory, and then define a language with but a single program whose implementation is that machine. 09:57:12 maybe for a particular program of this language, it runs the input as a TM, and after the completion of execution (if it does halt), the program returns 0 09:57:33 Oh, that's a good one 09:58:29 Just take any ordinary Turing complete language and make sure it can't produce any interesting output other than whether it terminated. 10:00:34 I think that might be too easy to argue it's not turing complete 10:00:40 It can semi-decide any semi-decidable language 10:01:01 Well, it's supposed to not be Turing complete 10:01:17 But have an uncomputable halting problem 10:02:00 Of course, you might be able to also hope for a more practical language that could be used to solve a wider range of problems... 10:02:58 Like, it should maybe contain a consistent type theory as a sublanguage. 10:02:58 I mean, argue it is turing complete 10:04:03 Well, you can't solve most ordinary decision problems 10:04:15 Like, the problem of whether the number on input is even 10:04:22 You can only semi-decide it 10:27:43 -!- atslash has quit (Ping timeout: 255 seconds). 10:33:31 -!- wib_jonas has joined. 10:41:35 -!- cpressey has joined. 10:51:46 -!- LKoen has joined. 10:58:16 -!- arseniiv has joined. 10:58:43 -!- kritixilithos has quit (Ping timeout: 240 seconds). 11:10:21 -!- Felixcesar15 has joined. 11:12:02 -!- Felixcesar15 has quit (Remote host closed the connection). 11:27:46 -!- LKoen has quit (Remote host closed the connection). 11:28:04 Welcome to the international center for esoteric programming libation design, development, and deployment! 11:29:03 libation design 11:30:55 This theme and variations will continue until someone fixes the topic. 11:32:23 -!- LKoen has joined. 11:33:48 -!- sprocklem has quit (Ping timeout: 265 seconds). 11:35:09 -!- sprocklem has joined. 11:49:48 -!- kritixilithos has joined. 11:57:47 -!- sprocklem has quit (Ping timeout: 260 seconds). 11:59:19 -!- sprocklem has joined. 12:00:04 -!- LKoen has quit (Remote host closed the connection). 12:01:26 -!- LKoen has joined. 12:12:22 [[Function x(y)]] M https://esolangs.org/w/index.php?diff=70267&oldid=70263 * PythonshellDebugwindow * (+17) /* Syntax */ 12:14:16 `? go 12:14:19 Go is a common irregular verbal game programming language invented by the Germanic Taneb tribes catching monsters in the strategic territories of East Asia. 12:18:11 [[Function x(y)]] M https://esolangs.org/w/index.php?diff=70268&oldid=70267 * PythonshellDebugwindow * (+271) /* Syntax */ 12:19:11 [[Function x(y)]] M https://esolangs.org/w/index.php?diff=70269&oldid=70268 * PythonshellDebugwindow * (-22) /* Syntax */ 12:27:11 cpressey: so no incentive to change anything then 12:27:43 `' 12:27:44 3) that's where I got it rocket launch facility gift shop 12:29:44 -!- kspalaiologos has joined. 12:34:59 is there a nonstandard model of natural numbers in a Heyting arithmetic (this is an intuitionistic counterpart to Peano arithmetic) 12:36:42 arseniiv: Just take any classical non-standard model? 12:37:15 though I should first find and understand what is a model of an intuitionistic first-order theory 12:38:17 int-e: yeah I thought that could be the case but there’s a strange lack of mentions of nonstandard models for the case so I thought maybe there’s something interesting going on 12:38:31 arseniiv: I think there's somethink like models in intuitionistic logic but it's much more complicated than ordinary models 12:40:27 https://en.wikipedia.org/wiki/Kripke_semantics ... but this only seems necessary if you want to capture the lack of excluded middle in the semantics, which seems unnecessary if you just want a non-standard model. 12:41:04 (Insofar as the term makes any sense at all... I mean, what is /the/ standard model anyway if you don't have the law of excluded middle?) 12:48:35 int-e: for a formula A without quantifiers, in Heyting arithmetic it’s provable A ∨ ¬A, so in particular equality of terms is decidable so the usual standard model should suffice if elevated to an intuitionistic model (in a way I don’t know yet) 12:53:18 (also it makes sense that in a constructive world there should be the standard natural numbers thing: where at all if not here? Though this isn’t an argument at all as I heard in type theories there are still issues analogous to nonstandard elements, but they aren’t as visible or petrifying) 12:54:49 so does that make the standard model of natural numbers a non-standard model :P 12:56:03 . o O ( And just to add to the fun, it could still not be non-standard. ) 12:59:58 -!- LKoen has quit (Remote host closed the connection). 13:03:37 -!- LKoen has joined. 13:09:06 -!- Lord_of_Life has quit (Ping timeout: 256 seconds). 13:15:33 -!- Lord_of_Life has joined. 13:22:57 int-e: *the* standard model is probaby still the classical logic one in which the exculded middle happens to hold, which intuitionistic logic still supports as a special case, or so this person with his traditional classical logic habits thinks 13:26:21 -!- LKoen has quit (Remote host closed the connection). 13:26:56 -!- art1 has joined. 13:29:33 -!- LKoen has joined. 13:31:10 [[2KWLang]] N https://esolangs.org/w/index.php?oldid=70270 * PythonshellDebugwindow * (+1102) Created page with "'''2KWLang''' (short for 2-Keyword Language) is an esolang by [[User:PythonshellDebugwindow]]. ==Syntax== There are only two keywords in this language, as the name implies, a..." 13:38:38 [[Truth-machine]] M https://esolangs.org/w/index.php?diff=70271&oldid=69138 * PythonshellDebugwindow * (+303) /* 2KWLang */ 13:40:13 [[2KWLang]] M https://esolangs.org/w/index.php?diff=70272&oldid=70270 * PythonshellDebugwindow * (+540) /* Quine (maybe cheating) */ 13:51:09 So we have lots of esolangs where we guess they are Turing-complete, and some where we even have informal proofs that they're TC. Do we have any where we have a formal, machine-checkable proof that it's TC? 13:52:35 cpressey: probably not machine-checkable, because nobody bothers to write those 13:53:01 but I can point to at least two books about theory of algorithms with formal proofs 14:00:37 cpressey: https://esolangs.org/wiki/Minsky_machine says "A proof of Turing-completeness is also given in the textbook ...", this is an important TC-ness theorem, because we often prove TC-ness by compiling Minsky machines (with a fixed number of counters) to an esolang 14:00:49 there are other similar classical computational models 14:02:59 that reminds me I haven’t finished a Python module with utilities for working with generalized Minsky machines. Maybe I should start a C# module for that instead 14:06:31 more like a reference implementation of the algorithm deciding whether an “algebraic type universe” is infinite and constructing a term and an unary function to realize Z and S 14:07:16 fungot: have you stocked up on toilet paper? 14:07:16 int-e: this is what you're trying to do, is to load it 14:16:30 -!- ais523 has joined. 14:16:55 cpressey: the proofs have varying levels of formality, I'm not sure if any are machine-checkable 14:17:06 ah yes, cpressey summoned ais 14:17:25 I have actually started writing TC proofs for a couple of esolangs in Agda, but abandoned them pretty early 14:17:38 cpressey: This kind of stuff is really tedious, hard to justify the effort (unless you do it just for fun). 14:17:43 it's not an easy sort of thing to translate into Agda 14:17:43 -!- ais523 has quit (Remote host closed the connection). 14:17:55 -!- ais523 has joined. 14:18:07 I was considering joining 14:18:17 the problem is that a lot of these proofs are really hairy, because eg. when you want to simulate a RAM machine with a turing machine, you need to be able to move all symbols on the tape to insert a space and get back to that space and copy all these move routines multiple times in the turing machine program so that you can return to the previous 14:18:17 state, 14:18:31 -!- ais523 has set topic: Welcome to the international center for esoteric programming discussion, design, development, and deployment! | https://esolangs.org | logs: https://esolangs.org/logs/ http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/?C=M;O=D https://github.com/KrzysztofSzewczyk/esologs/. 14:18:36 I felt we needed a fourth d word 14:18:54 and be able to store numbers on the tape, and copy or compare numbers between faraway palces in the tape, etc 14:19:11 right, I was concentrating mostly on simulating one queue-based language with another 14:19:17 but even that is hard to prove things about in Agda 14:19:47 I have a formalization that Minsky Machines can implement recursive functions in Isabelle/HOL. That went fairly well, but it's a really nice programming model compared to many esolangs. 14:20:23 For example it's very easy to compose Minsky machines; just rename the states apart and add a few glue transitions. 14:20:47 and then you want to prove that you can translate a structured program (with if blocks, while blocks, function definitions and non-recursive function calls) to a finite control structure (either with a state for each possible call stack in the original program, or by storing return addresses as data); 14:21:02 then you want to prove the same thing for programs with recursive calls too; etc 14:21:03 (And I did not impose any bound on the number of registers) 14:22:15 and then that you can translate a language that has closures (like lambda expressions) to a language that doesn't have closures but has recursive calls 14:22:30 there's a step between, that you can simulate function pointers 14:22:59 there are a lot of "high-level" abstractions in real programming languages that you need to be able to prove that a simple computation model can simulate 14:24:14 You have to consider that each of these "simple steps" probably involves defining an intermediate language, a semantics for it, a translation, and proofs that the translation preserves the semantics, all for something that we can handwave through in a couple of lines of text. 14:24:26 (Because it's highly intuitive.) 14:24:48 yeah 14:25:23 you have to define the translation of the intermediate states, and prove that each step preserves that translation, translating the effect of a step of one machine to the effect of a step of the other machine 14:26:03 of course it's more likely multiple steps of one machine 14:46:21 Is #coq a moderated channel? I tried to ask a question there but got "Cannot send to nick/channel". 14:46:38 you can try writing /mode #coq while you're there 14:46:50 afaict it's mode is [+cnt] and afaict that does not mean it's moderated 14:46:50 that should give you full information on what channel modes might prevent you sending there 14:47:24 hmm, perhaps you're banned from it (although you're unlikely to be banned personally, this could happen as a result of a ban that matches on characteristics other than nick/ident/IP) 14:47:52 cpressey: are you logged in to nickserv? a lot of channels ban everyone who isn't logged in to nickserv 14:48:08 int-e: Do you know anything about extraction in Coq? 14:48:12 err, muted, not banned 14:48:18 if you were banned you wouldn't be able to join it 14:48:30 cpressey: nothing beyond the term 14:49:25 OK. It's a really simple question, I expect I already know the answer, it would be nice to have it confirmed but I'll just keep reading and I'll eventually know 14:49:31 cpressey: Meaning I think I know what it is abstractly, but not how it's done. 14:51:21 int-e: Well, it's this: Coq is guaranteed to terminate. Are the programs extracted from Coq also guaranteed to terminate? 14:51:31 I think it's "yes" 14:52:23 -!- kritixilithos has quit (Ping timeout: 240 seconds). 14:53:30 -!- spruit11 has joined. 14:53:58 -!- kritixilithos has joined. 14:57:16 cpressey: I think so too (though you can mess up the setup) 15:03:35 Yeah, you can do some low-level things and mess it up. What I'm thinking though, is more like: you can't extract a Turing-complete interpreter from a Coq proof. You could extract a compiler, though. 15:06:29 Uh, but there's a loophole there. 15:06:34 Namely, codata 15:09:12 (co)data Res a = Continue (Res a) | Return a 15:09:46 Whatever that is in Coq, I haven't ventured there. 15:14:20 -!- LKoen has quit (Remote host closed the connection). 15:15:35 Is that a good loophole or a bad loophole 15:17:52 Or, to put it another way... 15:18:27 It's a good one? 15:18:56 [[Function x(y)]] https://esolangs.org/w/index.php?diff=70273&oldid=70269 * Hakerh400 * (+0) Fix category link 15:19:08 My understanding of it is bad though 15:19:29 The corresponding function Res a -> a is still not total. 15:20:08 We can't extract an big-step interpreter, but we can extract a single-step interpreter that we can iterate as much or as little as we like? 15:20:09 The corrsponding notion to termination for codata is productivity: The outermost constructor is produced in finite time. 15:20:19 Yes. 15:23:42 OK. 15:33:44 cpressey: my Agda interpreters for TC languages had a cycle limit and got around the no-nonprovably-halting-programs restriction that way 15:34:05 you proved two languages were equivalent by proving that if one halted after some number of cycles, the other would also halt after some number of cycles 15:42:01 (and vice versa) 15:42:50 makes sense 15:48:09 OK. There would also seem to be a stronger definition of equivalence, where their behaviours have some correspondence regardless of whether they halt or not. 16:03:13 cpressey: yes, and you almost certainly have to use such a stronger equivalence statement in the induction part of the proof of the weaker equivalence 16:08:03 cpressey: if you want to see formal a simulation proof, I have one written down in detail at http://www.madore.org/cgi-bin/comment.pl/showcomments?href=http%3a%2f%2fwww.madore.org%2f~david%2fweblog%2f2017-08.html%23d.2017-08-18.2460#comment-23792 , and this is an easy one, because the languages it talks about ((1) with arrays and (1)) are both 16:08:03 high-level and similar, so there's no messing about with low level details like how to copy a variable length string in a one-tape Turing machine 16:08:23 -!- kritixilithos has quit (Ping timeout: 240 seconds). 16:09:53 but even then I omit a lot of fiddly details that you'd have to expand on if you wanted a machine language proof 16:20:31 wib_jonas: OK, thanks. 16:22:02 and even there I'm lucky because (1) supports early function returns from inside loops, which simplifies the human-readable description a lot 16:27:16 -!- MTGBusyBeaver42 has joined. 16:29:12 codata above reminded me about how I tried to invent what a coeffect should look like when I couldn’t sleep the day before. Does anybody knows if coeffects are at all considered somewhere? 16:29:49 -!- LKoen has joined. 16:31:24 is that the dual of when nsiders are effected? 16:34:05 Regarding the non-TC halting problem I'd argue that forcing the output to be 0 is not enough to force something sub TC, as we also get how long it took to terminate. 16:34:20 I thought something like: in an effectful computation, one can choose and use effect constructors as many times as they like, and in an effect handler, one “deconstructs” exactly one effect and they don’t choose which one, so a coeffectful computation may be where one uses a coeffect constructor just once and doesn’t choose which and a coeffect (co?)handler allows one to pick how many coeffects to eliminate. Looks like gibberish 16:35:11 wib_jonas: hmmm? 16:35:52 arseniiv: sorry. stupid joke like the one about how cocoa is really just a 16:35:54 `? cocoa 16:35:56 A is a village in Norway. The BBC invented it by not understanding things on top of letters. 16:37:05 wib_jonas: ah, “considers”. I thought it’s a special spelling of “insiders” but didn’t understand why 16:37:44 though I don’t, still :D 16:38:00 no, that one is about Darth Sidious 16:38:02 I like co jokes but hadn’t got this one 16:38:10 hm 16:44:54 arseniiv: IIRC coeffects are a real area of research that's quite busy 16:45:01 I think I've met people who work on them 16:45:29 they're the sort of thing that you use comonads to implement, just like you can use monads to implement effects 16:45:44 and normally correspond to some sort of resource that is consumed by a computation 16:45:57 ais523: do you know an expository paper or something? 16:46:12 I was hoping there'd be a Wikipedia article but there isn't 16:46:16 .oO(if coeffects is a busy area with lots of researchers, then the coronavirus spreads there, so the ronavirus... nah, it doesn't work) 16:46:44 (yeah I thought about comonads and resources/contexts but inside one head in the early morning it’s not that fruitful) 16:48:30 I also imagined what it would do with a call stack but the result was of a mixed usefulness too 16:52:12 -!- kritixilithos has joined. 16:52:35 arseniiv: try this: http://tomasp.net/blog/2014/why-coeffects-matter/ 16:52:48 sorry for not answering earlier, I was reading it first to make sure that the author actually understood the subject, but he does 16:55:29 (it strikes me that linking a random coeffect tutorial would have had the same risks as linking a random monad tutorial, but fewer people seem to write coeffect tutorials so they're probably of higher average quality) 16:55:39 that said, the post does remind me a lot of a monad tutorial :-D 16:56:27 "co-" is a common prefix, so I'm confident that constant concentrated comedy (contingent on contex of course) could confound/confuse the constituents in the conversation 16:56:41 it's a running joke in #esoteric 16:56:42 what if you link to the Typeclassopedia instead, since that's known to be a good book? https://wiki.haskell.org/Typeclassopedia#Comonad 16:57:10 wib_jonas: that doesn't explain much about why you'd use them 16:57:22 true, but it links to references about comonads 16:57:28 presumably those are pre-vetted 16:58:07 I almost posted it like this: "-" is a mmon prefix, so I'm nfident that nstant ncentrated medy (ntingent on ntex of urse) uld nfound/nfuse the nstituents in the nversation 16:59:39 you have to be careful, if comedy is confounding constituents, then nstituents should nfound medy 16:59:50 because the co- relationship reverses subject and object 17:00:13 it's like a mathematical version of the "in soviet russia" jokes 17:00:29 (does this make Soviet Russia an untry?) 17:00:37 fair point 17:01:20 it works well because "co" is like the thickest part of an English dictionary 17:02:08 -!- wib_jonas has quit (Remote host closed the connection). 17:20:58 "co" jokes are one thing, cojokes are quite another. 17:21:04 -!- cpressey has quit (Quit: A la prochaine.). 17:22:42 -!- imode has joined. 17:27:44 ais523: :D 17:49:16 sorry for not answering earlier, I was reading it first to make sure that the author actually understood the subject, but he does => thanks! No problem, as coincidentally I was busy away from here 17:51:04 (it strikes me that linking a random coeffect tutorial would have had the same risks as linking a random monad tutorial, but fewer people seem to write coeffect tutorials so they're probably of higher average quality) => lol :D 17:55:53 a cojoke is probably a thing several people say crying and an unsuspecting person nearby then feels witless 18:22:38 I think a cojoke is something you say in the hope that someone else will cheer you up 18:22:45 I'm not sure though 18:23:14 -!- atslash has joined. 18:28:39 -!- atslash has quit (Ping timeout: 268 seconds). 18:29:11 -!- atslash has joined. 18:32:02 Does any web browser include the command to pause/rewind/fast-forward animations? 18:32:22 I think it depends on the nature of the animations 18:32:46 if they're based on a