< 1603757687 971414 :deltaepsilon23!~deltaepsi@cpe-24-208-148-153.insight.res.rr.com NICK :delta23 < 1603757763 572447 :arseniiv!~arseniiv@136.169.204.164 PRIVMSG #esoteric :`? compass < 1603757767 280047 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :compass? ¯\(°​_o)/¯ < 1603757771 689751 :arseniiv!~arseniiv@136.169.204.164 PRIVMSG #esoteric :`? pass < 1603757773 41228 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :pass? ¯\(°​_o)/¯ < 1603757785 313710 :arseniiv!~arseniiv@136.169.204.164 PRIVMSG #esoteric :`? password < 1603757786 765076 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :The password of the month is Algol Waterloo Athens aftermath quadrant hydraulic tissue exodus stormy decadence egghead resistor flatfoot escapade newborn recipe < 1603757804 482160 :arseniiv!~arseniiv@136.169.204.164 PRIVMSG #esoteric :eh < 1603757838 876385 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :yeah, I grabbed it at the start of this month < 1603759166 584970 :sftp!~sftp@unaffiliated/sftp QUIT :Ping timeout: 258 seconds < 1603759213 173828 :sftp!~sftp@unaffiliated/sftp JOIN :#esoteric < 1603759976 449100 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 240 seconds < 1603759979 108297 :Lord_of_Life_!~Lord@46.217.223.11 JOIN :#esoteric < 1603760086 547887 :arseniiv!~arseniiv@136.169.204.164 QUIT :Ping timeout: 246 seconds < 1603763105 121225 :sftp!~sftp@unaffiliated/sftp QUIT :Ping timeout: 240 seconds < 1603765841 945124 :sftp!~sftp@unaffiliated/sftp JOIN :#esoteric < 1603771663 693461 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com JOIN :#esoteric < 1603772761 523890 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com QUIT :Ping timeout: 264 seconds < 1603774247 530500 :adu!~arobbins@c-76-111-99-194.hsd1.md.comcast.net JOIN :#esoteric < 1603774925 905429 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com JOIN :#esoteric < 1603776758 905441 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com QUIT :Ping timeout: 260 seconds < 1603778846 884769 :Bowserinator!Bowserinat@hellomouse/dev/Bowserinator QUIT :Ping timeout: 256 seconds < 1603778892 870264 :moony!moony@hellomouse/dev/moony QUIT :Ping timeout: 260 seconds < 1603778893 910688 :ATMunn!ATMunn@gateway/shell/hellomouse/x-nflyrazfhwlwduwy QUIT :Ping timeout: 260 seconds < 1603778901 277745 :iovoid!iovoid@hellomouse/dev/iovoid QUIT :Ping timeout: 272 seconds < 1603780346 474635 :aaaaaa!~ArthurStr@host-91-90-11-13.soborka.net QUIT :Quit: leaving < 1603783008 835588 :tromp!~tromp@dhcp-077-249-230-040.chello.nl QUIT :Remote host closed the connection < 1603783532 7891 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com JOIN :#esoteric < 1603783850 535320 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1603784091 997760 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com QUIT :Ping timeout: 256 seconds < 1603784238 533659 :adu!~arobbins@c-76-111-99-194.hsd1.md.comcast.net QUIT :Quit: adu < 1603784273 263008 :ATMunn!ATMunn@hellomouse.net JOIN :#esoteric < 1603784309 798433 :Bowserinator!Bowserinat@hellomouse/dev/Bowserinator JOIN :#esoteric < 1603784573 272025 :iovoid!iovoid@hellomouse/dev/iovoid JOIN :#esoteric < 1603784601 217126 :moony!moony@hellomouse/dev/moony JOIN :#esoteric < 1603785192 927372 :tromp!~tromp@dhcp-077-249-230-040.chello.nl JOIN :#esoteric < 1603785289 731663 :wesleyac!~wesleyac@bouncer.wesleyac.com QUIT :Quit: ZNC 1.8.2 - https://znc.in < 1603785298 529225 :wesleyac!~wesleyac@bouncer.wesleyac.com JOIN :#esoteric < 1603785508 951200 :tromp!~tromp@dhcp-077-249-230-040.chello.nl QUIT :Ping timeout: 260 seconds < 1603785565 86391 :tromp!~tromp@dhcp-077-249-230-040.chello.nl JOIN :#esoteric < 1603786075 339367 :hendursa1!~weechat@gateway/tor-sasl/hendursaga JOIN :#esoteric < 1603786192 184335 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 260 seconds < 1603786223 718741 :hendursaga!~weechat@gateway/tor-sasl/hendursaga QUIT :Ping timeout: 240 seconds < 1603788555 96791 :Lord_of_Life_!~Lord@46.217.223.11 NICK :Lord_of_Life < 1603790830 149430 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com JOIN :#esoteric > 1603791186 994989 PRIVMSG #esoteric :14[[075D Brainfuck With Multiverse Time Travel14]]4 M10 02https://esolangs.org/w/index.php?diff=78175&oldid=78149 5* 03RocketRace 5* (+140) 10Recommended race condition strategies < 1603791231 763021 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 260 seconds < 1603792838 461685 :arseniiv!~arseniiv@136.169.204.164 JOIN :#esoteric < 1603793120 171215 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com QUIT :Ping timeout: 272 seconds < 1603793943 361281 :t20kdc!~20kdc@cpc139384-aztw33-2-0-cust220.18-1.cable.virginm.net JOIN :#esoteric < 1603794253 621805 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :There's an awful lot of maths out there < 1603794272 108818 :delta23!~deltaepsi@cpe-24-208-148-153.insight.res.rr.com QUIT :Quit: Leaving < 1603794405 239910 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com JOIN :#esoteric < 1603798621 149530 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Pfft, tfw you work half an hour building a stack of boxes to reach an area that turns out to be supposedly unreachable :) < 1603798696 390908 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :int-e: ...context? < 1603798944 686342 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Amnesia: The Dark Descent. I guess my reward is a closeup of this https://int-e.eu/~bf3/tmp/halla.jpg ... stack of boxes from above: https://int-e.eu/~bf3/tmp/outofbounds.jpg < 1603798974 610225 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :Ahaha < 1603798982 87033 :int-e!~noone@int-e.eu PRIVMSG #esoteric :the latter also has a few wooden boards whose backside face is missing. < 1603799041 918484 :int-e!~noone@int-e.eu PRIVMSG #esoteric :which is a strong indication that the designers didn't think the area could be reached. < 1603799052 252572 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :heh < 1603799060 4938 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :'hallå!', cute < 1603799063 33034 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :lit. 'hi!' < 1603799108 6012 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Yeah you can get a glimpse of that from a comparatively small stack of boxes. < 1603799121 954598 :int-e!~noone@int-e.eu PRIVMSG #esoteric :And one that actually looks climbable ;) < 1603799147 563749 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :is swedish like, a thing in the settnig of amnesia, or is the sign/message just an easter egg? < 1603799157 872297 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :setting* < 1603799169 221630 :int-e!~noone@int-e.eu PRIVMSG #esoteric :the latter < 1603799173 278076 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :makes sense < 1603799185 509503 :int-e!~noone@int-e.eu PRIVMSG #esoteric :language is english < 1603799187 607973 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :I played a tiny, tiny bit of penumbra but it was too terrifying fro me < 1603799189 159756 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :for* < 1603799194 516140 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :why am I so typoful today.. < 1603799352 375177 :FireFly!znc@freenode/staff/firefly PRIVMSG #esoteric :I don't think horror is my thing < 1603799355 749048 :int-e!~noone@int-e.eu PRIVMSG #esoteric :https://en.wikipedia.org/wiki/Frictional_Games is a swedish company though < 1603799386 40931 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Which is what I thought, but I wasn't sure.) < 1603799400 555764 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I'm not sure it's for me either. < 1603799433 394933 :int-e!~noone@int-e.eu PRIVMSG #esoteric :This is before it gets really scary though. < 1603799624 391889 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Just for completeness, this is the same stack from below https://int-e.eu/~bf3/tmp/boxes.jpg < 1603799663 797146 :int-e!~noone@int-e.eu PRIVMSG #esoteric :and initially those boxes were distributed over about 3 rooms. < 1603799708 939424 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Oh well. I kind of hoped for a proper secret area, so this is a bit disapppointing :) < 1603800323 528172 :arseniiv!~arseniiv@136.169.204.164 PRIVMSG #esoteric :hello bye! < 1603800325 424322 :arseniiv!~arseniiv@136.169.204.164 QUIT :Quit: gone too far < 1603800336 575863 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :I've been looking at this "reMarkable 2" device. Cons: a bit expensive, tips of the pens apparently wear out over time. Pros: seems quite hackable, all members of the GitHub org of the company that makes it have photos of cats as their profile pictures on GitHub. < 1603800354 239629 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Especially that last bit's pretty compelling. < 1603800399 767475 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :i baught a likebook with a pen for about half the price < 1603800412 435921 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :it runs on an older version of android, pretty hackable < 1603800451 451548 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Does the screen feel like glass or like paper? I've got a ChromeOS tablet with a pen on it, and it just doesn't do it for me. < 1603800494 366273 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :it's not as smooth as glass, but i wouldn't call it paper < 1603800930 796920 :arseniiv!~arseniiv@136.169.204.164 JOIN :#esoteric < 1603802458 738989 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :i am a bit angry that the noteslate pretty much never really came to be < 1603802577 891084 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :i heard about it like 6 or 7 years ago and got excited. now you can "pre-order" on the web page with shipping expected in august 2016 > 1603802723 595504 PRIVMSG #esoteric :14[[075D Brainfuck With Multiverse Time Travel14]]4 10 02https://esolangs.org/w/index.php?diff=78176&oldid=78175 5* 03RocketRace 5* (+141) 10Yeet pointers into the void < 1603803730 805816 :hendursa1!~weechat@gateway/tor-sasl/hendursaga QUIT :Quit: hendursa1 < 1603803749 734067 :hendursaga!~weechat@gateway/tor-sasl/hendursaga JOIN :#esoteric < 1603803853 302308 :hendursaga!~weechat@gateway/tor-sasl/hendursaga QUIT :Client Quit < 1603803865 726162 :hendursaga!~weechat@gateway/tor-sasl/hendursaga JOIN :#esoteric > 1603804349 97003 PRIVMSG #esoteric :14[[07Eternity14]]4 10 02https://esolangs.org/w/index.php?diff=78177&oldid=72746 5* 03Jabutosama 5* (+17) 10added year category < 1603804526 410322 :tromp!~tromp@dhcp-077-249-230-040.chello.nl QUIT :Remote host closed the connection > 1603804586 111684 PRIVMSG #esoteric :14[[075D Brainfuck With Multiverse Time Travel14]]4 10 02https://esolangs.org/w/index.php?diff=78178&oldid=78176 5* 03RocketRace 5* (+105) 10Interpreter < 1603805581 810963 :tromp!~tromp@dhcp-077-249-230-040.chello.nl JOIN :#esoteric < 1603807208 649251 :rain1!~rain1@unaffiliated/rain1 QUIT :Quit: Leaving < 1603807788 12091 :rain1!~rain1@unaffiliated/rain1 JOIN :#esoteric > 1603808025 291441 PRIVMSG #esoteric :14[[07AAEEEEEEEEEI14]]4 10 02https://esolangs.org/w/index.php?diff=78179&oldid=65118 5* 03Jabutosama 5* (-2504) 10 > 1603808053 40447 PRIVMSG #esoteric :14[[07AAEEEEEEEEEI14]]4 10 02https://esolangs.org/w/index.php?diff=78180&oldid=78179 5* 03Jabutosama 5* (-211) 10 < 1603808347 86626 :Frater_EST!~adrianbib@75.107.60.35 JOIN :#esoteric < 1603808420 755655 :Frater_EST!~adrianbib@75.107.60.35 QUIT :Read error: Connection reset by peer < 1603808983 696794 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1603809086 722974 :Arcorann_!~awych@121-200-5-186.79c805.syd.nbn.aussiebb.net QUIT :Read error: Connection reset by peer < 1603810035 81173 :t20kdc!~20kdc@cpc139384-aztw33-2-0-cust220.18-1.cable.virginm.net QUIT :Ping timeout: 265 seconds < 1603810510 73047 :t20kdc!~20kdc@cpc139384-aztw33-2-0-cust220.18-1.cable.virginm.net JOIN :#esoteric < 1603813962 179981 :Frankenlime!nchambers@learnprogramming/staff/nchambers QUIT :Quit: quit < 1603813974 379071 :also_uplime!nchambers@learnprogramming/staff/nchambers JOIN :#esoteric < 1603814606 773054 :tromp!~tromp@dhcp-077-249-230-040.chello.nl QUIT :Remote host closed the connection < 1603814735 781759 :imode!~linear@unaffiliated/imode JOIN :#esoteric > 1603814736 797202 PRIVMSG #esoteric :14[[07Talk:Modulous14]]4 M10 02https://esolangs.org/w/index.php?diff=78181&oldid=78019 5* 03Abyxlrz 5* (+21) 10 < 1603814878 988553 :FreeFull!~freefull@defocus/sausage-lover QUIT :Remote host closed the connection < 1603814952 799343 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1603815161 24474 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net JOIN :#esoteric < 1603815858 546721 :tromp!~tromp@dhcp-077-249-230-040.chello.nl JOIN :#esoteric > 1603816573 371004 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03Mantita223 5* 10New user account > 1603816757 106614 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=78182&oldid=78137 5* 03Mantita223 5* (+128) 10/* Introductions */ > 1603816779 29477 PRIVMSG #esoteric :14[[07User:Mantita22314]]4 N10 02https://esolangs.org/w/index.php?oldid=78183 5* 03Mantita223 5* (+2) 10Created page with "hi" < 1603816828 524702 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :joy seems to have a lot of combinators that it comes packed with. < 1603816838 538660 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :without a concrete explanation of what those combinators are. < 1603816984 173518 :dcristofani!~dcristofa@69-71-183-170.mammothnetworks.com QUIT :Ping timeout: 272 seconds < 1603818292 162432 :imode!~linear@unaffiliated/imode QUIT :Quit: WeeChat 2.9 < 1603819388 800573 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric < 1603821161 548871 :aaaaaa!~ArthurStr@host-91-90-11-13.soborka.net JOIN :#esoteric < 1603821815 894790 :orbitaldecay!c1941244@193.148.18.68 JOIN :#esoteric < 1603821833 303157 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :Greetings all < 1603822121 388446 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :I'm trying to wrap my head around the feasibility of developing an automatic SKI programmer (i.e. you feed the program constraints and it generates a SKI program that satisfies those constraints). If you think of SKI calculus as a term rewriting system, then there are E unification algorithms that do this for *convergent* term rewrite systems. Do < 1603822121 846677 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :any of you know if there are any semidecidable unification algorithms that would meet my needs or am I barking up the wrong tree for this? < 1603822151 142958 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1603822159 441151 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :what sort of constraints are you thinking of? < 1603822169 511114 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :It's hard to find places to ask these kind of questions, so forgive me for being a little off topic. < 1603822174 670065 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :automated lambda calculus → SKI translation exists (and vice versa), but I'm not sure I understand the problem < 1603822192 780477 :arseniiv!~arseniiv@136.169.204.164 QUIT :Ping timeout: 256 seconds < 1603822281 91773 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :ais523: For example, if there were a unification algorithm that worked for this, then it would be possible to provide the equation (c) (b) (a) apply apply = (b) and the unification algorithm would solve for (a) (b) (c), ideally finding the most general unifier, which would be (a) = K, (b) = (b), (c) = (c) < 1603822294 977746 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :(postfix) < 1603822337 149580 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :Equality here would represent beta equality, as can be deduced from rewrite rules < 1603822383 95926 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :I suspect that there is no decidable algorithm that does this, but I'd settle for semidecidable < 1603822396 225727 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :or rather, that this problem is not decidabe < 1603822397 678321 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :hi < 1603822398 714645 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :*decidable < 1603822400 672192 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :hi rain < 1603822406 408150 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1603822422 205748 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's probably decidable if the hardcoded parts of the program are simple enough < 1603822438 882642 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :you can write a computer program that will try to produce SKI terms that do certain things, and it can often succeed < 1603822441 492971 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :my reaction is that the only thing that would make it undecidable would be if the hardcoded parts of the program somehow ended up Turing-complete < 1603822501 555654 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :yeah, it get's tricky, because E unification is *in general* undecidable, but for specific equational theories it's either semidecidable, or completely decidable < 1603822527 837398 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :what's the exact problem in terms of input and output < 1603822578 792408 :ais523!~ais523@unaffiliated/ais523 QUIT :Read error: Connection reset by peer < 1603822590 271683 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :E unification is decidable modulo a convergent term rewrite system for an equational theory, but SKI as a term rewrite system is not convergent < 1603822599 416782 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :and any TC rewrite system won't be convergent < 1603822649 674436 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1603822651 750865 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I guess our language is ` s k i (Unlambda-style, not Underload-style) < 1603822672 826076 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :Either language would be interesting to look at, but I've been thinking in unlambda style so far < 1603822685 887917 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and we have an expression made of ` and some unknowns (not sure about if s k i themselves are needed) < 1603822686 513656 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :in theory, the same idea applies to both as we're just thinking of them as term rewrite systems < 1603822692 486945 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :two such expressions < 1603822695 366407 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and need to make them equal < 1603822699 381137 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :yep < 1603822716 621341 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :I *think* this is best thought of as a unification problem < 1603822722 196135 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :but there are other ways of thinking about it < 1603822746 350315 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :i dont understand the specifics of "automatic SKI programmer" < 1603822748 157753 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :expressions of the form ````…`AB…X = (insert arbitrary data structure which doesn't contain A here) are equivalent to the lambda→unlambda compilation < 1603822761 317382 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :is the input a list of equations like X a b c = b(cbb) < 1603822763 432057 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :and it finds X < 1603822766 835040 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so that's one fairly useful class that can be solved < 1603822770 767968 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :rain1: yes < 1603822777 450123 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :this problem is trivial < 1603822787 80314 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :How so? < 1603822810 61310 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :say you have ```Xabc = `b``cbb < 1603822831 143516 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :you can move the applys through the equals, to get X = \a.\b.\c.`b``cbb < 1603822851 267813 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :then the conversion of the nested lambda to SKI has known, entirely mechanical techniques < 1603822861 237987 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :That was more directed at rain1, but thank you for clarifying ais523 < 1603822872 744000 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I thought it might be, but decided to clarify anyway < 1603822879 801398 :arseniiv!~arseniiv@136.169.204.164 JOIN :#esoteric < 1603822885 593331 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :especially as rain1 may be thinking only of this class of equations when saying "this problem is trivial" < 1603822897 863013 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :I suspect where we'll likely run into issues is with programs that necessarily require fixed point combinators in their solution < 1603822921 708146 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :right, say if X appears on both sides < 1603822928 178833 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :exactly < 1603822933 919668 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :you can still mechanically generate a solution *but* it may correspond to an infinite loop, not the answer you want < 1603822936 976232 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :wait, that's usually backwards < 1603822942 655796 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :the lambda form X = < 1603822943 590925 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :just like fixed point combinators in other languages < 1603822955 460695 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :oh, should be \c.\b.\a, right < 1603822970 84366 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :X = \a.someexpr implies the equation Xa = someexpr < 1603822988 928897 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :but if you go backwards, you need equality up to something < 1603823004 148000 :ais523!~ais523@unaffiliated/ais523 QUIT :Remote host closed the connection < 1603823010 325313 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :what semantics do you even assign to your original eqution system < 1603823016 589245 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1603823041 356157 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :b_jonas: I'm approaching SKI as a term rewrite system in this instance, so it's equality modulo beta reduction < 1603823042 684265 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :b_jonas: I'm using observational equality here, e.g. same inputs produce same outputs < 1603823054 96685 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :Ah, got it < 1603823096 967787 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :I was really only worried about equality modulo beta reduction, as I figured that'd be a lot simpler < 1603823136 253313 :tromp!~tromp@dhcp-077-249-230-040.chello.nl QUIT :Remote host closed the connection < 1603823136 438131 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :>> let x a = 4/a in fix x < 1603823139 968847 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let x a = 4/a in fix x < 1603823142 984288 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : *Exception: <> < 1603823147 673810 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :the difficult problem is to find X when given equations like X S K = K < 1603823155 13322 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :the problem with fixed point combinators is < 1603823168 425730 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :ideally you would want that to output 2, rather than getting stuck in an infinite loop < 1603823188 640954 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :rain1: there are clearly an infinite number of unequal such X < 1603823213 401179 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :-2 is also a valid fixed point < 1603823265 653485 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :Yeah, certain unification theories have proof of the existence of a "most general unifier" which would be, in your case rain1, an X such that all other X's can be derived from it, but E unification does not generally have this < 1603823280 721818 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :a quadratic equation! we have a solver for that < 1603823292 744365 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :yes < 1603823306 427640 :rain1!~rain1@unaffiliated/rain1 QUIT :Quit: Leaving < 1603823341 456363 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :sage: x=var("x"); (x == 4/x).solve(x) < 1603823342 867821 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :[x == -2, x == 2] < 1603823352 35207 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :if I go to all this trouble to install a CAS, may as well use it for this sort of thing < 1603823369 225988 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :(y) < 1603823371 396561 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it wouldn't be hard to rejig that into a fixed-point operator, although I don't know what sorts of function it would work on < 1603823408 904641 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1603823506 609810 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :I'm thinking in the space between SKI and prolog and it's very strange territory < 1603823515 444760 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :simplest polynomial on which it fails appears to be x⁵ - x == 1, that makes sense < 1603823519 78510 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :sage is like a meta-CAS, it is bundled with a bunch of other CASes and can also use multiple commercial ones < 1603823527 11961 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :(this is the simplest polynomial with provably no solution in radicals) < 1603823538 593760 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :b_jonas: right, I think of it like glue for CASes < 1603823550 344675 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :you just write the problem you want and it figures out which CAS to use to solve it < 1603823552 36066 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :the sort of glue like bash is < 1603823564 398864 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :ugly but usable < 1603823579 882544 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :although, this means it probably isn't very good at complex problems that go through multiple domains because I wouldn't expect it to port your data structure from one CAS to another < 1603823722 348709 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :sage: x=var("x"); find_root(x**5 - x == 1,1,2) < 1603823723 664096 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :1.1673039782615173 < 1603823736 792560 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it can find it numerically even if it can't find it symbolically < 1603823835 814779 :Lord_of_Life!~Lord@46.217.223.11 QUIT :Changing host < 1603823835 814845 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1603823896 5635 :rain1!~rain1@unaffiliated/rain1 JOIN :#esoteric < 1603824164 882752 :tromp!~tromp@dhcp-077-249-230-040.chello.nl JOIN :#esoteric < 1603824539 377864 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :My final thoughts on this are the following: If we think about the naive algorithm of unifyiing an expression like X Y Z ` ` = Y in SKI calculus (i.e. iterating through all programs until we find one that works), it's clear to see why convergent rewrite rules are required because as we're iterating through those programs we might find one that < 1603824539 862821 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :doesn't terminate (in term rewriting language, doesn't converge). So I'm thinking that unifying a TC term rewriting system is always going to be undecidable. < 1603824662 278873 :orbitaldecay!c1941244@193.148.18.68 PRIVMSG #esoteric :So this might be a project for a sub Turing language < 1603824857 726232 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :ais523: anyway, that doesn't mean that the case that orbital asked about is hopeless, because such an equation is not pure combinator calculus, and you can't encode it to pure combinator calculus. you don't have a way to force (fix x) to be a number (whatever kind) with equations. < 1603824942 45382 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :b_jonas: indeed < 1603824990 101638 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :it can just give you (fix ) where fix is a fixed point combinator and so (fix x) < 1603825004 722344 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :give you (fix \a -> 4/a) where fix is a fixed point combinator and so (fix x) diverges < 1603825087 32567 :b_jonas!~x@catv-176-63-12-22.catv.broadband.hu PRIVMSG #esoteric :but there also won't always be a solution, because you can write some contradictory equations like X = k; X = `ki < 1603825148 278490 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :minikanren can discover a quine, can it discover a y combinator? < 1603826090 751192 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I just realised that a quine is basically just a fixed point of an interpreter < 1603826150 642352 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :This reminds me, one time I thought quines are related to Lawvere's fixed point theorem (and are constructed the same way), but then I wasn't sure the details worked out. < 1603826205 609013 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I should figure out the details. < 1603826337 200752 :rain1!~rain1@unaffiliated/rain1 PRIVMSG #esoteric :is kleenes fixed point theorem related to lawveres? < 1603826357 318152 :deltaepsilon23!~deltaepsi@cpe-24-208-148-153.insight.res.rr.com JOIN :#esoteric < 1603826376 92040 :deltaepsilon23!~deltaepsi@cpe-24-208-148-153.insight.res.rr.com NICK :delta23 < 1603826412 570187 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm, it looks more like Tarski's to me. > 1603826814 116978 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03Dregni 5* 10New user account > 1603826957 886302 PRIVMSG #esoteric :14[[07Special:Log/move14]]4 move10 02 5* 03SunnyMoon 5* 10moved [[029910]] to [[99 (Joke language)]]: There is another language called 99. > 1603826957 971608 PRIVMSG #esoteric :14[[07Special:Log/move14]]4 move10 02 5* 03SunnyMoon 5* 10moved [[02Talk:9910]] to [[Talk:99 (Joke language)]]: There is another language called 99. > 1603826989 684922 PRIVMSG #esoteric :14[[079914]]4 10 02https://esolangs.org/w/index.php?diff=78188&oldid=78185 5* 03SunnyMoon 5* (-32) 10This is left for something else now... > 1603827149 919903 PRIVMSG #esoteric :14[[0799 (disambiguation)14]]4 N10 02https://esolangs.org/w/index.php?oldid=78189 5* 03SunnyMoon 5* (+102) 10Disambiguation page created! > 1603827251 801565 PRIVMSG #esoteric :14[[079914]]4 10 02https://esolangs.org/w/index.php?diff=78190&oldid=78188 5* 03SunnyMoon 5* (+33) 10To the disambiguation page we go! > 1603827293 57652 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=78191&oldid=78182 5* 03Dregni 5* (+206) 10/* Introductions */ > 1603827363 632684 PRIVMSG #esoteric :14[[0799 (disambiguation)14]]4 M10 02https://esolangs.org/w/index.php?diff=78192&oldid=78189 5* 03SunnyMoon 5* (+4) 10Oh, it is italic... > 1603827520 793814 PRIVMSG #esoteric :14[[0799 (disambiguation)14]]4 M10 02https://esolangs.org/w/index.php?diff=78193&oldid=78192 5* 03SunnyMoon 5* (+13) 10Finally! > 1603827647 332971 PRIVMSG #esoteric :14[[07User:Dregni14]]4 N10 02https://esolangs.org/w/index.php?oldid=78194 5* 03Dregni 5* (+378) 10Dregni BrainFuckFart dev > 1603827933 295310 PRIVMSG #esoteric :14[[07User talk:Dregni14]]4 N10 02https://esolangs.org/w/index.php?oldid=78195 5* 03Dregni 5* (+34) 10Created page with "I don't know what I'm doing tbh..." > 1603829861 196547 PRIVMSG #esoteric :14[[0799 (Esolang)14]]4 N10 02https://esolangs.org/w/index.php?oldid=78196 5* 03SunnyMoon 5* (+239) 10Will finish this. I need to go to sleep :( > 1603830117 544500 PRIVMSG #esoteric :14[[07User talk:Dregni14]]4 10 02https://esolangs.org/w/index.php?diff=78197&oldid=78195 5* 03Dregni 5* (+1049) 10/* BrainFuckFart */ new section > 1603830135 936230 PRIVMSG #esoteric :14[[07User talk:Dregni14]]4 10 02https://esolangs.org/w/index.php?diff=78198&oldid=78197 5* 03Dregni 5* (-2) 10/* BrainFuckFart */ > 1603830196 698451 PRIVMSG #esoteric :14[[07User talk:Dregni14]]4 10 02https://esolangs.org/w/index.php?diff=78199&oldid=78198 5* 03Dregni 5* (+10) 10/* Open to */ > 1603831050 53627 PRIVMSG #esoteric :14[[07BrainFuckFart14]]4 N10 02https://esolangs.org/w/index.php?oldid=78200 5* 03Dregni 5* (+1055) 10Created page with "= BrainFuckFart = == BrainFuckFart a surprisingly fun language == === Concept === I started creating BrainFuckFart as a simple C++ interpreter for BrainFuck. As I went and..." > 1603831070 317935 PRIVMSG #esoteric :14[[07Language list14]]4 10 02https://esolangs.org/w/index.php?diff=78201&oldid=78166 5* 03Dregni 5* (+20) 10/* B */ < 1603831216 33153 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Quit: Quittin'. < 1603831239 943273 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1603832321 25887 :^[_!sid43445@gateway/web/irccloud.com/x-gnsjjoiabatnywnb QUIT :*.net *.split < 1603832321 25937 :dog_star!sid310875@gateway/web/irccloud.com/x-bkwcarqglktqystl QUIT :*.net *.split < 1603832321 104028 :ocharles!sid30093@musicbrainz/user/ocharles QUIT :*.net *.split < 1603832321 605685 :paul2520!~paul2520@unaffiliated/paul2520 QUIT :*.net *.split < 1603832331 996263 :dog_star!sid310875@gateway/web/irccloud.com/x-euscgudbdkpfhztd JOIN :#esoteric < 1603832334 219192 :ocharles!sid30093@musicbrainz/user/ocharles JOIN :#esoteric < 1603832336 721153 :paul2520!~paul2520@paulkaefer.com JOIN :#esoteric < 1603832336 836603 :paul2520!~paul2520@paulkaefer.com QUIT :Changing host < 1603832336 836642 :paul2520!~paul2520@unaffiliated/paul2520 JOIN :#esoteric < 1603832348 931687 :^[_!sid43445@gateway/web/irccloud.com/x-iztepeaguyumtzta JOIN :#esoteric < 1603833078 537127 :deltaepsilon23!~deltaepsi@cpe-24-208-148-153.insight.res.rr.com JOIN :#esoteric < 1603833206 73995 :delta23!~deltaepsi@cpe-24-208-148-153.insight.res.rr.com QUIT :Ping timeout: 265 seconds < 1603833222 159671 :deltaepsilon23!~deltaepsi@cpe-24-208-148-153.insight.res.rr.com NICK :delta23 < 1603833447 751020 :orbitaldecay!c1941244@193.148.18.68 QUIT :Remote host closed the connection < 1603837560 780706 :arseniiv!~arseniiv@136.169.204.164 QUIT :Ping timeout: 256 seconds < 1603837996 598050 :ineiros!ineiros@kapsi.fi QUIT :Ping timeout: 246 seconds < 1603838100 160454 :ineiros!ineiros@kapsi.fi JOIN :#esoteric < 1603839803 876991 :hendursaga!~weechat@gateway/tor-sasl/hendursaga QUIT :Ping timeout: 240 seconds < 1603839910 909786 :hendursaga!~weechat@gateway/tor-sasl/hendursaga JOIN :#esoteric < 1603840107 958041 :Arcorann_!~awych@121-200-5-186.79c805.syd.nbn.aussiebb.net JOIN :#esoteric > 1603840394 151708 PRIVMSG #esoteric :14[[07Talk:BrainFuckFart14]]4 N10 02https://esolangs.org/w/index.php?oldid=78202 5* 03Pipythonmc 5* (+269) 10Why is this in first person, and who even is the author? Needs fixing > 1603840506 143317 PRIVMSG #esoteric :14[[07BrainFuckFart14]]4 10 02https://esolangs.org/w/index.php?diff=78203&oldid=78200 5* 03Pipythonmc 5* (+10) 10Add stub template < 1603840730 735529 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr QUIT :Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.” > 1603842084 496333 PRIVMSG #esoteric :14[[07BrainFuckFart14]]4 10 02https://esolangs.org/w/index.php?diff=78204&oldid=78203 5* 03Pipythonmc 5* (+2155) 10Add command table from github with some grammar fixes > 1603842318 493048 PRIVMSG #esoteric :14[[07Talk:BrainFuckFart14]]4 10 02https://esolangs.org/w/index.php?diff=78205&oldid=78202 5* 03Pipythonmc 5* (+352) 10Add talk page entry < 1603842417 467676 :user3456!user3456@gateway/shell/insomnia247/x-zsntqrknwqoshzrw PRIVMSG #esoteric :wow, adding the table of commands tripled the character count