< 1553904368 269102 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Remote host closed the connection < 1553904485 917038 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Remote host closed the connection < 1553905385 935105 :AnotherTest!~turingcom@d51a4b8e1.access.telenet.be QUIT :Ping timeout: 246 seconds < 1553906406 528687 :oerjan!oerjan@sprocket.nvg.ntnu.no JOIN :#esoteric < 1553906421 23482 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1553906543 527189 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric < 1553906572 777198 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 250 seconds < 1553906573 592926 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life > 1553908251 115159 PRIVMSG #esoteric :14[[07Inflection14]]4 10 02https://esolangs.org/w/index.php?diff=60806&oldid=44480 5* 03Prof Apex 5* (+262) 10 > 1553910545 449366 PRIVMSG #esoteric :14[[07AlphaBeta14]]4 10 02https://esolangs.org/w/index.php?diff=60807&oldid=54154 5* 03Illuminatu 5* (+306) 10 < 1553910620 510364 :nikgre!~piman3141@rrcs-24-73-5-204.se.biz.rr.com JOIN :#esoteric > 1553910689 598338 PRIVMSG #esoteric :14[[07AlphaBeta14]]4 10 02https://esolangs.org/w/index.php?diff=60808&oldid=60807 5* 03Illuminatu 5* (+12) 10 < 1553911096 31892 :nikgre!~piman3141@rrcs-24-73-5-204.se.biz.rr.com QUIT :Quit: Leaving < 1553911711 510624 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Does any C compiler have "goto case" and "goto default"? < 1553912009 494143 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Not as far as I know, though some of the nearby languages (C#, D) do. < 1553912189 355673 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :. o O ( What about Db ) < 1553912287 768180 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :ah https://www.codeproject.com/Articles/13639/Db-The-Future-Is-Coming < 1553912331 994013 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :I'm guessing it's more common in languages with no implicit fall-through. < 1553915177 327645 :Essadon!~Essadon@81-225-32-185-no249.tbcn.telia.com QUIT :Quit: Qutting < 1553916022 166460 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Do you have any kind of advice of implementing NNTP server with SQLite? < 1553916760 436802 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :If they want us to defend their church from an attack (after they helped us to get underground through their passage) but now we are too tired to help them and should sleep instead, then what are we going to do? Hire someone else to help them? (This is the GURPS game.) < 1553917111 287810 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Do you know if FreeDOS can load overlong COM files? < 1553917629 646729 :FreeFull!~freefull@defocus/sausage-lover QUIT : < 1553918534 418562 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Nite < 1553919032 864997 :quintopia!~quintopia@unaffiliated/quintopia QUIT :Ping timeout: 272 seconds < 1553919040 837129 :quintopia!~quintopia@unaffiliated/quintopia JOIN :#esoteric < 1553933644 995670 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Remote host closed the connection < 1553933658 191878 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric < 1553937590 287472 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru JOIN :#esoteric < 1553938096 417758 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Remote host closed the connection < 1553938440 940837 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric < 1553940828 443153 :aloril_!~aloril@mobile-access-5d6a2f-120.dhcp.inet.fi QUIT :Remote host closed the connection < 1553941408 354254 :aloril!~aloril@mobile-access-5d6a2f-120.dhcp.inet.fi JOIN :#esoteric < 1553944602 657184 :rodgort!~rodgort@68.ip-149-56-14.net QUIT :*.net *.split < 1553944602 736805 :Melvar!~melvar@dslb-088-066-199-031.088.066.pools.vodafone-ip.de QUIT :*.net *.split < 1553944602 785268 :HackEso!~HackEso@techne.zem.fi QUIT :*.net *.split < 1553944602 976282 :oren!~oren@ec2-18-212-11-99.compute-1.amazonaws.com QUIT :*.net *.split < 1553944602 976320 :lifthrasiir_!~lifthrasi@ec2-52-79-98-81.ap-northeast-2.compute.amazonaws.com QUIT :*.net *.split < 1553944603 63343 :APic!apic@apic.name QUIT :*.net *.split < 1553944631 429601 :lifthrasiir!~lifthrasi@ec2-52-79-98-81.ap-northeast-2.compute.amazonaws.com JOIN :#esoteric < 1553944631 984699 :rodgort!~rodgort@68.ip-149-56-14.net JOIN :#esoteric < 1553944634 739246 :oren!~oren@ec2-18-212-11-99.compute-1.amazonaws.com JOIN :#esoteric < 1553944640 664039 :Melvar!~melvar@dslb-088-066-199-031.088.066.pools.vodafone-ip.de JOIN :#esoteric < 1553944742 6859 :HackEso!~HackEso@techne.zem.fi JOIN :#esoteric < 1553944798 48543 :vertrex!~vertrex@unaffiliated/vertrex QUIT :Ping timeout: 255 seconds < 1553944825 22288 :sftp!~sftp@unaffiliated/sftp QUIT :Ping timeout: 255 seconds < 1553944896 997735 :sftp!~sftp@unaffiliated/sftp JOIN :#esoteric < 1553944908 106918 :vertrex!~vertrex@digital-forensic.org JOIN :#esoteric < 1553944908 156799 :vertrex!~vertrex@digital-forensic.org QUIT :Changing host < 1553944908 156853 :vertrex!~vertrex@unaffiliated/vertrex JOIN :#esoteric < 1553944936 109897 :APic!apic@apic.name JOIN :#esoteric < 1553945737 963379 :AnotherTest!~turingcom@d51a4b8e1.access.telenet.be JOIN :#esoteric < 1553948169 45482 :int-e!~noone@int-e.eu PRIVMSG #esoteric :so quiet on the wiki - the A-team must be out of town. < 1553948375 632006 :int-e!~noone@int-e.eu PRIVMSG #esoteric :fungot: morning? < 1553948375 759218 :fungot!~fungot@2a01:4b00:82bb:1341::2 PRIVMSG #esoteric :int-e: curl is not the true finish. < 1553948399 168799 :int-e!~noone@int-e.eu PRIVMSG #esoteric :fungot: you can do better than that < 1553948448 923236 :int-e!~noone@int-e.eu PRIVMSG #esoteric :ouch. < 1553948617 727288 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :fungot: Giving them the cold shoulder, eh? < 1553948618 14088 :fungot!~fungot@2a01:4b00:82bb:1341::2 PRIVMSG #esoteric :fizzie: i.e. a list of words with him, regardless of whether scheme48 is being proper, it's important to know where it is < 1553948626 650486 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :(Is that even a correct idiom?) < 1553948662 954618 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I think so. < 1553948667 955148 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :@wn "cold shoulder" < 1553948668 786924 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :*** "cold shoulder" wn "WordNet (r) 3.0 (2006)" < 1553948668 898687 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :cold shoulder < 1553948669 339791 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : n 1: a refusal to recognize someone you know; "the snub was < 1553948671 341226 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : clearly intentional" [syn: {snub}, {cut}, {cold shoulder}] < 1553948703 230606 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Or maybe it's "show" rather than "give"? I don't know. < 1553948750 260806 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :"Even the best A&R—artist and repertoire—staff in the world couldn't save you if radio gave you the cold shoulder." < 1553948764 958991 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :(From the Google snippet of an OED entry.) < 1553948786 525812 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Yeah I think the "show" is inspired by the parallel idiom in German. < 1553948843 930217 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Which is "jemandem die kalte Schulter zeigen" - the verb is "zeigen": to show; to demonstrate; to point out) < 1553949022 34242 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Looks like it's also a verb. < 1553949023 214536 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :`` wn "cold shoulder" -over | sed -e '1,/verb/d;/^1/p;d' < 1553949024 205360 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :1. slight, cold-shoulder -- (pay no attention to, disrespect; "She cold-shouldered her ex-fiance") < 1553949080 239022 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :(Guess almost any noun can be verbed though.) < 1553949207 171440 :int-e!~noone@int-e.eu PRIVMSG #esoteric :verbificationizing is lots of fun. < 1553949788 435389 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1553949821 968061 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 246 seconds < 1553949931 948156 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1553951559 236346 :Essadon!~Essadon@81-225-32-185-no249.tbcn.telia.com JOIN :#esoteric < 1553956849 958218 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1553961129 62606 :oerjan!oerjan@sprocket.nvg.ntnu.no JOIN :#esoteric < 1553961456 839830 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :"This expression and its German equivalent are mistranslations of dederunt umerum recedentem from the Book of Nehemiah 9.29 from the Vulgate Bible, which actually means "stubbornly they turned their backs on you", which comes from the Septuagint Bible's equivalent ἔδωκαν ‎(édōkan‎) νῶτον ἀπειθοῦντα. Latin umerus means both "shoulder" and "back"." < 1553962830 963286 :Phantom_Hoover!~phantomho@cpc108439-cowc8-2-0-cust785.14-2.cable.virginm.net JOIN :#esoteric < 1553962831 277644 :Phantom_Hoover!~phantomho@cpc108439-cowc8-2-0-cust785.14-2.cable.virginm.net QUIT :Changing host < 1553962831 277688 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1553962852 293401 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :good morning y'all < 1553962877 551425 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :morn morn < 1553963701 304093 :rain1!~My_user_n@unaffiliated/rain1 PRIVMSG #esoteric :hiy < 1553963987 311456 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :hirain < 1553964404 762591 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :hello < 1553964586 269422 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :hm how do you think should “hot shoulder” mean misrecognition of people you don’t actually know? < 1553965423 4266 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :oh, another disadvantage of using sound cards as modems for ham radio: sometimes people end up transmitting their Windows alert sounds by accident :P < 1553965678 82010 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Other way is to not use Windows, or if you are using Windows to disable the alert sounds, or maybe you have surround sound you can use some channel for different purposes? There are other cases too where such a thing might be wanted. < 1553965685 340364 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :shocking < 1553965752 869697 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :zzo38: none of those ways help with accidents happening because some people are too dumb to know about them < 1553965976 450171 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :kmc: is that like when people give a presentation in a conference and there are popups prompting for software updates and friends who have come online on skype over the slides? < 1553965979 935594 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes, that is true probably > 1553966056 109362 PRIVMSG #esoteric :14[[07User:Sentry14]]4 N10 02https://esolangs.org/w/index.php?oldid=60809 5* 03Sentry 5* (+63) 10Created page with "a young aspiring programmer and student, open source enthusiast" < 1553966091 864884 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :`le/rn Aspiring is like perspiring, but more hopeful. < 1553966092 559717 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :Usage: `le/[/]rn // < 1553966094 535730 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :oops < 1553966099 23780 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :`learn Aspiring is like perspiring, but more hopeful. < 1553966101 55923 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :Learned 'aspiring': Aspiring is like perspiring, but more hopeful. < 1553966880 790223 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :b_jonas: yes < 1553967080 763681 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :zzo38: yeah, the best solution is to use a dedicated sound card for the radio. you can buy USB sound interfaces like RIGblaster and SignaLink that are made for this, they generally have better quality, better filtering and such, and some of them can control your radio too, so you can set the frequency etc from software < 1553967098 162570 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :and some of the newer radios have a USB port built in so that you get both audio and control with a single USB cable < 1553967106 185405 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :but yeah it still relies on the operator configuring their software correctly < 1553968941 637895 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Later < 1553969027 546871 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :`learn The password of the month is invalid. < 1553969029 492530 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :Relearned 'password': The password of the month is invalid. < 1553969031 938778 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :(Feel free to change, it just dawned on me we'll soon miss having one for March.) < 1553969198 202036 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :We did an escape room as a team thing the other day, and they did the "password IS invalid" thing. < 1553969215 694107 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :(Spoilers.) < 1553969339 980624 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :lol < 1553969359 794229 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :I know someone who chose their wifi password as "alllowercasenospaces" < 1553969552 758372 :int-e!~noone@int-e.eu PRIVMSG #esoteric :followtheinstructionstotheletter < 1553969765 681867 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :it turns out that French has a word with "à" in it other than "à", "là", and prefixed versions derived from "là". it's "en-deçà" and I don't think I've seen it until today. < 1553970228 631598 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :kmc: I've seen that but worse, lemme see if I can find a pic.. < 1553970243 194406 :Lymia!lymia@magical.girl.lyrical.lymia.moe QUIT :Remote host closed the connection < 1553970471 678522 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :Hmm, no picture, but something along the lines of "the wifi password is designed to mess with the use-mention distinction" < 1553970490 786970 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :lol < 1553970500 729351 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :with the password being literally the bit after 'is', with spaces and all-lowercase < 1553970501 859009 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :yeah I know people who would set that kind of password < 1553970561 515285 :Lymia!lymia@magical.girl.lyrical.lymia.moe JOIN :#esoteric < 1553970590 266490 :j4cbo!sid186930@gateway/web/irccloud.com/x-jvuunpjzubdepftz PRIVMSG #esoteric :the password is “contained in greengrocers’ quotes” < 1553970767 264268 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :The book Godel,Escher,Bach defines the TNT (Typographical Number Theory), and you can define the rules to make a theorem. But, then maybe you want to define if a sentence of TNT (open formulas don't count) is true? I thought maybe: [1] If X is a theorem then X is true. [2] If X and Y are true and are assumed as axioms then Z would be a theorem, then Z is true. [3] If X starts with a universal quantifier and all sentences formed by removing the < 1553970862 596641 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :What do you think? > 1553972231 426316 PRIVMSG #esoteric :14[[07Bitter14]]4 M10 02https://esolangs.org/w/index.php?diff=60810&oldid=58719 5* 03DMC 5* (-1) 10/* Truth Machine */ > 1553972270 471831 PRIVMSG #esoteric :14[[07Bitter14]]4 M10 02https://esolangs.org/w/index.php?diff=60811&oldid=60810 5* 03DMC 5* (+1) 10/* Truth Machine */ < 1553972305 798068 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :zzo38: and all sentences formed by removing the => is it only my IRC client, but it seems truncated after “the” < 1553972535 479335 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :I don’t remember what the formulation is in that book, though, to tell something useful > 1553972538 847183 PRIVMSG #esoteric :14[[07User:DMC14]]4 M10 02https://esolangs.org/w/index.php?diff=60812&oldid=60517 5* 03DMC 5* (+100) 10 < 1553972588 624252 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :zzo38: I think it uses the usual definition from modal logic < 1553972602 165960 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :or, not modal < 1553972604 856367 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :what's it called < 1553972629 959061 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :not not not intuitionistic? < 1553972636 38706 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :model theory < 1553972738 394847 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :there’s also another definition which is basically a simplification of this one applied to the canonical model, which I don’t remember if is always defined < 1553972739 477924 :int-e!~noone@int-e.eu PRIVMSG #esoteric :[1] has a name: soundness < 1553972767 349510 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :[3] If X starts with a universal quantifier and all sentences formed by removing the quantifer and replacing that variable with the same number everywhere is true no matter what number you put, then X is true. < 1553972786 654990 :int-e!~noone@int-e.eu PRIVMSG #esoteric :[2] is really just a facet of soundness. (if X and Y are axioms, then the models that are considered for soundness are those that make X and Y (and the other axioms) true) < 1553972820 691017 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :(cont. to mine) ah, yeah, it shouldn’t be defined if there’s no equality in the language (and equality axioms in the theory) < 1553972821 596936 :int-e!~noone@int-e.eu PRIVMSG #esoteric :[3] is part of the /definition/ of truth of a formula in a model. < 1553973004 863705 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(You usually need to do [3] a bit differently, working with assignments that assign model elements to the free variables of a formula, because for most models, the objects are not representable as expressions.) < 1553973085 916321 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(But in the special case that's treated in GEB that's not the case; only the standard model is really considered (just the natural numbers, no nonstandard ones), and all those can be represented as 0, S0, SS0, etc.) > 1553973823 605170 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03Fuzzyastrocat 5* 10New user account < 1553973959 66987 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :`? skolem < 1553973960 148635 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :skolem? ¯\(°​_o)/¯ < 1553974141 498075 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :btw a big ramble and a question: < 1553974141 621982 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :btw nonstandard naturals are a mind-blower: no simultaneously computable addition and multiplication is like wtf should it at all be possible right here, aren’t we talking about simple natural-numbery things? < 1553974141 622025 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :and we can’t get rid of nonstandard models either: say, we take second-order logic axiomatization, but now we don’t have several crucial properties of first-order language; < 1553974141 622034 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :should we specially pick the standard model, then we could ask ourselves how do we to understand sets (which are needed to define a model, and specifically the standard model)— < 1553974141 622049 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :and why aren’t there nonstandard set universe models then (and there are!); < 1553974142 217772 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :finally, informal set theory as a base is in this case not much better than simply informal arithmetic (which we were to formalize in the first place as we’re wary about things like those same nonstandards etc.) < 1553974142 257564 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :so if I’m getting things right, we are left to presuppose we can somehow work with the standard naturals, akin to presupposing ZFC or PA are consistent, and not much else? < 1553974193 749405 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :(oh forgot to delete the second “btw”) < 1553974391 652312 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I guess people mostly don't think much about it, probably taking a second-order view on the axiom of induction for most purposes. < 1553974437 20280 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(the second order version is, any set that contains 0 and is closed under taking the successor, contains all natural numbers) < 1553974467 514569 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :@quote skolem < 1553974467 612334 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :byorgey says: Escaped skolem! Authorities mount massive search. News at 11. < 1553974469 66871 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :@quote skolem < 1553974469 135173 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :byorgey says: Escaped skolem! Authorities mount massive search. News at 11. < 1553974471 392482 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :@quote skolem < 1553974471 483060 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :byorgey says: Escaped skolem! Authorities mount massive search. News at 11. < 1553974479 90134 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :@quote Tolkeinesque < 1553974479 197897 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :No quotes match. I can't hear you -- I'm using the scrambler. < 1553974483 144768 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :ACTION gives up < 1553974545 338442 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: that shifts the problem one level down the stack, of course; I have no clue how that plays out if you take an arbitrary model of ZFC (can we even pinpoint a standard model of ZFC? perhaps using some specific large ordinal?) < 1553974631 253891 :int-e!~noone@int-e.eu PRIVMSG #esoteric :@quote Tolkienesque < 1553974631 337024 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :chrisdone says: anyone got a fixed version of the split library for ghc7? some Tolkienesque error messages about skolems escaping < 1553974661 567339 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I'm not sure about the Tolkien connection. < 1553974731 938383 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Is this supposed to allude to the Balrog and Gandalf situation? "Thou shalt not pass!"? < 1553974759 854407 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: as far as I don’t know about it, I’ve thought there would be the same problem, and for a theory ZFC + there should be no less but maybe even more problems (though I don’t see how it can be more, either) < 1553974871 991336 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: one resolution is that mathematicians care more about provability than about truth :P < 1553974903 368514 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :"you shall not pass!" <--- me when I'm wearing a t-shirt :/ < 1553974909 13372 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: yeah, I suppose it delivers some peace of mind < 1553974973 399428 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Personally I also have this illusion that I understand the natural numbers... 0, 1, 2, and so on. < 1553974978 688787 :int-e!~noone@int-e.eu PRIVMSG #esoteric :What could possibly go wrong? :) < 1553974991 685102 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :there are still t-shirt haters in the world? :( isn’t it snobbish < 1553974996 248524 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(they really are *natural* that way) < 1553974997 860788 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :int-e: 0, 1, and 2 are easy. the problem is that there are more natural numbers than those. < 1553975034 908880 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :int-e> What could possibly go wrong? :) => yeah, the same feeling there < 1553975104 132885 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :I like to say something about inductive types, though it shouldn’t be a panacea if one’s to look closer, but I don’t know type theory on that level < 1553975121 348190 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :to see it clearly < 1553975229 122996 :int-e!~noone@int-e.eu PRIVMSG #esoteric :b_jonas: I'm not playing that game (the game being: who can name more natural numbers?) < 1553975236 203301 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :there's too many of them < 1553975271 343449 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> [0..] -- Or maybe I am. But not seriously. < 1553975273 180547 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :oh, also about something probably more discoverable: is there any connection between λ term (Y succ) aka ∞, and nonstandard naturals? Perhaps there are much more inequivalent such terms? < 1553975273 260600 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,2... < 1553975303 705774 :rain1!~My_user_n@unaffiliated/rain1 PRIVMSG #esoteric :no i don't think they have a relationship < 1553975332 499265 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: no, you can't compute with that term. For example x - x = 0 is true for all non-standard natural numbers. < 1553975335 803184 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :there seems to be an error in lambdabot, they say 2 is after both 1 and 27 < 1553975341 315357 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :(I’ll show myself out) < 1553975375 730531 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :rain1: int-e: thanks for straightening this out < 1553975375 770439 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: I think you hit the right level of insightfulness there, for this discussion. :) < 1553975387 497644 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric ::D > 1553975393 571027 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03KerbalEngineer 5* 10New user account < 1553975618 954191 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :(oh I have two friends playing KSP. They didn’t manage to pull me in yet, though) < 1553975678 75168 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I consciously try to avoid such time sinks as much as possible. Pure puzzle games are bad enough. < 1553975728 129662 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(KSP in particular also seems quite expensive. But that's a secondary issue.) < 1553975772 881257 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Pure puzzle games... Baba is You is at 35 hours... still not done. I'm stuck on level 3 in Depths...) < 1553975902 272740 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :to say about that ∞, or more precisely a coinductive type N̅, some time ago I bemusingly found it’s perfect in defining how many steps for some machine to run; the code uses solely `prev` destructor and becomes very clean (if the language is sufficiently good at expressing N̅) < 1553975923 416070 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :hm time sinks is my issue I think < 1553976169 913076 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :it even rhymes, it should be true < 1553976288 494549 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: that is a fairly standard trick to make total languages with coinductive types Turing-complete (not sure which it was... Agda, probably): data Result a = Skip (Result a) | Return a < 1553976302 93922 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(where data is the Haskell thing, so really a codata) < 1553976400 41870 :int-e!~noone@int-e.eu PRIVMSG #esoteric :For related reasons (avoiding recursion in a worker, helping the compiler to do the right kind of inlining) a similar "Skip" has found its way into some stream fusion libraries (bytestring?). < 1553976466 717825 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I should probably refresh my memory on where I really encountered those... < 1553977411 461849 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: thanks, I haven’t thought it reaches further! < 1553977604 262073 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :though my case even was in a language without explicit codata, and I defined ∞ as a special case, so one could see if the value is ∞. But operationally it was still codata Nat' = Z | S Nat' < 1553977669 869128 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :where “operationally” means interoperation between Z, S and prec. I should pick words more accurately < 1553977670 806088 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I guess it's dual in some sense to the Skip... you can provide an infinite amount of fuel to a computation. < 1553977756 491803 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :I thought Skip meant to be analogous to S? (and Return to Z) < 1553977782 463874 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: yes but it's used in a result of a computation rather than as input < 1553977796 299966 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :ah, in that sense < 1553977877 423164 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So the function can be productive (produce a new constructor in finite time) without ever producing an answer. < 1553977916 260514 :int-e!~noone@int-e.eu PRIVMSG #esoteric :In the end you'll have a non-total run-time system that discards all the 'Skip's and waits for the result. < 1553977949 52471 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But everything else can be total (respectively productive). < 1553978291 416944 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :hm, about duality: runSteps :: Nat' → s → s vs. runStep :: Result s → Result s. Could these be turned to something more explicitly dual?.. < 1553978444 87742 :int-e!~noone@int-e.eu PRIVMSG #esoteric :You'd have runStep :: s -> Result s. (Result is a monad, so that's where you can eat the Skips when forwarding results). I suppose (Nat' -> s) is isomorphic to (Result s) if you think about it operationally; whenever the former consumes a "Suc", the latter will produce a "Skip". < 1553978519 875275 :int-e!~noone@int-e.eu PRIVMSG #esoteric :This is not a perfect match; maybe Nat' -> (s, Nat') with the convention that the Nat' is the remaining fuel makes it better; then you have a corresponding (state) monad. < 1553978603 907529 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Maybe Cale will wake up and point out that this is just a pair of adjoint functors and that explains it all somehow. ;-) < 1553978657 994708 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :also have a sense of adjointness. Any unknown categorial magic should be due to adjoints! < 1553978762 462207 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :which... < 1553978763 640894 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :what < 1553978782 770961 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :What are we explaining? < 1553978790 979398 :AnotherTest!~turingcom@d51a4b8e1.access.telenet.be QUIT :Ping timeout: 255 seconds < 1553978796 332646 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric ::) < 1553978914 349246 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :Cale: hm I think it could be phrased as “in what sense is returning Result s is dual to taking Nat'), but int-e may say it better < 1553978933 260040 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :oh, s/)/” < 1553979052 965876 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :What is this Result type? < 1553979070 246335 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :oh < 1553979072 774255 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :I found it :) < 1553979076 82134 :int-e!~noone@int-e.eu PRIVMSG #esoteric :the Skip monad, I got the naming wrong. < 1553979113 699302 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :okay I’ll probably go and the next day will read the logs < 1553979118 669793 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :ah... hmm < 1553979119 712513 :int-e!~noone@int-e.eu PRIVMSG #esoteric :ACTION has always been better with ideas than with terminology. < 1553979128 333774 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :Maybe Free vs. Cofree can explain it... < 1553979144 949655 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :somehow :) < 1553979176 894066 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Cale: sorry for the bait, but it was too tempting :) < 1553979204 682803 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :could those types be resp. Free somethingsomething and Cofree cosomethingsomething maybe? < 1553979233 814365 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru PRIVMSG #esoteric :ok bye < 1553979310 633708 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Oh for this purpose we should probably take [co]data Nat' = Suc Nat'. The Zero constructor will produce a lot of garbage. < 1553979337 98416 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :hah < 1553979341 690869 :int-e!~noone@int-e.eu PRIVMSG #esoteric :And then it becomes really weird because we have only one value. < 1553979382 188614 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :.oO( Cofree Proxy a -> b vs. a -> Free Proxy b ) < 1553979396 785220 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :er, not proxy < 1553979432 80914 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :Identity? < 1553979439 496753 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :Identity. < 1553979452 730104 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :Kind of.. < 1553979466 476421 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :I don't actually want more a's :) < 1553979468 512514 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So there's a mismatch. Nat' -> s needs partiality in the arrows, in whatever category that lives in; the Result s has extra structure in the result (namely the number of Skips). < 1553979502 213750 :arseniiv!~arseniiv@95.105.1.23.dynamic.ufanet.ru QUIT :Ping timeout: 246 seconds < 1553979517 266241 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :Well, Nat' -> s -> s also means you're theoretically allowed to depend on that Nat' and not just use it as computational fuel < 1553979539 740237 :Cale!~cale@2607:fea8:995f:fb71:c1cd:b679:2768:c42a PRIVMSG #esoteric :and yeah, on the other side, you're effectively producing an additional Nat < 1553979541 578969 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Yes, that would be the garbage :) < 1553979544 5793 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :try taking powers modulo a large prime < 1553979555 659338 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(depending on the Nat' value) < 1553979620 343774 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So I want to do something intensional where I look inside the computation and see how many Suc are consumed, and shift that to the output. I guess category theory will not really help there. :) < 1553979662 453883 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(I also want some linearity... the shifting becomes difficult if the Nat' value ever gets duplicated) > 1553979884 431556 PRIVMSG #esoteric :14[[07Control Character14]]4 10 02https://esolangs.org/w/index.php?diff=60813&oldid=60790 5* 03EnilKoder 5* (+90) 10/* Syntax */ < 1553980422 408045 :FreeFull!~freefull@defocus/sausage-lover QUIT :Quit: Rebooting < 1553980503 772265 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1553980861 924571 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :`? sushi < 1553980862 948222 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :sushi? ¯\(°​_o)/¯ < 1553980866 239056 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :`? octopus < 1553980867 340025 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :octopus? ¯\(°​_o)/¯ < 1553980869 698806 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :`? squid] < 1553980870 748000 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :squid]? ¯\(°​_o)/¯ < 1553980871 193714 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :`? squid < 1553980872 620454 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :squid? ¯\(°​_o)/¯ < 1553981145 118876 :int-e!~noone@int-e.eu PRIVMSG #esoteric :why? > 1553981872 535856 PRIVMSG #esoteric :14[[07Control Character14]]4 10 02https://esolangs.org/w/index.php?diff=60814&oldid=60813 5* 03EnilKoder 5* (-6) 10 > 1553985012 316682 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03Amapires 5* 10New user account < 1553985105 238963 :b_jonas!~x@catv-176-63-25-78.catv.broadband.hu PRIVMSG #esoteric :`? octonion < 1553985106 387972 :HackEso!~HackEso@techne.zem.fi PRIVMSG #esoteric :octonion? ¯\(°​_o)/¯ < 1553986567 1601 :quintopia!~quintopia@unaffiliated/quintopia QUIT :Ping timeout: 255 seconds < 1553987019 95493 :quintopia!~quintopia@unaffiliated/quintopia JOIN :#esoteric < 1553987019 773300 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Remote host closed the connection > 1553988846 823203 PRIVMSG #esoteric :14[[07Special:Log/upload14]]4 upload10 02 5* 03Lartu 5* 10uploaded "[[02File:Ldpl-logo.png10]]": LDPL Programming Language Logo < 1553989147 956014 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric > 1553990287 639269 PRIVMSG #esoteric :14[[07LDPL14]]4 10 02https://esolangs.org/w/index.php?diff=60816&oldid=60283 5* 03Lartu 5* (+2311) 10 < 1553990307 11814 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Remote host closed the connection