`A`

. the tape is circular so going to the end of the tape will bring you back to the start === syntax === Command
> 1722237422 277230 PRIVMSG #esolangs :14[[07Xx14]]4 10 02https://esolangs.org/w/index.php?diff=134202&oldid=134201 5* 03Gggfr 5* (+14) 10
< 1722237605 956495 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
> 1722238688 439464 PRIVMSG #esolangs :14[[07Genera Tag14]]4 M10 02https://esolangs.org/w/index.php?diff=134203&oldid=125981 5* 03PkmnQ 5* (+2) 10/* Semantics */ Probably better wording
> 1722239115 787130 PRIVMSG #esolangs :14[[07Python but it's trash14]]4 10 02https://esolangs.org/w/index.php?diff=134204&oldid=134157 5* 03PkmnQ 5* (-141) 10No need for factorials
< 1722239197 936015 :__monty__!~toonn@user/toonn JOIN #esolangs toonn :Unknown
< 1722239937 369656 :X-Scale!~X-Scale@31.22.160.158 QUIT :Ping timeout: 256 seconds
< 1722241748 98198 :mtm_!~textual@c-71-228-84-213.hsd1.fl.comcast.net JOIN #esolangs * :Textual User
< 1722241773 966300 :mtm!~textual@c-71-228-84-213.hsd1.fl.comcast.net QUIT :Ping timeout: 245 seconds
< 1722242251 935212 :X-Scale!~X-Scale@31.22.160.232 JOIN #esolangs X-Scale :[https://web.libera.chat] X-Scale
< 1722243830 502076 :X-Scale66!~X-Scale@31.22.160.232 JOIN #esolangs X-Scale :[https://web.libera.chat] X-Scale
< 1722243915 352589 :X-Scale!~X-Scale@31.22.160.232 QUIT :Ping timeout: 256 seconds
< 1722244461 512140 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1722244493 361171 :X-Scale66!~X-Scale@31.22.160.232 QUIT :Ping timeout: 256 seconds
< 1722246552 165829 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
< 1722247330 510343 :salpynx!~salpynx@161.29.23.120 QUIT :Quit: Leaving
< 1722247962 343009 :Raoof!~Raoof@ip251.ip-167-114-76.net JOIN #esolangs * :[https://web.libera.chat] Raoof
< 1722248713 342966 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu JOIN #esolangs b_jonas :[https://web.libera.chat] wib_jonas
< 1722250001 342383 :Raoof!~Raoof@ip251.ip-167-114-76.net QUIT :Ping timeout: 256 seconds
< 1722250035 343841 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu QUIT :Ping timeout: 256 seconds
< 1722251114 936666 :X-Scale!~X-Scale@31.22.162.232 JOIN #esolangs X-Scale :[https://web.libera.chat] X-Scale
< 1722251590 22824 :Noisytoot!~noisytoot@user/meow/Noisytoot QUIT :Ping timeout: 260 seconds
< 1722252063 455169 :Noisytoot!~noisytoot@user/meow/Noisytoot JOIN #esolangs Noisytoot :Ron
< 1722252844 896571 :visilii!~visilii@46.61.242.52 JOIN #esolangs * :ZNC - https://znc.in
< 1722253126 895166 :visilii!~visilii@46.61.242.52 QUIT :Ping timeout: 272 seconds
< 1722253232 342592 :Raoof!~Raoof@ip251.ip-167-114-76.net JOIN #esolangs * :[https://web.libera.chat] Raoof
< 1722253288 896684 :visilii!~visilii@188.254.126.125 JOIN #esolangs * :ZNC - https://znc.in
< 1722253741 346392 :X-Scale!~X-Scale@31.22.162.232 QUIT :Ping timeout: 256 seconds
< 1722254117 34653 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :hello all, I came up with Ar2 (if you remember Ar from a few weeks ago) that only has one operation, one python function from Z* to Z that I conjecture you can use to define any other python function from Z^k to Z. anybody here interested to compute ackermann function with this function or show that it is not possible to compute ackermann function
< 1722254117 533089 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :using this function
< 1722254295 491722 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :you can find the source code of Ar2 [here](https://github.com/raoofha/Ar/blob/main/Ar2.py)
< 1722254668 865445 :mtm_!~textual@c-71-228-84-213.hsd1.fl.comcast.net QUIT :Ping timeout: 265 seconds
< 1722254766 640400 :mtm!~textual@c-71-228-84-213.hsd1.fl.comcast.net JOIN #esolangs mtm :Textual User
< 1722255973 965651 :X-Scale!~X-Scale@31.22.147.85 JOIN #esolangs X-Scale :[https://web.libera.chat] X-Scale
< 1722256693 343559 :Raoof2!~Raoof@ip251.ip-167-114-76.net JOIN #esolangs * :[https://web.libera.chat] Raoof
< 1722256699 343435 :Raoof!~Raoof@ip251.ip-167-114-76.net QUIT :Ping timeout: 256 seconds
< 1722256704 126458 :Raoof2!~Raoof@ip251.ip-167-114-76.net QUIT :Client Quit
< 1722256715 344237 :Raoof!~Raoof@ip251.ip-167-114-76.net JOIN #esolangs * :[https://web.libera.chat] Raoof
< 1722256952 928619 :visilii_!~visilii@188.254.110.38 JOIN #esolangs * :ZNC - https://znc.in
< 1722257154 865101 :visilii!~visilii@188.254.126.125 QUIT :Ping timeout: 272 seconds
< 1722257404 243508 :Raoof!~Raoof@ip251.ip-167-114-76.net QUIT :Quit: Client closed
< 1722257927 777391 :amby!~ambylastn@2a00:23c5:ce05:7801:d2c:186c:7e70:a223 JOIN #esolangs * :realname
< 1722258471 270506 :visilii!~visilii@46.61.242.163 JOIN #esolangs * :ZNC - https://znc.in
< 1722258486 201331 :X-Scale!~X-Scale@31.22.147.85 QUIT :Quit: Client closed
< 1722258691 880024 :visilii_!~visilii@188.254.110.38 QUIT :Ping timeout: 264 seconds
< 1722259116 31374 :visilii_!~visilii@46.61.242.91 JOIN #esolangs * :ZNC - https://znc.in
< 1722259218 467457 :visilii-!~visilii@46.61.242.229 JOIN #esolangs * :ZNC - https://znc.in
< 1722259273 173836 :visilii!~visilii@46.61.242.163 QUIT :Ping timeout: 252 seconds
< 1722259401 467672 :visilii!~visilii@188.254.110.171 JOIN #esolangs * :ZNC - https://znc.in
< 1722259429 961278 :visilii_!~visilii@46.61.242.91 QUIT :Ping timeout: 260 seconds
< 1722259560 468348 :visilii-!~visilii@46.61.242.229 QUIT :Ping timeout: 252 seconds
< 1722260047 468496 :visilii_!~visilii@188.254.126.209 JOIN #esolangs * :ZNC - https://znc.in
< 1722260146 902948 :visilii-!~visilii@46.61.242.98 JOIN #esolangs * :ZNC - https://znc.in
< 1722260264 445821 :visilii!~visilii@188.254.110.171 QUIT :Ping timeout: 252 seconds
< 1722260352 444506 :visilii_!~visilii@188.254.126.209 QUIT :Ping timeout: 252 seconds
< 1722260498 975501 :visilii!~visilii@213.24.125.189 JOIN #esolangs * :ZNC - https://znc.in
< 1722260499 54081 :visilii-!~visilii@46.61.242.98 QUIT :Read error: Connection reset by peer
< 1722260887 913475 :visilii_!~visilii@46.61.242.235 JOIN #esolangs * :ZNC - https://znc.in
< 1722261103 902318 :visilii!~visilii@213.24.125.189 QUIT :Ping timeout: 264 seconds
< 1722261578 269217 :visilii!~visilii@46.61.242.192 JOIN #esolangs * :ZNC - https://znc.in
< 1722261751 895558 :visilii_!~visilii@46.61.242.235 QUIT :Ping timeout: 264 seconds
< 1722261984 270174 :visilii_!~visilii@46.61.242.51 JOIN #esolangs * :ZNC - https://znc.in
< 1722262120 498585 :visilii-!~visilii@46.61.242.99 JOIN #esolangs * :ZNC - https://znc.in
< 1722262177 173479 :visilii!~visilii@46.61.242.192 QUIT :Ping timeout: 252 seconds
< 1722262331 173471 :visilii_!~visilii@46.61.242.51 QUIT :Ping timeout: 252 seconds
< 1722262970 4826 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1722263030 970993 :X-Scale!~X-Scale@31.22.162.149 JOIN #esolangs X-Scale :[https://web.libera.chat] X-Scale
> 1722263055 888715 PRIVMSG #esolangs :14[[07Xx14]]4 10 02https://esolangs.org/w/index.php?diff=134205&oldid=134202 5* 03Gggfr 5* (+70) 10/* syntax */
< 1722263465 347682 :X-Scale!~X-Scale@31.22.162.149 QUIT :Ping timeout: 256 seconds
< 1722264294 205781 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
< 1722264338 985338 :X-Scale!~X-Scale@83.223.250.22 JOIN #esolangs X-Scale :[https://web.libera.chat] X-Scale
< 1722264686 438285 :visilii-!~visilii@46.61.242.99 QUIT :Ping timeout: 252 seconds
< 1722264691 73577 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
< 1722264934 36467 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1722265223 345138 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu JOIN #esolangs b_jonas :[https://web.libera.chat] wib_jonas
< 1722265359 345293 :Raoof!~Raoof@ip251.ip-167-114-76.net JOIN #esolangs * :[https://web.libera.chat] Raoof
< 1722265573 356763 :X-Scale!~X-Scale@83.223.250.22 QUIT :Ping timeout: 256 seconds
< 1722265581 53833 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 have you looked at Ar2 ?
< 1722265732 116725 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :that general approach is usually capable of creating a TC language
< 1722265771 291550 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :although I can't immediately see a way to create a control structure capable of looping
< 1722265863 764190 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it's also a lot less tarpitty than I'd normally expect for something like that – generally such languages are defined to be just powerful enough to be TC, rather than having a range of operators like that
< 1722265911 465712 :visilii!~visilii@46.61.242.102 JOIN #esolangs * :ZNC - https://znc.in
< 1722265916 116855 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but, if you're looking for counterexamples, pick a function that requires TCness to calculate, such as a Spiral Rise interpreter
< 1722266230 467948 :visilii_!~visilii@213.24.125.21 JOIN #esolangs * :ZNC - https://znc.in
> 1722266258 228534 PRIVMSG #esolangs :14[[07User:TheCanon214]]4 M10 02https://esolangs.org/w/index.php?diff=134206&oldid=134184 5* 03TheCanon2 5* (+12) 10Subleq
< 1722266306 291378 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :(see https://logs.esolangs.org/libera-esolangs/2024-07-02.html#lDb for previous discussion)
< 1722266380 453488 :visilii!~visilii@46.61.242.102 QUIT :Ping timeout: 252 seconds
< 1722266450 460944 :ais523!~ais523@user/ais523 QUIT :Remote host closed the connection
< 1722266524 907073 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
< 1722266527 563842 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 since I'm looking for a total model of computation as far as I know it's not possible to interpret a partial language
< 1722266898 938291 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :Say you have a language with class inheritence, like python or C++. You have a library L that implements an interface/trait I, and a class P that implements I. There can be a third-party library M which uses L, and defines Q a subclass of P, and Q overrides the implementation of I's methods to something that differs from the original (but may call
< 1722266899 439102 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :its methods). Later you realize that you want an interface J that is similar to I but better, perhaps you can even implement I's methods from J's methods generically but this isn't required for my problem. If a class implements J then its implementation of I should behave consistently with its implementation of I. (Imagine Monad and Functor, or
< 1722266899 938425 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :less-than compare and three-way compare.) Now if you just modify L so P implements J then Q will suddenly be broken, because it will inherit an implementation of J that is inconsistent with the implementation of I. Is there a sane way to make sure this can't happen?
< 1722267656 440371 :visilii_!~visilii@213.24.125.21 QUIT :Ping timeout: 252 seconds
< 1722268065 919871 :FreeFull!~freefull@46.205.206.157.nat.ftth.dynamic.t-mobile.pl QUIT :Quit: rebooting
< 1722268182 153152 :FreeFull!~freefull@46.205.206.157.nat.ftth.dynamic.t-mobile.pl JOIN #esolangs FreeFull :FreeFull
> 1722268190 864421 PRIVMSG #esolangs :14[[07Ichi14]]4 M10 02https://esolangs.org/w/index.php?diff=134207&oldid=134194 5* 03TheCanon2 5* (+158) 10noted that divmeq is still better for tcness despite ichi being simpler
< 1722268536 809303 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :I guess this is why inheritance sucks
< 1722268742 24694 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :Raoof: ah – it is impossible in general to create a computable language that implements all total functions but is total itself
< 1722268751 564802 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because that would let you solve the halting problem
< 1722268828 47591 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
< 1722269068 904411 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 how do you prove that such a language let you solve the halting problem ? because I think that Ar2 or Ar3 (with hyperoperation as one of the basis) does not solve the halting problem it is just a total language on it's own
< 1722269159 479261 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :I also think that Ar1 aka Ar has a good chance of being a total model of computation
< 1722269347 876036 :ais523!~ais523@user/ais523 QUIT :Ping timeout: 264 seconds
< 1722269363 957921 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
> 1722269563 865578 PRIVMSG #esolangs :14[[07$+-?14]]4 M10 02https://esolangs.org/w/index.php?diff=134208&oldid=134004 5* 03TheCanon2 5* (-3) 10Register, not accumulator
< 1722269725 245760 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 notice that an anti-diagonal function is definable in Ar,Ar2 and Ar3
< 1722270390 623930 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it doesn't matter – you cannot write an interpreter, in a computable language, for a total language that is capable of implementing all total functions
< 1722270439 759253 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because, it is known that there are total functions for which it is impossible to prove that they're total (using a proof language for which a computable language is capable of verifying tge proof)
< 1722270479 812418 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :a language that's constructed to be total is, in effect, a method of proving that the programs written in it are total – and as such, there will always be total programs it can't implement
< 1722270514 71268 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :actually, hmm, I think I have that backwards
< 1722270560 373125 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I'm sorry it is possible to construct a total language which can run all total programs – you simply make an execution trace (that demonstrates halting) part of the program
< 1722270573 419498 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it would not be useful, because you would have to run the programs already to construct the trace
< 1722270605 863060 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :as for total *functions*, though, I think it's still impossible
< 1722270612 384213 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because the same workaround doesn't wrk
< 1722270613 873856 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :* work
< 1722270629 375345 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :please don't pressure me into doing this sort of complicated computational class proof when I'm not fully awake :-)
< 1722270742 442057 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :----
< 1722270766 853421 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :what is this unholy abomination https://raw.githubusercontent.com/raoofha/Ar/main/Ar2.py ? do you really have a string-eval with some string created in some complicated way with zero comments or documentation, and then expect me to tell how it behaves or even if it's total?
< 1722270793 427911 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :here's a simple example of the sort of thing that's very hard to implement in a computable total language: "given an even integer n>4, return a prime number p such that n-p is also a prime number"
< 1722270818 687095 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :this is total if and only if the Goldbach conjecture is true – thus, any proof that it was total would have to prove the Goldbach conjecture
< 1722270850 353825 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :this general technique can be generalised to a wide range of possible conjectures, eventually you reach one which is impossible to prove in the proof system you're using
< 1722270899 359083 :sprout!~quassel@2a02-a448-3a80-0-9023-d965-287a-ca2f.fixed6.kpn.net QUIT :Ping timeout: 260 seconds
< 1722270959 472814 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :Raoof: please write proper documentation of some sort to explain how you're supposed to use this, what kind of arguments it expects and what it does, because I'm not going to try to disentangle what the source code is trying to do.
< 1722270979 589980 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :OK, I found the diagonalisation: say you are using a proof system P to prove the language total, the total function you want to implement is "given a claimed demonstration that P is inconsistent, report the first fallacy in it"
< 1722270980 181581 :sprout!~quassel@2a02-a448-3a80-0-414d-4612-f265-dc79.fixed6.kpn.net JOIN #esolangs sprout :sprout
< 1722271012 402042 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :if P is consistent then this function is total – but proving it total would prove P consistent, and a consistent proof system cannot prove itself to be consistent (this is one of Gödel's theorems)
< 1722271136 381159 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :(and ideally write it without string-eval)
< 1722271239 369995 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :incidentally, this sort of argument doesn't rule out the possibility that there may be a computable language that happens to be total, can compute all total computable functions, but you can't prove that it's total
< 1722271263 880543 :int-e!~noone@int-e.eu PRIVMSG #esolangs :AFAICS that particular thing can't even do primitive recursion.
< 1722271377 20769 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 isn't the program itself the proof that it is total ?
< 1722271439 568646 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :Raoof: my point is that because you have proved the program total, it can't possibly implement all total functions – if it could, you wouldn't have been able to prove it
< 1722271564 511467 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :as far as I can see, this u function is trying to enumerate nested expressions in some fixed order, and then select one depending on its fixed argument, but then later in your example functions and tests you never try to use that functionality, so it's assumed untested and broken by default. I don't see why I should waste my time with this
< 1722271565 853998 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :wib_jonas I didn't think anybody wants to read that I add some documentation later
< 1722271579 158349 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :an example of a function you can't implement in it is "given an Agda program, return 0 if the program does not prove False, otherwise return the line number of the first error in the program"
< 1722271591 241370 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(this works because Agda is powerful enough to prove that your program is total)
< 1722271619 785767 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(and the function itself is total if Agda is consistent)
< 1722271621 422029 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :this is coded in a terrible style
< 1722271720 666592 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu PRIVMSG #esolangs :sorry, I shouldn't discourage you, please do experiment with trying to enumerate nested expressions or whatnot, but if you want other people to read it you'd better make it more understandable
> 1722272063 588107 PRIVMSG #esolangs :14[[07Talk:Divmeq14]]4 10 02https://esolangs.org/w/index.php?diff=134209&oldid=134183 5* 03TheCanon2 5* (+679) 10Added a section for algorithms
< 1722272068 14937 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 I see that as a challenge because I don't understand why you think a total and turing complete language is not possible so challenge accepted
< 1722272104 58453 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because this was already proved ages ago, it's a standard result in computability theory
< 1722272117 684747 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :there are lots of total functions that can be proved total, but (for any given proof language) some that can't be
< 1722272149 647827 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :assuming that the proof language is consistent, i.e. doesn't prove false statements – one that can prove false statements can prove all total functions total, but it is likely to prove some non-total functions total too
< 1722272192 957090 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(I should clarify – inconsistent languages prove false statements, but some consistent languages prove false statements too)
< 1722272212 62987 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :let's say "consistent and correct"
< 1722272255 471688 :wib_jonas!~wib_jonas@business-37-191-60-209.business.broadband.hu QUIT :Quit: Client closed
< 1722272257 616853 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but, the reason you can't do it is that even if diagonal arguments don't work directly against the language you are implementing, they will still work against the proof language you use to prove the language total
< 1722272312 589039 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 how do you prove the proof language to be total ?
< 1722272389 972557 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :you need to use a different proof language – if you keep going back through languages like that, eventually you reach a point where you can't
< 1722272423 352119 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :this is a well-known issue with the foundations of mathematics, it's known that there is eventually a point where you can't put mathematics on a sound mathematical basis any more
< 1722272459 947137 :visilii!~visilii@188.254.110.179 JOIN #esolangs * :ZNC - https://znc.in
< 1722272495 390243 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :btw, if you get to use uncomputable functions, it is much easier to show that no language can compute all total functions
< 1722272515 175549 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :e.g. the busy beaver function is uncomputable and obviously total, but because it's uncomputable you can't implement it in any programming langauge at all
< 1722272570 492754 :visilii_!~visilii@46.61.242.154 JOIN #esolangs * :ZNC - https://znc.in
< 1722272573 988104 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :the value of BB(5) was only calculated pretty recently – and it's quite possible that the value of BB(6) will never be known
< 1722272640 17461 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 why not think of Ar as a proof language ? you have to start somewhere
< 1722272658 807924 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :Raoof: because the thing you are trying to accomplish is known to be impossible
< 1722272679 409104 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :if you try to write, say, the busy beaver function in Ar or Ar2, you will probably not even figure out how to start
< 1722272693 240590 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it's just a totally different level of abstraction
< 1722272723 581542 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :ais523 can you write busy beaver in agda or peano arithmetic ?
< 1722272736 287270 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :no
< 1722272743 439687 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :you can't even write it in C or Python or lambda calculus
< 1722272799 916052 :visilii!~visilii@188.254.110.179 QUIT :Ping timeout: 252 seconds
< 1722272826 84033 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :I don't get your point then I'm claiming that there is a total language that can compute all total computable function and does not solve the halting problem
< 1722272846 641313 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :oh, you need a different example if you want to compute all total computable functions
< 1722272861 842069 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :such as the function that typechecks agda programs and enters an infinite loop if they prove false without containing type errors
< 1722272912 293085 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :that one *should* be total if agda is consistent, because the situation that enters an infinite loop would require an inconsistency
< 1722272915 536540 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and it's clearly computable
< 1722272920 103552 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but how do you prove it?
< 1722272981 19631 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :the point is that there are some total computable functions that can't be proven to be total – but if you can't prove them to be total, you can't implement them in your total language, because that *would* prove them to be total
< 1722273146 685967 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :how can a function that enters an infinite loop be total ?
< 1722273194 699905 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because the situation where it enters the infinte loop cannot occur
< 1722273317 805992 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :the problem basically reduces to dead code analysis: "given this program, prove that this particular line of the program never runs"
< 1722273325 308450 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and in general you can't do that, even if it does in fact never run
< 1722273465 844653 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :but that is a non-computable function
< 1722273522 361769 :visilii_!~visilii@46.61.242.154 QUIT :Ping timeout: 276 seconds
< 1722273523 253287 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :well, you can have computable functions that work similarly
< 1722273533 410013 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :you're confusing two levels, I think
< 1722273558 437424 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I have function A(x) that does "if x has a particular property, return 0, otherwise enter an infinite loop", and function B that checks whether or not A is total
< 1722273571 910632 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :function A can be trivially computable, if the property can be checked by brute force
< 1722273580 389893 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :function B is usually uncomputable
< 1722273613 699854 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :now, your language implementation is function B, but it's computable, which means there are some function As it can't handle
< 1722273662 884301 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because the property in question could be anything that's checkable by brute force
< 1722274062 260105 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :let me ask you a different question what is the set of functions that are computable using Ar3 meaning a single function that accept a composition number of hyperoperation,sub and div and a list of their argument and return the value of the composition u(f,...) := f(...)
< 1722274185 964271 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: Let's back up for a moment. Do you see how your Ar approach is similar to Kleene's definition of primitive recursion?
< 1722274194 283500 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :let me add that u() == 0 and u(x) == x+1 so you can define all integer using u alone
< 1722274271 792689 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :We can answer your question by adding higher-order functions to primitive recursion. This lets us talk about functions that take not just one number, but many numbers as an argument, like your Ar2.
< 1722274347 177580 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sadly, the literature on this sort of construction is not great. The magic search phrase is "primitive recursive functional".
< 1722274518 569915 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Anyway, yes, it's known that we can do "double recursion" with functionals; it's just a matter of taking two inputs instead of one. This lets us implement Ackermann's function.
< 1722274518 650019 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :Raoof: I have a specific function that is probably total, but I don't think you can implement in Ar2: http://nethack4.org/pastebin/62.txt
< 1722274520 65968 :int-e!~noone@int-e.eu PRIVMSG #esolangs :it shouldn't be too hard to show that all the u (of each arity) are primitive recursive, or u itself if you pick an encoding Z^* -> Z
< 1722274549 163729 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :(Also I'm going to say "PRF" for these functionals and consider them on N* → N instead of Z* → Z for simplicity.)
< 1722274558 894794 :int-e!~noone@int-e.eu PRIVMSG #esolangs :"probably"
< 1722274560 955493 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :part of the problem is that this hasn't been proven to be total yet, although it's widely believed to be – implementing it in a total language would require completing the proof
< 1722274621 633248 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1722274634 930885 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Heh. ais523's example is of a class of "anamorphisms" or "apomorphisms", which are operations that "unfold" or "build" indefinitely-large structures. Anamorphisms *cannot* be given by PRFs; you need a workaround, like bounding them with a maximum height/depth.
< 1722274662 152739 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: Okay, let's take a breath. How does all of this sound so far?
< 1722274732 661601 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: the funny thing is, we don't know for certain that that *isn't* primitive recursive – there might well be a primitive recursive bound on the result, we just don't know what it is
< 1722274824 466929 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :korvo all I know about primitive recursive functions is that they don't have a universal function and ack is not primitive recursive, and I guess higher order functions introduce non-termination
< 1722274844 388345 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: For sure! The curious fun of PRFs is that we can't even *express* an unbounded anamorphism, so we can't even express the search for a counterexample.
< 1722274887 800587 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :actually, this conversation has got me thinking a lot about function equivalence – we have a function written in form X, and don't know whether it can be expressed some other way in computational class Y – writing it in form X clearly doesn't help, but maybe there's an alternative way to write it that maps the same inputs to the same outputs
< 1722274918 235369 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: No worries. So, I'll tell you that all PRFs terminate, which makes them interesting for programming. Indeed they don't have universality or Turing-completeness; you can express a *single step* of a machine, but not an *infinite loop* of steps.
< 1722274960 28144 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I'll also give the punchline: the PRFs are precisely the arrows in a Cartesian-closed category with a natural-numbers object. This is an arcane definition, but it leads directly to a nice point-free language: https://esolangs.org/wiki/Cammy
< 1722274990 100049 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :e.g. "if (Agda is inconsistent) { enter infinite loop; } else { return 0; }", if it happens to be total, is trivial to implement (just implement "return 0;") – but proving the equivalence is hard
< 1722275019 524117 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: There's nothing wrong with your approach, but I think you should look at how Kleene did it. He used the same idea that you had: the first number can *choose* which operation to apply, like an index or code.
< 1722275057 882909 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Maybe you can take some inspiration or proofs from his work.
< 1722275115 889730 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: Yes. We can't prove the equivalence of PRFs in general, say PRFs with signatures like N → 2 (Cantor space) or N → N (Baire space), which were Kleene's Type I and Type II respectively. But for simpler signatures it can often be done.
< 1722275163 668731 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :e.g. there's only one function with signature X × Y → X up to unique isomorphism, and it's easy to encode the search as a unification.
< 1722275216 547183 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :oh, I see, examples like the Goldbach Conjecture can be expressed as a PRF equivalence problem
< 1722275217 983979 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :korvo thanks I sure do
< 1722275263 970064 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: Bingo. Jaw-dropping, right? It's like realizing that Gödel sentences are undetectable because they're all equivalent to fairly vacuous truthhoods.
< 1722275265 836651 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because "is number X a counterexample?" can be checked by a PRF
< 1722275302 748292 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :now I'm wondering how low computational class can become before equivalence becomes decidable
< 1722275320 973446 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :FSAs have decidable equivalence, for example
< 1722275357 643300 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I want to say it's an open question, but it can't be *that* open. CFGs have undecidable equivalence.
> 1722275383 920113 PRIVMSG #esolangs :14[[07Chicken14]]4 M10 02https://esolangs.org/w/index.php?diff=134210&oldid=132289 5* 03TheCanon2 5* (+11) 10/* See also */ H
< 1722275388 362730 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :(Because CFGs can encode Turing-machine traces as productions, kind of like Post correspondence machines.)
< 1722275479 326580 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :yep – CFG equivalence is one of my favourite Turing-complete (i.e. semi-decidable) problems
< 1722275508 303653 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but, I don't think that necessarily implies that DPDA equivalence is undecidable; does it immediately imply that NPDA equivalence is undecidable?
< 1722275605 91971 :iovoid!iovoid@hellomouse/dev/iovoid QUIT :Ping timeout: 248 seconds
< 1722275621 231377 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :actually my favourite related problem is CFG intersection, rather than CFG equivalence
< 1722275664 239872 :iovoid!iovoid@hellomouse/dev/iovoid JOIN #esolangs iovoid :guaranteed to not behave anticausally
< 1722275938 959385 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I'm not sure about PDAs. I only know the CFG stuff offhand from writing so many parsers.
< 1722275995 11114 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: Sorry, I just realized we didn't quite get to your second question. Do you want more intuition for totality vs computability? I know it's a hard topic.
< 1722276090 213211 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :korvo sure
< 1722276130 267116 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :korvo I meant to say of course I need more intution
< 1722276229 308715 :FreeFull!~freefull@46.205.206.157.nat.ftth.dynamic.t-mobile.pl QUIT :Quit: New kernel version
< 1722276255 186870 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: The usual thing we imagine, following Turing, is what ought to happen if we use a Turing-complete machine to emulate some other machine. Any state that we can reach inside the emulator is also a state that we can reach in our outer machine.
< 1722276303 356748 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :This is part of what makes Turing's proof work: we can build a funky program that doesn't do what we want when emulated by relating the funky program's inner states to the outer states. And then what happens if the funky program is an emulator?
< 1722276352 84400 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :The program doesn't reference itself. The outer program references the inner program. But the inner and outer programs are two copies of the same program.
< 1722276407 302184 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Or, paraphrasing Lawvere, the problem isn't that you have a fancy program x. The problem is that it's legal to write f(x) = x(x) which applies x to itself.
< 1722276875 640592 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :on an unrelated topic, I feel like I should report a combinator-related discovery I made recently
< 1722276902 32466 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :BCKW combinator calculus is Turing-complete: its combinators are (in Haskell notation) flip, (.), const, and \f \x -> f x x
< 1722276913 373069 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but I have been experimenting with replacing flip by (flip id)
< 1722276942 464667 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :korvo I didn't get your point about totality vs computability
< 1722276971 118200 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it turns out that this not only makes it possible to replace flip, but also makes it possible to replace const – you implement const recursively as \a b c -> const (a c) b
< 1722276985 670379 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and the remaining combinators have enough power to both construct that expression, and do the recursion
< 1722277020 665268 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :so, you end up with (flip id), (.), and \f \x -> f x x as your three combinators
< 1722277035 465780 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :this probably doesn't have any or many advantages over SK combinator calculus but I thought it was interesting
< 1722277048 451696 :FreeFull!~freefull@46.205.206.157.nat.ftth.dynamic.t-mobile.pl JOIN #esolangs FreeFull :FreeFull
< 1722277089 514160 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: That's...actually a really big deal IMO. Congratulations. What do we call (flip id)? Is it a bird?
< 1722277089 902513 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :err, I mean \f x -> f x x, sorry for the notational errors
< 1722277132 401565 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: I have been calling it V, initially for "inverse" or "reverse"
< 1722277134 765350 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: Well, you wanted to know why a total Turing-complete language is impossible. It's because there's a tension between totality and computability; a computer wants to be able to run forever but a total program must halt.
< 1722277144 912490 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it is \x y -> y x which is an intuitively simple combinator
< 1722277217 752172 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ACTION fetches their Smullyan
< 1722277251 924979 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :with (.) named A and (flip id) named V, then flip is ((A (V ((A A) V))) ((A A) V)) and id is ((A (V V)) ((A A) V))
> 1722277269 702429 PRIVMSG #esolangs :14[[07Talk:Divmeq14]]4 M10 02https://esolangs.org/w/index.php?diff=134211&oldid=134209 5* 03TheCanon2 5* (+427) 10Added OR
< 1722277300 153718 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: Smullyan calls it "Thrush", T for short, Txy = yx, in my copy of Mockingbird. I think that's the right one even with his conventions?
< 1722277330 761191 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: I was considering trying to find a copy of To Mock a Mockingbird just to see if it had been named alreayd
< 1722277338 247616 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I've never actually read the book, although of course I know of it
> 1722277382 29607 PRIVMSG #esolangs :14[[07MIRROR14]]4 10 02https://esolangs.org/w/index.php?diff=134212&oldid=133994 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+32) 10
< 1722277386 182271 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :if I read this correctly then this u function grows single exponentially, but not faster than that, but the code is written in a way that's hard to understand so it might be doing something completely different from what I expect, and also it's only exponential in the first argument of u and you never call u with anything but a very small first argument in the examples so it might not even work at all
< 1722277392 186953 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :(also the implementation is very slow).
< 1722277430 270398 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: I have a translation of Smullyan's To Mock a Mockingbird on my shelf, what did you want to know?
> 1722277474 113571 PRIVMSG #esolangs :14[[07MIRROR14]]4 10 02https://esolangs.org/w/index.php?diff=134213&oldid=134212 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+3) 10/* Compiler */
< 1722277481 149660 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: You might find it interesting reading. They build up bindings from scratch. One tough part for me was that the calling convention is backwards from what I'm used to, so a lot of equations are reversed.
< 1722277511 2820 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :He does that so that the SKI notation works correctly; it's not just for play.
< 1722277521 598151 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :b_jonas: so I have been looking into abstraction elimination using combinators, and there are nine (but actually seven) basic combinators that you would want to use (all of which can be made inefficiently using S, K, and I)
< 1722277540 718786 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :the two degenerate cases are \x.(A B) and \x.(A x), where x is not free in A or B
< 1722277556 905120 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: there's a list of most of the named birds at https://esolangs.org/wiki/Bird_sociology#Non-primitives
< 1722277567 918896 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :ah, this will probably do
< 1722277593 927000 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :although the notation is going to be a pain to read because I am used to lambda-calculus definitions of combinators
< 1722277612 10458 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :let me see who put that list there
< 1722277625 365983 :ais523!~ais523@user/ais523 PRIVMSG #esolangs ::t flip ((.) (.) (.))
< 1722277626 421087 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esolangs :(a1 -> a2 -> b) -> (b -> c) -> a1 -> a2 -> c
< 1722277647 593135 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :that one seems to come up often enough that I was wondering if it had a name, too
< 1722277664 166152 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :hppavilion1 added the list
< 1722277665 749042 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it seems to map the result of a 2-argument function
< 1722277730 284086 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :anyway, S seems to me to be a little flawed as a combinator, because unlike most other combinators it has more than one plausible evaluation order (and in fact it conceptually feels like it does two evaluations in parallel)
< 1722277863 456446 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it is also interesting how non-primitive flip seems – (flip id) feels like more of a sensible primitive; it has quite a bit of trouble implementing flip (although it can, with the help of (.)), but then so does SK combinator calculus
< 1722277882 111825 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: the table in the back of Mockingbird does define the named birds in a haskel-style way, as in "Bxyz = x(yz)" and "Exyzwv = zy(zwv)" and "Jxyzw = xy(xwz)", which is close to lambda calculus
< 1722277898 298871 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :but of course it's possible that some birds are mentioned in the main text but not in that table
> 1722277964 637619 PRIVMSG #esolangs :14[[07Talk:Divmeq14]]4 M10 02https://esolangs.org/w/index.php?diff=134214&oldid=134211 5* 03TheCanon2 5* (+885) 10added two inequalities
< 1722277980 269511 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :but also that table gives fewer names than the one on the wiki
< 1722277996 808049 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :anyway, the other big realisation I had was that you can implement a stack-like object with elements a0 (top), a1, a2, etc. as \f.f(a0)(a1)(a2) in untyped lambda calculus, and then almost all the operations of Underload can be implemented very easily on this kind of stack
< 1722278004 645240 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :which is strange because the wiki specifically says these are the named birds from the book
< 1722278015 998683 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :b_jonas as I wrote earlier u is defined as u(f,...) := f(...) and u() := 0 and u(x) := x+1 where f is the composition id of mul/hyerpoperation,sub and total div . I defined u such that you you can define a function using only u for example g(x) := u(u(),x) . now the question is what is the set of functions computable using only u ?
< 1722278095 480605 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but you need to write it in continuation-passing-style to make it work
< 1722278127 441190 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :e.g. if you have a "stack action" f, you apply it to a stack as call/cc \c.((f c) stack)
< 1722278240 561064 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :then, Underload's ~ is flip, ^ is (flip id), : is the W combinator, (x) is (flip id x), ! is const, I think – there are several layers of abstraction so it is hard to reason about
< 1722278245 608971 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :a and * don't implement as neatly, though
> 1722278262 929325 PRIVMSG #esolangs :14[[07Talk:Divmeq14]]4 M10 02https://esolangs.org/w/index.php?diff=134215&oldid=134214 5* 03TheCanon2 5* (+1) 10/* X == Y */ typo
< 1722278273 839413 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it is possible I have some of these wrong because I tried to calculate it entirely in my head, but I suspect it's correctable to produce a small functional implementation of Underload-without-S
> 1722278280 656261 PRIVMSG #esolangs :14[[07Talk:Divmeq14]]4 M10 02https://esolangs.org/w/index.php?diff=134216&oldid=134215 5* 03TheCanon2 5* (+1) 10/* X != Y */ capitalisation
< 1722278338 448650 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :Raoof: wait, I don't understand, you're asking about something called Ar3, but https://github.com/raoofha/Ar/tree/main only has an Ar2.py that defines a function u, so what is Ar3?
< 1722278393 777034 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :b_jonas Ar3 is just Ar2 where mul function replaced by hyperoperation function as one of the basis
< 1722278737 537567 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :Raoof: what does "hyperoperation" mean there?
< 1722278790 207097 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :b_jonas https://en.wikipedia.org/wiki/Hyperoperation
< 1722278803 226311 :int-e!~noone@int-e.eu PRIVMSG #esolangs :tetration I'd think
< 1722278810 908549 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :It's the standard tower: addition, multiplication, exponentiation, tetration, pentation, etc.
< 1722278997 779303 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :Raoof: ok, but that's not really enough of a definition, as that's a three-argument function, while your u calls two-argument functions in a way that has odd restrictions (basically one read-write register and any number of read-only registers)
< 1722279090 411688 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Oh, that's a really good point. Like, tetration would require one more RW register, either to hold an intermediate sum or a secondary counter.
< 1722279182 912316 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :I don't get your points, are you saying that u(f,...) := f(...) is not computable or I poorly described it ?
< 1722279219 659302 :int-e!~noone@int-e.eu PRIVMSG #esolangs :you haven't said how exactly your scheme extends to a three-argument function
< 1722279365 204970 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :Raoof: if I understand your implementation of u right then it is a computable total function on any number of integers, and it does at least grow exponentially so if you compose a bunch of it you might get some interesting behavior, or you might not, I can't tell. however, since u doesn't grow faster than exponential, int-e is right that you can't compute every primitive recursive function as a finite
< 1722279371 212523 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :composition of u.
< 1722279373 766177 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Anyway, whatever this is it's not more powerful than primitive recursion with the Ackermann function thrown in as a base function. So not TC, but potentially close enough for all practical purposes. That's totally unclear because you have to build meaningful expressions somehow to simulate control flow.
< 1722279413 723437 :int-e!~noone@int-e.eu PRIVMSG #esolangs :b_jonas: that was before we threw in a relatively fast growing base function
< 1722279422 671980 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :int-e: sure
< 1722279436 876271 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: The reasonable objections from b_jonas and int-e are why I recommend following Kleene. Your approach can work for representing PRFs, if you're careful about the details.
< 1722279454 198765 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :if you throw in a fast-growing base function then it gets complicated enough that I won't be able to analyze what you can get from a finite composition
< 1722279495 53050 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :But yeah, those who don't assume the Parameter Theorem (the Smn Theorem) are doomed to reimplement it. You might notice I skipped over all of this in Cammy, because I don't have the patience for it.
> 1722279595 397429 PRIVMSG #esolangs :14[[07Turtle just want to dig14]]4 10 02https://esolangs.org/w/index.php?diff=134217&oldid=133918 5* 03Gggfr 5* (-54) 10
< 1722279605 598382 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :int-e when you call the python function u you have access to the number of it's arguments so u define an infinite set of function u(), u(x), u(f,x), u(f,x,y), u(f,x,y,z) , ... for each number of arguments you define a list of variables x(0), x(1), x(2), ... and you copy the list into a list of expression and you define a three nested loop for each
< 1722279606 81000 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :argument of hyperoperation
< 1722279679 669244 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :b_jonas it is relatively simple when your mind is free but if you have to sleep or have a lot in your minds like it gets complicated
< 1722279681 812487 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sure. That's using Python's implementation of Parameters. It turns out that PRFs have the responsibility of doing it themselves.
< 1722279697 564004 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :b_jonas * like me
< 1722279713 871755 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Raoof: u/n is notation for an n-ary function from Prolog, so I did model the variadic part
> 1722279763 909826 PRIVMSG #esolangs :14[[07Turtle just want to dig14]]4 10 02https://esolangs.org/w/index.php?diff=134218&oldid=134217 5* 03Gggfr 5* (-62) 10
< 1722279870 602157 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
> 1722280319 894066 PRIVMSG #esolangs :14[[07$14]]4 10 02https://esolangs.org/w/index.php?diff=134219&oldid=118408 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+4) 10
> 1722280327 631810 PRIVMSG #esolangs :14[[07$14]]4 10 02https://esolangs.org/w/index.php?diff=134220&oldid=134219 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (-4) 10
> 1722280449 638462 PRIVMSG #esolangs :14[[07Turtle just want to dig14]]4 10 02https://esolangs.org/w/index.php?diff=134221&oldid=134218 5* 03Gggfr 5* (+173) 10/* how it works */
> 1722280617 247395 PRIVMSG #esolangs :14[[07Turtle just want to dig14]]4 10 02https://esolangs.org/w/index.php?diff=134222&oldid=134221 5* 03Gggfr 5* (-4) 10
> 1722280645 231207 PRIVMSG #esolangs :14[[07Turtle just want to dig14]]4 10 02https://esolangs.org/w/index.php?diff=134223&oldid=134222 5* 03Gggfr 5* (+22) 10
> 1722281040 419925 PRIVMSG #esolangs :14[[07Turtle just want to dig14]]4 10 02https://esolangs.org/w/index.php?diff=134224&oldid=134223 5* 03Gggfr 5* (+43) 10/* examples */
< 1722281705 930551 :X-Scale!~X-Scale@31.22.144.233 JOIN #esolangs X-Scale :[https://web.libera.chat] X-Scale
> 1722281874 195068 PRIVMSG #esolangs :14[[07Turtle just want to dig14]]4 10 02https://esolangs.org/w/index.php?diff=134225&oldid=134224 5* 03Gggfr 5* (+0) 10/* examples */
< 1722282724 342024 :Guest81!~Guest9@184.147.155.20 JOIN #esolangs * :[https://web.libera.chat] Guest9
< 1722282787 992493 :Guest81!~Guest9@184.147.155.20 QUIT :Client Quit
< 1722282931 849450 :dawids!~dawids@93.107.89.93 JOIN #esolangs * :realname
< 1722283291 842773 :dawids!~dawids@93.107.89.93 QUIT :Ping timeout: 265 seconds
< 1722283452 575648 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1722284449 533103 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
< 1722286959 374552 :Raoof!~Raoof@ip251.ip-167-114-76.net QUIT :Ping timeout: 256 seconds
> 1722286961 264740 PRIVMSG #esolangs :14[[07Talk:Divmeq14]]4 M10 02https://esolangs.org/w/index.php?diff=134226&oldid=134216 5* 03TheCanon2 5* (+0) 10typo
< 1722287129 345026 :X-Scale!~X-Scale@31.22.144.233 QUIT :Ping timeout: 256 seconds
< 1722287503 777781 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1722287852 406888 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Today's pick from the charts: someone must've shared a link to https://esolangs.org/wiki/Lambda:_the_Gathering on the fediverse, because (mostly within a 5-minute interval) 1683 different Mastodon instances fetched that same page.
< 1722287896 271446 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :fizzie: I think it's because it was posted to HN: https://news.ycombinator.com/item?id=41101068 Several aggregators would have scraped it from there.
< 1722287976 342620 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Ah, makes sense.
< 1722288378 604528 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Page popularity over time, in what I think are requests/second: https://zem.fi/tmp/lambda.png (mostly programs rather than people).
< 1722288402 805302 :salpynx!~salpynx@161.29.23.120 JOIN #esolangs salpynx :realname
< 1722288792 637347 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :fizzie: I was actually thinking of Lambda: the Gathering. IIUC this u function from Raoof's code is designed to have compose its built-in functions in a way where it has just one writable register, and you have to apply one of its four builtin functions to that one register in place either from the left or right or both, and if it's from the left or right then the other argument is one of the extra
< 1722288798 644004 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :arguments of the u function. LTG has a similarly annoying restriction on how you compose functions.
< 1722288824 130478 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :b_jonas: that reminds me of how BuzzFizz requires a constant on one side or the other of the \ operator, you can't use two variables
< 1722288829 833671 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(which is an intentional restriction to stop it being TC)
< 1722288893 430475 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: Raoof's function can use the *same* argument, as in the one writable register, on both sides of a built-in operation, and one of those builtins is multiply, which is the only reason why it grows exponentially.
< 1722289028 860179 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :fizzie: I did a little more digging. The top HN bot on Mastodon, @HackerNewsBot@m.einverne.info, did *not* reshare that link. It only publishes hot discussions and highly-upvoted links.
< 1722289199 526847 :lutherann!~lutherann@user/lutherann JOIN #esolangs lutherann :lutherann
< 1722289984 584481 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :"1683 different Mastodon instances fetched that same page." => ah, clients that automatically preview links, so great, especially when the previewer has vulnerabilities
< 1722290636 411235 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :"Within option names, dash (-) and underscore (_) may be used interchangeably in most cases, [..]. For example, `--skip-grant-tables` and `--skip_grant_tables` are equivalent. [..] except where underscores are significant. This is the case with, for example, `--log-bin` and `--log_bin`, which are different options."
< 1722290642 45434 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Thanks, MySQL, that's not confusing at all.
< 1722290908 215893 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :fizzie: oh no
< 1722290947 823830 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :isn't it fairly well established that mysql is a disaster? :-D
< 1722290950 36757 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :I have heard of programs where minus and underscore are interchangable in long option names, ffmpeg does that, but I haven't heard of one where there are exceptions
< 1722291164 522995 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Technically this is MariaDB (though that quote was from the MySQL manual), but I think they've had to inherit a lot of the disaster for compatibility reasons.
< 1722291214 580977 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :there are programs that take long options and let you abbreviate them by an arbitrary unambiguous prefix, which is a rather bad idea because it breaks existing scripts when they add more options to the program
< 1722291227 612790 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :gnu coreutils does that in particular
< 1722291325 924096 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :Rust sometimes has - and _ as interchangeable in package names, sometimes it doesn't, depending on context
< 1722291336 531373 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I think they should probably have banned - in all contexts to avoid the confusion
< 1722291381 473678 :lutherann!~lutherann@user/lutherann PRIVMSG #esolangs :underscore daughter or hypen son
< 1722291385 288013 :lutherann!~lutherann@user/lutherann PRIVMSG #esolangs :hyphen*
< 1722291646 411290 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: both perl and python can both give you very confusing errors if you store a module on a case-insensitive file system and import it using the wrong case
< 1722291685 705843 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :so that's also one of those things where the case difference sometimes matters and sometimes doesn't
< 1722291801 530567 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :Java, too
< 1722291855 548682 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :part of the problem is that case-insensitivity only really makes sense relative to a given language, which means that case-sensitivity normally makes more sense for programming languages that might have to deal with identifiers in a range of natural languages
< 1722291878 462946 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but case-insensitive file systems can mess that up in cases where the filename is important, especially if the program and filesystem are written in different natural languages
< 1722291951 547807 :__monty__!~toonn@user/toonn QUIT :Quit: leaving
< 1722291986 433747 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: wait, is that still a thing? I know that on DOS a filename can be valid or not depending on what codepage you loaded using MODE, and that affects casefolding too, but I'm hoping that on windows the file system itself determines what casefolding rules to use for filenames on it, it won't depend on random OS settings like the encoding
< 1722292024 105631 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :of course that can cause problems if you copy the source code elsewhere
< 1722292029 937108 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :b_jonas: I would expect that at least in Turkey, Windows would use Turkic casefolding for its case-insensitive file systems
< 1722292053 739450 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :IIRC the Java compiler cares or used to use the charset of your current locale when compiling to know what encoding the source code is written in
< 1722292108 25596 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: yeah, and the names of certain user groups as well as the names of some directories depend on what language you chose when you installed windows
< 1722292220 653513 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :not sure I understand the Ar claims about TCness from inc sub mul div. It looks like that is from the Z3 page which makes similar claims, and apparently I already doubted this 5 years ago based on my comment on the Z3 article discussion page
< 1722292278 228192 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it isn't that rare for people to make false claims of TCness on the wiki
< 1722292300 863709 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :although, it also isn't that rare for people to doubt correct TCness proofs
< 1722292311 779522 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :.. my 2019 comment doesn't really make anything clearer to me either. I think I'm just expressing doubt then also, rather than clarifying anything.
< 1722292353 678021 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :that reminds me of https://logs.esolangs.org/libera-esolangs/2023-07-18.html#lkb
< 1722292480 630591 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :b_jonas: I selected .... as the file extension for Incident fully in the knowledge that it would probably break something
< 1722292484 320175 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but I didn't expect it to be this recent
< 1722292499 110505 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :ACTION is tempted to make a language whose file extension is a period followed by a newline
< 1722292608 110612 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :files are traditionally supposed to end with newlines, right? :-)
< 1722292612 872974 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :.pl extension having three common meanings is the one that I find annoying. I even gave .pm as the extension of a few of my perl scripts just to avoid it.
< 1722292624 143649 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :b_jonas: Perl, Prolog, and?
< 1722292632 244723 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :some TeX-related thing
< 1722292652 451621 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I often use .pro for Prolog due to this clash (and writing more Perl than Prolog, although I write both), although that also runs into collisions
> 1722292690 778938 PRIVMSG #esolangs :14[[07Neoff14]]4 M10 02https://esolangs.org/w/index.php?diff=134227&oldid=134102 5* 03RainbowDash 5* (+83) 10
> 1722292691 225449 PRIVMSG #esolangs :14[[07Talk:Z314]]4 10 02https://esolangs.org/w/index.php?diff=134228&oldid=61228 5* 03Salpynx 5* (+293) 10/* instruction set with load, store, increment, zero and unconditional branching */
< 1722292880 948806 :X-Scale!~X-Scale@31.22.144.233 JOIN #esolangs X-Scale :[https://web.libera.chat] X-Scale
> 1722293101 2812 PRIVMSG #esolangs :14[[07Neoff14]]4 M10 02https://esolangs.org/w/index.php?diff=134229&oldid=134227 5* 03RainbowDash 5* (+15) 10
< 1722293110 700601 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :From the linked Raul Rojas paper on Z3: "The Z3 is therefore no universal computer in the sense of Turing". p.5
> 1722293457 945366 PRIVMSG #esolangs :14[[07Rnadom14]]4 N10 02https://esolangs.org/w/index.php?oldid=134230 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+971) 10Created page with "~~~~ made it ==commands== q: tape head := random(0,9) //also different from the current cell {: if tape head < 1 skip to matching "}" }: tape head decrement; if non-negative skip to matching "{" r: move tape
> 1722293478 467880 PRIVMSG #esolangs :14[[07Rnadom14]]4 10 02https://esolangs.org/w/index.php?diff=134231&oldid=134230 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (-183) 10
> 1722293494 243120 PRIVMSG #esolangs :14[[07Rnadom14]]4 10 02https://esolangs.org/w/index.php?diff=134232&oldid=134231 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (-3) 10/* Actual Random Number */
> 1722293528 49759 PRIVMSG #esolangs :14[[07Rnadom14]]4 10 02https://esolangs.org/w/index.php?diff=134233&oldid=134232 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+28) 10/* programs */
> 1722293541 548695 PRIVMSG #esolangs :14[[07Rnadom14]]4 10 02https://esolangs.org/w/index.php?diff=134234&oldid=134233 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+0) 10/* Random number generator */
< 1722293570 909668 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname
< 1722294219 790117 :ais523!~ais523@user/ais523 QUIT :Quit: quit
> 1722294823 655829 PRIVMSG #esolangs :14[[07Rnadom14]]4 10 02https://esolangs.org/w/index.php?diff=134235&oldid=134234 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+147) 10
> 1722294871 459003 PRIVMSG #esolangs :14[[07Rnadom14]]4 10 02https://esolangs.org/w/index.php?diff=134236&oldid=134235 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+38) 10/* polyglot */
> 1722294924 56438 PRIVMSG #esolangs :14[[07Z314]]4 10 02https://esolangs.org/w/index.php?diff=134237&oldid=96084 5* 03Salpynx 5* (+170) 10attempt to clarify the conditions under which Z3 can be made TC, and link to relevant papers
< 1722295202 616360 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :I've linked to the relevant papers and have a better idea of what Z3 is about now. Not 100% satisfied with my cite style, but I don't think this wiki has a standard?
< 1722295278 258270 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :Raoof: re. Ar, I think your statement "did you know that you don't need loop or recursion to program ?! you only need these four functions" is incorrect, and may have been based on incorrect or misleading info from that Z3 article
> 1722295571 721980 PRIVMSG #esolangs :14[[07Rnadom14]]4 10 02https://esolangs.org/w/index.php?diff=134238&oldid=134236 5* 03Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff 5* (+30) 10/* polyglot */
> 1722295642 834099 PRIVMSG #esolangs :14[[07Neoff14]]4 M10 02https://esolangs.org/w/index.php?diff=134239&oldid=134229 5* 03RainbowDash 5* (+106) 10Points added
< 1722295731 346769 :X-Scale!~X-Scale@31.22.144.233 QUIT :Ping timeout: 256 seconds
< 1722295897 343829 :Raoof!~Raoof@ip251.ip-167-114-76.net JOIN #esolangs * :[https://web.libera.chat] Raoof
< 1722296035 482820 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :hi Raoof, not sure if you saw the logs of my msg above about Ar?
< 1722296110 154299 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :salpynx hi, do you also doubt that Blindfolded arithmetic is not TC ? I'm looking for a way to workaround diagonalization and div,sub,mul,inc is a good candidate because as programs length goes to infinity Ar becomes TC and even super-TC
< 1722296112 772245 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca PRIVMSG #esolangs :Using the same file name extensions for multiple purposes is not so uncommon anyways though.
< 1722296308 41531 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :Without having read much on Blindfolded Arithmetic, I think that's safely TC, mainly because it says "you can use arbitrary control flow"
< 1722296320 295490 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :sorry what? Blindfolded arithmetic is definitely turing-complete if you have enough registers. enough is like two or three, but four or five is easy enough to prove.
< 1722296343 548429 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :salpynx: no, Blindfolded arithmetic specifically cannot use arbitrary control flow
< 1722296354 574695 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :its main restriction is the no control flow
< 1722296426 161455 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: You can't get around diagonalization. Consider: For a small number n, 2 ** n is much bigger than n; there's no way to count to 2 ** n using only n items.
< 1722296463 988665 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Diagonalization merely says that making n infinite isn't a solution; 2 ** n is still bigger than n even if n is an unlimited number of items.
< 1722296563 791117 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :oh, ok, I was reading the converting a state machine with arbitrary control flow part of the article... but that can be translated into control flow equivalents by placing code in an outer loop
< 1722296620 422452 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :which is what the Z3 TC conversion uses, and presumably what infinite length code simulates, which sounds like what Raoof wants to do with Ar?
< 1722296734 168623 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :I haven't thought much about infinite program length, but it seems pretty trivially equivalent to a potential loop. If you don;t want to just call it a loop, i'd be thinking of infinite non-repeating programs, which become hard to specify
< 1722297043 250882 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :maybe it's a terminology problem, but conditionally doing or not doing things in a single loop based on some state value is a way to "simulate" or do control flow, right?
< 1722297071 202826 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :korvo do you this that there is a simple algorithm that computes 2**n for a practically finite number using only Ar or Ar2
< 1722297078 679379 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :*think
< 1722297205 906681 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: Probably, but that's not what I'm saying. I'm saying that Cantor's theorem holds in the finite case, not just the infinite case.
< 1722297248 209350 :Raoof!~Raoof@ip251.ip-167-114-76.net PRIVMSG #esolangs :salpynx I have a hunch against conventional wisdom that there is a single universal function that you can use to compute all other total computable functions Ar, Ar2 and Ar3 and I have an idea for Ar4 are an attempt to make my hunch a reality
< 1722297280 751517 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: Like, diagonalization is usually done with an infinite table, right? Each row is a string of bits and we're assuming that there are infinitely many rows.
< 1722297334 17873 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :What is the main difference between Blindfold Arithmetic and Ar? I accept BA is TC (while not being sure of the exact details- the loop and access to registers, however simulated, is enouhg for me to believe it)
< 1722297357 605042 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :We can type-theoretically describe that table as a function from N to N → 2; it's a function from natural numbers to strings of bits. (We're saying a string of bits is a function from nats to bits.)
< 1722297399 875057 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :And then Cantor's theorem is that there isn't a surjection from N to N → 2. A surjection is a function which covers every possible output; here, it would be a function that has a natural number for every possible string of bits.
< 1722297453 815378 :salpynx!~salpynx@161.29.23.120 PRIVMSG #esolangs :also, I think a Total language cannot be TC, basically by definition. I think there's a terminology overlap with 'total' though, applying to functions vs. languages?
< 1722297517 41491 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Now, pretend that the table is finite and square. Like, suppose it's a table with four rows. Then we're talking about surjections from 4 to 4 → 2. But by type arithmetic, 4 → 2 has 2 ** 4 elements, which is more than 4. And if X has fewer elements than Y then there aren't any surjections X → Y.
< 1722297561 967561 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Raoof: So, let's start at the beginning again: *why* do you want to work around diagonalization?
< 1722297563 915382 :int-e!~noone@int-e.eu PRIVMSG #esolangs :salpynx: Well a priori it's conceivable that any partial recursive function has a corresponding total recursive function that encodes non-termination by an extra value.