< 1584058434 764460 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 256 seconds < 1584059013 133440 :LKoen!~LKoen@81.255.219.130 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.” < 1584059024 309376 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: what have you poke them with? < 1584059190 164527 :int-e!~noone@int-e.eu PRIVMSG #esoteric :pointy letters and rount letters < 1584059195 330440 :int-e!~noone@int-e.eu PRIVMSG #esoteric :round even < 1584059454 764632 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru QUIT :Ping timeout: 256 seconds < 1584059566 505328 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :The web thing's been a little flaky occasionally. I was meant to debug it, but haven't managed to. < 1584059609 841061 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Should be back now. < 1584059622 48574 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :...or maybe not. < 1584059625 466461 :FreeFull!~freefull@defocus/sausage-lover QUIT : < 1584059684 384418 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Well, at least it's started to hang up kind of consistently. < 1584059744 743194 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :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. < 1584059760 818767 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net JOIN :#esoteric < 1584059790 559846 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :When I restart it, it works for a bit, until there's a new stalker mode connection, and then it stops working again. < 1584059947 174838 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Might have something to do with there being two active stalkers at the same time, that's probably not something I actually tested. < 1584060745 414603 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :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, < 1584060785 234988 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :2-tag, but yes < 1584060824 633948 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :the eso wiki says not all variants of high rise are TC, what makes this implementation one of the TC ones? < 1584060873 762733 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's pretty easy to implement High Rise variants in The Waterfall Model, the hard part is to aim for a TC variant < 1584060885 211258 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I erred on the side of implementing a more powerful variant to make almost certain that it's TC < 1584060904 765246 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :(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) < 1584060919 146223 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 255 seconds < 1584060935 475407 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584060961 776536 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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) < 1584061010 322260 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :yeah, it looks like implementing it in TWM isnt asking for anything TWM has a hard time doing < 1584061037 765727 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061065 2244 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061124 503962 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061158 510960 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061180 665656 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :then small distances push the corresponding large distances onto the data string, large distances push a string of small distances onto the data string < 1584061217 343402 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061252 52486 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061277 695329 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and a few sporadic 1s in both halves which match up only when using a specific small distance < 1584061300 921435 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :err, I don't mean one half of the data string, I mean one half of the geometric sequence < 1584061312 48029 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :the ratio between successive elements is a very large power of 3 < 1584061321 42865 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and the two halves are around 3^n and 3^(n+1) < 1584061331 500593 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :actually this proof uses 9 rather than 3 but it's the same principle < 1584061353 398546 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061356 565155 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :to make it more formal < 1584061393 463090 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :thanks, this did actually help, high-rise is wierd < 1584061484 622638 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061504 785984 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1584061507 543092 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and nowadays, when we look into the simplest, most fundamental available tarpits, we get just as much weirdness but it's naturally occurring < 1584061554 518592 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :Yeah I actually was looking at 3-star programmer randomly like a year ago < 1584061607 135096 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061609 189786 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :so wierd for operations like that to be TC < 1584061706 63602 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061730 355313 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it doesn't seem that ridiculous to me that a program based on ++*k, ++**k, ++***k can be TC for constant k < 1584061767 321878 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061895 578216 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :yeah, it is still bizarre to think about, more common operations like XOR are a lot easier to understand why. < 1584061938 585406 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584061992 955810 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584062031 382852 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584062042 168719 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it was invented by Donald Knuth when he was programming in INTERCAL < 1584062116 148927 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :yeah I've definitely seen it before. < 1584062154 447879 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :anyway back to TWM->high-rise -> 2-tag -> TM < 1584062191 253352 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :what approximate ratio do we need in TWM to get an X state TM? < 1584062209 135910 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :let's see: a TWM program is defined by zeroing triggers and initial values < 1584062214 8803 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and number of waterclocks < 1584062217 280117 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :the number of waterclocks is fixed < 1584062234 96833 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :the initial values could be small because 2-tag is good at bootstrapping itself < 1584062262 396443 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :(by "small" I mean in the 1000-10000 range, although you could add an additional waterclock if you needed them smaller) < 1584062286 819844 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584062291 667670 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :Initial values are the same cost as the transitions < 1584062299 668254 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :right, that doesn't surprise me < 1584062374 913745 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584062385 938274 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but the 2-tag translation sees it as a string of digits < 1584062391 896641 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :which we'll be converting into a number using base 9 < 1584062451 717388 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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) < 1584062481 688441 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so we have a number of the form 9^(2^colors) < 1584062494 168694 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :this is larger than most reasonable one-arrow numbers, but smaller than almost all two-arrow numbers < 1584062506 193970 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :wait, no < 1584062518 705961 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's 9^(colors^2 * constant) which is much smaller < 1584062541 599962 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's large as one-arrow numbers go, but perhaps in reach, and thus easily dominated by two-arrow numbers < 1584062567 162367 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :the question is, how large of a 2-tag system do you need to implement a UTM < 1584062593 423094 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and I don't know that part because the 2-tag-from-UTM translation isn't one that I've personally worked on < 1584062629 470745 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :Well there are some pretty small UTMs < 1584062674 722535 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :there's a paper covering this but it isn't publicly available < 1584062693 629405 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so I can't just look up the complexity < 1584062707 912963 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :ofc, the simpler the UTM, the larger the encoding of its input you typically need < 1584062803 730225 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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) < 1584062804 821502 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :wait we dont need a UTM, we can encode the TM busy beaver as the 2-tag program < 1584062842 799164 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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) < 1584062870 102795 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :Yeah once we iterate the conversion doesn't particularly matter < 1584062877 210805 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584062920 777962 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :hmm, or maybe it will? that's an interesting question in its own right < 1584062945 366346 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :(and one that's very hard to answer because finding busy beavers is almost impossible even for very small machines) < 1584062991 122533 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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? < 1584063002 335276 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :Yeah, though how to define the size of a TWM busy beaver something like (Clocks, Max size) < 1584063023 131102 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :"number of Plant tokens required to set it up" < 1584063031 40724 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :yes < 1584063181 429890 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :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 < 1584063230 508757 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584063251 648928 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :if all your waterclocks are flooding, I'm still unsure what happens < 1584063293 126606 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584063322 464359 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but that way of thinking about it hasn't helped me much with actually programming in the language :-D < 1584063477 173500 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :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 < 1584066658 284453 :ais523!~ais523@unaffiliated/ais523 QUIT :Quit: quit < 1584066969 776607 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1584067027 502005 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584067091 841150 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584067168 301893 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :although, I think it isn't being used anyway in the current versions < 1584067169 423032 :ais523!~ais523@unaffiliated/ais523 QUIT :Client Quit < 1584067340 643356 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :"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. < 1584069320 469931 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :Well the score is actually how negative their life goes, not the total dealt. < 1584069409 62223 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net PRIVMSG #esoteric :is the federal tax code TC? > 1584069552 437071 PRIVMSG #esoteric :14[[07Lightlang14]]4 10 02https://esolangs.org/w/index.php?diff=70265&oldid=68026 5* 03Felixcesar15 5* (-2131) 10New instruction set > 1584069650 297452 PRIVMSG #esoteric :14[[07Lightlang14]]4 M10 02https://esolangs.org/w/index.php?diff=70266&oldid=70265 5* 03Felixcesar15 5* (-49) 10 < 1584069943 390753 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :I don't know, but that is independent. < 1584073061 932504 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Nite < 1584073607 303938 :MTGBusyBeaver42!4925260f@c-73-37-38-15.hsd1.or.comcast.net QUIT :Remote host closed the connection < 1584075911 141132 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1584077146 447735 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net QUIT :Ping timeout: 258 seconds < 1584079496 822818 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1584080513 774696 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net JOIN :#esoteric < 1584081529 374778 :myname!~myname@ks300980.kimsufi.com QUIT :Quit: Lost terminal < 1584082612 463217 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 265 seconds < 1584083530 445469 :myname!~myname@ks300980.kimsufi.com JOIN :#esoteric < 1584087603 692103 :xelxebar_!~xelxebar@gateway/tor-sasl/xelxebar QUIT :Ping timeout: 240 seconds < 1584088969 732345 :b_jonas!~x@catv-176-63-14-83.catv.broadband.hu PRIVMSG #esoteric :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. < 1584089050 699886 :b_jonas!~x@catv-176-63-14-83.catv.broadband.hu PRIVMSG #esoteric :like, the encryption isn't uncomputable because of some fancy complexity theory reason, only because by cardinality reasons most functions are uncomputable. < 1584089511 958947 :b_jonas!~x@catv-176-63-14-83.catv.broadband.hu QUIT :Quit: leaving < 1584089932 485383 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar JOIN :#esoteric < 1584092705 539870 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Can an actually-implementable language be sub-TC and have an uncomputable halting problem? < 1584092759 743330 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :It seems likely to me < 1584092798 492002 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Just saying "this thing has an uncomputable halting problem" doesn't feel like it should get you Turing completeness for free. < 1584092839 816524 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :A program p in Language P does no computation and halts if and only if p doesn't halt < 1584092903 199058 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Haha < 1584092965 384630 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :That sounds more like a description of a language with no correct implementation. < 1584092982 743272 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :But I can see what you're trying to do :) < 1584093189 544348 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :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. < 1584093432 277000 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos PRIVMSG #esoteric :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 < 1584093453 19526 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Oh, that's a good one < 1584093509 86329 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Just take any ordinary Turing complete language and make sure it can't produce any interesting output other than whether it terminated. < 1584093634 30092 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I think that might be too easy to argue it's not turing complete < 1584093640 372075 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :It can semi-decide any semi-decidable language < 1584093661 509380 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Well, it's supposed to not be Turing complete < 1584093677 933811 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :But have an uncomputable halting problem < 1584093720 576121 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :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... < 1584093778 786251 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Like, it should maybe contain a consistent type theory as a sublanguage. < 1584093778 896220 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I mean, argue it is turing complete < 1584093843 403335 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Well, you can't solve most ordinary decision problems < 1584093855 603304 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :Like, the problem of whether the number on input is even < 1584093862 795340 :Cale!~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com PRIVMSG #esoteric :You can only semi-decide it < 1584095263 187802 :atslash!~atslash@static.231.107.9.5.clients.your-server.de QUIT :Ping timeout: 255 seconds < 1584095611 879708 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 JOIN :#esoteric < 1584096095 855689 :cpressey!~cpressey@5.133.242.4 JOIN :#esoteric < 1584096706 631243 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1584097096 879470 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru JOIN :#esoteric < 1584097123 675001 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Ping timeout: 240 seconds < 1584097821 818832 :Felixcesar15!afb0128c@175.176.18.140 JOIN :#esoteric < 1584097922 998444 :Felixcesar15!afb0128c@175.176.18.140 QUIT :Remote host closed the connection < 1584098866 960578 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection < 1584098884 744508 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Welcome to the international center for esoteric programming libation design, development, and deployment! < 1584098943 526283 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :libation design < 1584099055 879855 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :This theme and variations will continue until someone fixes the topic. < 1584099143 276699 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1584099228 54488 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 265 seconds < 1584099309 269096 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1584100188 674897 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1584100667 279943 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 260 seconds < 1584100759 302311 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1584100804 908847 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection < 1584100886 209544 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric > 1584101542 512747 PRIVMSG #esoteric :14[[07Function x(y)14]]4 M10 02https://esolangs.org/w/index.php?diff=70267&oldid=70263 5* 03PythonshellDebugwindow 5* (+17) 10/* Syntax */ < 1584101656 571257 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :`? go < 1584101659 219788 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :Go is a common irregular verbal game programming language invented by the Germanic Taneb tribes catching monsters in the strategic territories of East Asia. > 1584101891 318943 PRIVMSG #esoteric :14[[07Function x(y)14]]4 M10 02https://esolangs.org/w/index.php?diff=70268&oldid=70267 5* 03PythonshellDebugwindow 5* (+271) 10/* Syntax */ > 1584101951 237669 PRIVMSG #esoteric :14[[07Function x(y)14]]4 M10 02https://esolangs.org/w/index.php?diff=70269&oldid=70268 5* 03PythonshellDebugwindow 5* (-22) 10/* Syntax */ < 1584102431 154721 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: so no incentive to change anything then < 1584102463 413821 :int-e!~noone@int-e.eu PRIVMSG #esoteric :`' < 1584102464 253822 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :3) that's where I got it rocket launch facility gift shop < 1584102584 280860 :kspalaiologos!~kspalaiol@176.221.122.71 JOIN :#esoteric < 1584102899 338924 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :is there a nonstandard model of natural numbers in a Heyting arithmetic (this is an intuitionistic counterpart to Peano arithmetic) < 1584103002 727961 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: Just take any classical non-standard model? < 1584103035 857153 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :though I should first find and understand what is a model of an intuitionistic first-order theory < 1584103097 999914 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :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 < 1584103111 776203 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :arseniiv: I think there's somethink like models in intuitionistic logic but it's much more complicated than ordinary models < 1584103227 833212 :int-e!~noone@int-e.eu PRIVMSG #esoteric :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. < 1584103264 785527 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(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?) < 1584103715 6712 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :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) < 1584103998 479280 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :(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) < 1584104089 769989 :int-e!~noone@int-e.eu PRIVMSG #esoteric :so does that make the standard model of natural numbers a non-standard model :P < 1584104163 307928 :int-e!~noone@int-e.eu PRIVMSG #esoteric :. o O ( And just to add to the fun, it could still not be non-standard. ) < 1584104398 901378 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection < 1584104617 57900 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric < 1584104946 798352 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 256 seconds < 1584105333 961715 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1584105777 893390 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584105981 313573 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr QUIT :Remote host closed the connection < 1584106016 988771 :art1!~a@31.221.164.241 JOIN :#esoteric < 1584106173 718885 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric > 1584106270 646581 PRIVMSG #esoteric :14[[072KWLang14]]4 N10 02https://esolangs.org/w/index.php?oldid=70270 5* 03PythonshellDebugwindow 5* (+1102) 10Created 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..." > 1584106718 923390 PRIVMSG #esoteric :14[[07Truth-machine14]]4 M10 02https://esolangs.org/w/index.php?diff=70271&oldid=69138 5* 03PythonshellDebugwindow 5* (+303) 10/* 2KWLang */ > 1584106813 195792 PRIVMSG #esoteric :14[[072KWLang14]]4 M10 02https://esolangs.org/w/index.php?diff=70272&oldid=70270 5* 03PythonshellDebugwindow 5* (+540) 10/* Quine (maybe cheating) */ < 1584107469 796526 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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? < 1584107555 729783 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :cpressey: probably not machine-checkable, because nobody bothers to write those < 1584107581 763770 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :but I can point to at least two books about theory of algorithms with formal proofs < 1584108037 639619 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584108049 697785 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :there are other similar classical computational models < 1584108179 255137 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :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 < 1584108391 302307 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :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 < 1584108436 822031 :int-e!~noone@int-e.eu PRIVMSG #esoteric :fungot: have you stocked up on toilet paper? < 1584108436 924056 :fungot!~fungot@unaffiliated/fizzie/bot/fungot PRIVMSG #esoteric :int-e: this is what you're trying to do, is to load it < 1584108990 233994 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1584109015 576868 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :cpressey: the proofs have varying levels of formality, I'm not sure if any are machine-checkable < 1584109026 692016 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :ah yes, cpressey summoned ais < 1584109045 90886 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I have actually started writing TC proofs for a couple of esolangs in Agda, but abandoned them pretty early < 1584109058 644991 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: This kind of stuff is really tedious, hard to justify the effort (unless you do it just for fun). < 1584109063 224710 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's not an easy sort of thing to translate into Agda < 1584109063 367663 :ais523!~ais523@unaffiliated/ais523 QUIT :Remote host closed the connection < 1584109075 369037 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1584109087 849728 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I was considering joining < 1584109097 36895 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584109097 554781 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :state, < 1584109111 19461 :ais523!~ais523@unaffiliated/ais523 TOPIC #esoteric :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/ < 1584109116 13099 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I felt we needed a fourth d word < 1584109134 333862 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :and be able to store numbers on the tape, and copy or compare numbers between faraway palces in the tape, etc < 1584109151 644813 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :right, I was concentrating mostly on simulating one queue-based language with another < 1584109157 281701 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but even that is hard to prove things about in Agda < 1584109187 344211 :int-e!~noone@int-e.eu PRIVMSG #esoteric :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. < 1584109223 860593 :int-e!~noone@int-e.eu PRIVMSG #esoteric :For example it's very easy to compose Minsky machines; just rename the states apart and add a few glue transitions. < 1584109247 773328 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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); < 1584109262 98585 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :then you want to prove the same thing for programs with recursive calls too; etc < 1584109263 296365 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(And I did not impose any bound on the number of registers) < 1584109335 841421 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584109350 954439 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :there's a step between, that you can simulate function pointers < 1584109379 496344 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584109454 800273 :int-e!~noone@int-e.eu PRIVMSG #esoteric :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. < 1584109466 775778 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Because it's highly intuitive.) < 1584109488 254504 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :yeah < 1584109523 434554 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584109563 535260 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :of course it's more likely multiple steps of one machine < 1584110781 973867 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Is #coq a moderated channel? I tried to ask a question there but got "Cannot send to nick/channel". < 1584110798 894734 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :you can try writing /mode #coq while you're there < 1584110810 158068 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :afaict it's mode is [+cnt] and afaict that does not mean it's moderated < 1584110810 473803 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :that should give you full information on what channel modes might prevent you sending there < 1584110844 352144 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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) < 1584110872 899639 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :cpressey: are you logged in to nickserv? a lot of channels ban everyone who isn't logged in to nickserv < 1584110888 820012 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :int-e: Do you know anything about extraction in Coq? < 1584110892 616766 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :err, muted, not banned < 1584110898 504883 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :if you were banned you wouldn't be able to join it < 1584110910 58591 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: nothing beyond the term < 1584110965 240908 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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 < 1584110971 35600 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: Meaning I think I know what it is abstractly, but not how it's done. < 1584111081 513921 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :int-e: Well, it's this: Coq is guaranteed to terminate. Are the programs extracted from Coq also guaranteed to terminate? < 1584111091 906632 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I think it's "yes" < 1584111143 674677 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Ping timeout: 240 seconds < 1584111210 899159 :spruit11!~unknown@ip56522cc1.speed.planet.nl JOIN :#esoteric < 1584111238 680199 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1584111436 91924 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: I think so too (though you can mess up the setup) < 1584111815 907737 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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. < 1584111989 239247 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Uh, but there's a loophole there. < 1584111994 665698 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Namely, codata < 1584112152 735287 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(co)data Res a = Continue (Res a) | Return a < 1584112186 880630 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Whatever that is in Coq, I haven't ventured there. < 1584112460 393075 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection < 1584112535 212940 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Is that a good loophole or a bad loophole < 1584112672 872931 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Or, to put it another way... < 1584112707 291288 :int-e!~noone@int-e.eu PRIVMSG #esoteric :It's a good one? > 1584112736 567584 PRIVMSG #esoteric :14[[07Function x(y)14]]4 10 02https://esolangs.org/w/index.php?diff=70273&oldid=70269 5* 03Hakerh400 5* (+0) 10Fix category link < 1584112748 749787 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :My understanding of it is bad though < 1584112769 550711 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The corresponding function Res a -> a is still not total. < 1584112808 736623 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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? < 1584112809 737830 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The corrsponding notion to termination for codata is productivity: The outermost constructor is produced in finite time. < 1584112819 725765 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Yes. < 1584113022 9635 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :OK. < 1584113624 654219 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :cpressey: my Agda interpreters for TC languages had a cycle limit and got around the no-nonprovably-halting-programs restriction that way < 1584113645 509390 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :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 < 1584114121 133636 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :(and vice versa) < 1584114170 39597 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :makes sense < 1584114489 60071 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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. < 1584115393 724690 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584115683 57315 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584115683 546957 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :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 < 1584115703 674886 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Ping timeout: 240 seconds < 1584115793 508754 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :but even then I omit a lot of fiddly details that you'd have to expand on if you wanted a machine language proof < 1584116431 332926 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :wib_jonas: OK, thanks. < 1584116522 51243 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :and even there I'm lucky because (1) supports early function returns from inside loops, which simplifies the human-readable description a lot < 1584116836 818583 :MTGBusyBeaver42!c73b3502@199.59.53.2 JOIN :#esoteric < 1584116952 747357 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :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? < 1584116989 605262 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1584117084 931870 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :is that the dual of when nsiders are effected? < 1584117245 416455 :MTGBusyBeaver42!c73b3502@199.59.53.2 PRIVMSG #esoteric :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. < 1584117260 153145 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :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 < 1584117311 648640 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :wib_jonas: hmmm? < 1584117352 526625 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :arseniiv: sorry. stupid joke like the one about how cocoa is really just a < 1584117354 491054 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :`? cocoa < 1584117356 609090 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :A is a village in Norway. The BBC invented it by not understanding things on top of letters. < 1584117425 174724 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :wib_jonas: ah, “considers”. I thought it’s a special spelling of “insiders” but didn’t understand why < 1584117464 7619 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :though I don’t, still :D < 1584117480 254670 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :no, that one is about Darth Sidious < 1584117482 567741 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :I like co jokes but hadn’t got this one < 1584117490 333125 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :hm < 1584117894 269776 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :arseniiv: IIRC coeffects are a real area of research that's quite busy < 1584117901 371815 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I think I've met people who work on them < 1584117929 835394 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :they're the sort of thing that you use comonads to implement, just like you can use monads to implement effects < 1584117944 672501 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and normally correspond to some sort of resource that is consumed by a computation < 1584117957 451163 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :ais523: do you know an expository paper or something? < 1584117972 843779 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I was hoping there'd be a Wikipedia article but there isn't < 1584117976 411656 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :.oO(if coeffects is a busy area with lots of researchers, then the coronavirus spreads there, so the ronavirus... nah, it doesn't work) < 1584118004 731572 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :(yeah I thought about comonads and resources/contexts but inside one head in the early morning it’s not that fruitful) < 1584118110 234138 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :I also imagined what it would do with a call stack but the result was of a mixed usefulness too < 1584118332 677261 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1584118355 444170 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :arseniiv: try this: http://tomasp.net/blog/2014/why-coeffects-matter/ < 1584118368 37390 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :sorry for not answering earlier, I was reading it first to make sure that the author actually understood the subject, but he does < 1584118529 289201 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :(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) < 1584118539 602607 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :that said, the post does remind me a lot of a monad tutorial :-D < 1584118587 14271 :MTGBusyBeaver42!c73b3502@199.59.53.2 PRIVMSG #esoteric :"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 < 1584118601 365405 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's a running joke in #esoteric < 1584118602 853124 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :what if you link to the Typeclassopedia instead, since that's known to be a good book? https://wiki.haskell.org/Typeclassopedia#Comonad < 1584118630 361364 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :wib_jonas: that doesn't explain much about why you'd use them < 1584118642 859732 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :true, but it links to references about comonads < 1584118648 868417 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :presumably those are pre-vetted < 1584118687 670273 :MTGBusyBeaver42!c73b3502@199.59.53.2 PRIVMSG #esoteric :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 < 1584118779 395462 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :you have to be careful, if comedy is confounding constituents, then nstituents should nfound medy < 1584118790 144496 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :because the co- relationship reverses subject and object < 1584118813 636383 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's like a mathematical version of the "in soviet russia" jokes < 1584118829 926746 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :(does this make Soviet Russia an untry?) < 1584118837 373336 :MTGBusyBeaver42!c73b3502@199.59.53.2 PRIVMSG #esoteric :fair point < 1584118880 480655 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :it works well because "co" is like the thickest part of an English dictionary < 1584118928 93163 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 QUIT :Remote host closed the connection < 1584120058 491980 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :"co" jokes are one thing, cojokes are quite another. < 1584120064 588540 :cpressey!~cpressey@5.133.242.4 QUIT :Quit: A la prochaine. < 1584120162 268183 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1584120464 920573 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :ais523: :D < 1584121756 687221 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric : 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 < 1584121864 69053 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric : (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 < 1584122153 346892 :arseniiv!~arseniiv@94.41.9.97.dynamic.ufanet.ru PRIVMSG #esoteric :a cojoke is probably a thing several people say crying and an unsuspecting person nearby then feels witless < 1584123758 232258 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I think a cojoke is something you say in the hope that someone else will cheer you up < 1584123765 828639 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I'm not sure though < 1584123794 727331 :atslash!~atslash@46.188.0.82 JOIN :#esoteric < 1584124119 725152 :atslash!~atslash@46.188.0.82 QUIT :Ping timeout: 268 seconds < 1584124151 114688 :atslash!~atslash@static.231.107.9.5.clients.your-server.de JOIN :#esoteric < 1584124322 458094 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :Does any web browser include the command to pause/rewind/fast-forward animations? < 1584124342 991751 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I think it depends on the nature of the animations < 1584124366 946208 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :if they're based on a