< 1571098012 490459 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :kmc: are you into sat solvers yet < 1571098321 295591 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :not really < 1571098329 387688 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :i've been into them for brief periods in the past < 1571098338 771010 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :i wanted to use sat solvers to run Game of Life backwards < 1571098341 579526 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :but couldn't get it working < 1571098512 359987 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I was reading Knuth's fancy thing that does that. < 1571098815 977051 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1571099245 981934 :atslash!~atslash@static.231.107.9.5.clients.your-server.de QUIT :Quit: This computer has gone to sleep < 1571099690 877022 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru QUIT :Ping timeout: 240 seconds < 1571100399 240474 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :oh? < 1571100505 695150 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It's in TAOCP volume 4 fascicle 6. < 1571100551 638103 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Also there's a program at http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/knuth/pdf/sat-life.pdf ? < 1571100634 804808 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :TACOP < 1571102877 93237 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 240 seconds < 1571104289 285873 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1571106707 570182 :atslash!~atslash@static.231.107.9.5.clients.your-server.de JOIN :#esoteric < 1571109627 977091 :tromp!~tromp@2a02:a210:1585:3200:71a7:a53b:39d4:8c7e JOIN :#esoteric < 1571109884 956232 :tromp!~tromp@2a02:a210:1585:3200:71a7:a53b:39d4:8c7e QUIT :Ping timeout: 246 seconds < 1571111246 622517 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1571111282 928220 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 240 seconds < 1571111331 962719 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1571113083 549711 :imode!~linear@unaffiliated/imode QUIT :Quit: WeeChat 2.6 < 1571114586 888026 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net JOIN :#esoteric < 1571115039 969728 :tromp!~tromp@2a02:a210:1585:3200:71a7:a53b:39d4:8c7e JOIN :#esoteric < 1571115281 977589 :tromp!~tromp@2a02:a210:1585:3200:71a7:a53b:39d4:8c7e QUIT :Ping timeout: 246 seconds < 1571115872 495011 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Under what conditions does a programming language have quines? < 1571116525 357963 :aloril!~aloril@mobile-access-bcee07-58.dhcp.inet.fi QUIT :Ping timeout: 265 seconds < 1571117255 268718 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I wanted to figure out whether the existence of quines was a direct consequence of Lawvere's fixed point theorem. < 1571117269 407396 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It's surely related, but the construction is usually somewhat different. < 1571118281 969486 :tromp!~tromp@2a02:a210:1585:3200:71a7:a53b:39d4:8c7e JOIN :#esoteric < 1571118537 2379 :tromp!~tromp@2a02:a210:1585:3200:71a7:a53b:39d4:8c7e QUIT :Ping timeout: 246 seconds < 1571120293 315566 :aloril!~aloril@mobile-access-b0484f-127.dhcp.inet.fi JOIN :#esoteric < 1571122059 531077 :tromp!~tromp@2a02:a210:1585:3200:71a7:a53b:39d4:8c7e JOIN :#esoteric < 1571124537 620403 :cpressey!~cpressey@5.133.242.4 JOIN :#esoteric < 1571124713 666033 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :shachaf: I'm pretty sure any Turing-complete language whose programs can be enumerated has a quine, by the s-n-m theorem. < 1571124731 76689 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :s-m-n theorem. whetevr. it's early. < 1571124831 454501 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I guess "running a program" in the language has to considered to be able to produce an integer, or whatever the programs are enumerated with. < 1571124859 518870 :MDead!~MDude@76.5.108.106 JOIN :#esoteric < 1571125057 782577 :MDude!~MDude@76.5.108.106 QUIT :Ping timeout: 268 seconds < 1571125065 736975 :MDead!~MDude@76.5.108.106 NICK :MDude < 1571125112 709177 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm. < 1571125396 863139 :int-e!~noone@int-e.eu PRIVMSG #esoteric :@teill arseniiv "we should just wait for arriving of a good AI photo sorter" <-- I'm waiting for the AI that will create the photos that I should have taken < 1571125396 963935 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :Consider it noted. < 1571125674 209624 :b_jonas!~x@catv-176-63-24-179.catv.broadband.hu QUIT :Remote host closed the connection < 1571125831 870372 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :On the subject of quines, I was reading about Richard's paradox last night, and if I'm not mistaken, a Richardian number is basically the same as a https://esolangs.org/wiki/Narcissist < 1571125863 304071 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :cpressey: I think maybe https://en.wikipedia.org/wiki/Kleene%27s_recursion_theorem has an answer to my question. < 1571126153 566091 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :cpressey: Hmm, what's interesting about this paradox as opposed to all the other well-known paradoxes that seem identical to it? < 1571126163 929956 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, maybe it's just old. < 1571126282 911834 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net QUIT :Ping timeout: 240 seconds < 1571126384 25452 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I found it when trying to research why lambda calculus and combinatory logic are not used as deductive systems, even though they were invented as deductive systems. The Kleene-Rosser paradox that shows that ^c is inconsistent, is apparently more or less a version of Richard's paradox. < 1571126384 643943 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: Oh I didn't know of that paradox. Of course on a formal level it'll be resolved by Tarski's theorem < 1571126414 634583 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I also don't particularly see narcissists as very interestingly different from quines, though it's possible I'm missing something there. < 1571126480 888642 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Tarski's theorem = undefinablility of truth. The sentence whose truth is of interest here is "F defines a unique real number") < 1571126481 715007 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I'd have to imagine that every Turing-complete language admits a quine. How could it not? < 1571126506 511949 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :(Unless you're playing games with encoding, which don't seem that interesting to me.) < 1571126547 89006 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net JOIN :#esoteric < 1571126553 408122 :int-e!~noone@int-e.eu PRIVMSG #esoteric :TC-ness doesn't require any output capability (beyond one bit). < 1571126593 14652 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Yes, that's true. One semibit. < 1571126616 974315 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I mean a mathematical truth value. < 1571126629 236244 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But I guess I don't care about that too much. I'm looking for interesting ways in which languages can fail to have quines. < 1571126649 234996 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Not a weird three-state bit. < 1571126670 202107 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Which truth value are you talking about in particular? Halts/doesn't halt? < 1571126721 899082 :int-e!~noone@int-e.eu PRIVMSG #esoteric :accept/doesn't accept < 1571126747 692151 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :OK, sure, I guess. < 1571126753 661573 :int-e!~noone@int-e.eu PRIVMSG #esoteric :We have some wild cases that never halt. < 1571126769 278670 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, here's a different question. < 1571126776 746445 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm, I'm actually not sure how to phrase this question. < 1571126817 790183 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Lawvere's theorem is along the lines of, say you a function : A -> (A -> B) which is surjective. Then every function : B -> B must have a fixed point. < 1571126833 988950 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :(For appropriate values of "function" and "surjective" and "(A -> B)".) > 1571126847 964628 PRIVMSG #esoteric :14[[07Wagon14]]4 10 02https://esolangs.org/w/index.php?diff=66655&oldid=65529 5* 03Chris Pressey 5* (+332) 10Expand lead a little bit < 1571126849 167796 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :say you have < 1571126870 549160 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: any TC formalism will allow the kind of circularity that Kleene's fixed point theorem embodies. I.E. a program can contain a full description of itself, suitable for simulation or other analysis. < 1571126883 840283 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: Yes, that's what I was getting at. < 1571126903 714599 :int-e!~noone@int-e.eu PRIVMSG #esoteric :And I agree that it's really hard to capture this more rigorously. < 1571126916 347464 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :That seems more interesting than insisting on quines which gets into a bunch of nonsense. < 1571126928 507157 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I guess that question was about sub-TC systems. < 1571126955 680021 :int-e!~noone@int-e.eu PRIVMSG #esoteric :For the most part, Quines are just cute programming puzzles of no real importance. < 1571126960 592460 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Clearly some of those can still create quines (and use the same techniques that you'd normally use, not something one-off). < 1571126981 996543 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Also on the subject of quines: https://github.com/dpiponi/infinite-quine < 1571126984 96771 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Yes, I'm certainly not concerned with the quine itself. < 1571127042 91351 :int-e!~noone@int-e.eu PRIVMSG #esoteric :We have a notion of I/O-completeness on the wiki. An O-complete TC language has quines. < 1571127042 322654 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Anyway, on Lawvere's theorem. < 1571127075 863980 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What should I call A and B? I'm tempted to call A "Name", where A names an element of A -> B < 1571127097 268122 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :(And with that element in turn an A names a B.) < 1571127108 884810 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Surjectivity means that everything has a name. < 1571127131 539350 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :One concrete example is A as any set, and B as 2, which gives you Cantor's theorem. < 1571127171 249262 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :If you can map elements of A to subsets of A such that every subset can be named by an element, then ¬ : 2 -> 2 has a fixed point. < 1571127260 511205 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Why is (A -> B) the right codomain here in general? < 1571127355 771323 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :That's clearly not the question I want to be asking. < 1571127483 302132 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Maybe instead of B=2 I should take an example with an arbitrary B. < 1571127504 770652 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :The Y combinator gives you fixed points for any function : B -> B this way. < 1571127836 989055 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net QUIT :Ping timeout: 240 seconds < 1571127890 938486 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :OK, I guess you can say that eval : A -> (A -> B) is a two-argument function doing the same sort of thing Q(x, y) is? < 1571127901 884483 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm, no, that's nonsense. < 1571127974 631296 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :How would you phrase "eval : A -> (A -> B) is surjective" on an uncurried function eval : A×A -> B? < 1571128076 406944 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net JOIN :#esoteric < 1571128721 90193 :nfd!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net JOIN :#esoteric < 1571128802 872278 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net QUIT :Ping timeout: 240 seconds < 1571129136 989927 :nfd!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net QUIT :Ping timeout: 240 seconds < 1571129485 893366 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net JOIN :#esoteric < 1571129542 525790 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Is SK-calculus known to be confluent? I mean it *must* be, right? I've just never seen anyone say anything about it one way or the other. < 1571129618 59446 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :You can probably show it just by showing that the translation to lambda calculus preserves confluence. < 1571129618 823272 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Do you mean something other than the confluence you get if you expand every S and K to lambdas? < 1571129928 283953 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Confluence as a rewriting system? < 1571129963 113522 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm, I guess that makes more sense. < 1571129999 44242 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Speaking of SK, I still don't understand why BCKW is a good system. < 1571130014 565730 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I already like it but I'd like to like it for a good reason. < 1571130037 753641 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :shachaf: I found it easier to understand the translation between lambda calculus and BCKW than lambda calculus and SK < 1571130072 725600 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What I'd like is a connection to reordering, weakening, and contraction. < 1571130110 951906 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What's the lambda calculus translation? < 1571130145 397741 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: SK and SKI are confluent < 1571130165 454496 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I can't remember, this was about 8 years ago I did this < 1571130172 400289 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Near when I was first in here < 1571130202 820536 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :you're still in the top ten in here hth < 1571130218 900211 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net QUIT :Ping timeout: 240 seconds < 1571130227 778720 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: They are orthogonal first-order term rewriting systems. This is usually shown by introducing a parallel reduction relation and something called a "parallel moves lemma" that shows that that relation has the diamond property (ensuring confluence); the terminology is similar to that used for the lambda calculus but the proofs are actually quite a bit simpler. < 1571130253 680701 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: I forgot, did you mention having looked at Baader/Nipkow's book on term rewriting? < 1571130293 559468 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(because that stuff is all covered in that book) < 1571130313 796500 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net JOIN :#esoteric < 1571130320 349106 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Except maybe the concrete case of combinatory logic < 1571130443 956265 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Btw, orthogonal = left-linear (no duplicate variables in left-hand sides of rules) + absence of critical pairs (which you might know from Knuth/Bendix completion or the corresponding confluence criterion for terminating systems). < 1571130509 200335 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Taneb: do you also approach these systems from a point of view of abstraction elimination? < 1571130532 668856 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(BCKW(I) and SK(I)) < 1571130555 268517 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Actually, hrm. I want SBCKI, I don't like W at all. < 1571130578 779037 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :SBICK < 1571130603 361444 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :W is supposed to replace S presumably, as the only combinator that does duplication. < 1571130607 650854 :nfd9001!~nfd9001@c-67-183-33-240.hsd1.wa.comcast.net QUIT :Ping timeout: 268 seconds < 1571130611 257010 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Why don't you like W? < 1571130612 416172 :int-e!~noone@int-e.eu PRIVMSG #esoteric :myname: you missed the oppertunity there: BSICK (be sick) < 1571130634 434052 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: because it has no immediate use for abstraction elimination < 1571130634 786622 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :damn < 1571130668 760887 :int-e!~noone@int-e.eu PRIVMSG #esoteric :\x. M[x] N[x] -> S (\x.M[x]) (\x.N[x]) < 1571130703 147550 :int-e!~noone@int-e.eu PRIVMSG #esoteric :but with BCKW you artificially (to my mind) deduplicate the x first, ... -> W (\x1 x2. M[x1] N[x2]) x. < 1571130757 130942 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Well, you might be interested in talking about substructural logic. < 1571130774 96347 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I'm usually not. < 1571130779 395018 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So I could be interested in what you get with BCK without W, for instance. < 1571130794 39689 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Sure, but I also get that from SBCKI by dropping the S. < 1571130849 864333 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I don't like the flavour of duplication offered by W; I prefer the flavor offered by S. < 1571130855 683723 :int-e!~noone@int-e.eu PRIVMSG #esoteric :That's it in a nutshell. < 1571130856 787086 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :The S is serving multiple purposes, I guess. < 1571130879 77740 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I like S but I'm curious whether a simpler basis will let you pick out parts you like better. < 1571130902 45334 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm, is there a standard combinatory basis for some kind of linear lambda calculus? < 1571130903 551860 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But I'm definitely not approaching this from a logical perspective. My first encounter of combinatory logic was as a model of computation. < 1571130906 925590 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 JOIN :#esoteric < 1571130941 329443 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: Sure, BCI is the standard basis for that, add K if you allow deletion. < 1571130957 378604 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :" I'd have to imagine that every Turing-complete language admits a quine. How could it not?" => only if they can do universal IO < 1571130968 93601 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I do like B and C precisely because they capture linearity. < 1571130979 72686 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Something that SK hides. < 1571130979 971327 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :wib_jonas: Yes, see the discussion below. < 1571130989 724843 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :ah wait, I'll read on < 1571130992 358860 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :How do you turn a lambda term into BCKW? < 1571131004 37357 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Let's see. < 1571131012 939627 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :BCKW => we just had a discussion about that < 1571131028 228744 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :http://www.cs.ox.ac.uk/people/samson.abramsky/pcpt.pdf < 1571131053 51862 :int-e!~noone@int-e.eu PRIVMSG #esoteric :you have \x. M[x] N -> X (\x.M[x]) N, \x. M N[x] -> Y M (\x.N[x]), where X,Y \in {B,C}. < 1571131059 979367 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I can never remember which is which. < 1571131075 29208 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :OK, that PDF indeed makes the connection I wanted. < 1571131101 415559 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :int-e: I don't quite know what you mean by abstraction elimination (my brain isn't fully awake yet) < 1571131105 702798 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(So these look like specializations of \x. M[x] N[x] -> S (\x.M[x]) (\x.N[x]) when x does not occur freely in N or M) < 1571131112 28569 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :delambdification? < 1571131113 30973 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :SBCKI would be better, I think < 1571131124 191976 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :in particular, there are no non-empty quines in geo because it can only output decimal integers (followed by a newline), but the source has to have "print" in it to output anything < 1571131147 357766 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Taneb: the process of starting from a lambda term (which has lambda-abstractions) and turning it into an equivalent (in some sense) abstraction-free term using your combinator basis < 1571131162 440135 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :but this probably isn't an interesting reason < 1571131172 886274 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :wib_jonas: OK, but I already said that that's an encoding detail that I don't find interesting. < 1571131221 941181 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :int-e: yeah, I think that's what I do < 1571131250 626119 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :" For the most part, Quines are just cute programming puzzles of no real importance." => Smullyan and Hofstadter would disagree < 1571131328 138882 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: "quine" is just a surface phenomenon (a program that prints its own source code)... you need much more to make it computationally interesting < 1571131379 404124 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: right, that's why Golf SE tried to qualify interesting quines with a rule, so that non-cheating quines are ones that are useful for building self-referential programs < 1571131385 132910 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :int-e: Right, yes. I've read Baader and Nipkow, also some other texts on term rewriting. Didn't remember about orthogonality of term rewrite systems. Didn't really occur to me at the time to look at SK-calculus as a rewrite system. And I guess lots of other ppl don't usually look at it that way either. < 1571131410 327053 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :and, in particular, empty quines, or quines that are just a numeral in languages that echo a numeral, are considered cheating for them < 1571131501 307365 :int-e!~noone@int-e.eu PRIVMSG #esoteric :``` dc <<<6581840dnP < 1571131502 545450 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :6581840dnP < 1571131540 24554 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, I like this connection to polynomial time. < 1571131555 976818 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I don't really know good ways of talking about computational complexity for lambda calculus at all. < 1571131570 338053 :int-e!~noone@int-e.eu PRIVMSG #esoteric :That's a quine, but hardly interesting from a logical perspective... there's no real quoting (quining) going on here. < 1571131615 225890 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: That's fair. Happy to help with connecting dots :) < 1571131624 764504 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I imagine lambda calculus is just bad at talking about things like time and space constraints. < 1571131638 597334 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e, KBCSI => yeah, that could work < 1571131649 665831 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Since reduction is so unrealistic. < 1571131698 613844 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :but my problem is sort of that all of these get weird if you try to abstraction-eliminate multiple variables < 1571131730 765043 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :so could I instead advocate Amicus, which deals with functions of multiple variables naturally? < 1571131837 765064 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :«It was always hard for many to comprehend how Cantor’s mathematical theorem could be re-christened as a ”paradox“ by Russell and how Gödel’s theorem could be so often declared to be the most significant result of the 20th century. There was always the suspicion among scientists that such extra-mathematical publicity movements concealed an agenda for re-establishing belief as a substitute for s < 1571131843 723005 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :cience. Now, one hundred years after ... < 1571131846 232036 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :... Gödel’s birth, the organized attempts to harness his great mathematical work to such an agenda have become explicit.» < 1571131905 932916 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: The other thing that makes writing quine more of a puzzle is that ultimately the quining process is very automatic (one cute trick: take a description of a program P(x) that takes a description of a program Q and produces Q([Q]) by whatever notation) but you have a lot of leeway in choosing the encoding for Q, so that's what the focus tends to be on. < 1571132000 164572 :int-e!~noone@int-e.eu PRIVMSG #esoteric :In the end 6581840dnP doesn't depart from the core idea at all... but the encoding is chosen such that both priting [Q] and printing Q is done by a single dc instruction. < 1571132098 916822 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: no no, the argument Q is printed by [n] instruction, the program Q is pritned by the [P] instruction < 1571132117 836765 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: You may have mis-parsed what I wrote. < 1571132158 339818 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :`dc -e 6581840dn < 1571132158 933807 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :6581840 < 1571132162 275914 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :`dc -e 6581840dP < 1571132164 681275 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :dnP < 1571132170 488030 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: I KNOW HOW IT WORKS DAMNIT < 1571132180 741730 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :yeah, sorry, but I wasn't sure how it worked < 1571132194 933975 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :because I don't write dc stuff and the instructions are weird < 1571132204 696778 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :so I had to test it < 1571132277 851147 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(I came up with that quine myself some years ago. But it's obvious enough that I would be surprised if I was the first.) < 1571132368 144107 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :yeah. the perl quine that starts with print<< x2,$/ is also like that, multiple people come up with it independently by simply trying to write a very short quine < 1571132393 952710 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :whereas some of the other perl quines that I wrote are much less canonical < 1571132447 326010 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> text$ap(++)show"text$ap(++)show" < 1571132449 97107 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : text$ap(++)show"text$ap(++)show" < 1571132456 28171 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :https://www.perlmonks.com/?node_id=835076 these for example < 1571132500 232609 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :and I have ones like < 1571132508 342832 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :`perl -eprint+("`perl -eprint+(","\"",",","\\",")[g1012131121212133121414=~/./g]")[g1012131121212133121414=~/./g] < 1571132509 2893 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :​`perl -eprint+("`perl -eprint+(","\"",",","\\",")[g1012131121212133121414=~/./g]")[g1012131121212133121414=~/./g] < 1571132521 385225 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :where the order of the strings in the list is totally arbitrary < 1571132542 866038 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :`perl -eprint+("\\","\"",",","`perl -eprint+(",")[3,1,0,0,1,2,1,0,1,1,2,1,2,1,2,1,3,1,2,1,4,1,4]")[3,1,0,0,1,2,1,0,1,1,2,1,2,1,2,1,3,1,2,1,4,1,4] < 1571132542 957808 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So does this pattern fit into the Lawvere theorem form? < 1571132543 563546 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :​`perl -eprint+("\\","\"",",","`perl -eprint+(",")[3,1,0,0,1,2,1,0,1,1,2,1,2,1,2,1,3,1,2,1,4,1,4]")[3,1,0,0,1,2,1,0,1,1,2,1,2,1,2,1,3,1,2,1,4,1,4] < 1571132797 852842 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :ais523: here's a perl quine by mtve that has only ascii punctuation and spaces. I don't know how it works, but perhaps it also helps with your string eval question: https://www.perlmonks.com/?node_id=836752 < 1571133715 414955 :int-e!~noone@int-e.eu PRIVMSG #esoteric :woah, really... 'In late 2011, Intel [35]introduced a performance enhancement to its line of server processors that allowed network cards and other peripherals to connect directly to a CPU's last-level cache' < 1571133744 949478 :int-e!~noone@int-e.eu PRIVMSG #esoteric :[35] is https://www.intel.com/content/www/us/en/io/data-direct-i-o-technology.html < 1571133821 663294 :int-e!~noone@int-e.eu PRIVMSG #esoteric :context is https://www.schneier.com/blog/archives/2019/09/another_side_ch.html (I'm reading the october CRYPTO-GRAM) < 1571133835 632020 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: yeah, that's what spawned all the rumors about NSA backdoors < 1571133880 202185 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I'm a bit surprised I missed this. < 1571133918 960312 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I didn't miss the ME stuff (which is a backdoor by design, if you look at it cynically enough) < 1571133927 173157 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :well, it's one of the things that spawned the rumors at least < 1571133939 563184 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(I mean ME = management engine) < 1571133978 737962 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I think IME is the official abbreviation. < 1571133983 826758 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: how about the enclave thing, that lets you create encrypted parts of the memory that can run code but where the rest of the programs that the cpu runs can't read that code and its state? < 1571134027 291786 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I didn't miss that either... I see it as related really. < 1571134058 366921 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(It's also a bit of the extension of the decades old system manangement mode.) < 1571134106 214620 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :OK, when you have f.g = id, what should you call f and g? < 1571134117 259651 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :"left inverse" and "right inverse" is too confusing, I think. < 1571134124 151676 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I mean, SMM is almost as invasive, also based on hiding a region of memory, just not /designed/ to be secure. < 1571134143 81473 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :you should consider the other side though. rather than keeping all the technology that they use for the backdoors a secret that nobody will find unless they spend a man-decade of studying electron-microscope scans, they benevolently document all the backdoor capabilities of the cpu so that you can write high performance backdoors too < 1571134144 645962 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: left inverse of g; right inverse of f. < 1571134154 130682 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I've been going with "retraction" and "section" but I'm suspecting that's not so great either. < 1571134155 905742 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :it's not exclusive to the NSA, you can backdoor the bios too < 1571134173 713961 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: The problem is that if you say "f is a right inverse", I have to write down the thing to see what's going on. < 1571134258 312665 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Maybe the intuition I want is "object" and "name": Every object has at least one name, and you can pick out a canonical name (at least if you have choice). < 1571134289 947972 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :why would every object have at least one name? no way < 1571134296 841269 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: It's not even necessary to involve the NSA as a driver here... SMM was introduced to simulate legacy hardware capabilities. Secure enclaves can be perfectly explained by the desire to enforce copyright. Data direct I/O addresses a genuine (if very high-end) performance problem. < 1571134303 85550 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :especially not when the names come from a countable set and the objects come from a bigger one < 1571134309 636633 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Well, it does in this case, because you have a surjection. < 1571134329 645405 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :wait, what is SMM? < 1571134347 296728 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What's a better terminology where I can easily remember which set is the bigger one and which function goes in which direction? < 1571134352 396529 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: I mean I would be surprised if the NSA were not involved in this at all... they are too big. But I don't think they have to do anything beyond subtle nudging here. < 1571134358 260554 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: System Management Mode < 1571134368 725743 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: sure < 1571134387 413752 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: Not sure when that was introduced, i386 or i486 maybe? Around that time I think. < 1571134388 374524 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: I don't mean that it has to be the NSA specifically, that's just the name that people use in rumors < 1571134432 639066 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: but in reality it's usually the big secret agencies of all other countries that puts the backdoors there, rather than the secret agency of your country < 1571134455 538846 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: system management mode, how does that differ from ME? < 1571134456 196731 :int-e!~noone@int-e.eu PRIVMSG #esoteric :SMM can be used for things like simulating the AT keyboard interface (port 60h/61h) for USB hardware. < 1571134465 77147 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :in i386? no way < 1571134476 21863 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: It runs on the same processor. < 1571134504 156065 :int-e!~noone@int-e.eu PRIVMSG #esoteric :It's just that certain I/O operations can trigger a software emulation layer. Nothing really deep. < 1571134523 204673 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :huh, ok < 1571134532 454627 :int-e!~noone@int-e.eu PRIVMSG #esoteric :'It was first released with the Intel 386SL.' < 1571134621 131035 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: ah, so five years after the 386 < 1571134625 105196 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :that's more believable > 1571134627 449355 PRIVMSG #esoteric :14[[07Wagon14]]4 10 02https://esolangs.org/w/index.php?diff=66656&oldid=66655 5* 03Chris Pressey 5* (+599) 10More describing language overview < 1571134634 257515 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The ME is a full (but less powerful) separate core... that's a fairly recent thing. < 1571134719 80336 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But even there its existence can be explained in a perfectly innocent way. < 1571134821 347584 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Initializing a processor (memory subsystem (training DRAM, probably other I/O lines as well)) has become so complex that it's better to do it in software than in pure hardware. As a bonus, you get the ability to work around some hardware bugs in software. Now if you're Intel, which hardware platform are you likely to use for this? < 1571134872 535051 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :intel did use a 3rd party architecture (ARC) for the ME for a long time until they switched to a x86 core AFAIK < 1571134880 935395 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So now you have a separate processor on your die... and it's dormant for most of the system's operation. That's stupid maybe you can find a use for it? ... and suddenly you end up with an ME-like device. < 1571134941 884483 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :(which I found quite funny, given the origin of ARC as the superfx chip used in starfox on the super nintendo) < 1571134943 60233 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Of course the architecture is secondary. If it's a universal machine... it can be used for arbitrary purposes.) < 1571134977 383791 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :"Now if you're Intel, which hardware platform are you likely to use for this?" => I'm not familiar with the licensing situation of cpus really < 1571135024 312512 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Intel tried to make a GPU out of X86. < 1571135079 58470 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Or are trying to make... according to https://en.wikipedia.org/wiki/Larrabee_(microarchitecture) they've revived that project. < 1571135129 276359 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Intel is back at it with Larrabee? < 1571135135 760165 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :The only reason I can think of why they didn't went with x86 in the first place is that an ARC core is smaller than what intel had at that time < 1571135136 927753 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :int-e: that sounds like a ... ugh < 1571135145 690020 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :seriously, a gpu out of x86? < 1571135183 545895 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(The timing makes sense actually... now that we want to do raytracing with (I suspect) hardly predictable memory access patterns, the SIMT model will run into severe problems.) < 1571135194 603008 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: Intel. < 1571135211 20683 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: That page is very ambiguous about it. < 1571135212 994822 :int-e!~noone@int-e.eu PRIVMSG #esoteric :wib_jonas: The ones with the 0x8086 vendor id. < 1571135222 103813 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(PCI) < 1571135226 73751 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Or rather it's not ambiguous enough. Is there any definite connection to Larrabee? < 1571135471 733799 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I don't find any tangible evidence of that connection either. < 1571135478 723725 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Still, it's Intel ;-) < 1571135612 600440 :int-e!~noone@int-e.eu PRIVMSG #esoteric :And anyway, it definitely *tried*, which was my main point. < 1571137288 78393 :anima!~androirc@2a04:cec0:1006:b9e6:0:14:fd83:f401 JOIN :#esoteric < 1571137296 852734 :anima!~androirc@2a04:cec0:1006:b9e6:0:14:fd83:f401 QUIT :Client Quit < 1571137680 961384 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric : But I'm definitely not approaching this from a logical perspective. My first encounter of combinatory logic was as a model of computation. <-- That would seem to be the dominant paradigm for it these days. But I'm interested in the logical perspective of it atm. I guess you can write proofs in SKI by treating it like the Hilbert system it was derived from. But you can't use the deduction theorem < 1571137682 329466 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :for brevity, you have to write it all out in full. < 1571137718 680083 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :It sounds awful, but it also sound like you could "compile" a sentence in first-order logic, into it. < 1571137790 676623 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :my first encounter of combinatory logic was unlambda < 1571137796 825972 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Rather I think I mean, "compile" a proof written in natural deduction style in FOL, into it. < 1571137939 258127 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :"Under the Curry–Howard correspondence, the above conversion process for the deduction meta-theorem is analogous to the conversion process from lambda calculus terms to terms of combinatory logic" oh. Well. Okay then < 1571137944 216250 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: W makes perfect sense if you have an explicit rule for duplicating premises in a sequent < 1571137978 929116 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :int-e: which W is that? < 1571137993 611136 :int-e!~noone@int-e.eu PRIVMSG #esoteric :the C f x = f x x one < 1571138005 100122 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Ugh < 1571138006 261469 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :W combinator# < 1571138012 311028 :int-e!~noone@int-e.eu PRIVMSG #esoteric :W f x = f x x < 1571138031 923498 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :cpressey: see https://esolangs.org/wiki/Combinatory_logic < 1571138034 375727 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(is there another?) < 1571138115 904750 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru JOIN :#esoteric < 1571138137 602770 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :what's its bird name? < 1571138139 186218 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I was just hoping you weren't referring to some System W that I'd never heard of. Anyway yes. W is dup and C is swap and this is Forth < 1571138392 71888 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :So if the answer to my (unspoken) question "What's one of the simplest languages in which a proof can be stated and mechanically checked?" is "SK-calculus" then I guess my question becomes "How complex would a compiler from a tolerable proof language, to SK-terms, be?" < 1571138421 282481 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :that depends on what you'd call tolerable < 1571138428 981194 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :haskell to SK should be pretty easy < 1571138459 308793 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :like, we do that manually in first semester here < 1571138480 897764 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :You convert proofs written in Haskell into proofs written in SKI-calculus? < 1571138528 685409 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :not proofs as such but small programms to lambda calculus and lambda calculus to SKI < 1571138539 578057 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :removing I should be fairly easy < 1571138985 716179 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :I only remember the bird name of two combinators really: S is seregély and K is vércse < 1571139016 388040 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :also, do we have a link from the wiki to the crocodile family interpretation of lambda calculus_ < 1571139035 846339 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :we don't. I'll have to add one < 1571139092 261546 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :aren't those alligators? < 1571139108 957921 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :yeah, alligators < 1571139129 5519 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :K is clearly for cancel < 1571139245 890780 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :wib_jonas: what is that? > 1571139313 249021 PRIVMSG #esoteric :14[[07Lambda calculus14]]4 10 02https://esolangs.org/w/index.php?diff=66657&oldid=58720 5* 03B jonas 5* (+732) 10Alligator eggs < 1571139326 537002 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :Taneb: ^ < 1571139354 213118 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :I don't really like them that much < 1571139475 497379 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Birdlife: Kestrels compete with starlings for nest cavities < 1571139488 923023 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I didn't know that there was so much competition in the SK world. > 1571139663 764420 PRIVMSG #esoteric :14[[07Lambda calculus14]]4 10 02https://esolangs.org/w/index.php?diff=66658&oldid=66657 5* 03B jonas 5* (+16) 10/* External resources */ > 1571142163 263457 PRIVMSG #esoteric :14[[07Deadfish~14]]4 M10 02https://esolangs.org/w/index.php?diff=66659&oldid=66653 5* 03A 5* (-9) 10/* Implementation */ > 1571143782 538361 PRIVMSG #esoteric :14[[07Wagon14]]4 10 02https://esolangs.org/w/index.php?diff=66660&oldid=66656 5* 03Chris Pressey 5* (+1032) 10Create partially-filled-out table of primitive Wagon macros. > 1571144339 9055 PRIVMSG #esoteric :14[[07Wagon14]]4 10 02https://esolangs.org/w/index.php?diff=66661&oldid=66660 5* 03Chris Pressey 5* (+1074) 10Finish the primitives stable. No longer a stub, I think. > 1571149178 455583 PRIVMSG #esoteric :14[[07User:Camto14]]4 M10 02https://esolangs.org/w/index.php?diff=66662&oldid=60398 5* 03Camto 5* (+19) 10Lmao > 1571149256 544607 PRIVMSG #esoteric :14[[07User:Camto14]]4 M10 02https://esolangs.org/w/index.php?diff=66663&oldid=66662 5* 03Camto 5* (+6) 10Rewording > 1571149442 901085 PRIVMSG #esoteric :14[[07User:Camto14]]4 10 02https://esolangs.org/w/index.php?diff=66664&oldid=66663 5* 03Camto 5* (-70) 10Friendship ended with OOT Now Thue is my best friend > 1571149472 382768 PRIVMSG #esoteric :14[[07User:Camto14]]4 M10 02https://esolangs.org/w/index.php?diff=66665&oldid=66664 5* 03Camto 5* (+6) 10Aha > 1571149574 264797 PRIVMSG #esoteric :14[[07User:Camto14]]4 M10 02https://esolangs.org/w/index.php?diff=66666&oldid=66665 5* 03Camto 5* (+7) 10BF dialecs < 1571151464 685527 :cpressey!~cpressey@5.133.242.4 QUIT :Quit: ... < 1571153121 979498 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1571154479 72901 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1571154585 608121 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 250 seconds < 1571154586 110562 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1571156765 177823 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 QUIT :Remote host closed the connection < 1571158923 391215 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1571159381 289250 :Vorpal!~Vorpal@c193-150-231-149.bredband.comhem.se JOIN :#esoteric < 1571159381 365686 :Vorpal!~Vorpal@c193-150-231-149.bredband.comhem.se QUIT :Changing host < 1571159381 365732 :Vorpal!~Vorpal@unaffiliated/vorpal JOIN :#esoteric < 1571159814 39812 :Vorpal!~Vorpal@unaffiliated/vorpal QUIT :Quit: ZNC - http://znc.sourceforge.net < 1571160518 119203 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection < 1571160903 554896 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1571161138 593867 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1571161552 409523 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru PRIVMSG #esoteric :I had a thought to take from J its part-of-speech terminolody and strange rules (which I don’t know) and from Lojban its puristic non-european-centric approach to terminology and that to result in an obfuscation-first language but it would need more good ideas < 1571161567 822321 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu JOIN :#esoteric < 1571161932 115377 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :so I have a silly idea < 1571161975 850206 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :épelung: a spelling reform for the English language where you spell words the same as the most corresponding etymologically related word in modern German or modern French < 1571162017 642407 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :this sounds like it probably has a canonical execution somewhere on the internet, but searching for "épelung" or "épeleung" shows that those words are quasi-nonexistent, and what else would you call this system? < 1571162161 62296 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :https://repl.it/repls/ShadowyBumpyLinkedlist < 1571162341 126493 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :I don't know what it is call, perhaps, is English without English. < 1571163016 457824 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :also, yesterday's SMBC http://www.smbc-comics.com/comic/mathematicians about matrix multiplication algorithm asymptotics is fun < 1571163376 511979 :FaeFly!znc@freenode/staff/firefly PRIVMSG #esoteric :hah < 1571163951 344936 :hppavilion[1]!~omegasome@172.98.86.92 JOIN :#esoteric < 1571165869 606637 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 250 seconds < 1571167442 870394 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru QUIT :Ping timeout: 240 seconds < 1571167568 451138 :hppavilion[1]!~omegasome@172.98.86.92 QUIT :Ping timeout: 245 seconds < 1571169311 21136 :arseniiv!~arseniiv@95.105.3.55.dynamic.ufanet.ru JOIN :#esoteric < 1571169390 314385 :arseniiv!~arseniiv@95.105.3.55.dynamic.ufanet.ru PRIVMSG #esoteric :oh int-e I’ve just read what you @told that time < 1571169417 977033 :arseniiv!~arseniiv@95.105.3.55.dynamic.ufanet.ru PRIVMSG #esoteric :I’m so fast < 1571171070 45894 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Do you know how to make text formatting in PostScript? To implement printer output in the implementation of Z-machine in PostScript, I should know how to do that. < 1571171791 446597 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection < 1571172068 282036 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1571172081 614486 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection < 1571172944 247813 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :.oO(A legendary land that enters untapped and taps for one mana of any colour that could not be produced by your other mana in play.) < 1571172988 27327 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :other lands* in play < 1571172997 210742 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :OK, that might do. < 1571173002 587034 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Is there such a card? < 1571173008 456574 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :I don't know < 1571173014 735745 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :Would be kind of interesting < 1571173048 155879 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Any lands on the battlefield or any lands you control? < 1571173072 700982 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :hmm < 1571173081 129492 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :lands you control, probably? < 1571173081 238729 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Can it also be tapped for colorless? < 1571173156 697436 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :Any lands on the battlefield (including your opponents') might make it unusable < 1571173191 369774 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :I don't think it'd be able to tap for colourless, but obviously that could be a variation on the idea < 1571173628 958769 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :If you have more than one land with that ability, then what? Rule 106.7 doesn't seem to mention if they interfere with each other in this way. < 1571173638 522527 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :(Although, rule 106.7 could be fixed so that it does work.) < 1571173691 473457 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :zzo38: Well, it's a legendary land anyway. < 1571173699 793612 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes, but there are still ways to work around that. < 1571173725 553350 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :(e.g. Mirror Gallery) < 1571173848 838264 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :Probably it should be considered a land that could produce mana of any colour, so that it shuts off any other copies of itself entirely. < 1571173874 690242 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :(but yeah, there's a funny paradox there) < 1571173894 336365 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I don't think it's much of a paradox. < 1571173904 646898 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm, maybe. < 1571173910 484864 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It is a bit different from other mana abilities. < 1571173932 153469 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :It's almost exactly Russell's paradox :D < 1571173978 425263 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Sure, but I meant that answers to this kind of question are established. < 1571174014 195667 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Note that rule 106.7 does not say only mana abilities or only activated abilities. < 1571174133 47723 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :Or how about a land that can produce 2 mana of any colour that you have no devotion to? < 1571174156 250672 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes, that is another possibility, I think. < 1571174160 862534 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :That might be too good for activated abilities... < 1571174170 754275 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :O, yes, I suppose so < 1571174183 207289 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Maybe base it on color identity < 1571174325 85800 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :Cale: how does that behave if you have such a land and a Forest in play and the opponent has a Plains and an Exotic Orchard in play? < 1571174325 178441 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :In RDF format, "add one mana of any color that no other land you control could produce" might be something like: [:add-mana [:choose [:and :color, [:not [:any-could-produce [:and :land, [:controller :you], [:not :this]]]]]]]] < 1571174432 914113 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :b_jonas: I'm not sure, does Exotic Orchard usually care about predicates that restrict mana abilities? < 1571174481 261431 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :b_jonas: "Exotic Orchard doesn’t care about any restrictions or riders your opponents’ lands (such as Ancient Ziggurat or Hall of the Bandit Lord) put on the mana they produce. It just cares about colors of mana." < 1571174482 488539 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes, that is another case. Rule 106.7 mentions Exotic Orchard as an example. < 1571174515 328482 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :Cale: or more simply, how does it work if you have that land and a Forest and Reflecting Pool in play, and the opponent has four Plains? < 1571174522 860355 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :But that what you quoted is clear enough from the rules I think, but it is not relevant to the case you have here < 1571174540 290667 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :ah, okay < 1571174618 427325 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :ah, right, it does actually care about the state of the cards in play < 1571174636 991556 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :Lands that produce mana based only on what other lands “could produce” won’t help each other unless some other land allows one of them to actually produce some type of mana. For example, if you control an Exotic Orchard and your opponent controls an Exotic Orchard and a Reflecting Pool, none of those lands would produce mana if their mana abilities were activated. On the other hand, if you control a Forest and an Exotic Orc < 1571174637 154427 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :hard, and your opponent controls an Exotic Orchard and a Reflecting Pool, then each of those lands can be tapped to produce Green. Your opponent’s Exotic Orchard can produce Green because you control a Forest. Your Exotic Orchard and your opponent’s Reflecting Pool can each produce Green because your opponent’s Exotic Orchard can produce Green. < 1571174724 753436 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :But yeah, it's an additional weird twist when it's "can't produce" < 1571174790 845928 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes, all of that you mentioned is what would be done by rule 106.7. But, yes, the "can't produce" can result in no stable result, it seem like. < 1571174994 216954 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :(I would think that the RDF code I mentioned probably wouldn't compile (if a compiler for it were implemented), or if it does compile, result in an infinite loop or stack overflow.) < 1571175110 512101 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :There are a few sensible ways that one could clarify what happens, like explicitly disallowing cycles in the determination of whether an ability can produce mana of a given type. < 1571175145 575514 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes, that was also my idea about how to amend rule 106.7 < 1571175179 881172 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1571175255 657071 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :I was thinking that if you put this effect into the triggered ability of a Growth-like enchantment, maybe it becomes impossible to make a cycle, but I'm not really sure < 1571175423 571513 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Since that triggered ability is not an ability of a land, then it might work. Still, I think the rule should be amended in case > 1571175482 237419 PRIVMSG #esoteric :14[[07Unlambda14]]4 10 02https://esolangs.org/w/index.php?diff=66667&oldid=51370 5* 03B jonas 5* (+312) 10/* External resources */ IOCCC winner interpreter < 1571175557 115939 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :zzo38: right, but it's hard to know whether there is a way to turn it into a land, or have an ability that cares about what mana some non-land permanents could produce, now or in future cards < 1571175586 482643 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes, I thought of that, which is why the rule should be amended anyways in case < 1571175601 524912 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :Imprisoned in the Moon can turn an existing permanent into a land < 1571175654 337328 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Although it deletes that permanent's abilities, too. < 1571175712 968871 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :yes, that's why I think that doesn't help < 1571175853 681231 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes. < 1571175933 664292 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :(My own opinion is the rules ought to support combinations that do not currently exist.) < 1571175970 379029 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :I also made up this land card (based on the story of the GURPS I have played): Sun Town {-} Legendary World Land ;; Vehicles cannot enter the battlefield. ;; At the beginning of each end combat step, end the turn. ;; {T}: Add {C}. ;; {1}, {T}: Add {W}. < 1571176031 235301 :b_jonas!~x@catv-176-63-25-66.catv.broadband.hu PRIVMSG #esoteric :Song of the Dryads is another such card < 1571176108 514377 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Yes, but rule 305.7 causes its abilities to be deleted. < 1571176191 34739 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Still, if something else can grant it an ability, then it can be kept and rule 305.7 only deletes the abilities due to its own text. < 1571176364 173235 :Cale!~cale@2607:fea8:9960:35:8d5b:8718:10af:5872 PRIVMSG #esoteric :Wow, vehicle hate < 1571179953 44364 :imode!~linear@unaffiliated/imode QUIT :Quit: WeeChat 2.6 < 1571180274 874286 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1571180413 436358 :tromp!~tromp@2a02:a210:1585:3200:71a7:a53b:39d4:8c7e QUIT :Remote host closed the connection < 1571181072 165388 :FreeFull!~freefull@defocus/sausage-lover QUIT : < 1571181893 953471 :arseniiv!~arseniiv@95.105.3.55.dynamic.ufanet.ru QUIT :Ping timeout: 246 seconds < 1571182558 720004 :Sgeo_!~Sgeo@ool-18b982ad.dyn.optonline.net JOIN :#esoteric < 1571182777 736259 :Sgeo__!~Sgeo@ool-18b982ad.dyn.optonline.net QUIT :Ping timeout: 268 seconds < 1571183528 903498 :tromp!~tromp@ip-213-127-58-74.ip.prioritytelecom.net JOIN :#esoteric < 1571183786 872260 :tromp!~tromp@ip-213-127-58-74.ip.prioritytelecom.net QUIT :Ping timeout: 240 seconds