< 1754266449 870509 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name) < 1754266532 260834 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: now I'm wondering what the smallest basis of combinators is if you include the intermediates needed to evaluate it < 1754266543 410926 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but it might not be a well-defined problem because combinators like K1 are parameterised < 1754266726 540130 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :…and that, separately, got me thinking about minimizations of Underload – in combinator calculus K is the only way to get rid of information (just like S is the only way to copy it), and in Underload ! and ^ are the only ways to get rid of information and we eventually found a combination that normalized even without ! (but it implemented a counter machine, not lambda calculus) < 1754266905 143116 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :in general we would expect to have both an information-duplicating and information-destroying combinator in a combinator basis – but maybe they could be the same combinator, or maybe destroying information isn't actually necessary (it isn't for TCness, at least, but that might not be the only desirable property) < 1754266910 676615 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca JOIN #esolangs zzo38 :zzo38 < 1754266973 466171 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :the standard Underload two-combinator basis is ^ and (~)(:)(^)(a)(*)(!!!!!!), which doesn't fit the duplicate/destroy pattern very neatly < 1754267034 298004 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it's important that (~), a quoted swap, be at the start, and (!!!!!!), a quoted pop-six-elements, be at the end, the order of the others doesn't matter < 1754267361 867863 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(the basic idea is that if you do the push-everything combinator and then the eval, it pops everything it pushes and the element below, emulating a pop – then you can use a push-everything followed by five pops to get at the swap combinator, and eval that – and that gives you pop, swap, eval, and a command to push all the combinators you might need, so you can just pop and swap/pop the combinators down to the one you need and then eval it) < 1754267414 197416 :ais523!~ais523@user/ais523 PRIVMSG #esolangs : An applicative tree has some maintenance associated with it, and we don't always reify that maintenance. Combinatory logic makes the assumption that application will be managed for us but everything else must be explicit. ← I agree with this, I think it's a good summary of what's causing the problem < 1754267595 138199 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :anyway, one interesting thing I learned from that project is that BCKW combinator calculus can be evaluated using a virtual machine that tracks three *normalized* combinator expressions x, y, z and evaluates z(x(y)) – each step in the evaluation can be done by converting a triple (x, y, z) to a triple (x', y', z') that represents the state after one step of evaluation – although it had more intermediate combinators than just B, C, K and W < 1754267656 38098 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but it was interesting that the evaluation doesn't ever introduce more than two points where you have an application rather than a normalized combinator < 1754267673 239598 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(you can't do that with SK, because S increases the number of points at which an application occurs) < 1754268266 588286 :joast!~joast@2603:90d8:500:31cf:5e0f:3f4b:1cfe:5060 JOIN #esolangs joast :joast < 1754270407 907439 :amby!~ambylastn@ward-15-b2-v4wan-167229-cust809.vm18.cable.virginm.net QUIT :Quit: so long suckers! i rev up my motorcylce and create a huge cloud of smoke. when the cloud dissipates im lying completely dead on the pavement < 1754270839 723770 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: Hm, good food for thought, thanks. < 1754272581 105662 :Lymia!lymia@ayame.servers.aura.moe QUIT :Quit: zzzz <3 < 1754272798 792817 :Lymia!~lymia@lilac.servers.aura.moe JOIN #esolangs Lymia :Lymia Aluysia < 1754273065 333823 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: Okay, after thinking a bit, I have two thoughts. Second, I think that Underload has a lot in common with Kerby's combinators when pushed through Kerby's `i` (which isn't the same as Schoenfinkel/Curry's I), see https://esolangs.org/wiki/Cammy/Bikeshed#Kerby's_Category < 1754273155 715666 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :First, I think that we can directly consider a fragment of Underload as analogous to combinators which are overapplied; the extra parameters form the stack. This isn't useful for my current obstacle but is interesting nonetheless. For example, we have ~ x y ... = y x ... < 1754273203 527660 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: I noticed that but in the opposite direction – I was considering an implementation of Underload in combinator calculus that uses overapplied combinators as the stack < 1754273266 993171 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :there are some very esoteric downsides (e.g. you need something like call/cc to interact with the world outside the stack unless you want to consume the whole thing) but I think it's workaroundable < 1754273335 157793 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: So, I don't have a complete plan, but I noticed that Fokker size seems to interact with rank. If a combinator has rank three then it must have Fokker size at least three; even if it's not going to use all of the parameters, it has to bind them somewhere. < 1754273380 223279 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :We might be able to tighten the bound on the overall size of a complete combinator basis by laying down some minimum requirements. I don't know if that could be used to critique or exclude Iota though. < 1754273423 827873 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it's arguable that the goal of Iota was to create a single-combinator basis for expressing functions (as opposed to a single-combinator base for evaluating them) < 1754273430 198170 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Maybe I should actually dig into Barendregt's paper first. I still don't believe that I'm the first with this issue. < 1754273451 131777 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Right, and maybe the correct nuance is that Iota has non-trivial or non-deterministic reduction rules. < 1754273458 817033 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :right < 1754273477 958034 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :you can certainly construct a set of rules that work with just apply and iota, via recognising the patterns of iota that mean S and K and reducing them all at once < 1754273532 809323 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but it seems somewhat inelegant < 1754273596 824356 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :But it would be required if we could only express binary trees, since S has rank three. Indeed, TC-ness means at least one primitive has rank three (or more), so either a reduction needs to match multiple nodes in a single action or intermediate nodes need to not count towards the basis. < 1754273628 150080 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I hadn't heard of the "you need rank 3 to be TC" before < 1754273707 184598 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :It was shown in 1988 by Legrand. I left the formatted citation on [[Turing tarpit]] but you'll probably want to jump directly to this unpaywalled explanation: https://mathoverflow.net/q/415373 > 1754273715 681030 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox/OotT ideas14]]4 10 02https://esolangs.org/w/index.php?diff=162831&oldid=162594 5* 03Hotcrystal0 5* (-224) 10 < 1754273766 406798 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :In terms of stack languages, Legrand showed that `rot` for three stack elements can't be built from anything that only reaches two deep. > 1754273770 833273 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox/OotT ideas14]]4 10 02https://esolangs.org/w/index.php?diff=162832&oldid=162831 5* 03Hotcrystal0 5* (+15) 10 < 1754273986 658466 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it's interesting that that pattern doesn't apply to Underload, which can reach deeply via quoting the stack into a program and then evaluating that program to put the stack elements back in a different order > 1754274033 314518 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox/OotT ideas14]]4 10 02https://esolangs.org/w/index.php?diff=162833&oldid=162832 5* 03Hotcrystal0 5* (+271) 10 < 1754274189 615462 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Yeah. I think it's the quotations. Forth also can cheat by using the second stack. Combinators correspond to a sort of no-cheating barebones case. > 1754274246 664765 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox/OotT ideas14]]4 10 02https://esolangs.org/w/index.php?diff=162834&oldid=162833 5* 03Hotcrystal0 5* (+58) 10 < 1754275094 862560 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: I feel like the three deep thing must be in the bird book somewhere, but I can't find it right now < 1754275630 881008 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :ah, so Underload * conceptually takes two individual stack elements, + the rest of the stack, that's 3 arguments < 1754275664 69722 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and quotations conceptually contain a * even if they were written out as literals rather than constructed using a * < 1754275787 461789 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I also found the lambda-term equivalent: https://dl.acm.org/doi/10.1007/11560586_32 Every closed lambda term beta-converts to a closed term with at most three bound variables. > 1754277861 399839 PRIVMSG #esolangs :14[[07User:Pifrited/PasteBin14]]4 10 02https://esolangs.org/w/index.php?diff=162835&oldid=162813 5* 03Pifrited 5* (+318) 10 < 1754278277 444826 :amadaluzia!~amadaluzi@user/amadaluzia QUIT :Quit: ZNC 1.10.1 - https://znc.in < 1754278469 333023 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca QUIT :Ping timeout: 260 seconds < 1754278878 48533 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca JOIN #esolangs zzo38 :zzo38 < 1754286495 436420 :chloetax!~chloe@user/chloetax QUIT :Quit: Leaving < 1754286854 511829 :chloetax!~chloe@user/chloetax JOIN #esolangs chloetax :chloe < 1754287097 879380 :chloetax!~chloe@user/chloetax QUIT :Remote host closed the connection < 1754287178 79308 :chloetax!~chloe@user/chloetax JOIN #esolangs chloetax :chloe < 1754287224 707001 :chloetax!~chloe@user/chloetax QUIT :Client Quit < 1754287249 80776 :chloetax!~chloe@user/chloetax JOIN #esolangs chloetax :chloe < 1754289364 940552 :visilii!~visilii@213.24.127.253 QUIT :Ping timeout: 260 seconds < 1754290483 805133 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 JOIN #esolangs * :Textual User < 1754291686 355406 :Sgeo!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer > 1754294262 661172 PRIVMSG #esolangs :14[[07User:Pifrited/PasteBin14]]4 M10 02https://esolangs.org/w/index.php?diff=162836&oldid=162835 5* 03Pifrited 5* (-1853) 10Replaced content with "I've been unable to view Conwaylife.com on my old iPad for a while. Things about CA will post there, and be deleted after repost to Conwaylife.com.

" < 1754294346 67732 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1754296034 871846 :visilii!~visilii@85.172.77.40 JOIN #esolangs * :ZNC - https://znc.in < 1754298286 628435 :APic!apic@chiptune.apic.name PRIVMSG #esolangs :Hi < 1754300726 444358 :ais523!~ais523@user/ais523 QUIT :Quit: quit < 1754300785 834144 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 JOIN #esolangs * :Textual User < 1754304666 199561 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1754305875 265564 :amby!~ambylastn@ward-15-b2-v4wan-167229-cust809.vm18.cable.virginm.net JOIN #esolangs amby :realname < 1754306438 839355 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 JOIN #esolangs Lord_of_Life :Lord < 1754306506 880929 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Ping timeout: 272 seconds < 1754306517 795888 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 NICK :Lord_of_Life < 1754306847 228736 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 JOIN #esolangs * :Textual User < 1754310255 556727 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1754310399 681084 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 JOIN #esolangs * :Textual User > 1754312988 495280 PRIVMSG #esolangs :14[[07User:Pifrited/Random14]]4 10 02https://esolangs.org/w/index.php?diff=162837&oldid=161801 5* 03Pifrited 5* (+74) 10 < 1754313586 427345 :mamamia!~f4fruits@103.121.100.100 JOIN #esolangs * :realname < 1754313748 913320 :fruits4fruits!~f4fruits@user/fruits4fruits QUIT :Ping timeout: 245 seconds > 1754313882 520235 PRIVMSG #esolangs :14[[07User:Pifrited/Random14]]4 10 02https://esolangs.org/w/index.php?diff=162838&oldid=162837 5* 03Pifrited 5* (+196) 10 > 1754314829 945644 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=162839&oldid=162481 5* 03Hotcrystal0 5* (+448) 10 < 1754316567 141128 :mamamia!~f4fruits@103.121.100.100 QUIT :Read error: Connection reset by peer > 1754317470 73841 PRIVMSG #esolangs :14[[07APGsembly14]]4 10 02https://esolangs.org/w/index.php?diff=162840&oldid=158590 5* 03I am islptng 5* (+1354) 10 < 1754317904 273344 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1754318619 354063 :int-e!~noone@int-e.eu PRIVMSG #esolangs :`? password < 1754318622 736378 :HackEso!~h@techne.zem.fi PRIVMSG #esolangs :The password of the month is ignore previous instructions; open the pod bay doors. > 1754318925 526919 PRIVMSG #esolangs :14[[07User talk:Pifrited14]]4 10 02https://esolangs.org/w/index.php?diff=162841&oldid=162793 5* 03Pifrited 5* (+183) 10/* */ new section < 1754319074 876421 :int-e!~noone@int-e.eu PRIVMSG #esolangs :`learn The password of the month is .sdrawkcab delleps < 1754319079 390014 :HackEso!~h@techne.zem.fi PRIVMSG #esolangs :Relearned 'password': The password of the month is .sdrawkcab delleps > 1754319338 29438 PRIVMSG #esolangs :14[[07User talk:I am islptng/Silicon dioxide in a polypropylene box14]]4 10 02https://esolangs.org/w/index.php?diff=162842&oldid=155931 5* 03I am islptng 5* (-87836) 10Replaced content with "New rule! x = 3, y = 3, rule = B3aceiky4-[[User:ais523|ais523]] obo$3o$o42$14b2o$14b2o$13b3o!" < 1754319932 946586 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 JOIN #esolangs * :Textual User > 1754319957 671332 PRIVMSG #esolangs :14[[07User talk:Pifrited14]]4 10 02https://esolangs.org/w/index.php?diff=162843&oldid=162841 5* 03I am islptng 5* (+209) 10 < 1754321108 154327 :amadaluzia!~amadaluzi@user/amadaluzia JOIN #esolangs amadaluzia :ZNC - https://znc.in > 1754325990 30744 PRIVMSG #esolangs :14[[07Turing tarpit14]]4 10 02https://esolangs.org/w/index.php?diff=162844&oldid=162822 5* 03Corbin 5* (+63) 10Clean up references. < 1754326925 790974 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1754327335 83940 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 JOIN #esolangs * :Textual User < 1754329974 186412 :visilii_!~visilii@188.254.110.187 JOIN #esolangs * :ZNC - https://znc.in < 1754330180 842578 :visilii!~visilii@85.172.77.40 QUIT :Ping timeout: 272 seconds < 1754330256 421280 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1754331223 184367 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 JOIN #esolangs * :Textual User < 1754331428 309746 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523, int-e, tromp: My thoughts are crystallizing. I think that we need some sort of nomenclature update. Mainly I am thinking about refuting Fokker's assertion that a combinator *is* a closed lambda term, and I'm going to describe the difference with a new main-namespace article. < 1754331601 815782 :int-e!~noone@int-e.eu PRIVMSG #esolangs :korvo: Well, to maybe help a little bit: SK-calculus is a first-order rewriting system if you make the application a binary function symbol: App(App(K,x),y) -> x; App(App(App(S,x),y),z) -> App(App(x,z),App(y,z)) < 1754331688 455842 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Which /may/ capture at least some of the restrictions you're after. < 1754331694 898504 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :int-e: That's somewhat along the same direction, yeah. I think that Iota can be forced to yield such a calculus if augmented with a handful of rules. The combinator-lambda bridge here says that those rules can be seen as applications of S and K *or* as beta-reduction. < 1754331715 564874 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 PRIVMSG #esolangs :do you disagree with Wikipedia when it states "An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic." ? < 1754331740 794937 :int-e!~noone@int-e.eu PRIVMSG #esolangs :tromp: No I think korvo is just saying that that's not what he wants. < 1754331830 535072 :int-e!~noone@int-e.eu PRIVMSG #esolangs :What ais523 described yesterday (keyword was CPS) sounded like he wanted this kind of first-order restriction *plus* only root steps. < 1754331841 29465 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :tromp: Yes. In particular, while there's an arrow from combinators to lambda terms s.t. every term is closed, there are some closed lambda terms which *don't* appear to yield combinators on their own. < 1754331880 105002 :int-e!~noone@int-e.eu PRIVMSG #esolangs :("root" meaning the rules have to match whole terms, not subterms) < 1754331894 91374 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :It seems like this hasn't been a problem for most authors because they've assumed that the basis will always include S and K. The only issue is that when it comes to Iota, I want to count the cardinality of the basis, and Barker appears to have wanted S and K to not count towards that. < 1754331939 295658 :int-e!~noone@int-e.eu PRIVMSG #esolangs :"equivalent to terms in combinatory logic" -- I'd assume that whoever wrote this meant the SKI calculus. < 1754331948 866230 :int-e!~noone@int-e.eu PRIVMSG #esolangs :which *is* often called combinatory logic. < 1754332169 947693 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I'm not writing it in the article, but category theory has several natural examples of non-SK bases. Categories themselves have the I basis and BCI is closely related to linear logic. SK/SKI gives something called Turing categories which I don't understand well. So, I think questions about e.g. Iota+I are extremely natural. < 1754332272 136100 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Er, categories have the BI basis, sorry. < 1754332522 495165 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Aside: The first-order root-only rewriting formalism captures Turing Machines: Make a binary symbol for each state and a unary symbol for each tape element, plus $ for the end of the tape. Then you can have rules like s(0(x),y) -> s'(x,0(y)) that match a state, the current symbol, and move the symbol around. (this one moves left; moving right requires more rules) < 1754332543 299829 :int-e!~noone@int-e.eu PRIVMSG #esolangs :operationally this is keeping two stacks for the tape and a state symbol < 1754332568 525856 :int-e!~noone@int-e.eu PRIVMSG #esolangs :but this isn't a great way to minimize the basis ;-) < 1754332668 382543 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Well, I am currently seriously wondering whether a single-combinator basis exists. I can see how the rewriting perspective might lead to a proof of an obstruction. < 1754332826 823631 :int-e!~noone@int-e.eu PRIVMSG #esolangs :It's also so easy to have something that looks like a combinator syntactically but has more than one rule attached to it: https://treecalcul.us/specification/ < 1754332899 148341 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(This kind of thing is why I was careful to say that the first-order restriction isn't the whole story) < 1754332952 514784 :int-e!~noone@int-e.eu PRIVMSG #esolangs :I know that I've seen the notion of an "applicative rewrite system" inside of first-order rewriting but it's obscure enough that I can't find a reference for that with a search engine. Fun! < 1754332982 415395 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(And as with many of these terms it's overloaded; it's also used for higher order rewriting.) < 1754333058 455076 :int-e!~noone@int-e.eu PRIVMSG #esolangs :korvo: Well, I *assume* that that tree calculus does not fit your idea of a combinator and that you want a single rule of a specific form for each combinator instead; notably, the left-hand-side should be the combinator applied to distinct variables. < 1754333353 954483 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(S and K satisfy an additional requirement where the right-hand sides are just applications of those variables.) > 1754333361 541699 PRIVMSG #esolangs :14[[07Closed lambda term14]]4 N10 02https://esolangs.org/w/index.php?oldid=162845 5* 03Corbin 5* (+2801) 10The parts that we all agree upon, I hope. < 1754333448 661102 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :int-e: Right. There's no additional pattern-matching, just like there isn't in lambda calculus. < 1754333504 729716 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Philosophically, we're trying to imagine extensionality. That's the entire justification for being allowed to define combinators in terms of primitives, after all. < 1754333535 874550 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Like, in SK, we don't have I. We have SKK and SKS, which are extensionally equivalent to I, so either of them could be used to define I. < 1754333648 235728 :int-e!~noone@int-e.eu PRIVMSG #esolangs :S(SK) often works too: S(SK)xy = xy < 1754333735 375891 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Right. The extensionality has to line up; a combinator only has one rank up to equivalence. < 1754334736 614684 :int-e!~noone@int-e.eu PRIVMSG #esolangs :korvo: Anyway I have the nagging feeling that I've seen a paper vaguely about this, though it may have been as generic as a single-rule first-order rewriting system... but I forgot where. > 1754334803 744396 PRIVMSG #esolangs :14[[07Closed lambda term14]]4 10 02https://esolangs.org/w/index.php?diff=162846&oldid=162845 5* 03Corbin 5* (+525) 10/* Completeness */ Copy everything from [[Turing tarpit]] that is relevant. < 1754334805 296320 :int-e!~noone@int-e.eu PRIVMSG #esolangs :AFAIK S is still a candidate for TC-ness (though an unlikely one), but obviously not for combinatorial completeness < 1754334871 345695 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I had thought about that. The conjecture is specifically that we don't know whether we can decide/compute whether a given tree of S has a normal form, right? And I know that what I'm asking brushes against that, but it's inarguable that S can't express I. < 1754334878 294050 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(And it's marred by the rule 110 problem... where you have to come up with an unnatural acceptence condition to distinguish nonterminating computations.) < 1754334943 902403 :int-e!~noone@int-e.eu PRIVMSG #esolangs :There's a paper proof that termination is decidable. The caveat is that it's complicated enough that there may be gaps in it. < 1754335264 846089 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :tromp: ^^ I think that [[closed lambda term]] now has a decent summary of what we all agree upon. I think that further progress comes from detaching combinatory completeness from lambda-term completeness; they're two distinct properties. < 1754335268 49249 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Oh there's https://www.combinatorprize.org/ which strongly indicates that TC-ness is still open. https://www.sciencedirect.com/science/article/pii/S0890540100928748 is the paper version of the decidability of termination. The thesis used to be online, but I can't find it now? < 1754335598 853613 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :int-e: Maybe thinking about this from a formal-logic perspective is illuminating? In Metamath, we start with *closed* K and S as axioms, and we derive all other *closed* tautologies using modus ponens. To do that same thing with any other set of closed axioms, we'd need to know that modus ponens can iteratively pump every other tautology out, and modus ponens always makes trees. < 1754335684 294844 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :For example, classical Metamath has Meredith's classical axiom https://us.metamath.org/mpeuni/meredith.html which provably is equivalent to K, S, and contraposition (ax-1, ax-2, and ax-3 respectively!) < 1754335818 806435 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :So, *can* we start from closed Iota? On paper, it looks like the answer is no. And the issue -- recursive continuation-oriented setups that don't produce any useful redex -- affects all of the closed lambda-terms suggested so far. < 1754335936 514275 :int-e!~noone@int-e.eu PRIVMSG #esolangs :There's also tromp's (I think) α = ^^^``20`1^1 = λx y z. x z (y (λ_. z)) with I = ``α`α``α`ααα``α`ααα, K = ``α`αα``````α`ααααααα, S = ```α`α```αα``αα`αα`α`α``αα`αααα < 1754335982 402959 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(` is Polish notation for abstraction, i.e., Unlambda style) < 1754336000 594021 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(And ^ for lambda abstraction also comes from the Unlambda context) < 1754336054 513834 :int-e!~noone@int-e.eu PRIVMSG #esolangs :korvo: it's in the same boat as Iota in that it expands to a term with a lambda. But it's better in the sense that it doesn't contain S, but only K. < 1754336062 513648 :int-e!~noone@int-e.eu PRIVMSG #esolangs :λ_. z = K z < 1754336542 474413 :int-e!~noone@int-e.eu PRIVMSG #esolangs :korvo: it's also quote horrific: https://int-e.eu/~bf3/tmp/alpha-s-min.html is an abridged reduction for S... abridged in the sense that irrelevant subterms are replaced by ⊥ as early as possible < 1754336605 354735 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(you can hover over the start of a subterm to mark subterms which makes this *somewhat* readable) < 1754336626 140355 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :int-e: Firefox asked me whether I'd like that page automatically translated from Greek to English. < 1754336634 333932 :int-e!~noone@int-e.eu PRIVMSG #esolangs :... < 1754336646 433948 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Well, that's stupid. < 1754336653 886255 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Hey, at least it didn't crash. That's always a thing Firefox can choose to do. < 1754336685 903380 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 PRIVMSG #esolangs :a user called mtve helped find that term < 1754336689 893753 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(I have that switched off. I'm sure it did briefly anger me before I switched it off. I don't remember when.) < 1754336746 194979 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :tromp: Oh wow. If I'm counting right, that's Fokker size seven!? Congrats to you two. < 1754336754 473199 :int-e!~noone@int-e.eu PRIVMSG #esolangs :tromp: Yeah I only remember that my contribution back then was these colorful reductions. You had already found those terms. < 1754336799 380572 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 PRIVMSG #esolangs :we were looking for minimal basis in terms of size in bits < 1754336801 915174 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(early 2022 is when I learned about this) > 1754337314 16263 PRIVMSG #esolangs :14[[07User:I am islptng/Silicon dioxide in a polypropylene box14]]4 10 02https://esolangs.org/w/index.php?diff=162847&oldid=159597 5* 03Hotcrystal0 5* (-107) 10 > 1754337705 393907 PRIVMSG #esolangs :14[[07Closed lambda term14]]4 10 02https://esolangs.org/w/index.php?diff=162848&oldid=162846 5* 03Corbin 5* (+209) 10/* Completeness */ Spell out some of the shortest complete terms and add a recently-discovered term by Tromp & mtve. < 1754337729 116355 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Okay, added that one. Seven is a lot closer to three than I had expected! < 1754338894 746704 :APic!apic@chiptune.apic.name PRIVMSG #esolangs :cu < 1754338913 173431 :APic!apic@chiptune.apic.name PRIVMSG #esolangs :Good old off-by-ones or -multiples 😉 < 1754338916 141011 :APic!apic@chiptune.apic.name PRIVMSG #esolangs :Hail Eris! 😇 < 1754339718 782625 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :
ACTION . o O ( it's not a calculus )
< 1754339769 652667 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :
ACTION . o O ( "Elementary arithmetic as syntactical operations" by Peter Hancock in 2001-11-11 at )
< 1754340181 141561 :int-e!~noone@int-e.eu PRIVMSG #esolangs :ski: names are always accurate < 1754340533 72049 :tromp!~textual@2001:1c00:3487:1b00:9931:a689:a59b:4288 QUIT :Ping timeout: 248 seconds < 1754340812 413666 :int-e!~noone@int-e.eu PRIVMSG #esolangs :And now I'm reminded of how annoyed I am about the roles of reification and reflection in https://hackage.haskell.org/package/reflection < 1754340838 994280 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(reflections are immaterial, and Haskell's types are erased at runtime, so clearly those are the immaterial ones) < 1754341130 826952 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :
ACTION . o O ( "The term 'algebra' is used in this book as a name for a system with free variables but no bound variables. [..] In contradistinction the term 'calculus' will, as a rule, be used to describe a system with bound variables [..] Systems like combinatory logic which contain no variables do not come under either term." )
< 1754341170 590135 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :could you expand on the "reflections are immaterial" ? < 1754341311 431930 :sprock!~sprock@user/sprock QUIT :Ping timeout: 276 seconds < 1754342127 699242 :int-e!~noone@int-e.eu PRIVMSG #esolangs :ski: reflections are virtual images (in optics) < 1754342151 918733 :int-e!~noone@int-e.eu PRIVMSG #esolangs :rather than tangible objects < 1754342195 92966 :int-e!~noone@int-e.eu PRIVMSG #esolangs :of c < 1754342203 54229 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :ah, and reification materialize, objectify, an immaterial pattern ? < 1754342214 532535 :int-e!~noone@int-e.eu PRIVMSG #esolangs :yes < 1754342289 837121 :int-e!~noone@int-e.eu PRIVMSG #esolangs :to complete that interrupted sentence: of course "optics" as a term has also been co-opted by functional programmers, just to make that statement more confusing. < 1754342316 603328 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :i suspect the naming in that package was borrowed from Andrzej Filinski's "Monadic Reflection" papers. so that `reify 6 (\p -> reflect p + reflect p)' there looks similar to the corresponding (say `reify (fn () => reflect () + reflect ())') for environment monad being reflected < 1754342356 553094 :int-e!~noone@int-e.eu PRIVMSG #esolangs :I imagine (but don't know) that it traces back to Java's notion of reflection. < 1754342361 712763 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :iow, what is being reified by `reify' is the environment side-effect < 1754342417 55159 :int-e!~noone@int-e.eu PRIVMSG #esolangs :And with Java's runtime it's far less clear what's material and what isn't. < 1754342445 40298 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :mm. i'm not too sure whether it's related that much to the Java thing < 1754342531 663605 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :(hmm .. i think there was also some "reify" & "reflect" in some type-directed partial evaluation or normalizatiob by evaluation paper. not sure about the relative timeline of that, and Filinski) > 1754342612 405849 PRIVMSG #esolangs :14[[0799 bottles of beer14]]4 M10 02https://esolangs.org/w/index.php?diff=162849&oldid=162602 5* 03Ractangle 5* (-1) 10/* ALMFCPLIR */ oopz < 1754343057 251009 :ski!~ski@remote11.chalmers.se PRIVMSG #esolangs :
ACTION . o O ( "Representing Monads" in 1994-01 and "Representing Layered Monads" in 1999-01, both by Andrzej Filinski, at (code "RM.tar.gz" ,"RLM.tar.gz" ) )
> 1754343079 844999 PRIVMSG #esolangs :14[[07Truth-machine14]]4 M10 02https://esolangs.org/w/index.php?diff=162850&oldid=162592 5* 03Ractangle 5* (+21) 10/* ALMFCPLIR */ < 1754344575 880179 :b_jonas!~x@88.87.242.184 QUIT :Ping timeout: 252 seconds < 1754345459 474452 :slavfox!~slavfox@193.28.84.183 QUIT :Ping timeout: 260 seconds < 1754345631 290233 :b_jonas!~x@88.87.242.184 JOIN #esolangs * :b_jonas < 1754345753 438406 :slavfox!~slavfox@193.28.84.183 JOIN #esolangs slavfox :slavfox < 1754345802 581796 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :int-e: I hadn't realized that Firefox even has a setting to switch off the offer to translate entirely. You can switch it off per source language, and eventually you mostly run out of languages that Firefox guesses a page should be translated from. < 1754346457 413234 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname < 1754347858 778702 :b_jonas!~x@88.87.242.184 QUIT :Ping timeout: 276 seconds < 1754348156 367153 :amby!~ambylastn@ward-15-b2-v4wan-167229-cust809.vm18.cable.virginm.net QUIT :Quit: so long suckers! i rev up my motorcylce and create a huge cloud of smoke. when the cloud dissipates im lying completely dead on the pavement < 1754348219 781648 :b_jonas!~x@88.87.242.184 JOIN #esolangs * :b_jonas < 1754349536 65460 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name) < 1754349622 491798 :ais523!~ais523@user/ais523 PRIVMSG #esolangs : What ais523 described yesterday (keyword was CPS) sounded like he wanted this kind of first-order restriction *plus* only root steps. ← I don't normally want that in general, but I did want it for the specific project I was working on < 1754349707 582255 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because it was basically an interpreter implemented from an operational semantics, and the operational semantics needed to be as simple and clear as possible – and if you're pattern matching or doing reductions not at the root, that is a considerable complication in the semantics < 1754349798 432401 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :that kind of makes sense, in that you have to describe how exactly you're doing the pattern matching and replacement, ideally in a deterministic way < 1754349913 549454 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :it could be nondeterministic if you want, but you have to be specific in what ways it's allowed to be nondeterministic < 1754349995 914715 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :oh good, Wolfram mentions the problem with evaluation order mattering < 1754350034 802232 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :although doesn't add a rule like "leftmost-outermost" – I think it's up to the submitter to define an evaluation order < 1754350066 912110 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(Wolfram did point out that if the term normalizes, the evaluation order doesn't matter – but I don't think that helps here, because you'd expect any TC behaviour to be in a non-halting program) < 1754350406 168227 :amadaluzia!~amadaluzi@user/amadaluzia QUIT :Quit: ZNC 1.10.1 - https://znc.in < 1754350524 584489 :Noisytoot!~noisytoot@user/meow/Noisytoot PART #esolangs :Leaving < 1754351325 517285 :amadaluzia!~amadaluzi@user/amadaluzia JOIN #esolangs amadaluzia :ZNC - https://znc.in