< 1424304026 299801 :dulla!~rikc@108-65-78-116.lightspeed.sntcca.sbcglobal.net PRIVMSG #esoteric ::^) < 1424304185 876364 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :http://orteil.dashnet.org/randomgen/?gen=http://mdude1350.webs.com/generators/random-code/one-liner.txt < 1424304425 569964 :wool!47b76c17@gateway/web/freenode/ip.71.183.108.23 JOIN :#esoteric < 1424304553 751877 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :http://wurstcaptures.untergrund.net/music/?oneliner=(Math.log(sin(215%26t)))-(Math.sqrt(124%7Ct))%2Bcos((tan(t))%26201%7Ct)%20&oneliner2=(Math.log(sin(215%26t)))-(Math.sqrt(124%7Ct))%2Bsin(sin(cos(117%7Ct)))&t0=0&tmod=0&duration=30&separation=100&rate=8000 < 1424304699 497400 :dulla!~rikc@108-65-78-116.lightspeed.sntcca.sbcglobal.net PRIVMSG #esoteric :fucking byte bytes < 1424304705 556128 :dulla!~rikc@108-65-78-116.lightspeed.sntcca.sbcglobal.net PRIVMSG #esoteric :byte beats < 1424304869 734082 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Random number generator is not always the best composer. < 1424304887 801519 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :But it did come up with this as I was typing that: http://wurstcaptures.untergrund.net/music/?oneliner=t%3E%3E(sin(t*28))%7Ct%20&oneliner2=t%3E%3E(198-t*(Math.log(t%7C62)))%2F(cos(cos(233%3E%3Et)))&t0=0&tmod=0&duration=30&separation=100&rate=8000 < 1424304983 913255 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :girl genius late < 1424305113 43826 :dulla!~rikc@108-65-78-116.lightspeed.sntcca.sbcglobal.net PRIVMSG #esoteric :that weird comic? < 1424305414 416802 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :http://wurstcaptures.untergrund.net/music/?oneliner=Math.sqrt(81*t)%3E%3Et%25121%20&oneliner2=Math.sqrt(81*t)%3E%3Et&t0=0&tmod=0&duration=30&separation=100&rate=8000 < 1424305893 638418 :adu!~ajr@c-69-243-56-49.hsd1.md.comcast.net JOIN :#esoteric < 1424305949 138821 :kcm1700!~kcm1700@175.117.8.72 QUIT :Read error: Connection reset by peer < 1424305954 362766 :kcm1700_!~kcm1700@175.117.8.72 JOIN :#esoteric < 1424306301 112043 :Gregor!dlopen@libdl.so PRIVMSG #esoteric :oerjan: I see my name highlighted multiple times. < 1424306309 777539 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :it's alive! < 1424306320 976319 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Gregor: the wiki server is/was down < 1424306373 173911 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :make that is < 1424306450 732971 :shikhin_!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424306465 683976 :dulla!~rikc@108-65-78-116.lightspeed.sntcca.sbcglobal.net PRIVMSG #esoteric :install gentoo < 1424306485 155032 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Why do resolution changes permanently resize windows? < 1424306501 694297 :Gregor!dlopen@libdl.so PRIVMSG #esoteric :Wow, it's very down. Weird. < 1424306504 70135 :Gregor!dlopen@libdl.so PRIVMSG #esoteric :I'll kick the server. < 1424306516 705465 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :
ACTION has his oculus rift
< 1424306523 321042 :Lymia!~lymia@inportb/loli/cirno-chan JOIN :#esoteric < 1424306602 913210 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 240 seconds < 1424306648 658116 :Gregor!dlopen@libdl.so PRIVMSG #esoteric :
ACTION has his occultus rift.
< 1424306650 961903 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1424306671 934957 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Gregor: is this the portal-to-another-dimension kind < 1424306691 39243 :Gregor!dlopen@libdl.so PRIVMSG #esoteric :It's a portal to the esolangs server panel, anyway. < 1424306840 318299 :mitchs!~canissimi@unaffiliated/canissimia QUIT :Quit: mitchs < 1424306956 208189 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :http://wurstcaptures.untergrund.net/music/?oneliner=Math.sqrt(t*253)%2Btan(Math.sqrt(166%7Ct))%20&oneliner2=Math.sqrt(t*253)%2BMath.log(tan(cos(57-t)))&t0=1000&tmod=0&duration=30&separation=100&rate=8000 < 1424307177 686183 :mihow!~mihow@108.30.58.169 QUIT :Quit: mihow < 1424307235 396757 :hjulle!~hjulle@ankadagen.vth.sgsnet.se QUIT :Ping timeout: 250 seconds < 1424307581 625876 :mitchs!~canissimi@unaffiliated/canissimia JOIN :#esoteric < 1424307611 998687 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :oh it's back < 1424307628 421339 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :but HackEgo hasn < 1424307634 173014 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :'t rejoined the channel < 1424308006 632939 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :MDude: syllogisms hth < 1424308191 894933 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Oh right, that's the other thing I was thinking of. < 1424308196 386559 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Thanks oerjan. < 1424308204 66732 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :yw < 1424308324 579354 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Anyway, what I was thinking with categorical propositions was to have it used in OOP to make inheritence better/worse. < 1424308419 896101 :Lymee!~lymia@inportb/loli/cirno-chan JOIN :#esoteric < 1424308448 976331 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :All JavaBeanVisitorFactories are Factories < 1424308451 804003 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :I'm pretty sure that's what I was thinking. < 1424308462 334041 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Not that. < 1424308466 990023 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :aww < 1424308468 466201 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Maybe? < 1424308481 579379 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :
ACTION _was_ joking hth hth
< 1424308492 68407 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :also forgetting the script bug < 1424308504 848874 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :I just meant you entered that right before me,,. < 1424308580 236614 :Lymia!~lymia@inportb/loli/cirno-chan QUIT :Ping timeout: 265 seconds < 1424308613 193152 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :But yeah, the idea was mostly that if you has "some" or "not all" of a class as something, you could more easily have exceptions to things. < 1424308651 332766 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :And other parts would know that such exceptions are possible, as oppossed to if it was "all" or "none". < 1424308703 170650 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :And then you could have conditionals like "if (instance) might be a (class)". < 1424308748 867655 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Read error: Connection reset by peer < 1424308790 273714 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :And that is the fine joke. < 1424309119 275180 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net JOIN :#esoteric < 1424309135 889751 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :My computer wont turb on < 1424309143 589051 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :It just shows a black screeb < 1424309172 840168 :Tritonio!~tr@2a04:1980:3100:1aac:92e2:baff:fe42:f24c QUIT :Ping timeout: 252 seconds < 1424309348 855042 :mitchs!~canissimi@unaffiliated/canissimia PRIVMSG #esoteric :not a burnt out backlight on a laptop is it? < 1424309381 933820 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :How would i tell? < 1424309398 940047 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :The screen does turb on < 1424309406 585015 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Turn < 1424309436 457025 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :I don't even see POST stuff < 1424309492 369589 :mitchs!~canissimi@unaffiliated/canissimia PRIVMSG #esoteric :you could tell by shining a flashlight on the screen or hooking up an external monitor < 1424309604 712189 :Thedarkb!~thedarkb@86-43-192-3-dynamic.b-ras1.wtd.waterford.eircom.net JOIN :#esoteric < 1424309660 547302 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Rift counts as external monitor i think < 1424309679 953755 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Buy it didn't receive video info when i do that < 1424309759 501128 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Last time this happen ed, one of my name restarts was black as usual but eventually showed windows login screen < 1424309790 142853 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :I may have been pressing F8 or something < 1424309799 488727 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :I'm about to lose my mind < 1424309814 555638 :Thedarkb!~thedarkb@86-43-192-3-dynamic.b-ras1.wtd.waterford.eircom.net PART #esoteric :"Konversation terminated!" < 1424310046 906784 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca JOIN :#esoteric < 1424310108 636646 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :So I dissasembledmy laptop to see if I could fix the screen problems. Now the screen seems to have stopped acting up... but the touchpad doesn't work. < 1424310171 670610 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Most recent restart seems to be working < 1424310182 341089 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :In the sense of getting the Lenovo logo < 1424310199 109261 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Going to try to be patient now < 1424310244 929652 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :I've decided I can live with using an external mouse all the time < 1424310449 783936 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :http://wurstcaptures.untergrund.net/music/?oneliner=((t%3E%3E88*(Math.log(6%2Ft)))%2B(t%7C(cos(sin(242%25t)))))%25(t%7C78)%26(83%25t)%20&oneliner2=%20((t%3E%3E88*(Math.log(6%2Ft)))%2B(t%7C(cos(sin(242%25t)))))%25(234%3E%3Et-227%7Ct)*(sin(sin(t)))&t0=1000&tmod=0&duration=30&separation=100&rate=8000 < 1424310576 647006 :AndoDaan!~AD@188.188.91.86 QUIT :Quit: Bye < 1424310583 454325 :AndoDaan_!~AndoDaan@188.188.91.86 JOIN :#esoteric < 1424310592 487926 :tswett!~tswett@192.241.237.138 PRIVMSG #esoteric :MDude: well... that's interesting. < 1424310600 619429 :AndoDaan_!~AndoDaan@188.188.91.86 NICK :AndoDaan < 1424310677 124091 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :I'm trying to figure out how to have it put parens. < 1424310757 430348 :FreeFull!~freefull@defocus/sausage-lover QUIT :Ping timeout: 255 seconds < 1424310862 603315 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1424310906 274841 :wool!47b76c17@gateway/web/freenode/ip.71.183.108.23 QUIT :Quit: Page closed < 1424310950 113155 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net JOIN :#esoteric < 1424311074 180334 :Lymee!~lymia@inportb/loli/cirno-chan QUIT :Ping timeout: 265 seconds < 1424311171 732714 :tswett!~tswett@192.241.237.138 PRIVMSG #esoteric :http://mrob.com/pub/ries/zeta.html - this is one of the best-sounding simple mathematical things I know of. < 1424311206 241170 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net QUIT :Ping timeout: 244 seconds < 1424311347 11669 :Lymia!~lymia@inportb/loli/cirno-chan JOIN :#esoteric < 1424312148 488969 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net JOIN :#esoteric < 1424312872 428799 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :I am currently typing this from in a nebula of some sort < 1424312888 190232 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :But the resolution is crap, I can barely make out the words I am typing < 1424312901 928225 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Sgeo: is it omg full of stars? < 1424312916 997467 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Did you say "omg full of stars"? < 1424312928 938054 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :There's a starfield option, but it's crap, it looks like a posterboard near me < 1424313020 120382 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :so not a real nebula then < 1424313946 799216 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Apparently I should put my glasses on < 1424313951 851771 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Closed right eye, everything got fuzzy < 1424313956 362117 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net PRIVMSG #esoteric :Which is what reality does too < 1424314271 972312 :Lymia!~lymia@inportb/loli/cirno-chan QUIT :Ping timeout: 250 seconds < 1424315222 70805 :Tritonio!~tr@2a04:1980:3100:1aac:92e2:baff:fe42:f24c JOIN :#esoteric < 1424316688 395060 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net QUIT :Quit: later chat < 1424316711 753435 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net JOIN :#esoteric < 1424317331 986360 :Lymia!~lymia@inportb/loli/cirno-chan JOIN :#esoteric < 1424317358 793777 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca QUIT :Quit: Lost terminal < 1424317695 590527 :Sgeo|phone!~androirc@ool-44c2aebc.dyn.optonline.net QUIT :Quit: AndroIRC - Android IRC Client ( http://www.androirc.com ) < 1424321291 324196 :bb010g!uid21050@gateway/web/irccloud.com/x-cfsgwyxrnktcqohm QUIT :Quit: Connection closed for inactivity < 1424322369 397616 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net JOIN :#esoteric < 1424322595 201827 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net PRIVMSG #esoteric :Hi < 1424322626 67635 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Hi < 1424322680 936241 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net PRIVMSG #esoteric :CDXX < 1424322791 306268 :heroux!sandroco@gateway/shell/insomnia247/x-ifgqebgwkdjgvnii QUIT :Remote host closed the connection < 1424322847 618346 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :CDIII < 1424322855 330386 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net NICK :MDream < 1424322989 749370 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net PRIVMSG #esoteric :Ayyy :) < 1424323017 307995 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net QUIT :Ping timeout: 244 seconds < 1424323032 610892 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net PRIVMSG #esoteric :return: None < 1424323061 860575 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net PRIVMSG #esoteric :I literally am Complete shit at coding I have no idea how I got here < 1424323076 241662 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net PRIVMSG #esoteric :Ill just go practice and whateverrr < 1424323118 503487 :MDream!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :That sounds cool. I'd stay to talk about stuff, but I'm probably better off getting to bed earlier. < 1424323128 450104 :MDream!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :In terms of being more alert to get things done. < 1424323197 259435 :ProofTechnique!~ptech@c-24-147-92-185.hsd1.vt.comcast.net QUIT :Ping timeout: 256 seconds < 1424323279 92283 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net PRIVMSG #esoteric :Go sleep Mdream ya need it for the stuff we gonna do tommorow < 1424324087 561491 :zzo38!~zzo38@24-207-58-35.eastlink.ca JOIN :#esoteric < 1424324384 903806 :Oolicile!~Syntaxflu@74-61-60-199.war.clearwire-wmx.net QUIT :Ping timeout: 246 seconds < 1424324400 370581 :GeekDude!~GeekDude@unaffiliated/g33kdude QUIT :Quit: ZNC - http://znc.in < 1424324581 376742 :Sgeo!~quassel@ool-44c2aebc.dyn.optonline.net JOIN :#esoteric < 1424325660 125237 :bb010g!uid21050@gateway/web/irccloud.com/x-qemwbknysindboan JOIN :#esoteric < 1424326190 892987 :ProofTechnique!~ptech@c-24-147-92-185.hsd1.vt.comcast.net JOIN :#esoteric < 1424326219 189126 :contrapumpkin!~copumpkin@unaffiliated/copumpkin JOIN :#esoteric < 1424326309 967674 :copumpkin!~copumpkin@unaffiliated/copumpkin QUIT :Ping timeout: 250 seconds < 1424327025 429851 :copumpkin!~copumpkin@unaffiliated/copumpkin JOIN :#esoteric < 1424327124 912847 :contrapumpkin!~copumpkin@unaffiliated/copumpkin QUIT :Ping timeout: 252 seconds < 1424328075 125403 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424328271 259789 :shikhin_!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 265 seconds < 1424329841 212888 :contrapumpkin!~copumpkin@unaffiliated/copumpkin JOIN :#esoteric < 1424330035 402454 :copumpkin!~copumpkin@unaffiliated/copumpkin QUIT :Ping timeout: 255 seconds < 1424330059 665566 :contrapumpkin!~copumpkin@unaffiliated/copumpkin NICK :copumpkin < 1424330471 863572 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 246 seconds < 1424331298 385642 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au JOIN :#esoteric < 1424333653 281416 :heroux!sandroco@gateway/shell/insomnia247/x-jkdbifcvisfmpeca JOIN :#esoteric < 1424335041 766782 :AndoDaan!~AndoDaan@188.188.91.86 QUIT :Quit: Going, going, gone. < 1424335187 914187 :vanila!~vanila@unaffiliated/vanila JOIN :#esoteric < 1424335190 386293 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :hello < 1424336866 468404 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: leaving < 1424338544 750669 :adu!~ajr@c-69-243-56-49.hsd1.md.comcast.net QUIT :Quit: adu < 1424340798 601387 :TieSoul_!~quassel@86.89.119.147 JOIN :#esoteric < 1424340836 665388 :TieSoul!~quassel@86.89.119.147 QUIT :Disconnected by services < 1424340841 53677 :TieSoul_!~quassel@86.89.119.147 NICK :TieSoul < 1424340863 892517 :hjulle!~hjulle@ankadagen.vth.sgsnet.se JOIN :#esoteric < 1424341098 464620 :Tritonio!~tr@2a04:1980:3100:1aac:92e2:baff:fe42:f24c QUIT :Remote host closed the connection < 1424341437 50379 :MoALTz!~no@78.11.179.104 QUIT :Ping timeout: 246 seconds < 1424342095 810072 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :zzo38: ping < 1424342164 833330 :vanila!~vanila@unaffiliated/vanila QUIT :Quit: Leaving < 1424342356 601403 :TieSoul_!~quassel@86.89.119.147 JOIN :#esoteric < 1424342380 760395 :AnotherTest!~turingcom@2a02:2c40:400::1:6e46 JOIN :#esoteric < 1424342392 600443 :TieSoul!~quassel@86.89.119.147 QUIT :Ping timeout: 245 seconds < 1424342407 281571 :TieSoul_!~quassel@86.89.119.147 NICK :TieSoul < 1424342530 817583 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :zzo38: You have 6 life, opponent has 20. Opponent has Arcane Laboratory and Asceticism in play, you have a Soltari Foot Soldier. It's the start of the opponent's turn, both of you have no lands, but have some suspended Lotus Blooms so that the opponent can play a spell his turn, you can play a spell your turn, and a spell in your next turn, but that's all. < 1424342565 585078 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :no wait < 1424342612 706149 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :this might not work, I need some more cards < 1424342616 99753 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :let me think < 1424342766 867152 :AnotherTest!~turingcom@2a02:2c40:400::1:6e46 QUIT :Ping timeout: 252 seconds < 1424342778 184686 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :Right, let you also have a Bedlam in play. Both of you hvae some mathcing 1/1 creatures that are vanilla or have no relevant abilities (flying or first strike are ok), and you also have an Echoing Decay. < 1424342811 496226 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :Opponent will play a creature, and the only way you can win is by playing the same creature then playing Echoing Decay on your own creature next turn, then beating him with the Soltari. < 1424342830 489130 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :zzo38: I think that works for your Babson thing, though it's not very elegant. < 1424343369 276839 :AnotherTest!~turingcom@2a02:2c40:400::1:6e46 JOIN :#esoteric < 1424343542 238574 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :(The key is Echoing) < 1424343624 808399 :AnotherTest!~turingcom@2a02:2c40:400::1:6e46 QUIT :Ping timeout: 252 seconds < 1424343639 445360 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424344846 11498 :boily!~alexandre@96.127.201.149 JOIN :#esoteric < 1424345246 615664 :MoALTz!~no@78.11.179.104 JOIN :#esoteric < 1424345444 505739 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :@tell AndoDaan https://github.com/FMNSSun/P/tree/master/psrc/std < 1424345444 689949 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Consider it noted. < 1424345539 297216 :MoALTz_!~no@78.11.179.104 JOIN :#esoteric < 1424345627 723938 :mhi^!~mhi@unaffiliated/mhi/x-9993184 JOIN :#esoteric < 1424345642 604851 :MoALTz!~no@78.11.179.104 QUIT :Ping timeout: 245 seconds < 1424345662 609065 :MoALTz__!~no@78.11.179.104 JOIN :#esoteric < 1424345837 240706 :MoALTz_!~no@78.11.179.104 QUIT :Ping timeout: 252 seconds < 1424345876 519527 :shikhin!~shikhin@unaffiliated/shikhin NICK :shikhout < 1424345958 947962 :shikhout!~shikhin@unaffiliated/shikhin NICK :shikhin < 1424346000 570639 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :My lisp dialect has a module system now < 1424346055 121623 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :mroman: is it just the scheme r7rs module system? < 1424346163 869315 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :No there are *.pm files < 1424346174 767449 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :which contains a list of files to load < 1424346182 154518 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :i.e. other *.pm files or *.p files < 1424346186 124746 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :*.p files contain actually code < 1424346193 164270 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :*.pm just is a list of includes < 1424346197 725602 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :for example < 1424346207 933026 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :map_par.pm includes prelude.pm and map_par.p < 1424346214 73483 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :and prelude.pm includes prelude.p < 1424346229 344794 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :so including map_par.pm results in loading map_par.p and prelude.p < 1424346457 443763 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :wait what? why do you call them *.pm ? that's the extension we use for perl < 1424346469 353985 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au QUIT :Ping timeout: 264 seconds < 1424346571 400879 :Frooxius!~Frooxius@cust-101.ktknet.cz QUIT :Read error: Connection reset by peer < 1424346589 933108 :Frooxius!~Frooxius@cust-101.ktknet.cz JOIN :#esoteric < 1424346910 864379 :boily!~alexandre@96.127.201.149 PRIVMSG #esoteric :@massages-loud < 1424346911 49804 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :You don't have any messages < 1424347120 241974 :lifthrasiir!~lifthrasi@115.68.131.49 PRIVMSG #esoteric :but you have some massages. < 1424347236 932964 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :b_jonas: Yeah < 1424347242 444772 :boily!~alexandre@96.127.201.149 PRIVMSG #esoteric :it's been a long time I've had a massage. I'm overdue to have my feet lightly marinated, then forcefully reflexed by strong thumbs. < 1424347251 689849 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :with one to three letter extensions it's hard to take anything that hasn't been used yet < 1424347454 972212 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :mroman: sure, but still, perl is already complicated because *.pl is used for two things < 1424348152 895846 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :prolog < 1424348157 181137 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :yep < 1424348199 422504 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :@tell boily I can massage you over TCP. < 1424348199 568709 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Consider it noted. < 1424348212 365701 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :elliott taught me < 1424348248 385702 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I only over UDP-based massages. < 1424348499 315906 :boily!~alexandre@96.127.201.149 PRIVMSG #esoteric :ah, the feeling of a lower ACK massage... < 1424348507 503853 :boily!~alexandre@96.127.201.149 PRIVMSG #esoteric :@clear < 1424348507 650447 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Maybe you meant: clear-auto-reply clear-messages clear-topic learn < 1424348512 315858 :boily!~alexandre@96.127.201.149 PRIVMSG #esoteric :@clear-massages < 1424348512 462423 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Messages cleared. < 1424348537 313970 :boily!~alexandre@96.127.201.149 QUIT :Quit: ANATOMIC CHICKEN < 1424349104 578031 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :*offer < 1424349345 496331 :int-e!~noone@static.88-198-179-137.clients.your-server.de PART #esoteric :"ERUDITE POULTRY" < 1424349348 851850 :int-e!~noone@static.88-198-179-137.clients.your-server.de JOIN :#esoteric < 1424349670 849019 :shikhin_!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424349851 214833 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 264 seconds < 1424349851 361497 :Koen_!~Koen@vbo91-6-78-245-243-132.fbx.proxad.net JOIN :#esoteric < 1424350199 934352 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :these fast convolution algorithms (various kinds of fast fourier transforms on various types of elements, plus the Nussbaumer convolution algorithm) are magical, and I think I should try to understand them at least a little. < 1424350210 826692 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :I probably won't fully understand them, but I should try to understand them partially. < 1424350535 116443 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: are you familiar with polynomial rings? < 1424350797 489480 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :If so, http://cr.yp.to/papers.html#m3 is a very terse but uniform description of various tricks surrounding fast multiplication (including FFT). < 1424350952 970044 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: there's also the Cormen-Leiserson-Rivest-Stein book which gives a nice description < 1424350956 147910 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :(and Knuth of course) < 1424351000 68184 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :thanks for the reference < 1424351258 56625 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :in particular, I'd like to understand whether fourier transforms on real or complex numbers (whether approximated with fixed point or floating point) are really always more useful for convolution than ones on finite fields (called "number theoretic transforms" for some reason), or just more popular. < 1424351269 838490 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :But I might not be able to answer this. < 1424351366 881463 :shikhin_!~shikhin@unaffiliated/shikhin NICK :shikhin < 1424351537 377748 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net JOIN :#esoteric < 1424351759 265096 :MDream!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net QUIT :Ping timeout: 264 seconds < 1424351987 183281 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: as a data point, https://gmplib.org/repo/gmp-6.0/file/2ff56d3c5dfe/mpn/generic/mul_fft.c does FFT modulo various 2^N+1 (note that for normal FFT's, you need 2 to be invertible, and a suitable root of unity; you don't actually need a field.) < 1424352058 887633 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: I see < 1424352098 672441 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :The existence of the root is ensured by making N divisible by a large enough power of 2. (If N = 2^k l, then 2^l is a 2^(k+1)-th root of unity modulo 2^N+1) < 1424352218 649851 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: I think I can see the basic problem, namely that for many practical applications, you'd have to use a 32-bit integer to represent an element of the field, but then to do four multiplication in that field, you need not one instructions, but like ten: you need two separate 32-bit-to-64-bit multiplications, some rearrangements, then two 32-bit-to-32-bit multiplications and lots of extra instructions to do the modulus by a constant. < 1424352302 394890 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :Yes, finite fields are a bit awkward. :) < 1424352377 924111 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :Intel is doing something about that for small GF(2^k) at least: http://en.wikipedia.org/wiki/CLMUL_instruction_set < 1424352384 462983 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :with real numbers, these smart modern algorithms avoid _most_ of the penalty of having to use complexes rather than reals, and you just have to use single multiplications with reals, or a few instructions with reals. < 1424352437 749289 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: that's for cryptography, but is GF(2^k) relevant for convolutions? I thought you need a field with characteristic at least as large as the size of data in my input and output, < 1424352450 908920 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: the modulo 2^N+1 thing is really quite clever: Multiplying by the root of unity is a shift (or perhaps just an offset for addresses) and reduction moduloy 2^N+1 is basically one subtraction. < 1424352463 695383 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :eg. if I want to convolve image data with 8-bit deep pixels, I need at least 16 bit deep data, in fact more because you have to add logarithm of the array size. < 1424352476 702713 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: probably not :) < 1424352529 161964 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :I know you said you don't really need a field, but still, I don't see how GF(2^k) would work here < 1424352640 144662 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: I'm a victim of free association :P < 1424352739 738753 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: Perhaps one can implement multiplication over fields of order 2^(kn). < 1424352760 191616 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :But mostly it just doesn't work. (You can't even use the base 2 FFTs, because 2 = 0) < 1424353539 58882 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :A cute use for FFT is string searching with single-letter wildcards. < 1424353647 921637 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :Some people (such as GMP developers) prefer finite fields because they don't want to deal with floating point rounding. < 1424353800 280179 :MoALTz__!~no@78.11.179.104 QUIT :Ping timeout: 244 seconds < 1424353812 438394 :MoALTz!~no@78.11.179.104 JOIN :#esoteric < 1424353966 441668 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :(or finite-field-like-rings) < 1424353977 574930 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :`thanks rings < 1424354000 454933 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :Jafet: it needn't be floating point. you can represent the complexes with fixed point numbers. the Knuth book explains how that's supposed to be enough to work for Schonhage-Strassen integer multiplication. < 1424354011 59807 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :Jafet: they're only using that for really large numbers; the smallest N for i386 is 464, which has to be multiplied be approximately 32, I guess. < 1424354043 469344 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(to get a number of bits) < 1424354044 921782 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :You still need to consider rounding for fixed-point numbers. < 1424354050 979120 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: yes, because there's other algorithms to multiply integers < 1424354052 917129 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :hmm, I wonder < 1424354058 855441 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :Hmm. "sufficiently field-like rings". < 1424354097 449722 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :are there also simple algorithms to convolve polynomials that aren't O(n*polylog(n)) operations like FFT-based ones, but instead just O(n**p) where p is between 1 and 2? < 1424354120 521958 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :probably there are, analogous to integer multiplication < 1424354149 484044 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: But you're probably right that there's no floating point FFT in libgmp. At least I don't recall seeing one. < 1424354176 399318 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :the question is whether these can be faster than FFT stuff in reality < 1424354188 311846 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :maybe they can, I should try to read up on that < 1424354351 699428 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: sure; the integer multiplications are implemented as polynomial multiplications after all. So the Karatsuba trick is: (ax + b)(cx + d) = ac x^2 + ((a+b)(c+d) - ac - bd) x + bd < 1424354388 184470 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: right, the question is how fast that could be for the kind of operations I'm interested in < 1424354422 755417 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :most likely, you still can't get away with only 16-bit multiplications, even if the input is only 8 bits in size < 1424354443 93641 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :so you need 32 bits for all intermediate results < 1424354454 834931 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: what kind of platform are you targeting? < 1424354482 86725 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(32 bit arithmetic doesn't scare me) < 1424354500 279996 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: let's say modern x86_64 cpus with SSE4_1 instructions and a decent cache, so 32 bit arithmetic is available, it's just more expensive than 16 bit one < 1424354507 638796 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :because you need twice the memory < 1424354548 660732 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :but of course I'd like to know a bit in general, not just answers for this < 1424354580 911042 :ProofTechnique!~ptech@c-24-147-92-185.hsd1.vt.comcast.net QUIT :Ping timeout: 252 seconds < 1424354640 633921 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :it may matter a lot about the speed how the intermediate results fit in the caches < 1424354710 201715 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :and of course it matters whether I'm doing merely 1D convolution or 2D < 1424354713 305883 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :have you mentioned the degree of the involved polynomials? < 1424354713 609242 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :Since the convolution algorithms don't use division, it doesn't matter what the register size is, you should still get the remainder of the correct result (for integer polynomials) < 1424354746 200932 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :I gathered that the coefficients are 8 bit numbers (unsigned? signed? it probably doesn't matter much.) < 1424354787 753509 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :Jafet: yes, but even then, the final results in each digit is the sum of n multiplications of two 8-bit resutls, where n is oyur array size, whcih is still more than 16 bits < 1424354793 191780 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :Jafet: so no < 1424354821 465132 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: 8 bit unsigned, but I'm also interested in cases where you want more precision than that < 1424354849 722969 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :b_jonas: I don't know how you're hoping to fit the final result into 16 bits in the first place. < 1424354850 821700 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :and I'm thinking mostly of degrees up to 2048 < 1424354853 337898 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :In that case, you need more than 16 bits to store the result no matter what algorithm is used. < 1424354866 205358 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :int-e: yes, even the final result doesn't fit < 1424354872 654733 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :pity < 1424354948 522509 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :28 bits, hmm. that's tight. < 1424354972 868255 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :Another cute thing about the FFT mod 2^N+1 is that it always gives you the correct result mod 2^N+1, which is useful for people playing with Fermat numbers. < 1424354988 283259 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :s/FFT/FFT multiplication/ < 1424355138 153605 :Koen_!~Koen@vbo91-6-78-245-243-132.fbx.proxad.net QUIT :Quit: The struct held his beloved integer in his strong, protecting arms, his eyes like sapphire orbs staring into her own. "W-will you... Will you union me?" < 1424355542 937988 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :Ah, the CHICKEN! have a history of Poulet! which appeared out of nowhere on 2012-08-08. < 1424355594 533344 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :A sufficiently round chicken in space is just a dwarf-planet. < 1424355625 272066 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :That can spawn asteroids. < 1424355724 958536 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :http://int-e.eu/~bf3/tmp/eboilution.txt < 1424356615 958748 :ProofTechnique!~ptech@65-183-137-193-dhcp.burlingtontelecom.net JOIN :#esoteric < 1424356979 236246 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :you're right, using 16 bit arithmetic would be totally unrealistic < 1424357019 964317 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :I should try to imagine how the Karatsuba-based convolution would really work, as in, how much temporary space it uses and then what operations it does on what arrays in what order < 1424357635 729925 :Frooxius!~Frooxius@cust-101.ktknet.cz QUIT :Quit: *bubbles away* < 1424357897 340883 :AnotherTest!~turingcom@2a02:2c40:400::1:6e46 JOIN :#esoteric < 1424358039 215435 :Frooxius!~Frooxius@cust-101.ktknet.cz JOIN :#esoteric < 1424358060 933901 :`^_^v!~nycs@gw.hq.meetup.com JOIN :#esoteric < 1424358320 738577 :GeekDude!~GeekDude@c-73-31-240-150.hsd1.wv.comcast.net JOIN :#esoteric < 1424358320 922076 :GeekDude!~GeekDude@c-73-31-240-150.hsd1.wv.comcast.net QUIT :Changing host < 1424358320 922187 :GeekDude!~GeekDude@unaffiliated/g33kdude JOIN :#esoteric < 1424359212 600356 :skj3gg!~skj3gg@unaffiliated/skj3gg JOIN :#esoteric < 1424359708 209857 :skj3gg!~skj3gg@unaffiliated/skj3gg QUIT :Quit: ZZZzzz… < 1424359789 601108 :skj3gg!~skj3gg@unaffiliated/skj3gg JOIN :#esoteric < 1424360146 821820 :AnotherTest!~turingcom@2a02:2c40:400::1:6e46 QUIT :Ping timeout: 252 seconds < 1424360385 88986 :skj3gg!~skj3gg@unaffiliated/skj3gg QUIT :Quit: welp, see you later. < 1424361177 573455 :newsham!~chat@udp217044uds.hawaiiantel.net QUIT :Read error: Connection reset by peer < 1424361194 223107 :newsham!~chat@udp217044uds.hawaiiantel.net JOIN :#esoteric < 1424361952 908181 :koo7!~kook@236.152.broadband3.iol.cz QUIT :Ping timeout: 240 seconds < 1424362058 734685 :koo7!~kook@236.152.broadband3.iol.cz JOIN :#esoteric < 1424362578 700852 :trn!jhj@trnsz.com QUIT :Remote host closed the connection < 1424362835 230882 :trn!jhj@trnsz.com JOIN :#esoteric < 1424363380 508618 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 255 seconds < 1424363382 598442 :Koen_!~Koen@vbo91-6-78-245-243-132.fbx.proxad.net JOIN :#esoteric < 1424363850 901817 :cpressey!~cpressey@35.87.2.81.in-addr.arpa JOIN :#esoteric < 1424363922 975302 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :
ACTION is beating his head over what exactly is "total" about total functional programming that uses corecursion and codata to work on "infinite" data structures
< 1424363965 965704 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :they do realize that on a finitary computer, those "infinite" data structures aren't actually infinite, and when you try to realize them, it... doesn't terminate. don't they? < 1424363983 846494 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :hi, btw < 1424364086 122624 :Koen_!~Koen@vbo91-6-78-245-243-132.fbx.proxad.net PRIVMSG #esoteric :hi cpressey < 1424364258 345801 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :hi Koen_ < 1424364286 606790 :mihow!~mihow@108.30.58.169 JOIN :#esoteric < 1424364294 603921 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1424364315 169557 :Koen_!~Koen@vbo91-6-78-245-243-132.fbx.proxad.net PRIVMSG #esoteric :I witnessed a Master 2 class (Master 2 meaning fifth year of college) where the students were asked the complexity of an algorithm about inversing n x n matrices < 1424364324 276383 :Koen_!~Koen@vbo91-6-78-245-243-132.fbx.proxad.net PRIVMSG #esoteric :apparently they agreed the complexity was n < 1424364328 433505 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :cpressey: they produce böhm trees without bottoms. that's nice. < 1424364352 92920 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(in the limit, of course) < 1424364372 995487 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: well, the distinguishing property of codata is productivity; you don't consider the fully unrolled trees, but only what you get after "one step" < 1424364388 878674 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :> [1..] -- and initial segments can be computed in finite time < 1424364390 344373 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : [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,28,... < 1424364403 740145 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(that is productivity) < 1424364407 167732 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :"looking further" is considered an explicit operation rather than something you can ascribe to the result in the abstract < 1424364443 90862 :Koen_!~Koen@vbo91-6-78-245-243-132.fbx.proxad.net PRIVMSG #esoteric :so if you try to "observe" it you're disturbing it? sounds quantic < 1424364452 567315 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :elliott: that's pretty lazy :) < 1424364456 955133 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :if you have "f : A -> Colist B", you know that (f x) is always something, you can look at as much of it as you want < 1424364462 747131 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :(whereas in Haskell it could bomb out) < 1424364502 616119 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :> filter odd [2,4..] < 1424364505 937581 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :elliott: that grates against my idea of "total". w.r.t. how "total" is used in computability, anyway. *how do you know how much of it you want* < 1424364506 397152 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : mueval-core: Time limit exceeded < 1424364507 955270 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: an alternative way of thinking about it is that functions are codata too. (Nat -> A) is exactly the same as (Colist A), and it's still "total" because we can look at as many "elements" as we want, even if the tree of them is infinitely deep < 1424364540 449584 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :cpressey: it's funny how people still try to invent total turing complete languages < 1424364574 953081 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: er, Stream A. < 1424364577 490740 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :b_jonas: https://github.com/wouter-swierstra/ < 1424364578 94139 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :Colist can end. < 1424364599 729309 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :sorry, wrong url < 1424364599 971177 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :codata allows that. the non-termination comes from trying to write a codata structure (like a stream) out completely. < 1424364602 445895 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :Colist A would be, like, {f : Nat -> Maybe A | forall i, isNothing (f i) -> forall j, j >= i -> isNothing (f j)}. < 1424364631 412993 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :you can probably come up with a function type for, like, potentially infinite binary trees too, it'll just be annoying. this gets kinda domain theory-ish < 1424364633 333598 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :https://github.com/wouter-swierstra/Brainfuck/ and my inquiry https://github.com/wouter-swierstra/Brainfuck/issues/1 < 1424364666 447214 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :like, you can do Partial A as {f : Nat -> Maybe A | forall i j, i >= j -> f i >= f j}, where Just >= Just, Just >= Nothing, Nothing >= Nothing < 1424364679 772769 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :afaict the author wrote this to demonstrate that you can have something which is both total and Turing-complete < 1424364715 632023 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :which may be true, for his definition of total -- but it's hard to fit it into my idea of total. < 1424364717 447280 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :"A system is total iff it always produces a final result." <-- but the totality refers to functions whose codomain can be codata. < 1424364721 75515 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :my definition of "total functional programming" is just that every function is total < 1424364725 820429 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :not considering it as a global property < 1424364738 811574 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :int-e: right. and to me, an infinite list is not a final result < 1424364748 322246 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: let's put it this way -- it's the same argument as haskell being pure < 1424364757 498029 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :from the point of view of running a haskell program, obviously it's not < 1424364762 497179 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :the trick is you have an RTS to walk the pure results < 1424364775 152860 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :er, *the pure descriptions of effects < 1424364778 533040 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :here, you have [something] to walk the brainfuck execution trail < 1424364790 211207 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(This is closing a circle. In math, it's perfectly clear what a total function is. If you consider functions on natural numbers, then that notion happens to conicide with terminating functions on a Turing machine. But *defining* totality through termination is wrong once infinite data is involved.) < 1424364795 117855 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :(Agda's IO is actually codata, so you can write a full Agda brainfuck interpreter and have the RTS chase the codata for you, potentially forever.) < 1424364806 115248 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(I'm *very* sloppy) < 1424364859 815010 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(what I mean is that total, partial recursive functions on naturals are terminating) < 1424364869 762493 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :https://personal.cis.strath.ac.uk/conor.mcbride/pub/Totality.pdf this is about this exact topic, and might help. < 1424364881 309395 :hjulle!~hjulle@ankadagen.vth.sgsnet.se QUIT :Ping timeout: 256 seconds < 1424364900 806187 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :McBride is probably the strongest advocate of totality =/= turing-incompleteness. he even told me off about it once even though I agree :( < 1424364922 574533 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(Oh I see that Wouter is attacking the same point.) < 1424364940 789141 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :I will probably just stop using the term "total", honestly. < 1424365000 503385 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I mean, totality in this sense is still a good guarantee. < 1424365009 922548 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :As I wrote, it's a perfectly sensible term for saying that a partial function, is, in fact, nowhere undefined. < 1424365011 977367 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :you know your programs won't get "stuck" < 1424365017 306828 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :int-e: well yes < 1424365018 746280 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ok look < 1424365025 65932 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :i can't talk to both of you at once < 1424365033 158967 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :i can barely talk to one of you at once < 1424365035 192997 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :(though of course if you just go back and model general recursion again you don't gain anything from the internal POV)x < 1424365038 195334 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :heh < 1424365043 450644 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ok nevermind < 1424365050 785070 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I'll shut up < 1424365051 634407 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :*-x < 1424365077 762965 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :I'm afk for a bit anyway. < 1424365079 521695 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric ::-P < 1424365090 44092 :bb010g!uid21050@gateway/web/irccloud.com/x-qemwbknysindboan QUIT :Quit: Connection closed for inactivity < 1424365093 464093 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Often the limit as to how many computation steps a computer can afford to take invloves factors beyond the architecture of the computer itself. < 1424365151 847183 :Koen_!~Koen@vbo91-6-78-245-243-132.fbx.proxad.net PRIVMSG #esoteric :heat comes to mind < 1424365191 485572 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :I'm going to at least stop using "total" to describe Turing machines that always halt (sorry Kozen), because if you want to look at it as *each transition* of the TM, with the *option* to GET the next transition, well then of COURSE each transition terminates. < 1424365195 436327 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :it's not helpful. < 1424365209 256506 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :(to look at it that way. at least, not to me.) < 1424365213 762916 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Until zeno machines exist, I'm not too worried about the contradictions that might happen if my turing machines runs an infinite amount of time. < 1424365239 326512 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I guess this use of "total" to describe languages comes from Turner's Total Functional Programming, as the obvious generalisation of talking about writing total functions. < 1424365250 383517 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :*run < 1424365263 925583 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :elliott: yes. linked to in that github issue. i read it (mostly). some parts i like. others, not so much < 1424365311 547445 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :like... you can't write a self-interpreter in this... but you are thinking you might write an operating system in it? really? < 1424365321 552660 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Well, it is distinct from a machine that could get stuck infinitely trying to proccess one command. < 1424365419 246690 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :MDude: I'm a bit "worried" about such contradictions, but they don't keep me up at night. < 1424365425 879382 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I mean, you can write a self-interpreter in a way. < 1424365433 762063 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :you can't write ProgramWithType A -> A. < 1424365434 244978 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca JOIN :#esoteric < 1424365435 64356 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :I guess you could call such mcachines micricode-total. < 1424365441 264549 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :but you can write ProgramWithType -> Partial A, with the codata partiality monad. < 1424365441 434880 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :*microcode-total. < 1424365451 61832 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Or just micro-total. < 1424365470 68062 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :you can write the computation internally (like you can model IO in Haskell), you just can't prove that it actually always finishes, because Goedel. < 1424365492 753151 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I think that paper defines 0 / 0 = 0 instead of doing something reasonable though. and probably doesn't cover codata or dependent types? I wouldn't want to program in "Haskell with a termination checker" < 1424365496 127189 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :elliott: partiality monad in a total functional language, is that right? < 1424365508 518940 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: like IO monad in a pure functional language, sure < 1424365523 191573 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :zzo38: ping? < 1424365531 730490 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :entirely black horse with white legs < 1424365533 201736 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1424365534 965173 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :you can define it easily with a normal codata mechanism, even prove things terminate and so on < 1424365548 928886 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :a.k.a. oxymoron < 1424365550 153674 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :if you haven RTS that will chase it forever, you can use it to write any potentially non-terminating program you want, like that brainfuck interpreter does < 1424365595 283762 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :ooh, cpressey is here? < 1424365600 791431 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: no < 1424365602 412640 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :that might be enough to make me pay attention to the channle < 1424365603 897291 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: I'm Phantom_Hoover < 1424365605 515916 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :ah right < 1424365606 972777 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: you can define the partiality monad regardless of language support for doing things for it. it's like saying the ability to define "data MyIO = GetChar (Char -> MyIO) | PutChar Char MyIO | Halt" makes Haskell an impure language *shrug* < 1424365608 248398 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :Phantom_Hoover: eat that < 1424365621 304935 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :i'm cool with it, i'm actually aloril < 1424365903 553790 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :having a total function from partial objects to partial objects is nice. i'm not contesting that. i'm trying to say that it doesn't tell you much about the properties of the program that uses them. and that's really the important part, isn't it < 1424365907 607228 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :? < 1424365938 352853 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I don't personally see, e.g. (Colist Nat) as a partial object < 1424365943 456587 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :this is really deep into definition-arguing though < 1424365972 914831 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :like, I can't see any way to claim (f : Colist A -> Colist B) can't be total without claiming (f : (Nat -> A) -> (Nat -> B)) can't be total, since the two are exactly isomorphic. < 1424366015 5628 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :erm. *Stream for Colist there (sigh) < 1424366036 398291 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :
ACTION sobs
< 1424366047 704963 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :
ACTION too old for this
< 1424366055 788023 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :har < 1424366077 415938 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :how do you still have the ability to program computers without burning out < 1424366077 562470 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :in other news, no one here will care, but Cat's Eye Technologies has a Twitter account now. https://twitter.com/catseye_tc < 1424366094 387388 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :um... I eat a lot of fruit? < 1424366094 738221 :pikhq!~pikhq@2001:470:c47a:1:eade:27ff:fe08:b48b PRIVMSG #esoteric :The best of news. < 1424366097 889863 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :actually I don't < 1424366102 609659 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :this is a lot of fancy unicode quotes < 1424366120 909002 :Froox!~Frooxius@cust-101.ktknet.cz JOIN :#esoteric < 1424366130 354878 :Frooxius!~Frooxius@cust-101.ktknet.cz QUIT :Read error: No route to host < 1424366130 804442 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :not as many as some of the weirdos I'm following < 1424366151 54192 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :they're much better at it than I < 1424366338 287345 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :unicode quotes as in < 1424366340 182848 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :!quote unicode < 1424366345 269231 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :or as in “”? < 1424366348 536361 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :err < 1424366350 236052 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :`quote unicode < 1424366352 224470 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :elliott: would learning about corecursion help me with my consternation here, or should I just give up? keep in mind that my understanding of monads is, after all these years, still fuzzy, at best < 1424366407 960817 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: it might, yes, but you might still just come down to not liking how the terminology is used < 1424366420 435275 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I don't know of a good introduction to codata though < 1424366432 247368 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt is classic, at least < 1424366438 134859 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :isn't codata just the subject of corecursion? < 1424366444 810462 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :but, uh, pretty technical < 1424366446 671716 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: sure < 1424366482 55160 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :i confess, there's another angle i'm interesting in corecursion for < 1424366499 378694 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :the two-sentence explanation is "data is easy to produce but you have to consume it carefully (i.e., structural recursion)", "codata is easy to consume but you have to produce it carefully (i.e., "guarded" corecursion; making sure you're "productive")" < 1424366502 757998 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :/ing/ed/ < 1424366505 727861 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :corresponding to folds and unfolds specifically. blah blah blah F-coalgebras < 1424366517 541283 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :right ok sure < 1424366561 483805 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I'm sorry for getting into a terminology argument, anyway. I really don't care about it, heh < 1424366604 198581 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I do think "languages where every function is total and your data recursion is structural and your only infinite data is properly guarded codata are useless for doing actual things, because they're not TC" is too prevalent an attitude but people should stop equating general usefulness with TCness anyway < 1424366624 613771 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :I agree wholeheartedly with that < 1424366695 794434 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424366704 73133 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :btw, I think I saw an article on HN about HTML+CSS3 being TC -- it came back from an unrelated search & I did not click on it but ISTR there was some discussion on that at one point in here < 1424366720 388970 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :yeah it was one of those "by TC I mean FSA" type things < 1424366731 127213 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :thought it might be < 1424366737 554964 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :there's a reason i don't get my news from HN < 1424366752 72340 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :well, clearly you do :p < 1424366771 89546 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :cpressey: that article made me sign up to Reddit to debunk it < 1424366778 66901 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's not TC due to not having infinite memory < 1424366785 596865 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: thank you < 1424366790 428083 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :assuming it's the one I'm thinking of < 1424366805 367454 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :i really *don't* read HN, so I don't know, but it probably was < 1424366809 289651 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's possible you could salvage it using WebForms, but nobody's figured out how yet < 1424366842 602541 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 245 seconds < 1424366848 601780 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1424366862 342629 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :i've had some really frustrating conversations with people who can't accept that the human brain isn't TC < 1424366899 718872 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I think you need to talk about things like quantum uncertainty to prove it isn't, though < 1424366910 397892 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :human brain is analog in time, and you can store an infinite amount in a single real number < 1424366913 781830 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :I think we need about 8 more words that are variations on TC < 1424366917 772930 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but you can prove that it can't measure a time delay accurately enough < 1424366940 302196 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :even then, maybe it's just pointless < 1424366943 686563 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :cpressey: well I've been thinking a lot about how to define TCness because of the 2,3 Turing machine thing < 1424366971 545575 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: I have a something too, based on thinking about Wang tiles < 1424366992 527310 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :actually's it's just an old thing < 1424367010 509404 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :my latest approach has been along the lines of "a language is TC if you can compile any TC-language program to it, via a function that can output the 'nth' byte of the resulting program in finite time" < 1424367014 497780 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :err, O(1) time, that is < 1424367028 728010 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but I'm getting bogged down in details of what operations you're allowed < 1424367044 84931 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: ah, so I give the "compiler" the source program, and n, and it outputs "byte" number n ? < 1424367054 446555 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :in constant time < 1424367065 160576 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :yep < 1424367066 178525 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :ais523: so you mean, the program that produces the output program has to give a productive colist of bytes back, huh < 1424367069 450363 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :well, symbol, not byte < 1424367071 918392 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :how appropriate < 1424367075 136975 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :or maybe O(x) where x is the length of the source program, no? < 1424367081 351804 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :because it's gotta read it < 1424367084 808884 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :and it's gotta read n < 1424367088 990079 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :cpressey: oh, I'm treating the source program as fixed here < 1424367093 47552 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ah, ok < 1424367107 825912 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :as in, for any given source program, we can produce the nth symbol of the target-language program in finite time < 1424367109 660846 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :but the "compiler" is invariant of the choice of source program? < 1424367130 666658 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :oh, ooh, yeah we have to be careful here < 1424367150 237693 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :definitions get really complex when you're trying to avoid exploits while still allowing as much as possible < 1424367150 597382 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :i assume we can't just OPTOMIZE it for each program we want to compil < 1424367151 693191 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :e < 1424367175 472672 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :
ACTION should really be "optomizing" a database query right now
< 1424367196 289505 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :ais523, so are you saying that the compiler has to be 'local' when emitting a byte, basically? < 1424367210 877876 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I guess the compiler has to be a fixed program, which can scale with the size of the source program, but not the target program < 1424367251 701950 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :Phantom__Hoover: I'm not quite sure what you mean < 1424367265 298166 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :well, in comparison, my insight was simple: Wang tiling ~= Conway's GoL ~= CA-complete ~= can simulate any Turing machine which *never* halts < 1424367268 307046 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :that's all < 1424367293 650042 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :well, that the time it takes to emit the nth byte can't increase without bound < 1424367296 424898 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :aha, we define it like this: a compiler is a single program, which, for any given source program, there is some finite bound within which it can produce any given byte of the target program < 1424367300 176446 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :~= meaning "computationally equivalent" because I don't do fancy unicode in IRC (yet) < 1424367323 836330 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I do fancy Unicode in IRC all the time, but that one isn't on my compose key < 1424367354 99599 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :i.e. what you're trying to prevent is situations where the compilation process is introducing an unbounded amount of computational 'strenght' < 1424367356 6057 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :*strength < 1424367399 210701 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :right < 1424367428 807150 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so for example, imagine a programming language which takes an infinitely long program as input, and only has two commands, "halt" and "nop" < 1424367450 285510 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :you can compile into that language by running your input program for n steps, then outputting "halt" or "nop" based on whether it halted within those n steps < 1424367452 501466 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :to output the nth command < 1424367469 292437 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :presumably because the trouble with the 2,3 turing machine was that, in some sense, most of the computation was done in that way? < 1424367473 903936 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :the problem I'm having is that, to define O(1), you need to define which operations you're allowed < 1424367479 226202 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :Phantom__Hoover: actually it wasn't < 1424367484 949766 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :my problem is proving that it wasn't thouhg < 1424367486 445695 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :*though < 1424367493 23167 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :which means defining what it means to do that < 1424367498 680921 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :ah < 1424367567 899808 :vanila!~vanila@unaffiliated/vanila JOIN :#esoteric < 1424367574 536214 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :hello < 1424367618 128865 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :hi vanila < 1424367723 428077 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: this sounds reminiscent of one part of Minsky's old book where he frets about mappings between languages wrt TC-ness. He's not conclusive. I think he says the mapping function should not be more than primitive-recursive < 1424367751 969701 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :that's close to the argument I made in the first submission of the 2,3 Turing machine proof < 1424367752 208381 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :if you allow any PR function, that still gives you an awful lot of leeway < 1424367775 16634 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :however, primitive recursive programs can't run for infinite time < 1424367779 480728 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so they can't produce infinite output < 1424367780 732491 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :and if we're trying to find the "smallest" TC things, it seems likely we're going to get into the territory of these "powerfulish" mappings < 1424367792 663227 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: yeah, but a mapping doesn't need to < 1424367800 308344 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :you're just mapping one finite program to another < 1424367807 775221 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :no, the problem with the 2,3 proof is < 1424367810 800375 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :the input program is infinitely long < 1424367818 269136 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :?! < 1424367818 415470 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Maybe you meant: v @ ? . < 1424367836 702552 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :no lambdabot, I meant an interrobang, but as I said, no fancy unicode yet < 1424367839 187003 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :because it has to initialize the whole tape of the Turing machine < 1424367849 559496 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and the pattern it initializes it with isn't finite or repeating < 1424367867 207457 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :yeah that ain't right < 1424367879 558803 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :in my view, it needs to lazily create that pattern as it uses thar part of the tape < 1424367886 563481 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :and the complexity of doing so needs to be factored in < 1424367908 179420 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so you would consider the 2,3 machine to be sub-TC, then < 1424367929 711963 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I still haven't found the simplest pattern that works < 1424367931 165728 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :("needs to" ... er... simpler to consider systems that only do that, rather than ones that need a "prepared tape") < 1424367931 535712 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :An operating system made in common lisp - https://dl.dropboxusercontent.com/u/46753018/Screen%20Shot%202015-01-19%20at%2001.29.31.png < 1424367939 995120 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :(is that like a perpared piano, John Cage...?) < 1424367961 351116 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but suspect it's along the lines of "infinitely repeating pattern, except that all cells with index 2^n are replaced with the same specific value as an exception to the pattern" < 1424367975 513915 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: I guess I... not exactly; I would consider it to be an abbreviated description of a TC system which, if not abbreviated, would be >2,3 < 1424367982 488457 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :or in other words, yes < 1424368015 232507 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :have you heard of the language "sequential tag"? it's something that #esoteric sometimes discusses < 1424368039 665951 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :vanila: nice! (is the nethack written in lisp too?) < 1424368042 458019 :arjanb!8259abdc@gateway/web/freenode/ip.130.89.171.220 JOIN :#esoteric < 1424368043 460254 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :basically, it has infinitely long programs; each command in the program is a sequence of subcommands, either "run" or "skip" < 1424368059 710618 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: I... don't think I have < 1424368069 326598 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :all data is stored in one queue, which is initialized as "run" < 1424368070 534707 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :oh, infinitely long THIS, infinitely long THAT, what madness is this < 1424368087 273425 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :(might make more sense if you saw my rant about "total" earlier) < 1424368113 419276 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :it's just telnet talking to nethack server, but the mandelbrot and stuff is in lisp :) < 1424368120 750937 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :then repeatedly, you pop the start of the queue, if it's "run" you append the current command of the program to the end of the queue and move to the next command, if it's "skip" you move to the next command of the program without appending anything to the queue < 1424368127 720205 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and it halts if the queue ever becomes empty < 1424368159 564121 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's one of the easiest languages to implement, if you have the ability to read an infinitely long program < 1424368165 314038 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :because it's so simple < 1424368181 713297 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and it's TC if you allow an infinitely repeating input prorgam < 1424368239 471487 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :um, hm. < 1424368261 189522 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :(because with an infinitely repeating input program, it becomes cyclic tag) < 1424368294 88967 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :wait, i totally do not follow. the queue is not a queue of... maybe i should look this up on the wiki < 1424368315 674250 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :I still find it hard to accept that cyclic tag machines can be TC, I get how they are but.. they shouldn't be.. < 1424368324 47167 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I'm not sure it's on the wiki < 1424368327 623019 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but the queue is of "run" and "skip" < 1424368349 219497 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :vanila: they "feel" sub-TC? < 1424368357 205524 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ok, so you pop "run", and the "current command" is -- the next thing on the queue? < 1424368393 419382 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :does not appear to be on the wiki, btw < 1424368426 892123 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :yes - but just because my intuition is wrong I guess < 1424368452 604943 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :cpressey: the next command in the program < 1424368458 313609 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :the queue tells you whether to run or skip each command in the program < 1424368474 676197 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and when you run a command, it shifts a specific sequence onto the end of the queue < 1424368489 471554 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ok, so the queue is not infinite, and the program is not on the queue < 1424368513 318664 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :replace "infinite but repeating" with a "goto" and I'm fine with it < 1424368532 680337 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :infinitely long programs, though... no. < 1424368540 171347 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :they defeat the point < 1424368555 961279 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :an infinitely long program could contain something very dangerous... unless you know that it was generated by a simple program < 1424368585 221164 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :cpressey: right < 1424368602 417166 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :now, the problem with things like cellular automata and turing machines < 1424368611 90582 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :is that the programs are inherently infinitely long < 1424368632 410017 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: i disagree. unbounded, yes. infinite, no. < 1424368632 898958 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so the conventional wisdom is that you have to initialize them with a repeating pattern < 1424368648 917422 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :hmm < 1424368657 529996 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :for a Turing machine, you can have an unbounded tape, plus a rule for initializing it < 1424368673 224228 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and I assume you'd treat that initialization rule as part of the Turing machine, rather than part of the input to it? < 1424368674 504870 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: yes. and yes, it's a bit more difficult to work that into a CA, but < 1424368682 922702 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ais523: and yes < 1424368686 598515 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :oh irc < 1424368713 394402 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :i consider a tape cell of a TM to essentially not exist until the head gets to it < 1424368724 442256 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :but the head can always get to a new tape cell and make it exist < 1424368728 390679 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :"This is a little surprising: greatest fixpoints allow infinite objects, such as streams, yet the strong normalisation property is preserved." I guess wadler sums up the totality thing pretty well < 1424368730 663234 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :hmm, this viewpoint is quite at odds to mine < 1424368775 224173 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :elliott: I find it a little hard to define strong normalization if you have infinite input < 1424368794 1911 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :about the strongest concept I can manage to define on that is weak confluence < 1424368797 677901 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: that's sort of like how the next cell of an infinite codata stream doesn't exist until you observe it, but you can always observe a new one and make it exist in finite time :) < 1424368818 761942 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :I hope wadler is ok, he was ill < 1424368864 820867 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :elliott: yes, but this is happening *inside a Turing machine*, not *in my program* < 1424368887 285492 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :it's only to avoid questions about infinite tapes < 1424368927 827321 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :and a way to collect the complexity of "prepared tape" into one place, where you were already caring about complexity -- the running of the TM itself < 1424368964 895491 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1424368991 678887 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :with codata, semantically, the observation is explicit < 1424369001 755977 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :that can get hidden in sugar and bad implementation of it, though. < 1424369017 602070 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 245 seconds < 1424369071 346904 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :elliott: question: could you formulate codata that represents a Wang tiling? < 1424369092 226736 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :a "total" tiling of the plane < 1424369093 909025 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :oh god < 1424369096 984980 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :someone shoot me < 1424369099 189431 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :hahaha < 1424369153 544340 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: I guess I don't see why not. "current tile" and four neighbours, say. < 1424369160 274096 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :well < 1424369169 462066 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :that gets annoying because of overlapping ways to observe the same square < 1424369173 280841 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :http://catseye.tc/installation/Backtracking_Wang_Tiler fwiw < 1424369181 772194 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: okay, alternate answer: sure, it's just (Nat,Nat) -> Tile < 1424369182 377819 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :fun to watch for about 50 seconds < 1424369198 715690 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :functions are one type of codata (the best-supported, usually) and codata can be implemented as functions, so < 1424369212 873888 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :okay, (Z,Z) -> Tile < 1424369239 955645 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :cpressey: uh, or do you mean something that ensures you're tiling properly < 1424369251 78082 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :that sounds like you'd end up with proof objects and stuff and this is out of my pay grade < 1424369252 903445 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :no elliott, I want an invalid Wang tiling! < 1424369269 778639 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I'm an invalid Wang tiling :( < 1424369343 725083 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :I'm trying very hard not to lol < 1424369403 63982 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :#esoteric: the channel where everyone can disagree about infinite < 1424369407 390001 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :infinity* < 1424369506 58429 :olsner!~salparot@c80-217-116-33.bredband.comhem.se PRIVMSG #esoteric :oh, cpressey is here < 1424369519 624424 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :hi olsner < 1424369607 625892 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :corecursion looks interesting, because i've been hanging out with people in generative art circles, and they're interested in grammars, but they're more interested in *generating* things from than, than *parsing* things with them < 1424369628 725075 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :which is easy, programming-wise, in an RDP: replace scan("x") with emit("x") {more or less} < 1424369642 937626 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :but, theory? < 1424369646 440188 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :this might be it < 1424369732 930148 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :also logic programming to run recognizers backwards to generate things < 1424369847 198852 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :vanila: yes, I'm reading the wikipedia article on it now, and it's looking a bit like that < 1424369921 289108 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :elliott: maybe I'm a finitist? would that be terrible? istr that might be terrible < 1424369938 118924 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :an infinite list is REALLY a finite list plus a continuation! < 1424369951 874114 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :that's more or less the codata perspective though < 1424369962 79270 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :thinking of Colist A as an infinite list is up to you < 1424370016 657295 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :ok, maybe that will help me think about what i don't like about this "TC and total too!" thing < 1424370029 444274 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :oh that's funny, I just learned about TC & total < 1424370035 5522 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :a Colist A is just something you can construct from an X and (X -> Maybe (A, X)) (for any X) (e.g. nats = unfold 0 (\n -> Just (n, n+1))) and that gives you Colist A -> Maybe (A, Colist A) < 1424370043 322730 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :I got my own view on it < 1424370046 517332 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :meaning is for humans < 1424370067 935488 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :or more simply, Stream A from X and (X -> (A, X)), yielding head : Stream A -> A and tail : Stream A -> Stream A < 1424370073 955991 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :(eliding the possibility of stopping) < 1424370129 134958 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :oh wait < 1424370134 313644 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :no n/m < 1424370152 684192 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :"total" ~= "well-typed"? < 1424370155 639259 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :look just ignore me < 1424370167 398808 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :depends on your type system :p < 1424370173 500374 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :yes < 1424370174 473922 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :Agda and Coq rely on a termination checker separate to their type system < 1424370175 685785 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :Here's what I came to understand: < 1424370181 856785 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I prefer type systems that ensure termination by construction. < 1424370205 3733 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :fwiw: map f stream = unfold stream (\strm -> (f (head strm), tail strm)) < 1424370229 771930 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :map f colist = unfold colist (\cl -> case observe cl of Nothing -> Nothing; Just (hd,tl) -> (f hd, tl)) < 1424370232 754125 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :fun times < 1424370240 358932 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :(of course your function has to be, um, total.) < 1424370251 571018 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :My idea of 'turing complete' was you could write any nat -> nat function that you can with 'recursive functions' (primitive rec + mu-minimization) < 1424370303 432274 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :agda isn't turing complete in that sense, but if you the notion to allow functions like: nat -> partial nat then it is turing complete < 1424370309 121354 :mihow!~mihow@108.30.58.169 QUIT :Quit: mihow < 1424370382 175147 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :elliott: I... almost see what you're saying < 1424370387 971210 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :it's like a negative photograph < 1424370393 348238 :mihow!~mihow@108.30.58.169 JOIN :#esoteric < 1424370492 252602 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :that was why I was thinking total = well-typed; if the function maps every value in X to any value in Y, it is total, and you can type it X->Y < 1424370507 43618 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :sure < 1424370513 771009 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :if for some values in X it doesn't, well, no Y for it then < 1424370522 460918 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :you can have well types programs that infinite loop, e.g. omega = omega < 1424370526 348857 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :then the question is what type in Haskell corresponds to the naturals < 1424370532 747120 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :YEAH BARRING BOTTOM AND ALL THAT < 1424370533 844860 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :data Nat = Z | S !Nat is so close, but it has _|_ < 1424370539 280635 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :but bottom is exactly what makes things non-total >_> < 1424370557 965992 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :since it means you don't have total mathematical \mathbb{N} -> \mathBB{N} functions < 1424370585 541589 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :well, but f : Nat -> {0, _|_} is total right? < 1424370592 754373 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :sure < 1424370603 215488 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :also the functions have to be monotone/continuous/whatever blah blah blah < 1424370608 214263 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :
ACTION transforms into dana scott
< 1424370702 116281 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :unfortunately I need to leave no < 1424370705 331483 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :*now < 1424370715 676999 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :unfortunately, I'm sure :p < 1424370785 550147 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :ttyl < 1424370806 18861 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :my AMAZINGLY ORIGINAL AND NOVEL AND EARTH-SHATTERING THEORY about how IRC destroys productivity has been proven < 1424370816 310404 :cpressey!~cpressey@35.87.2.81.in-addr.arpa PRIVMSG #esoteric :see you later :) < 1424370818 488367 :cpressey!~cpressey@35.87.2.81.in-addr.arpa QUIT :Quit: leaving < 1424370912 703639 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :i dont like to think of agda as TC, it just seems misleading and flame-war-inviting to me < 1424370941 184409 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :now I'm wondering what goes wrong if you try to get Agda to prove itself consistent < 1424370959 290925 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :the termination checker won't buy it < 1424370962 734873 :mihow!~mihow@108.30.58.169 QUIT :Quit: mihow < 1424371007 57178 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :you can't get conAgda :: Proof (Consistent Agda) < 1424371020 275274 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :but you can produce conAgda' :: partiality (Proof (Consistent Agda)) < 1424371034 100903 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :won't that just be fix later < 1424371058 615236 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I don't believe that can ever work if it's not (clasically), eventually you have to produce a now (p : Proof (Consistent Agda)) < 1424371069 641267 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :its just the same as a lisp program that tries fitting together axioms randomly to prove agda consistent < 1424371072 510259 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :*ever work since if it's not fix later (classically), < 1424371083 667410 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :well, it'll never find such a proof though < 1424371086 645462 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :but sure < 1424371092 854182 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :the simpler way to write that value is fix later :p < 1424371122 281046 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :sometimes you can construct a value of type partiality Foo < 1424371123 868650 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :well, it might terminate after all < 1424371132 931979 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :and then actually provide a proof that it terminates, to get a Foo out < 1424371133 305033 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :it won't < 1424371141 544558 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :unless you are, for some reason, convinced that Agda is in fact consistent. < 1424371144 340462 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :in the caes of this Proof, you will not be able to proof that it terminates inside agda < 1424371157 194615 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :int-e: I am convinced that Agda will never find an internal proof of its own consistency... < 1424371175 99212 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :okay, I guess this is pointless without defining Proof here < 1424371178 899676 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :but you can make it to do arbitrary computation < 1424371203 970470 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :okay, here's what I mean: meta-theoretically, we can prove that conAgda' ~~ fix later < 1424371210 249726 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :i dont think so < 1424371213 385120 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :but that might not be true depending on what Proof is. < 1424371251 800379 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :if we can prove meta-theoretically that conAgda' ~~ later^n (now p) for some n and p, though, then there is an Agda term conAgda : Proof (Consistent Agda) < 1424371269 807654 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :if our metatheory is classical we can prove one of those. < 1424371278 891136 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :okay, it might not give us an n and p < 1424371284 496087 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :arguing about constructivism is too hard < 1424371363 412224 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :okay: there is no expression e : Partial A such that not not (e = later e, or there is an expression e' : A). I hope that's double-negated enough < 1424371367 886145 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :oh! I get you now < 1424371369 391673 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :again metatheoretically < 1424371405 309063 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :so if you say, there is no e : A, but I have e' : partial A, then I don't believe that e' can be anything other than later e', with enough "not not"s in there < 1424371411 249547 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :so it will not not not halt :p < 1424372241 871528 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :@djinn (((a -> r) -> r) -> r) -> (a -> r) < 1424372242 58314 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :f a b = a (\ c -> c b) < 1424372937 972510 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :elliott: I still think your assumption that A is empty is a tad optimistic. < 1424372951 39733 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :int-e: what do you mean? < 1424372969 297452 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :if the logic is inconsistent then it might well "prove" its own consistency < 1424372977 332856 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :well, sure < 1424372981 140826 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :Agda has had proofs of _|_ before. < 1424372997 945060 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :what I said applies regardless of A, though < 1424373003 864950 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :(and djinn just showed that not not not foo is the same as not foo, even intuitionistically) < 1424373021 433738 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :yes, that was what we call a joke >_> < 1424373026 678252 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :ah < 1424373039 218821 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :it was not not funny < 1424373499 888168 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 250 seconds < 1424373581 544723 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1424373638 542338 :dianne!~diannes@unaffiliated/dianne JOIN :#esoteric < 1424373765 834084 :mihow!~mihow@108.30.58.169 JOIN :#esoteric < 1424373994 108547 :ais523!~ais523@unaffiliated/ais523 QUIT : < 1424374001 575538 :shikhin_!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424374001 721968 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1424374011 892317 :shikhin_!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424374105 310228 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 244 seconds < 1424374106 13103 :shikhin_!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424374521 993361 :shikhin_!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424374599 9071 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424374807 607956 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424374902 104993 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424375159 639567 :`^_^v!~nycs@gw.hq.meetup.com QUIT :Quit: This computer has gone to sleep < 1424375365 258731 :`^_^v!~nycs@gw.hq.meetup.com JOIN :#esoteric < 1424375454 672726 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424375489 680211 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424376106 886422 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1424376114 581558 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 245 seconds < 1424376197 896478 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :ok, so I'm not sure in this, but I believe for polynomial convolution Karatsuba multiplication needs about as much space as twice the outplut plus once the input, but it might still be a bit too slow, and FFT multiplication needs twice the space of the output. so luckily, neither needs too much extra space, which is very useful. < 1424376291 257539 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au JOIN :#esoteric < 1424376354 952345 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424376425 352169 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424376604 100017 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424376697 945086 :Phantom__Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 250 seconds < 1424376725 741155 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424377308 904064 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424377351 549341 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424377502 126012 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424377653 488844 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424377755 745829 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424377957 786884 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424377958 372488 :J_Arcane_!~chatzilla@dsl-trebrasgw1-50dff2-22.dhcp.inet.fi JOIN :#esoteric < 1424377976 788659 :MoALTz_!~no@78.11.179.104 JOIN :#esoteric < 1424378122 513350 :J_Arcane!~chatzilla@dsl-trebrasgw1-50dff2-22.dhcp.inet.fi QUIT :Ping timeout: 255 seconds < 1424378132 943172 :J_Arcane_!~chatzilla@dsl-trebrasgw1-50dff2-22.dhcp.inet.fi NICK :J_Arcane < 1424378149 262005 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424378149 533707 :MoALTz!~no@78.11.179.104 QUIT :Ping timeout: 255 seconds < 1424378197 285766 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au QUIT :Ping timeout: 244 seconds < 1424378468 610944 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424379050 282618 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424379103 399982 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424379226 841502 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424379298 163471 :bb010g!uid21050@gateway/web/irccloud.com/x-snigollvmaoraxug JOIN :#esoteric < 1424379401 165655 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424379596 690519 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424379704 351393 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424379932 480743 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424380017 411605 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424380101 893158 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424380315 843500 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424380358 729650 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424380617 408235 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1424380858 507671 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Read error: Connection reset by peer < 1424381135 856400 :ChanServ!ChanServ@services. MODE #esoteric +o :elliott > 1424381136 117190 NAMES :#esoteric < 1424381143 712093 :elliott!~elliott@unaffiliated/elliott MODE #esoteric +b :shikhin!*@*$##fixyourconnection > 1424381143 739007 NAMES :#esoteric < 1424381145 958022 :elliott!~elliott@unaffiliated/elliott MODE #esoteric -o :elliott > 1424381145 979364 NAMES :#esoteric < 1424381333 255832 :PinealGlandOptic!~PinealGla@82.144.205.57 JOIN :#esoteric < 1424381793 791200 :aretecode!~aretecode@50.23.131.206-static.reverse.softlayer.com QUIT :Read error: Connection reset by peer < 1424381990 123013 :aretecode!~aretecode@50.23.131.206-static.reverse.softlayer.com JOIN :#esoteric < 1424382078 783483 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :what does _|_ mean? < 1424382096 361784 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Is is the upside down T? < 1424382105 281269 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :oren: yes, it's called "bottom" < 1424382228 890269 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :I suppose it is smaller on the page than the word "false". < 1424382257 334605 :`^_^v!~nycs@gw.hq.meetup.com PRIVMSG #esoteric :it's a middle finger to logic < 1424382257 480981 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :http://en.wikipedia.org/wiki/False_%28logic%29 < 1424382260 505927 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :its an ascii picture of this < 1424382280 379007 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Maybe the easiest logical literals for me to type are "0=0" and "0=1" < 1424382356 267324 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Idea: an algolike language which lacks literals other than 0 and 1. < 1424382388 884489 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Wait... That would be the peano axioms... < 1424382390 296774 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :PCF? although that doesn't even have 1 really < 1424382391 797467 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :just +1 < 1424382396 672800 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :(1+1)*(1+(1+1)*(1+(1+1))) I can do binary like this < 1424382456 184847 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :assignment should be <- . It should always have been <- . < 1424382466 42386 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :I think those +s and *s might need switched around? < 1424382470 56452 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :I agree oren. < 1424382518 330317 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :ChucK knows how to assign properly. < 1424382565 998678 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Though I would also accept "set [var] to [value]" if allowing the language to be more verbose. < 1424382637 446436 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :I made a calculator once that did exactly what ChucK does. < 1424382650 444332 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :(in assignment, not in anything else) < 1424382762 565203 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Oh, ChucK actually uses => < 1424382784 309603 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :In math, assignment is "let x be [value]" < 1424382833 272438 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :But in math, the evaluation is explicitly controlled, like "now subsitutute in the value of x"... < 1424382858 432329 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :God damn it how do you spell subsitute? < 1424382859 286889 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :there's no evaluaton < 1424382871 881490 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :I was imagining let would be for lazy evaluation statements, while set would be for eager evaluation. < 1424382873 416681 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :you just treat all equal values as identical < 1424382881 48415 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :"substitute" I think < 1424382886 974835 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Because obviously having both in a language makes sense. < 1424382947 548846 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :MDude: that is a cool idea. < 1424383079 167185 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :vanila: A math paper is a syntax-tree-rewriting program with verification, which a mathematician's brain runs and checks. < 1424383211 419862 :MDude!~fyrc@pa-67-235-2-71.dhcp.embarqhsd.net PRIVMSG #esoteric :Oh, good then. I wasn't sure if that was a good idea or not. < 1424383264 458181 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :idont agree < 1424383273 387435 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Eager evaluation is a good idea for time-critical parts of a program < 1424383333 731283 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :E.g. we don't want to go out of the polygon drawing loop to lazy-evaluate the enemies' positions. < 1424383529 930706 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :But in other parts of a program, being lazy can help performance. So having both is a good idea < 1424383664 24537 :`^_^v!~nycs@gw.hq.meetup.com QUIT :Quit: This computer has gone to sleep < 1424383695 1883 :ais523!~ais523@unaffiliated/ais523 QUIT :Quit: dinner < 1424383704 986512 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :22:02:13 E.g. we don't want to go out of the polygon drawing loop to lazy-evaluate the enemies' positions. < 1424383709 97044 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :this isn't what lazy evaluation is. < 1424383716 24087 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I mean that is one possible non-strict evaluation strategy. < 1424383727 556108 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :but that is just not something that really happens when you write in Haskell or whatever. < 1424383740 8382 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :unless you're writing your polygon drawing loop extremely weirdly < 1424383743 357760 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :well < 1424383753 302577 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :ok I can see how that would happen with certain kinds of data flow, I misread what you meant < 1424383758 414231 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Why not? You don't need to evaluate anything until it would have visible effects, right? < 1424383769 79157 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :there are tools for solving that within a lazy evaluation discipline though < 1424383774 880389 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :like, the thing is that making the polygon drawing loop eager wouldn't solve that < 1424383779 136780 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :because it's a non-local property you're talking about here < 1424383787 273704 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :it would be the position evaluation prior to that that would need to be strict < 1424383913 970362 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Why not have an evaluate operator that forces the value to be stored? < 1424383927 514811 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :haskell tried that < 1424383930 487950 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :its awful < 1424383937 884628 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Why? < 1424384103 322922 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :i guess it just doesn't seem aesthetic to me < 1424384104 63987 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :oren: well, you can't quite have a -> a < 1424384108 732595 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :but you can have a -> b -> b < 1424384130 675825 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :in haskell (a `seq` b) is b, but where a must be evaluated (to WHNF) < 1424384134 872690 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :note: no guarantees as to the ordering of the two < 1424384142 770894 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :and (f $! x) is (x `seq` f x) which is useful < 1424384149 376458 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :it can be annoying to juggle though. < 1424384157 637757 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :but you can use it to enforce invariants about evaluation. < 1424384209 926797 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :It's cool how you can do strictness analysis on code and automatically use strict evaluation instead of lazy < 1424384226 662172 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :except when it doesn't work :( < 1424384241 276702 :ProofTechnique!~ptech@65-183-137-193-dhcp.burlingtontelecom.net QUIT :Ping timeout: 265 seconds < 1424384255 344454 :vanila!~vanila@unaffiliated/vanila PRIVMSG #esoteric :yeah its undecidable but you can hopefully get a good result a lot of times by abstract interpretation < 1424384419 928350 :Lymia!~lymia@inportb/loli/cirno-chan QUIT :Ping timeout: 250 seconds < 1424384549 208054 :Lymia!~lymia@inportb/loli/cirno-chan JOIN :#esoteric < 1424384645 253608 :`^_^v!~nycs@gw.hq.meetup.com JOIN :#esoteric < 1424385857 244385 :`^_^v!~nycs@gw.hq.meetup.com QUIT :Quit: This computer has gone to sleep < 1424386070 687329 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :I find it intensely annoying that I can get all the ingredients for gunpowder in Dwarf Fortress, but can't make cannon or shot. < 1424386213 340429 :Taneb!~Taneb@runciman.default.hacksoc.uk0.bigv.io PRIVMSG #esoteric :DF has saltpetre? < 1424386256 724262 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Yup. < 1424386279 142277 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :And brimstone (e.g. sulphur), and charcoal. < 1424386311 674125 :Taneb!~Taneb@runciman.default.hacksoc.uk0.bigv.io PRIVMSG #esoteric :I am not sure that DF does have saltpetre < 1424386341 833969 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric : it has "saltpeter" < 1424386360 789075 :pikhq!~pikhq@2001:470:c47a:1:eade:27ff:fe08:b48b PRIVMSG #esoteric :That's the US spelling. < 1424386375 756289 :Taneb!~Taneb@runciman.default.hacksoc.uk0.bigv.io PRIVMSG #esoteric :Aaah < 1424386620 208116 :oren!~oren@TOROON0949W-LP130-04-1096704252.dsl.bell.ca PRIVMSG #esoteric :Currently I am building my fortress hovering over a freshwater lake. < 1424386854 398721 :vanila!~vanila@unaffiliated/vanila QUIT :Quit: Leaving < 1424387882 844664 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1424387917 391312 :adu!~ajr@c-69-243-56-49.hsd1.md.comcast.net JOIN :#esoteric < 1424387980 62072 :PinealGlandOptic!~PinealGla@82.144.205.57 QUIT :Quit: leaving < 1424388311 678264 :Froox!~Frooxius@cust-101.ktknet.cz QUIT :Quit: *bubbles away* < 1424388722 757301 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1424389230 773754 :Tritonio!~tr@2a04:1980:3100:1aac:92e2:baff:fe42:f24c JOIN :#esoteric < 1424389377 281565 :PinealGlandOptic!~PinealGla@82.144.205.57 JOIN :#esoteric