< 1562889804 776525 :tromp!~tromp@2a02:a210:1585:3200:5167:ad32:a88b:647a QUIT :Ping timeout: 252 seconds < 1562890186 263910 :Sgeo__!~Sgeo@ool-18b98455.dyn.optonline.net JOIN :#esoteric < 1562890384 873882 :Sgeo_!~Sgeo@ool-18b98455.dyn.optonline.net QUIT :Ping timeout: 258 seconds < 1562890733 216273 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :You know, it's very rare that I receive an email from another human being sent specifically to me. :D < 1562890733 940268 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Most of my email comes from "the Algorithm". < 1562890805 524106 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Then what is it for if not specifically for you? Mailing lists? Wide notifications? < 1562890843 379759 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Yeah, mailing lists and automated emails. < 1562890967 649605 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :ACTION obeys and worships The Algorithm < 1562890993 977811 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :I do not have any mailing lists or automated notifications (although I have occasionally received automated replies); all of the messages I receive are someone writing to me specifically. I have sometimes received spam messages, but when that happens I edit my /etc/aliases file so that they can't send it anymore. < 1562891074 435395 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :(I have several email addresses, so if the spam is prevented in this way, it will not usually prevent legitimate messages.) < 1562892444 21963 :tromp!~tromp@2a02:a210:1585:3200:2478:f928:694e:d106 JOIN :#esoteric < 1562892709 970295 :tromp!~tromp@2a02:a210:1585:3200:2478:f928:694e:d106 QUIT :Ping timeout: 252 seconds < 1562892822 7600 :tromp!~tromp@2a02:a210:1585:3200:9422:e3b8:edd1:b6d1 JOIN :#esoteric < 1562892898 975866 :tromp_!~tromp@2a02:a210:1585:3200:94d7:c820:dd9f:a50f JOIN :#esoteric < 1562893083 970357 :tromp!~tromp@2a02:a210:1585:3200:9422:e3b8:edd1:b6d1 QUIT :Ping timeout: 252 seconds < 1562893171 976099 :tromp_!~tromp@2a02:a210:1585:3200:94d7:c820:dd9f:a50f QUIT :Ping timeout: 252 seconds < 1562893753 117418 :atslash!~atslash@static.231.107.9.5.clients.your-server.de QUIT :Quit: This computer has gone to sleep < 1562894131 622854 :tromp!~tromp@2a02:a210:1585:3200:545:10f5:6b77:bc2e JOIN :#esoteric < 1562894271 512150 :tromp_!~tromp@2a02:a210:1585:3200:15d7:67be:887:703b JOIN :#esoteric < 1562894446 512466 :tromp!~tromp@2a02:a210:1585:3200:545:10f5:6b77:bc2e QUIT :Ping timeout: 276 seconds < 1562894563 536350 :tromp_!~tromp@2a02:a210:1585:3200:15d7:67be:887:703b QUIT :Ping timeout: 276 seconds < 1562896060 250671 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 246 seconds < 1562896074 258639 :xkapastel!uid17782@gateway/web/irccloud.com/x-tmcnudoobvfwtjfi QUIT :Quit: Connection closed for inactivity < 1562896573 892443 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1562896828 699516 :FreeFull!~freefull@defocus/sausage-lover QUIT : < 1562911466 464466 :mapleBloodRed!~mapleBloo@223.11.219.140 JOIN :#esoteric < 1562911898 160761 :mapleBloodRed!~mapleBloo@223.11.219.140 QUIT :Read error: Connection reset by peer < 1562912136 278217 :Frater_EST!~adrianbib@wsip-68-15-198-210.ok.ok.cox.net JOIN :#esoteric < 1562912922 839316 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com JOIN :#esoteric < 1562914599 569554 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com PRIVMSG #esoteric :`? < 1562914600 592657 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :​? ¯\(°​_o)/¯ < 1562914633 796188 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com PRIVMSG #esoteric :`help < 1562914634 54369 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch [] " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ < 1562914638 810479 :tromp!~tromp@2a02:a210:1585:3200:a54b:884f:3036:801d JOIN :#esoteric < 1562915362 585952 :int-e!~noone@int-e.eu PRIVMSG #esoteric :akozar: I came up with https://int-e.eu/~bf3/tmp/primes.sme.txt just after you left earlier < 1562915406 555011 :int-e!~noone@int-e.eu PRIVMSG #esoteric :akozar: (which is borderline cheating because all the sieving is already done during initialization) < 1562915500 988785 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com PRIVMSG #esoteric :WOW! That's incredible! < 1562915609 166395 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com PRIVMSG #esoteric :Nice work! I'm assuming that it requires more lines to search higher? < 1562915889 420084 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com PRIVMSG #esoteric :I think that you can remove the steps An+A where A is not prime, but of course then you have to know some of the primes in advance. ;-) < 1562916212 930116 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com PRIVMSG #esoteric :int-e: I was figuring out how your unary counter program worked earlier. Thanks for these examples! < 1562916480 387359 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com PRIVMSG #esoteric :And just before you messaged, I was checking out the info about tiling rectangles on your web site. Neat stuff. I enjoy combinatorial problems. ^_^ < 1562916799 103632 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hmm I might still revisit that one at some point. < 1562916995 734693 :b_jonas!~x@catv-176-63-24-45.catv.broadband.hu QUIT :Quit: leaving < 1562917345 15453 :tromp!~tromp@2a02:a210:1585:3200:a54b:884f:3036:801d QUIT :Remote host closed the connection < 1562918552 629179 :tromp!~tromp@2a02:a210:1585:3200:a54b:884f:3036:801d JOIN :#esoteric < 1562918992 392945 :akozar!~akozar@cpe-174-104-169-20.neo.res.rr.com QUIT :Quit: akozar < 1562919473 123889 :int-e!~noone@int-e.eu PRIVMSG #esoteric :tswett[m]: I have an unbounded binary counter :) https://int-e.eu/~bf3/tmp/binary.sme.txt > 1562920061 395373 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 N10 02https://esolangs.org/w/index.php?oldid=64228 5* 03A 5* (+644) 10Thank you @Areallycoolusername > 1562920134 786112 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 10 02https://esolangs.org/w/index.php?diff=64229&oldid=64228 5* 03A 5* (+3932) 10Fix typos and more info; Ctrl+C Ctrl+V first > 1562920743 958309 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 M10 02https://esolangs.org/w/index.php?diff=64230&oldid=64229 5* 03A 5* (+120) 10Do partial work < 1562921569 242599 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But this should not distract from the fact that this is a really annoying language to work in. > 1562921599 542648 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 M10 02https://esolangs.org/w/index.php?diff=64231&oldid=64230 5* 03A 5* (+29) 10Hello World not yet translated. < 1562921680 321652 :atslash!~atslash@46.188.0.82 JOIN :#esoteric < 1562921800 263973 :arseniiv!~arseniiv@136.169.229.227 JOIN :#esoteric < 1562921953 325419 :atslash!~atslash@46.188.0.82 QUIT :Ping timeout: 245 seconds < 1562921990 162841 :atslash!~atslash@static.231.107.9.5.clients.your-server.de JOIN :#esoteric > 1562922202 278 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 M10 02https://esolangs.org/w/index.php?diff=64232&oldid=64231 5* 03A 5* (+124) 10 > 1562922684 138421 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 M10 02https://esolangs.org/w/index.php?diff=64233&oldid=64232 5* 03A 5* (-33) 10Simpler syntax to compile to Klaus > 1562922905 160304 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 M10 02https://esolangs.org/w/index.php?diff=64234&oldid=64233 5* 03A 5* (+2) 10 > 1562923427 557697 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 M10 02https://esolangs.org/w/index.php?diff=64235&oldid=64234 5* 03A 5* (-100) 10 > 1562923641 203415 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 M10 02https://esolangs.org/w/index.php?diff=64236&oldid=64235 5* 03A 5* (+5) 10 < 1562924106 216388 :atslash!~atslash@static.231.107.9.5.clients.your-server.de QUIT :Quit: Leaving > 1562924142 986444 PRIVMSG #esoteric :14[[07Klaus/Dense14]]4 M10 02https://esolangs.org/w/index.php?diff=64237&oldid=64236 5* 03A 5* (+12) 10 < 1562924713 316052 :atslash!~atslash@static.231.107.9.5.clients.your-server.de JOIN :#esoteric < 1562927311 777966 :AnotherTest!~turingcom@ptr-82l26zcdc6imrwoapg3.18120a2.ip6.access.telenet.be JOIN :#esoteric > 1562928400 293378 PRIVMSG #esoteric :14[[07Playlist14]]4 N10 02https://esolangs.org/w/index.php?oldid=64238 5* 03A 5* (+1108) 10Created page with "[[Playlist]] is an esoteric programming language based on playlists. ==Rules of operation== Playlist operates over a playlist. There are a few commands in Playlist; they are..." > 1562928450 222670 PRIVMSG #esoteric :14[[07Playlist14]]4 M10 02https://esolangs.org/w/index.php?diff=64239&oldid=64238 5* 03A 5* (+91) 10 > 1562928539 500918 PRIVMSG #esoteric :14[[07Playlist14]]4 M10 02https://esolangs.org/w/index.php?diff=64240&oldid=64239 5* 03A 5* (+127) 10 > 1562928654 242503 PRIVMSG #esoteric :14[[07Playlist14]]4 M10 02https://esolangs.org/w/index.php?diff=64241&oldid=64240 5* 03A 5* (+65) 10/* Example programs */ < 1562929191 280611 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net JOIN :#esoteric < 1562929240 219208 :nfd!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net QUIT :Ping timeout: 246 seconds < 1562930733 267512 :xkapastel!uid17782@gateway/web/irccloud.com/x-qcvosjbhqrvrofik JOIN :#esoteric < 1562931985 759973 :Frater_EST!~adrianbib@wsip-68-15-198-210.ok.ok.cox.net PART :#esoteric < 1562932590 797245 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :@time < 1562932594 251446 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :Local time for shachaf is Fri Jul 12 04:56:31 2019 < 1562932626 31340 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :ski: This probably doesn't make much sense because it's a thought I had lying in bed at 5 in the morning, but I feel like linear logic par is actually obvious and straightforward. < 1562932705 804651 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It just means "or" in one aspect of the classical logic sense: A # B means that "at least one" of A,B is true. < 1562932758 636278 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Which means you can turn a refutation of A into a proof of B, and a refutation of B into a proof of A. Which is just the standard thing that document said. < 1562932787 591996 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Say, for any natural n, I can tell you that either n is odd or Sn is odd. That means that if you show me that n is even, then I can prove that Sn is odd, and vice versa. < 1562932809 266173 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :That all seems very simple so can someone remind me what's confusing about par? < 1562933084 126057 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :well, consider the proof that for any prime integer `p', if `p' divides `a*b', then `p' divides `a', or `p' divides `b' < 1562933131 492357 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :the standard proof of this has the basic shape "suppose `p' does not divide `a'. ... thus `p' divides `b'" < 1562933170 742177 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :which seems to me to be exactly the kind of thing that a proof of a multiplicative disjunction would be < 1562933245 331483 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :instead of "eagerly" pointing out which alternative we're to prove, we "lazily" wait for our opponent to disprove one disjunct, and only then do we prove the other one (possibly using information that we get from the disproof) > 1562933294 235549 PRIVMSG #esoteric :14[[07Klaus14]]4 M10 02https://esolangs.org/w/index.php?diff=64242&oldid=64225 5* 03A 5* (+108) 10No, it is TC < 1562933303 838624 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :however, when using this proof, what if we instead of disproving the first disjunct, instead disprove the second one ? < 1562933331 775528 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :then we'd have to be able to from that derive a proof of "`p' divides `a'" -- how does that work ? > 1562933338 699111 PRIVMSG #esoteric :14[[07Klaus14]]4 M10 02https://esolangs.org/w/index.php?diff=64243&oldid=64242 5* 03A 5* (+30) 10+CAT < 1562933349 370070 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :well, in this case, we're in a symmetric situation. but in general, that won't be the case < 1562933395 27252 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :so, it seems that one option would be to store both a function from disproof of left disjunct to proof of right disjunct, and a function from disproof of right disjunct to proof of left disjunct < 1562933457 691966 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :and here my creeping suspicion is coming in that perhaps, if we take any such pair of functions, then won't necessarily "correspond to each other" (whatever that means) < 1562933470 476134 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Here's one odd thing -- I think people end up with expressions like "A # A" in linear logic. I'm not quite sure what that would mean. < 1562933507 918039 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Probably because I'm now thinking of these things as truth values, which doesn't work. < 1562933528 419569 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :anyway, another option might be to analyze the construction from disproof of left disjunct to proof of right disjunct, in such a way that we can also interpret it as function from disproof of right disjunct to proof of left disjunct, effectively "reversing" it < 1562933554 450876 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I kind of like the fact that par is obviously symmetric, unlike functions. < 1562933582 199113 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :(But the connection to modus tollens that someone mentioned the other day is what made me think of this.) < 1562933602 495035 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :so, the one direction (considered as an intuitionistic function, via some forgetful, perhaps) would begat the other direction (which we can also consider in such a way), and then these two (the forgetful versions) would "correspond" in the desired way to each other < 1562933641 484447 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I'm not sure quite what you would want from such a correspondence. < 1562933686 147484 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Whatever it is it makes sense to want it to arise naturally from the way you write your proofs-or-whatever. < 1562933688 450987 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :yeah, by "in this case, we're in a symmetric situation. but in general, that won't be the case", i meant that it's not obvious how to reach from `A^- -> B^+' to `B^- -> A^+', where `A' and `B' may look quite different (as opposed to the above example) < 1562933740 790621 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :All your logic rules should presumably package up the forward and backward directions together. < 1562933752 602334 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :"it makes sense to want it to arise naturally from the way you write your proofs-or-whatever" -- yes < 1562933799 298699 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :but from a model-theoretic viewpoint, where we don't consider proofs ? < 1562933825 584492 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I don't know what you would want. < 1562933835 690653 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :ACTION neither .. < 1562933848 16380 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Informally, I think of "!a" as meaning something like "T & a & a*a & a*a*a & ..." -- a tensor of some number of copies of a, where you get to choose the number. < 1562933881 125985 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :The De Morgan dual of that would be (0 + a + a#a + a#a#a + ...) < 1562933888 78655 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What does that mean? < 1562933969 537721 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :As an implication, you can say that a#a#a = (~a*~a*~a -o _|_) < 1562933997 865463 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So it's a thing that takes some number of copies of ~a < 1562934035 785585 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Wait, instead of T I should have said 1, and instead of 0 I should have said _|_ < 1562934043 680009 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :anyway, you can perhaps consider a rule something like from `Gamma , n : neg A |- e : B' derive `Gamma |- {@n |-> e} : A # B' .. hmm < 1562934079 377183 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :the point being that we decide to "wait for" a refutaion of `A', and express the proof of `B' in terms of that < 1562934134 205228 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :re `!', in that case i'm also pondering if we want some kind of condition on that, to express that "all the `a's are copies of each other" < 1562934156 941814 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :(all the `a's in a single "term", i.e.) < 1562934197 88374 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :the `T & a & a*a & a*a*a & ...' means that we'll pick how many `a's we like, at least < 1562934231 237420 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :and so `0 + a + a#a + a#a#a + ...' means that the context (the opponent) will pick "how many `a's" we'll get fed by it < 1562934233 496709 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :(It's 1 & a & ..., not T & a & ... -- T is the unit of & and 1 is the unit of *, which was the one I meant.) < 1562934266 22089 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :(yea, but i write the additive truth as `1' anyway, so .. :) < 1562934280 331386 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :oh no < 1562934284 946316 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :(because it's terminal object) < 1562934298 823282 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :That's actually a pretty good reason. < 1562934324 145900 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :maybe. i'm not sure ;) < 1562934330 929090 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Thinking of "a" as a thing that's true or false, a#a makes no sense < 1562934343 753647 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :right < 1562934354 393508 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So that's not the thing to think in linear logic. Which I already knew of course. < 1562934396 872936 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :some systems have a "mix" rule that allows you to derive `A * B |- A # B', iirc < 1562934411 254626 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Yes. < 1562934421 620374 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :pretending that the computations corresponding to `A' and `B' communicate, while they actually don't < 1562934444 851541 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :and then you can prove `|- 1 # 1' (`1' being mult. truth) < 1562934466 537913 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I don't think I have a good feel for the meaning of the four units. < 1562934520 299855 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :`*' is "aggregation", and so `1' is "an empty space" < 1562934521 199547 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :​/srv/hackeso-code/multibot_cmds/lib/limits: line 5: exec: *': not found < 1562934620 259224 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :(er, i should have used `T' of course in `T # T', if i was intending to be consistent with myself. `T' being mult. truth) < 1562934635 380742 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :anyway, say you want to prove `T -o A' and `A -o _|_' (`_|_' being mult. false) < 1562934643 22179 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Do you have a + b |- a # b in any case? < 1562934645 755284 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :prove them together, i mean < 1562934660 735115 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, you shouldn't. < 1562934737 597173 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :hmm < 1562934840 813704 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :(i was trying to remember a point which i thought i had made in this situation. but now i'm not sure it's there. perhaps because i misremembered some details about the situation ?) < 1562934940 373097 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :@time < 1562934943 742829 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :Local time for shachaf is Fri Jul 12 05:35:40 2019 < 1562934948 250213 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I should go to sleep. < 1562934954 39193 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :hm, okay < 1562934979 169769 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Thanks for the help. I'll think about it more when I wake up. < 1562934983 625753 :ski!~ski@remote11.chalmers.se PRIVMSG #esoteric :ACTION nods < 1562936331 243417 :nfd!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net JOIN :#esoteric < 1562936334 270502 :arseniiv_!~arseniiv@136.169.229.227 JOIN :#esoteric < 1562936381 781540 :stux-!stux@cosmo.lunarshells.com JOIN :#esoteric < 1562936414 952293 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :Something I've just thought about < 1562936414 952346 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :Consider the category "2" which has two objects and a morphism between them < 1562936414 952355 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :I think there is an adjunction Set |- 2 (if I've got that notation right, I'm not very good at adjunctions) < 1562936414 952363 :arseniiv!~arseniiv@136.169.229.227 QUIT :Read error: Connection reset by peer < 1562936415 43318 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :Which maps the empty set to the codomain of the single non-identity arrow in 2, and all other sets to its domain < 1562936415 136659 :sftp!~sftp@unaffiliated/sftp QUIT :Excess Flood < 1562936431 256407 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :The reverse of this maps the codomain to the empty set and the domain to any non-empty set, e.g. {{}} < 1562936436 273331 :sftp!~sftp@unaffiliated/sftp JOIN :#esoteric < 1562936503 337249 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net QUIT :Ping timeout: 245 seconds < 1562936529 282894 :stux|away!stux@cosmo.lunarshells.com QUIT :Ping timeout: 245 seconds < 1562937449 438 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :So, par in linear logic. < 1562937547 814125 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Usually I just think of a # b as meaning ~a -o b, or equivalently ~b -o a, or equivalently ~(~a * ~b). < 1562937780 322342 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Let me try to remember here. There's a "protocol semantics" for linear logic. Any formula in linear logic represents a protocol. < 1562937858 988629 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Generally, you can submit a request to a protocol. After you do, you must wait for a response from that protocol. A protocol can "finish" after responding; if it does, then you have successfully consumed that protocol. However, a protocol can also finish *without* responding, in which case you have not successfully consumed the protocol. < 1562937903 238946 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :You know what, I don't think I'm making any sense. So I'm going to start over. < 1562937919 329017 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :There's a "ball game" semantics for linear logic. Any formula in linear logic represents a person who desires to participate in the game. < 1562937943 879054 :stux-!stux@cosmo.lunarshells.com QUIT :Quit: Aloha! < 1562937957 144452 :stux|away!stux@cosmo.lunarshells.com JOIN :#esoteric < 1562938011 223972 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Initially, you have the ball. In order to win the game (that is, in order to successfully consume the formula you are given), you must get everyone to leave the game, and you must possess the ball. < 1562938030 150198 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :The semantics of the various connectives are... < 1562938039 966914 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :1 - A player who goes home immediately. < 1562938074 478721 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Bot - A player who waits to be thrown the ball, and then takes the ball and goes home with it. < 1562938096 262056 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Top - A player who refuses to go home under any circumstances. < 1562938158 946391 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :0 - A player who allows you to win the game immediately, by sending all the other players home (even Top), taking any excess balls, and giving you a ball if you need one. < 1562938180 700780 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :a + b - A player who chooses either a or b to substitute for herself. < 1562938203 910766 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :a & b - A player who allows you to pick either a or b, and has the player you chose substitute for herself. < 1562938262 332874 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :a * b - A player who has both a and b standing behind her; when you throw her the ball, she will pass it on to either a or b (your choice), and also pass along any messages. When she receives the ball back from a or b, she throws it back to you. < 1562938678 560827 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :a # b - A player who has both a and b standing behind her, and also has a ball in her pocket. When you throw her the ball, she then throws one ball each to a and b. Whenever she gets a ball back from either one, she throws it back to you; her team then sits and waits to receive the ball again, at which point she will throw it to whichever of her two subordinates she most recently got the ball from. < 1562938792 340348 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :She will not go home until both of her subordinates have gone home and she has thrown you as many balls as you have thrown her. < 1562938824 800752 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Finally: < 1562938920 174133 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :~a - A player who waits to be thrown the ball, then behaves like *you* are a player of type "a". This player will not go home until she has won (that is, she's done what is necessary to make a player of type "a" go home, and she has the ball). < 1562938986 825311 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :So, all this explains why 1 # Bot can be successfully consumed, but 1 # 1 and Bot # Bot cannot be. < 1562939034 556867 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :In the case of 1 # Bot, 1 goes home immediately; # throws a ball to Bot, who goes home with it; and # throws the other ball to you and goes home. < 1562939045 85802 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :In the case of 1 # 1, both 1s go home immediately, so # has nobody to throw the extra ball to. < 1562939059 803980 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :And in the case of Bot # Bot, # throws a ball to each Bot, they both go home, and # will never get the ball back like she wants. < 1562939172 896562 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1562939374 885180 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 258 seconds < 1562939376 146526 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1562939431 793113 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Sorry for the tswettologue. :D < 1562942654 990369 :int-e!~noone@int-e.eu PRIVMSG #esoteric :⅋ is weird < 1562942711 813808 :xkapastel!uid17782@gateway/web/irccloud.com/x-qcvosjbhqrvrofik QUIT :Quit: Connection closed for inactivity < 1562943479 227660 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :I know I didn't get it *quite* right, but I think I was pretty close. < 1562943512 985401 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Way back when, I wanted to create a "linear Haskell" programming language. < 1562943527 704259 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :I remember I really liked whatever name I came up for it, but I don't remember what that name was. < 1562943645 133232 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Hylisk, that's it. < 1562943818 804213 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :I think the name was mostly arbitrary. It was chosen for how it has a lot of the sounds from "Haskell" and "linear". < 1562943838 973601 :user24!~user24@p2E50C34D.dip0.t-ipconnect.de JOIN :#esoteric < 1562943858 57722 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :It comes from the word "Hydralisk" from StarCraft, with the middle syllable dropped. < 1562944011 613387 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :I had the idea to give it a rather fun "disjointed lambda" syntax, where you could write definitions such as this one: < 1562944016 160141 :int-e!~noone@int-e.eu PRIVMSG #esoteric :mmm straight line haskell < 1562944034 738382 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :dual f = (f \x) -> x < 1562944073 587312 :int-e!~noone@int-e.eu PRIVMSG #esoteric :. o O ( I even hava a slogan for it: "Don't declare. Just do!" ) < 1562944080 462404 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :The type signature would be... < 1562944098 725345 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :dual :: ((a -> Bottom) -> Bottom) -> a < 1562944126 807078 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :So in context, f :: (a -> Bottom) -> Bottom; \x :: a -> Bottom; and x :: a. < 1562944160 371453 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :The -> operator sees an expression of type Bottom on the left, and a on the right, and forms an expression of type a. < 1562944506 551460 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :It expresses the following rule: given "X, (a -o Bot) |- Bot" and "Y, a |- b", form "X, Y |- b". < 1562948228 773701 :shotover!gilesgate@sdf-eu.org JOIN :#esoteric < 1562948508 482882 :shotover!gilesgate@sdf-eu.org QUIT :Client Quit < 1562948544 504606 :shotover!gilesgate@sdf-eu.org JOIN :#esoteric < 1562948720 465682 :moei!~moei@softbank221078042071.bbtec.net JOIN :#esoteric < 1562951880 323997 :user24!~user24@p2E50C34D.dip0.t-ipconnect.de QUIT :Quit: Leaving < 1562951948 585908 :budonyc!~budonyc@c-24-62-204-147.hsd1.ma.comcast.net QUIT :Ping timeout: 272 seconds < 1562952555 973154 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :ACTION waves to tswett[m]  < 1562952633 59612 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-vxonmuimljvqcvdw PRIVMSG #esoteric :Yo. < 1562952645 741870 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :how's life? < 1562953426 214179 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1562956133 963972 :int-e!~noone@int-e.eu PRIVMSG #esoteric :convoluted < 1562956153 104758 :int-e!~noone@int-e.eu PRIVMSG #esoteric :`" < 1562956154 25159 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :537) OMG What if we shoot Hitler with neutrinos \ 1080) boily: so i guess a really savvy glass programmer could make some money, maybe start a home based business of a profiler to spot outright dead code. macro-generated code often has big swaths of it. i'd hate learning cobol and fortran just for getting wiki work. < 1562956197 432599 :int-e!~noone@int-e.eu PRIVMSG #esoteric :^style < 1562956197 512844 :fungot!~fungot@2a01:4b00:82bb:1341::2 PRIVMSG #esoteric :Available: agora* alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp ukparl youtube < 1562956204 506863 :int-e!~noone@int-e.eu PRIVMSG #esoteric :^style irc < 1562956204 546826 :fungot!~fungot@2a01:4b00:82bb:1341::2 PRIVMSG #esoteric :Selected style: irc (IRC logs of freenode/#esoteric, freenode/#scheme and ircnet/#douglasadams) < 1562956214 74925 :int-e!~noone@int-e.eu PRIVMSG #esoteric :fungot: blasphemy < 1562956214 284520 :fungot!~fungot@2a01:4b00:82bb:1341::2 PRIVMSG #esoteric :int-e: just copy-pasted from http://en.wikipedia.org/ wiki/ irp < 1562957236 260491 :int-e!~noone@int-e.eu PRIVMSG #esoteric :@metar lowi < 1562957237 26982 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :LOWI 121820Z VRB04KT 9999 -RA FEW015 BKN050 OVC090 15/13 Q1015 TEMPO SHRA < 1562957279 629426 :int-e!~noone@int-e.eu PRIVMSG #esoteric :@metar loww < 1562957280 206920 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :LOWW 121820Z 28008KT 9999 FEW030CB SCT060 BKN300 21/12 Q1011 NOSIG < 1562957321 299815 :int-e!~noone@int-e.eu PRIVMSG #esoteric :@metar eddt < 1562957321 819015 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :EDDT 121820Z VRB02KT 9999 FEW025CB 20/14 Q1009 NOSIG < 1562958925 439993 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1562959979 534578 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :i like 537 because it's now an obscure reference to a very brief period in popular science > 1562960142 819419 PRIVMSG #esoteric :14[[07Esolang:General disclaimer14]]4 10 02https://esolangs.org/w/index.php?diff=64244&oldid=59371 5* 03Areallycoolusername 5* (+122) 10Import Compensation Notice > 1562960175 168540 PRIVMSG #esoteric :14[[07Esolang:General disclaimer14]]4 10 02https://esolangs.org/w/index.php?diff=64245&oldid=64244 5* 03Areallycoolusername 5* (+1) 10 < 1562961133 390884 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Taneb: I don't understand your adjunction. Where do the functors map the arrows? < 1562961161 673388 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :For example don't you need a function from {{}} to {}? < 1562964051 610616 :atslash!~atslash@static.231.107.9.5.clients.your-server.de QUIT :Quit: This computer has gone to sleep < 1562965266 271254 :arseniiv_!~arseniiv@136.169.229.227 PRIVMSG #esoteric : There's a "ball game" semantics for linear logic => the following was interesting! < 1562965590 365372 :arseniiv_!~arseniiv@136.169.229.227 NICK :arseniiv < 1562966804 797236 :AnotherTest!~turingcom@ptr-82l26zcdc6imrwoapg3.18120a2.ip6.access.telenet.be QUIT :Ping timeout: 252 seconds < 1562967490 806235 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Finally, now I implemented the ability to post articles with bystand. < 1562968253 334386 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :(It still isn't complete, though. Many additional stuff might be added/changed.) < 1562968615 240278 :arseniiv!~arseniiv@136.169.229.227 QUIT :Ping timeout: 246 seconds < 1562970302 263026 :budonyc!~budonyc@c-24-62-204-147.hsd1.ma.comcast.net JOIN :#esoteric < 1562972639 806742 :lambdabot!~lambdabot@haskell/bot/lambdabot QUIT :Quit: When will I be back? Only time will tell! < 1562972745 576391 :tromp_!~tromp@213.127.55.170 JOIN :#esoteric < 1562972914 518984 :tromp!~tromp@2a02:a210:1585:3200:a54b:884f:3036:801d QUIT :Ping timeout: 276 seconds < 1562973549 415363 :lambdabot!~lambdabot@haskell/bot/lambdabot JOIN :#esoteric < 1562973667 603021 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :lambdabot: Time has told. > 1562975026 718641 PRIVMSG #esoteric :14[[07Category:Works-in-Progress14]]4 M10 02https://esolangs.org/w/index.php?diff=64246&oldid=63964 5* 03Salpynx 5* (-31) 10Undo revision 63964 by [[Special:Contributions/A|A]] ([[User talk:A|talk]]) redundant category theory joke < 1562975461 270227 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 246 seconds < 1562975585 872475 :zzo38!~zzo38@24-207-15-213.eastlink.ca QUIT :Ping timeout: 248 seconds < 1562975631 426676 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: Well there's a Theseus problem... it's all newly compiled code now! < 1562975650 842055 :zzo38!~zzo38@24-207-15-213.eastlink.ca JOIN :#esoteric < 1562975736 466763 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Did you ship it? < 1562975804 417234 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I don't know how to answer that. (But I do see the pun.)