00:27:57 [[Godencode]] https://esolangs.org/w/index.php?diff=84400&oldid=84395 * ResU * (+17) 00:46:39 [[Coeus]] https://esolangs.org/w/index.php?diff=84401&oldid=78485 * Kaveh Yousefi * (+150) Added a section Interpreters with a reference to my implementation and changed the category to Implemented. 01:09:36 -!- dbohdan has quit (Read error: Connection reset by peer). 01:10:13 -!- dbohdan has joined. 01:16:10 [[Truth-machine]] https://esolangs.org/w/index.php?diff=84402&oldid=84357 * Plasmath * (+2108) 01:17:09 -!- dbohdan has quit (Excess Flood). 01:17:22 -!- dbohdan has joined. 01:33:39 [[User talk:Ais523]] https://esolangs.org/w/index.php?diff=84403&oldid=83539 * Plasmath * (+400) /* Program too long to add into page */ new section 01:34:54 [[Language list]] M https://esolangs.org/w/index.php?diff=84404&oldid=84385 * Plasmath * (+16) Added [[Godencode]]. 01:35:15 -!- lukalot_ has quit (Remote host closed the connection). 01:41:59 -!- xkapastel has quit (Remote host closed the connection). 01:48:16 [[Godencode]] https://esolangs.org/w/index.php?diff=84405&oldid=84400 * Plasmath * (+87) Added an infinite loop. First really simple program. 01:48:43 [[Godencode]] M https://esolangs.org/w/index.php?diff=84406&oldid=84405 * Plasmath * (+1) Forgot the code formatting. 01:49:42 -!- xkapastel has joined. 02:03:58 Why do they use YCoCg rather than YCgCo? 02:10:17 (It seem to me that YCgCo is making a better prediction based on the valid range due to the value of the previous channels) 02:11:45 [[User talk:Plasmath]] N https://esolangs.org/w/index.php?oldid=84407 * Ais523 * (+1030) reply 02:14:30 [[User talk:Plasmath]] https://esolangs.org/w/index.php?diff=84408&oldid=84407 * Ais523 * (+269) what about linking to the language page? 02:41:10 [[User talk:Plasmath]] https://esolangs.org/w/index.php?diff=84409&oldid=84408 * Plasmath * (+124) 02:46:46 [[User talk:Plasmath]] https://esolangs.org/w/index.php?diff=84410&oldid=84409 * Plasmath * (+158) 03:13:54 -!- tromp has joined. 03:14:31 -!- tromp has quit (Client Quit). 03:24:21 zzo38: you mean like how you order the information in jpeg and such formats? how it would work better if you ordered the channels differently? I don't even know what order it has the channels in. I guess you'd have to test whether it yields a better compression, and of course that may depend on the progressive JPEG scheme. you would have to use an encoder that can take the YUV values directly rather 03:24:28 than RGB though, and I'm not sure what encoder can do that -- I mean ffmpeg can but its jpeg encoder is also terrible and not configurable so it's not a fair test, maybe libjpeg can but I don't know how 03:25:24 though the YUV space that JPEG uses isn't quite the same as YCoCg apparently 03:25:37 I'm confused by so many different linear transformations of color spaces 03:30:57 I guess you'll have to ask the HAM enthusiasts of esolangs 03:31:36 -!- Lord_of_Life_ has joined. 03:32:49 -!- Lord_of_Life has quit (Ping timeout: 265 seconds). 03:32:50 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 03:47:11 -!- oerjan has quit (Quit: Nite). 04:36:29 b_jonas: I don't mean JPEG, since I think JPEG doesn't take advantage of the order of the channels to make predictions and that stuff. But, it seems to me that the valid range of values for Cg can depend on Y, and the valid range of values for Co can depend on Cg and Y once they are known. 04:36:50 Actually I did make up a picture compression based on this, and it seems to work a bit better than PNG 04:37:27 (and, unlike PNG, does not require guessing things in order to improve the compression) 04:53:58 -!- tromp has joined. 04:55:06 -!- tromp has quit (Client Quit). 05:11:18 zzo38: oh yeah, it's Huffman compression after that linear transformation on blocks, you' 05:11:53 re right that it can't take advantage of that kind of thing. I guess I was thinking of PNG, where the deflate step *can* take advantage of correlation between channels 05:12:07 so JPEG was irrelevant 05:14:31 I should have known that, because I know how JPEG worked, but I didn't realize. oh well. 05:15:21 but still, if you think something like flipping the order of chroma channels can help, which I doubt, then you might want to experiment with that on more modern image/video compression formats, ones where it could matter 05:15:39 I doubt that just flipping two channels would help, but still 05:15:49 I'm not all that good about image compression 05:16:45 I had some ideas about them and thought about it enough to realize just how difficult the topic is 05:17:54 See the piccomp.c file (SHA-1 hash is c4e5438e358e174cde4b25ecd536d52f59beb702) in TeXnicard 05:19:51 basically I tried to think of how to design a good image compression algorithm, and I didn't find a way to get the properties that I want, anything I try would either be bad at compression or would be impossible to implement efficiently, and I have also experimented with existing video compression libraries and they're just too good 05:20:03 What properties do you think that you want? 05:20:24 it shouldn't stop me from thinking of course, but I haven't been able to think of a good enough design yet, so I want to think about it more before I can implement anything 05:23:06 zzo38: basically the problem is that decoding something variable width like Huffman is hard in a way that takes advantage of the SIMD capabilities of a CPU (or the same of a GPU). you can parallelize decompression and compression by handling individual large chunk of course, and all the other parts, as in color space transforms and DFT or other linear transforms and PNG-like prediction from previous 05:23:12 value and video compression's testing which neighboring block is the most similar or even estimating the motion delta more efficiently than trying every possible delta, those can be done in SIMD 05:23:40 but for the variable bit size huffman-like compression in the end (it doesn't necessarily need to be huffman, could be arithmetic coding) you have to iterate through individual values in series 05:23:53 I think what PNG does compressing the filter types together with the pixel data is a bad idea; it would be better to be separate 05:24:44 and if you want something that avoids that, better predicting how much to shift the input data or have a fixed width encoding, that is possible, but then you probably have to rearrange the output pixels in an unpredictable order which is even worse, or do some other intersting thing, 05:24:55 and I think it's probably possible to avoid this trap, but I couldn't yet think of a good way, 05:25:15 so I should read up if any existing algorithm does that and still manage to do not terrible compression 05:26:05 and also think about how it could be done 05:26:36 because that's what I'd like to see form an algorithm, at least for *decompression*, it could be slower for compression perhaps, though it's also worth to have other compression methods that are also fast to encode 05:29:56 there is some balance between slower compression as a price for slightly smaller encoded form while keeping the same quality and decompression time, and a more important tradeoff of slower compression and decompression and much larger encoded size for better quality, and good image/video encodings already offer both tradeoffs as a somewhat tunable parameter 05:30:45 though there is something odd here now that I think of it 05:30:45 wait 05:31:32 hmm no, nothing 06:15:50 [[Column]] M https://esolangs.org/w/index.php?diff=84411&oldid=84366 * Dominicentek * (-2) /* Truth Machine */ 08:07:39 -!- hendursa1 has joined. 08:10:34 -!- hendursaga has quit (Ping timeout: 252 seconds). 08:14:12 -!- tromp has joined. 08:15:49 -!- imode has quit (Ping timeout: 272 seconds). 08:30:38 [[Column]] M https://esolangs.org/w/index.php?diff=84412&oldid=84411 * Dominicentek * (+12) /* Truth Machine */ 08:48:52 -!- tech_exorcist has joined. 09:05:34 [[Column]] M https://esolangs.org/w/index.php?diff=84413&oldid=84412 * Dominicentek * (+17) /* Fizz Buzz */ 09:20:47 -!- sweatsuit has joined. 09:20:48 -!- sweatsuit has quit (K-Lined). 09:27:57 -!- dutch has quit (Quit: WeeChat 3.1). 09:30:44 I don't get it 09:31:30 this is function k7*x**7+k6*x**6+k5*x**5+k4*x**4+k3*x**3+k2*x**2+k1*x+k0 and this should be its derivative, right? k7*x**6+k6*x**5+k5*x**4+k4*x**3+k3*x**2+k2*x+k1 09:33:05 but the bottom line doesn't look like derivative of upper one https://i.imgur.com/Pljjzyq.png 09:33:24 it doesn't get above 0 in the middle 09:33:45 -!- Sgeo has quit (Read error: Connection reset by peer). 09:34:10 k0..k7 = [86.37483858758613, -4.3258409149187855, 0.13119312931328275, -0.0022258811427750126, 2.156489053721058e-05, -1.1221319014114155e-07, 2.8163872939164175e-10, -2.530165279150212e-13] 09:36:11 oh no, forgot to multiply by 7, 6, ... 10:00:21 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 10:05:11 b_jonas I've got another example https://i.imgur.com/BlsjZrI.png -- problem here is that they use several different captcha generators and this one doesn't rotate but skews the letters 10:08:21 -!- tromp has joined. 10:12:02 nakilon: yeah, that can help with the captchas 10:12:38 uhm, the derivative of k7*x^7 isn't k7*x^6 but 7*k7^6 10:13:08 same issue with each other part of the sum except the last because x^1 will get a factor of 1 10:13:34 also, bit surprise, captchas are made to be hard to read 10:15:34 [[Special:Log/move]] move * Ultlang * moved [[Delta Salein Ao]] to [[Delta Salein ]]: the actual name 10:15:52 this one is skewed too, not rotated https://i.imgur.com/dVMMdkT.png 10:16:22 [[Delta Salein ]] M https://esolangs.org/w/index.php?diff=84416&oldid=84414 * Ultlang * (+5) 10:17:30 gotta somehow differentiate them to switch the way of chosing the closest line dot -- using "min x1-x2" instead of "min hypot x1-x2, y1-y2" 10:18:46 or just try both ways until I see which one makes better results on the OCR stage 10:24:32 -!- riv has quit (Quit: Leaving). 10:27:26 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 10:28:45 -!- tromp has joined. 10:35:25 [[What's the dog doin?]] https://esolangs.org/w/index.php?diff=84417&oldid=84389 * GreenThePear * (+827) Revamped the commands, all [x] input will be used as an index + fixing some mistakes 10:53:05 -!- riv has joined. 10:55:37 -!- lambdabot has quit (Quit: brb). 10:56:48 -!- lambdabot has joined. 11:18:24 myname: yes, and nakilon corrected himself about the derivatives a few lines later, and this time I wasn't hasty enough to reply before reading that 11:22:42 [[Column]] https://esolangs.org/w/index.php?diff=84418&oldid=84413 * Dominicentek * (+137) 11:26:05 -!- arseniiv has joined. 11:29:06 [[NumberPankackes]] N https://esolangs.org/w/index.php?oldid=84419 * TinyGuy32 * (+1110) Created page with "==NumberPankackes== NumberPankackes is a stack-based esoteric programing language what a stck is: https://esolangs.org/wiki/Stack ==Commands== 1X: pushes X to the st..." 11:29:44 [[User:TinyGuy32]] https://esolangs.org/w/index.php?diff=84420&oldid=84394 * TinyGuy32 * (-829) Blanked the page 11:30:08 is there a tool that lets me easily cut a picture from an image out/remove background 11:30:17 GIMPs 'intelligent scissors' aren't that great for it 11:30:48 I feel like with modern stuff.. it should be possible to just draw a rough outline and get a perfect cutout 11:34:54 [[Language list]] https://esolangs.org/w/index.php?diff=84421&oldid=84404 * TinyGuy32 * (+44) 11:39:10 [[NumberPankackes]] https://esolangs.org/w/index.php?diff=84422&oldid=84419 * TinyGuy32 * (+2) 11:39:23 riv: it really depends on the image, but try ones that require both a positive and negative sample, that is, points marked strictly inside and strictly outside the object, rather then a rough outline. try (1) GIMP's new foreground select tool, and (2) the GMIC QT gimp plugin's colorizer tools, which are intended to color black and white photos and black and white line art respectively (that's two 11:39:29 separate tools) based on another image with sample points of color in the objects, but you can ask them for the masks of which colors go exactly where and use that to get a selection mask that you use for something other than selecting an object 11:39:47 they aren't perfect, but I think they work better than GIMP intelligent scissors 11:40:19 http://gmic.eu/ to download the G'MIC QT Gimp plugin on windows; install from distro on debian 11:40:49 note that Gimp has a decent ABI so the same plugin compiled once can be reused for different minor versions of GIMP 11:41:56 which means you can install G'MIC QT from debian and it will work for a newer version of Gimp that you install from source, as I learned 11:42:21 that was back when Gimp 2 wasn't yet in debian and I really really wanted Gimp 2 so I installed from source 11:42:33 now Gimp 2 is in debian stable, and I love that 11:44:29 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 11:45:31 -!- tromp has joined. 12:01:49 -!- tech_exorcist has quit (Quit: tech_exorcist). 12:02:44 -!- tech_exorcist has joined. 12:08:07 now the correctness is limited by how well I apply dilations to make skeletonization go well https://i.imgur.com/ckuQeDp.png 12:08:50 -!- freon has joined. 12:09:05 -!- freon has quit (Write error: Broken pipe). 12:09:11 riv there was online service 12:09:14 nakilon: yes, and that part is hard 12:09:42 this or maybe it's a clone https://www.remove.bg/ru 12:11:59 -!- freon has joined. 12:14:22 https://i.imgur.com/Ux0aQTH.png 12:15:12 thanks 12:16:18 I actually could apply the whole process twice but pixels are rotting 12:16:43 are you trying to teach bot to cheat at captchas? 12:17:21 yeah, script that would send me new vacancies from local job search site 12:17:44 note that there was a fun trick at some point where captchas consisted in two words; the first word was meant to tell whether the user was human or not; the second word was much easier to decipher and actually came from scanned books 12:18:06 and in two months they had digitalized an entire library without optical recognition software 12:18:24 yeah I guess that was recaptcha 12:18:43 now they are teaching self-driving cars 12:21:49 nakilon: and Google Maps to read house numbers from blurred photos, surely you noticed those captchas 12:22:40 blurred or just photos taken from the distance by self-driven cars to teach them navigate? 12:23:30 I don't remember house numbers 12:24:30 nakilon: not deliberately blurred, just taken from a distance either by the same cars that Google Maps uses to make street view, or more likely by the airplane cameras that they used to make the incredibly high resolution "satellite view" from five different camera directions that isn't actually from satellites 12:25:02 didn't know about airplanes 12:25:14 as in, satellite view _is_ from satellites in most areas of the map, but in those places it's also low resolution and only has one camera direction 12:25:39 so in more populated places that most people view on the map, they used airplane cameras, which can give much higher quality 12:25:46 that would explain how they made all the trees and buildings 3d in there 12:25:51 just because they're closer 12:26:33 nakilon: well that's only part of it, part of the 3D buildings are modeled from their street view photos and from random location-tagged photos from the internet corellated by really clever software, the same way as we model 3d objects from 2d photos except they do it better 12:27:27 and of course some of this is just speculation because they don't tell all the details about how they got every image, they only tell when that was a requirement to buy a license of pictures that other people made not specifically for them 12:40:34 [[NumberPankackes]] M https://esolangs.org/w/index.php?diff=84423&oldid=84422 * PythonshellDebugwindow * (-45) Link to page directly 12:41:10 [[Language list]] M https://esolangs.org/w/index.php?diff=84424&oldid=84421 * PythonshellDebugwindow * (-22) /* Non-alphabetic */ Remove duplicate 12:42:19 at first they were croudsourcing 12:42:38 it was called Warehouse 3d and people could make models of things in Sketchup 12:42:54 Sketchup was freeware and a great fun 12:44:02 [[What Mains Numbers?]] M https://esolangs.org/w/index.php?diff=84425&oldid=64983 * PythonshellDebugwindow * (+35) /* Implementations */ Cat 12:44:08 so I made models for 2-3 buildings in my town, uploaded and they were in Google Earth since then; but now I can't even find them on their website, idk 12:44:41 you could create collections and become moderator of them, similar to how people build wikipedia 12:45:21 [[User:Soundandfury/ECLAIR]] M https://esolangs.org/w/index.php?diff=84426&oldid=33340 * PythonshellDebugwindow * (+13) /* Implementation */ Deadlink 12:46:48 -!- leah2 has quit (Remote host closed the connection). 12:47:12 -!- leah2 has joined. 13:05:48 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 13:08:00 -!- tromp has joined. 13:13:46 -!- hendursa1 has quit (Quit: hendursa1). 13:15:13 -!- hendursaga has joined. 13:18:52 [[Column]] M https://esolangs.org/w/index.php?diff=84427&oldid=84418 * Dominicentek * (-42) /* Interpreter */ 13:19:17 [[FolderCode]] M https://esolangs.org/w/index.php?diff=84428&oldid=84361 * Dominicentek * (-41) /* Development Kit */ 13:20:50 [[User:Plasmath]] https://esolangs.org/w/index.php?diff=84429&oldid=84393 * Plasmath * (-66) Added [[Godencode]]. 13:29:50 [[Hello world program in esoteric languages]] M https://esolangs.org/w/index.php?diff=84430&oldid=83967 * Plasmath * (+20) I'm trying to add Godencode, but it hasn't been letting me. Making it a 2-step process might work? 13:34:24 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 13:35:38 [[Hello world program in esoteric languages]] https://esolangs.org/w/index.php?diff=84431&oldid=84430 * Plasmath * (+47) 13:42:32 -!- FreeFull has joined. 13:47:10 -!- FreeFull has quit (Client Quit). 13:47:55 -!- tiggilyboo has joined. 14:03:45 [[Cheese]] M https://esolangs.org/w/index.php?diff=84432&oldid=83055 * Sanscicondos * (+49) 14:04:09 [[Cheese]] https://esolangs.org/w/index.php?diff=84433&oldid=84432 * Sanscicondos * (+13) Added Version 1.3.5 to Github 14:11:01 -!- tromp has joined. 14:35:20 -!- tiggilyboo has quit (Quit: tiggilyboo). 14:48:52 [[Special:Log/newusers]] create * Kermek * New user account 14:55:02 [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=84434&oldid=84388 * Kermek * (+407) 14:55:53 [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=84435&oldid=84434 * Kermek * (-76) 14:56:22 [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=84436&oldid=84435 * Kermek * (-6) 15:49:30 made the second pass https://i.imgur.com/Jq2LUCj.png 15:57:49 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 15:59:01 [[Dick]] M https://esolangs.org/w/index.php?diff=84437&oldid=79507 * Cybertelx * (+15) Added LongDick language 15:59:22 -!- tromp has joined. 16:12:05 -!- arseniiv has quit (Ping timeout: 272 seconds). 16:13:27 [[LongDick]] M https://esolangs.org/w/index.php?diff=84438&oldid=83816 * Cybertelx * (+19) link me 16:18:58 -!- Sgeo has joined. 16:30:37 -!- craigo has joined. 16:33:12 [[VBF]] N https://esolangs.org/w/index.php?oldid=84439 * VilgotanL * (+2464) created the page 16:34:20 [[VBF]] M https://esolangs.org/w/index.php?diff=84440&oldid=84439 * VilgotanL * (+15) add "and transpiler" to implementation link 16:40:16 [[For The Worthy]] N https://esolangs.org/w/index.php?oldid=84441 * Kermek * (+5730) Created page with "'''For The Worthy''' is an esolang witch only interprets the '1' and '0' characters, thus enabling programmers to reach their final hackerman form. ==Language Overview== ===In..." 16:41:59 Greetings all. I have a quick question. Is the sort of completeness that Godel talks about equivalent to TC under the Curry-Howard correspondence? 16:44:22 [[Language list]] M https://esolangs.org/w/index.php?diff=84442&oldid=84424 * Kermek * (+21) 16:45:02 And, if so, is it fair to say that one way to describe the split between computer science and mathematics is in how each field responds to Godel's incompleteness theorem? i.e. mathematicians err on the side of consistency while computer scientists err on the side of completeness? 16:45:33 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 16:49:11 Godels completeness theorem states that in a first order logic, if a formula is true in all models it is provable 16:49:20 -!- arseniiv has joined. 16:50:05 Godels incompleteness theorem states that arithmetic (and extensions) contain statements that are neither provable or disprovable 16:51:37 the halting problem gives an explicit example of a problem that cannot be solved by a turing machine 16:51:53 [[User:VilgotanL]] M https://esolangs.org/w/index.php?diff=84443&oldid=83804 * VilgotanL * (+10) add vbf to language list 16:52:14 Right, and under the Curry-Howard correspondence, a type system is in some sense equivalent to a Hilbert style deductive system in logic. If a no non-normalizing expression is well typed, then the corresponding logic is consistent, right? 16:52:47 Curry-Howard correspondence equates proofs and programs 16:53:25 Yes, and formulas as type definitions, among other things, right? 16:53:34 generally consistency of a typed lambda calculus based logic is proven by showing (A) strong normalization (B) False does not have a normal form - this implies consistency as inconsistency would let you prove False 16:53:55 orbitaldecay72: If you want the short answer, then yes, by Lawvere's fixed-point theorem: http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf 16:54:26 Yeah, looking for the short answer to test my intuition. Thanks for the link. 16:54:29 Appreciate you both. 16:54:30 This is a very abstract category-theoretic statement. It can be specialized to get Gödel's Incompleteness, and also to get Turing's Halting. 16:55:03 Looks like I need to learn category theory :) 16:55:46 The completeness that Godel talks about is not the same as turing completeness 16:56:04 the fact that there are problems a turing machine can't solve is a type of incompleteness 16:56:23 I think that there were many different reactions to our discovery of computability theory. I don't think it's reasonable to cleave computer science from maths; computer science is the study of algorithms and data structures, which is a special case of studying abstraca. 16:56:28 turing completeness <- may be better referred to as turing equivalence 16:57:17 Oh, I misread the original question, sorry. 16:57:54 Gödel's Completeness is quite different from Gödel's Incompleteness! I don't know how the former relates to Turing's work, sorry. 16:58:13 Okay, so in the Curry-Howard sense the halting problem corresponds to some theorem that can neither be proven nor disproven? 16:58:16 Np, thanks Corbin 16:58:59 Sorry for my vagueness 16:59:06 Still learning 16:59:06 https://www.andrew.cmu.edu/user/avigad/Teaching/halting.pdf there is a direct proof here of godels first incompleteness theorem using the halting problem as the key element, rather than godels original proof which used a self referential formula as the key element 16:59:25 riv: beautiful, this is exactly what I was looking for 16:59:26 thanks 16:59:32 > in the Curry-Howard sense the halting problem corresponds to some theorem that can neither be proven nor disproven? 16:59:34 :1:1: error: parse error on input ‘in’ 16:59:45 [[Language list]] M https://esolangs.org/w/index.php?diff=84444&oldid=84442 * VilgotanL * (+67) add my newest 5 languages 16:59:49 no, turing machines aren't a typed lambda calculi - so you cannot apply Curry-Howard here 17:00:37 yeah, I get that, but typed lambda calculi are of course in some sense equivalent to turing machines, just wondering if it makes sense theoretically 17:00:54 a typed lambda calculus must not be turing equivalent 17:00:57 or rather, lambda calculi in general are in some sense equivalent to turing machines 17:00:59 yeah 17:01:10 the strong normalization condition says that every algorithm terminates in a finite number of steps 17:01:11 I understand that simply typed lambda calculus is not tc 17:01:19 right 17:01:23 neither is dependently typed, like Coq for example 17:01:37 this is what enables a consistency proof to be done 17:01:42 riv: Note that Curry-Howard-Lambek still applies, and typed lambda calculi each give a Cartesian closed category for a model, where we can try to apply Lawvere's fixed-point theorem. 17:02:43 But yeah, generally when it *does* apply, there's enough data for a Turing category, where there's an object representing all of the untyped terms. 17:02:58 -!- tromp has joined. 17:03:31 the untyped lambda calculus is turing equivalent, but it doesn't have types that you can interpret as logical formulae - so no Curry-Howard bridge there 17:03:35 There's nice tables at https://ncatlab.org/nlab/show/computational+trilogy which are recently redone and looking nice. 17:04:57 Okay, so, another related question, when Godel talks about incompleteness, is this in some sense equivalent to sub tc? Re: what Corbin was mentioning. 17:05:27 Turing showed that there's a computer program which, if given a program that could solve Halting, creates a contradiction. 17:06:34 That is my understanding of how the halting problem is proven to be uncomputable 17:06:37 Let "Truth" be the question of whether a formula in arithmetic is true. Gödel showed that there's a proof which, if given a proof that could solve Truth, creates a contradiction. 17:07:09 (Technically Tarski showed this, and similarly we can't mention Turing without the far-more-useful Rice's Theorem; there's too many people to remember~) 17:07:30 Of course, we all stand on the shoulders of history :) 17:08:50 What is the connection between Tarski's undefinability of truth and Godels incompleteness? 17:09:10 > The undefinability theorem is conventionally attributed to Alfred Tarski. Gödel also discovered the undefinability theorem in 1930, while proving his incompleteness theorems published in 1931, and well before the 1933 publication of Tarski's work 17:09:11 :1:124: error: parse error on input ‘in’ 17:09:13 oh that is funny I didn't know that 17:12:06 it doesn't seem to imply godels incompleteness 17:15:30 BTW, https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf is quite good, for anybody wanting to understand all that Gödelian stuff. I had to take it slow, because the details are extremely nuanced. 17:16:30 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 17:17:19 -!- craigo has quit (Quit: Leaving). 17:18:15 If you just want to see how category theorists might apply Lawvere's work to simplify thinking about all of this, then https://arxiv.org/pdf/math/0305282.pdf is so good. 17:27:56 -!- tromp has joined. 17:29:17 [[What's the dog doin?]] https://esolangs.org/w/index.php?diff=84445&oldid=84417 * GreenThePear * (+47) Clarifications and fixes about the number system, plus other polishing 17:31:35 https://arxiv.org/pdf/math/0305282.pdf <- this is really cool! 17:35:26 [[Godencode]] M https://esolangs.org/w/index.php?diff=84446&oldid=84406 * Plasmath * (+124) Forgot one small part of if command. 17:36:21 The Lob's Paradox one is a bit jarring 17:42:31 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 17:54:36 -!- tromp has joined. 17:55:33 [[Godencode]] M https://esolangs.org/w/index.php?diff=84447&oldid=84446 * Plasmath * (-3) Made another mistake in the description. 18:05:16 [[Godencode]] M https://esolangs.org/w/index.php?diff=84448&oldid=84447 * Plasmath * (+16) I think I finally worded this in a good way. 18:11:32 Corbin: I'm thinking more about my comments on the distinction between computer science and mathematics. Most of my experience is as a software engineer. My education is in math, but I don't know a lot about proof theory. The thing I noticed is that, AFAIK, a program which does not halt corresponds to a proof of a contradiction in mathematics by 18:11:33 Curry-Howard. In programming, we use languages that permit infinite loops, but in mathematics we don't use axiom systems that allow proving contradictions. 18:12:02 On the surface, this makes sense because in classical logic if we permit a contradiction as a theorem, then everything entails. But in paraconsistent logics this is not true. 18:12:23 As paraconsistent logics explicitly reject the principle of explosion. 18:13:32 So, why don't mathematicians use paraconsistent logics to permit a small class of contradictions as theorems but software engineers use languages that permit infinite loops? 18:13:49 [[Godencode]] https://esolangs.org/w/index.php?diff=84449&oldid=84448 * Plasmath * (+31) Forgot yet another thing about this command. This is it though. I've made sure. 18:13:49 Does this make sense, or am I way off? 18:16:23 I recognize that what I'm proposing is a totally reformulation of how math is done, but just wondering in the spirit of intellectual inquiry 18:17:29 Sure, and the philosophy of why logic is even a good idea is historically important. Frege and Quine had strong but inscrutable opinions on this sort of thing. 18:18:54 forbidding infinite loops would need you to solve the halting problem, doesn't it? 18:18:55 [[Meta Memes]] M https://esolangs.org/w/index.php?diff=84450&oldid=72253 * Caenbe * (+9) Stubbify 18:19:02 Okay, glad I'm making sense. I recently learned about paraconsistent logics and dialetheism and immediately sensed a correlation between what those philosophies are advocating and what I do as a software engineer. 18:19:05 doesn't sound like an easy task for me 18:19:16 myname: nah, just make your language sub turing 18:19:25 There is an old question: Shouldn't contradictions be relevant to the proofs which use them? If I prove that the sky is simultaneously blue and not-blue, does that make 1=2? If so, *how*? 18:19:39 [[Godencode]] https://esolangs.org/w/index.php?diff=84451&oldid=84449 * Plasmath * (+0) My documentation was hard to read. 18:19:40 great, have a language that probably cannot do the task you are trying to solve 18:20:30 Ah, sure. Note that a proper dialethist cannot refute a trivialist, who claims that all things are true. In particular, a dialethist cannot prove to them that anything is false; the law of non-contradiction is a missing logical lever they'd need. 18:20:54 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 18:21:23 Corbin: Yeah, of course. There are definitely philosophical issues with dialetheism too, I just noticed that philosophically it was closer to what I was doing than classic logic was. 18:21:24 myname: Most GPU programs are not Turing-complete. Instead, a Turing-complete CPU program repeatedly takes bounded steps by submitting bounded programs to the GPU. 18:22:09 sure, you can have arbitrary many sub-tc sub-tasks, but you want to have a tc system at some point or another 18:22:12 i.e. by using a language that allows for infinite loops I'm implicity rejecting non-contradiction 18:22:34 orbitaldecay72: I'm looking for a good reference, but a simple slogan is "there's no type of non-halting programs", along myname's lines. This means that it's not possible to use Curry-Howard to try to construct a family of usable contraditions. 18:23:35 also, at least in terms of semantics, an infinite loop is considered to have no semantical meaning. it's just one of the points where theory and practice diverge 18:23:36 In general, computers are constructive and effective, so while we don't have LEM or Choice, we do still have intuitionistic type theory, which is plenty powerful. 18:23:37 this is where I don't know enough about formal type theory to recognize what is a limitation of classical logic, and what is a limitation of type theory 18:23:47 imperative programming makes things hard 18:24:20 orbitaldecay72: Lucky 10000: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf 18:25:46 Corbin: thanks! 18:26:20 Ha, don't thank me yet. It took me a while to personally overcome old beliefs about maths and accept topos theory as a reasonable way to get things done. 18:27:03 My thinking is this. We can definitely construct a Hilbert style axiom system that allows us to prove a contradiction (we have to try hard to avoid this). If type systems are basically equivalent to these, then why can't we construct a type system in which a non-normalizing term is well typed? 18:27:12 Corbin: I'm always trying to overcome old beliefs :) 18:28:01 Again, I'm way out of my depth here. Just trying to develop some sort of intuition for the topic. 18:29:13 No worries. The answer I'd choose to keep going with Curry-Howard-Lambek, and do some category theory. We usually say that proofs of contradiction are rare because they can be shown to be categorically equivalent. 18:30:06 Categorically, an arrow into the initial object can only come from another initial object, and they're isomorphic. Logically, a proof of contradiction can only come from another contradiction, and they're equivalent. 18:30:17 Cool. I'll follow up with the category theory. Whenever I start barking about these questions I almost universally hear, "See category theory". Unfortunately I haven't done that yet, so I suppose I should! 18:30:42 -!- tromp has joined. 18:30:44 (Constructively, recally that a proof of contradiction ~P is literally something like "P -> false". Being able to logically entail falsity is the ur-contradiction.) 18:31:16 Corbin: But doesn't this all presuppose classical logic? i.e. what if we are using a logic in which contradiction doesn't entail everything? 18:31:26 Or am I missing the point? 18:31:54 Category theory's just so much neater for logic. Like, take *any* formal logic with rewrite rules. There's a category whose objects are equivalence classes of terms, and whose arrows embody the rewrite rules. 18:32:07 [[User:GreenThePear]] N https://esolangs.org/w/index.php?oldid=84452 * GreenThePear * (+702) Created 18:32:16 Got it. Alright, next stop category theory :) 18:32:23 Thanks so much for your help. I really appreciate it. 18:33:35 This all presupposes some constructive logic, but not classical logic. That's the key change in POV. And yes, it's possible to build interesting paraconsistent models, and also to require relevance for contradictions, but we don't necessarily know how to implement those in computers. 18:34:03 No worries. Sorry for dumping so much information onto you; hopefully it makes a little sense. Bauer's paper is really eye-opening on its own. 18:38:05 The information is great. I come here whenever I have a question that I'm having trouble answering because invariably I get a ton of information dumped on me haha 18:44:41 -!- oerjan has joined. 18:44:50 if categories are great why aren't there 2-categories? 18:46:00 riv: there are 18:47:36 https://golem.ph.utexas.edu/category/ (note: i'm not really a follower but i've heard about it) 18:47:53 :O 18:48:15 [[What's the dog doin?]] https://esolangs.org/w/index.php?diff=84453&oldid=84445 * GreenThePear * (-4) /* Examples */ 18:50:10 [[Python is Magic]] N https://esolangs.org/w/index.php?oldid=84454 * Gilbert189 * (+6954) Created page with "Python is Magic is a very restricted version of Python 3. On Python is Magic, only magic functions can be used. ==Warm-up== This is a valid Python is Magic code: __name__.__..." 18:50:24 https://en.wikipedia.org/wiki/Higher_category_theory might be more elucidating. (i haven't read that either.) 18:50:35 If cats are so great why aren't there 2-cats? 18:50:52 i was about to mention shachaf, i think he knows a lot more about it than i 18:51:18 if you can keep him from doing feline puns 18:51:41 [[User:Gilbert189]] https://esolangs.org/w/index.php?diff=84455&oldid=81403 * Gilbert189 * (-61) 18:51:42 https://www.reddit.com/r/confusing_perspective/comments/c95247/siamese_twins_cats/ here is a 2-cat 18:58:03 As a warmup, my housecat was yowling all last night. We got a little cat opera'd. 18:58:35 I still like "sets are 0-categories"; all of the structure of set theory is like a "decategorified" version of category theory. 19:00:57 Remember, booleans are just -1-categories. 19:01:41 O_O 19:01:46 is this true? 19:02:26 * oerjan wonders too 19:02:29 The "just" bit? 19:03:00 See https://ncatlab.org/nlab/show/negative+thinking 19:03:05 one conversation about image processing and one about formal logic. I don't contribute much today, but I'm glad the channel is back to its old weird self 19:03:18 it slightly reminds me that certain definitions of dimension consider the empty set -1-dimensional 19:03:50 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 19:04:16 Which definitions? 19:05:02 i'd have to look that up 19:06:31 https://en.wikipedia.org/wiki/Dimension#Topological_spaces starts with the lebesgue covering dimension which is an example 19:08:55 Aha. 19:09:48 b_jonas, thanks! 19:10:02 seems to be true for the inductive ones too 19:52:57 [[Talk:Emoji-gramming]] https://esolangs.org/w/index.php?diff=84456&oldid=83822 * Qwertyu63 * (+563) /* Sign checking */ 19:52:58 -!- sech1ptheythem[m has joined. 19:58:59 and the weird thing is, half of the nicks I don't even recognize from earlier, and I wonder if people just took the opportunity at the network switch to choose new nicks and I'm so stupid as to not recognize them after that, but that probably isn't the case 19:59:52 this channel does somehow indeed manage to pull in new weird people, even though I have no idea how they find their way here because we don't advertise ourselves very much and I find it hard to find my way into these kinds of communities 20:00:17 also I have all sorts of personal problems and sometimes you help but sometimes you cause me to stay up at night when I really shoulnd't, not that I'm blaming you, just saying 20:00:48 and the sad part is when that happens and I know that the other people who I'm talking to are Europeans and have a messed up sleep cycle hurting them too 20:00:55 -!- imode has joined. 20:01:20 the "booleans are just -1-categories" thing sounds somehow wrong though 20:01:48 or at least not true in the literal sense but perhaps there's some interesting enough analogy there that might work even if not in the literal sense 20:01:56 b_jonas, i used to be rain1 20:02:04 oh! 20:02:14 that explains part of it 20:02:25 and I knwo that moony renamed himself to, um, let me consult NAMES 20:03:19 b_jonas: i know at least keegan took that opportunity too 20:04:10 and perhaps some old people who left #esoteric for years but stayed on freenode, they took this oppurtunity to just CHECK on which old channels move there because they wanted to know just in case, and joined, and got stuck 20:04:19 because that's certainly something I'd do with other channels 20:04:51 anyway, moony took a short nick and I think I'll recognize him if he returns under that 20:05:00 I had to change my nickname to velik 20:05:08 and rename bot to nakilon 20:05:28 what? "had to" but renamed the bot to the old name? 20:05:58 I just realised that I had to 20:05:58 (well he's called "moon" now, but some people switch between nicks) 20:06:03 ah, that thing 20:06:04 to confuse b_jonas 20:06:32 yeah, that makes more sense even though I never felt the need, perhaps because I feel lucky for choosing b_jonas because it's a better name than I knew when I came up with it 20:06:38 i thought moon had always been switching nicks 20:06:45 I still don't know who's the pythondebugshell 20:06:46 oerjan: yeah 20:06:49 but usualy not very far 20:06:56 that's why I recognize him more easily 20:07:18 I still don't know who Corbin is, and of course sometimes wonder about people who I do recall but don't seem to come in anymore 20:07:44 although... there is a certain person who used to come in and I think used to ask about formal logic... I wonder 20:07:47 i know who Corbin is :> 20:08:19 no, probably no, because I think they're from another continent 20:08:27 * oerjan looks quizzically at Corbin 20:08:29 orbitaldecay72 is the one who had that amazing stuff about bitfuck right? 20:08:43 "I have all sorts of personal problems" -- heh, I'm a meter away from losing a flat and being kicked out of the country, and it makes me have bad dreams every night now 20:08:57 omg that sounds horrible and stressful D: 20:09:05 it does, yes 20:10:31 ouch 20:10:50 also, don't take this the wrong way, but hearing that from other people also makes it seem like this is back to good old #esoteric, because they're willing to share more than I do 20:11:09 about their problems, that is, not that I'm too careful about letting private details on 20:14:39 and I think that one terrible time when I was in a psychiatric hospital in 2018, the one I don't talk about often, part of what helped me shrug some of it off (besides my parents' care and being lucky about which doctor happened to do urgent care that night) was that I recalled that at least two different people on #esoteric told me earlier about when they were in psychiatric hospital, and I wasn't 20:14:45 thinking they were in great state, but they survived being in a hospital, one even for an extended time and IRCing from there, and didn't seem to be completely broken even months after, 20:15:05 plus similar stories from other weird parts of the internet 20:15:44 although it also worked because at least I did learn what I really should pay attention to in order to not get back there again 20:16:35 I just rarely feel stupid enough to discuss it in logged and googleable parts of the internet, especially as I know my nick isn't all that secret 20:18:01 and it would have been wiser to use a disposable alternate nick, if not now, at least that one time when I posted about it to a forum 20:19:35 woah, there are at least three people here who were in psychiatric hospitals? 20:20:27 I do miss some of the people who used to come here 20:22:14 I would probably not mind to get stuck in anywhere as long as there are some family members or friends to take care of your home, bills, hypothetical cat, etc. 20:22:31 lol, hypothetical cat 20:27:09 -!- tromp has joined. 20:31:59 nakilon: yes 20:32:14 at least if you count people who used to be here at some point but might not visit now 20:34:04 I wasn't *stuck*. it was a short time, I knew I'd get out soon, that's what the doctor said to me and she was right, and once she even allowed me to temporarily leave for a few hours in what she said was against the hospital's rules (not that I have illusions about those rules consistently being kept) because my family promised to bring me back 20:34:36 it's the at least one other user, the one who IRCed from the hospital, regularly, who was stuck 20:35:30 I don't pretend that I'm not stuck with a psychiatric condition that I'd have to be careful with for my whole life even if I managed to get my life mostly normal, but I was not stuck in the hospital 20:59:01 also hi future boss, who will probably find this months or years from now when searching for my name, I know you're listening and want to find out what I'm hiding by looking on the internet and asking previous employers' opinions, and you're going to pay me less money if you don't just reject me completely, but I think I wouldn't want to work in a company that has managers less diligent than that, I 20:59:07 couldn't trust that they could keep themselves in the business 21:04:37 -!- sech1ptheythem[m has quit (Remote host closed the connection). 21:04:39 -!- jryans has quit (Read error: Connection reset by peer). 21:05:54 -!- jryans has joined. 21:06:31 -!- dbohdan has quit (Read error: Connection reset by peer). 21:06:36 -!- arseniiv has quit (Ping timeout: 245 seconds). 21:06:41 -!- riv has quit (Read error: Connection reset by peer). 21:06:41 -!- arseniiv_ has joined. 21:06:51 -!- dbohdan has joined. 21:07:22 -!- citrons has quit (Ping timeout: 252 seconds). 21:08:11 -!- citrons has joined. 21:08:44 -!- Trieste_ has joined. 21:09:05 -!- moon5 has joined. 21:09:48 -!- moon has quit (Killed (copper.libera.chat (Nickname regained by services))). 21:09:48 -!- moon5 has changed nick to moon. 21:12:24 -!- sech1ptheythem[m has joined. 21:12:25 -!- int-e_ has joined. 21:12:49 -!- Trieste has quit (Quit: Be well!). 21:14:46 -!- zegalch has quit (Quit: Ping timeout (120 seconds)). 21:14:47 -!- int-e has quit (Ping timeout: 264 seconds). 21:14:47 -!- HackEso has quit (Ping timeout: 264 seconds). 21:14:58 -!- Sgeo_ has joined. 21:15:11 -!- riv has joined. 21:15:53 -!- zegalch has joined. 21:17:44 -!- moon2 has joined. 21:18:20 -!- moon has quit (Killed (iridium.libera.chat (Nickname regained by services))). 21:18:20 -!- moon2 has changed nick to moon. 21:19:09 -!- Trieste has joined. 21:21:28 -!- citrons_ has joined. 21:22:04 -!- ski has quit (Ping timeout: 265 seconds). 21:22:04 -!- integral has quit (Ping timeout: 265 seconds). 21:22:23 -!- ski has joined. 21:22:47 -!- imode has changed nick to FuckAndrewLee. 21:23:02 -!- Lord_of_Life_ has joined. 21:23:18 -!- perlbot_ has joined. 21:23:34 -!- integral has joined. 21:24:51 -!- perlbot has quit (Ping timeout: 265 seconds). 21:24:51 -!- yuu has quit (Ping timeout: 265 seconds). 21:24:53 -!- Trieste_ has quit (*.net *.split). 21:24:53 -!- citrons has quit (*.net *.split). 21:24:54 -!- Sgeo has quit (*.net *.split). 21:24:54 -!- Lord_of_Life has quit (*.net *.split). 21:24:54 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 21:25:03 -!- perlbot_ has changed nick to perlbot. 21:25:32 -!- lifthrasiir has quit (Read error: Connection reset by peer). 21:25:49 -!- V has quit (Ping timeout: 265 seconds). 21:26:28 -!- V has joined. 21:26:40 -!- lifthrasiir has joined. 21:27:01 -!- yuu has joined. 21:27:38 -!- HackEso has joined. 21:27:52 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 21:28:29 Happy pigeon appreciation day! 21:32:07 -!- FuckAndrewLee has changed nick to rusted-root. 21:35:39 Does anyone by chance have a copy of the HaPyLi compiler? It's a Haskell/Python/Lisp-like language that compiles to Whitespace. 21:36:41 The website went offline around 2012 and it wasn't completely archived on the Internet Archive. 21:36:43 -!- tromp has joined. 21:44:21 -!- rusted-root has changed nick to imode. 21:44:24 -!- freon has quit (Ping timeout: 250 seconds). 21:56:52 * pikhq counts herself very glad nobody else wants pikhq 21:57:36 riv: yeah, i miss some people who used to be here too. still in touch with some though i don't talk with them much; also still frequently in touch with others 21:57:51 oh that's nice 21:58:23 and re: psych hospital. glad i've never been in one but fuck i've been close 22:00:03 turns out being into absolutely weird programming languages has a high overlap with just being weird as a person in one of a few different ways 22:01:53 [[User:Zzo38/Programming languages with unusual features]] https://esolangs.org/w/index.php?diff=84457&oldid=84358 * Zzo38 * (+94) The {edit} macro in Free Hero Mesh 22:11:25 i mean i am very much a weird person so :p 22:22:40 pikhq: yes, but how do so many of those kinds of people actually find their way here, that's what I don't understand 22:24:13 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 22:24:46 I don't understand that even after I just personally recommended this channel to someone and they came here 22:25:09 because how did I find them in first place 22:25:17 if you're that sort of weird you're gonna actively seek it out 22:26:59 I don't have a copy of the HaPyLi 22:32:01 [[Special:Log/newusers]] create * Hjoker4 * New user account 22:36:00 -!- imode has changed nick to ch0de. 22:49:13 Do you like the picture editor of Free Hero Mesh? 22:56:32 -!- salpynx has joined. 23:06:39 -!- user3456 has quit (Quit: ZNC - https://znc.in). 23:07:42 Will they add the Quasijarus compression format into newer versions of GNU/Linux and/or non-Quasijarus BSD? 23:08:38 -!- user3456 has joined. 23:14:51 [[Among Us]] https://esolangs.org/w/index.php?diff=84458&oldid=84356 * Zero player rodent * (+211) 23:18:03 if you ever dig into esolangs even a bit and want to talk to people into them this channel is hard to not find. the esolangs wiki is like the resource referenced everywhere after all 23:25:10 yep 23:26:28 hence how i found it when i was, like, 15 23:29:15 -!- tech_exorcist has quit (Quit: tech_exorcist). 23:40:42 [[Among Us]] https://esolangs.org/w/index.php?diff=84459&oldid=84458 * Zero player rodent * (+99) 23:47:01 [[VBF]] M https://esolangs.org/w/index.php?diff=84460&oldid=84440 * PythonshellDebugwindow * (+53) /* Implementations */ Cats 23:47:51 [[Among Us]] https://esolangs.org/w/index.php?diff=84461&oldid=84459 * Zero player rodent * (+149) 23:48:24 [[GotoFuck]] M https://esolangs.org/w/index.php?diff=84462&oldid=83713 * PythonshellDebugwindow * (+78) /* Implementations */ Cats, see also 23:48:41 [[Jumplang]] M https://esolangs.org/w/index.php?diff=84463&oldid=74090 * PythonshellDebugwindow * (+15) /* See also */ See also. 23:53:25 riv: yep! I was playing around with bitfuck a few years ago. 23:53:57 specifically messing around with the reversible variant, which permits some interesting minimizations