00:01:04 -!- X-Scale28 has quit (Quit: Client closed).
00:02:32 -!- ais523 has joined.
00:02:54 -!- mtm has quit (Ping timeout: 260 seconds).
00:05:41 -!- mtm has joined.
00:08:18 -!- salpynx has quit (Remote host closed the connection).
00:08:36 -!- salpynx has joined.
00:09:35 -!- Lord_of_Life has quit (Ping timeout: 255 seconds).
00:12:07 -!- Lord_of_Life has joined.
00:28:06 -!- ais523 has quit (Remote host closed the connection).
00:28:49 -!- ais523 has joined.
00:44:23 -!- amby has 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).
00:52:40 -!- ignucio has joined.
00:57:43 <int-e> This looks cute, I think: https://viewer.shapez.io/?--Wb----:Cg--Cg--:--Sr--Cc:Rw--Rw--
01:25:57 <esolangs> [[User:TheCanon2]] M https://esolangs.org/w/index.php?diff=134184&oldid=134128 * TheCanon2 * (+25) Added Ichi
01:41:03 -!- ignucio has quit (Quit: Leaving).
01:41:20 -!- ignucio has joined.
01:44:52 <Sgeo> Would online multiplayer games be a usecase for reversible computing? If a client mispredicts, just reverse the computation a bit?
01:47:07 <int-e> In principle, perhaps; in practice I suspect they maintain more than one game state (one definitive and one with tentative changes).
01:49:51 -!- ais523 has quit (Remote host closed the connection).
01:51:05 -!- ais523 has joined.
01:51:15 <esolangs> [[Talk:INTERCAL]] https://esolangs.org/w/index.php?diff=134185&oldid=70794 * BoundedBeans * (+389)
02:10:50 -!- X-Scale has joined.
02:11:13 <esolangs> [[Talk:INTERCAL]] https://esolangs.org/w/index.php?diff=134186&oldid=134185 * BoundedBeans * (+293)
02:19:59 <esolangs> [[Ichi]] N https://esolangs.org/w/index.php?oldid=134187 * TheCanon2 * (+1088) Added ichi
02:22:01 -!- ais523 has quit (Quit: quit).
02:43:09 <esolangs> [[Fractran]] M https://esolangs.org/w/index.php?diff=134188&oldid=118705 * Salpynx * (+25) /* External resources */ pre-1993, (papers and articles from the 80s exist on Fractran)
02:43:16 -!- Cale has joined.
02:44:15 <esolangs> [[Esolang talk:Community portal]] https://esolangs.org/w/index.php?diff=134189&oldid=132982 * Ais523 * (+547) /* Clarification for "Unusable for programming" category */ some thoughts
02:55:43 <esolangs> [[SLet]] N https://esolangs.org/w/index.php?oldid=134190 * ZCX islptng * (+713) Created page with "This esolangs has 5 data types: 1.Set: e.g. {1,2,3} 2.Instruction: e.g. Print "Hello, world!" 3.List: e.g. [{1},{2},{3}] 4.Boolean: True or False 5.Nil: just like lua's A program is written in 1 line. Comments are written between parentheses. Commands are only l
03:14:06 <esolangs> [[Ichi]] https://esolangs.org/w/index.php?diff=134191&oldid=134187 * TheCanon2 * (+1156) Completed the article
03:16:37 <esolangs> [[Talk:INTERCAL]] https://esolangs.org/w/index.php?diff=134192&oldid=134186 * BoundedBeans * (+1)
03:21:19 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=134193&oldid=134066 * TheCanon2 * (+39) Added Ruckfish, Divmeq, and Ichi
03:35:11 <esolangs> [[Ichi]] M https://esolangs.org/w/index.php?diff=134194&oldid=134191 * TheCanon2 * (+69) Added truth machine and a category
03:51:48 <esolangs> [[Simpler Subskin]] https://esolangs.org/w/index.php?diff=134195&oldid=79061 * Ais523 * (+1) /* I/O */ O has to be positive, not just nonzero (but I can be negative)
03:54:58 <esolangs> [[Simpler Subskin]] https://esolangs.org/w/index.php?diff=134196&oldid=134195 * Ais523 * (-11) Undo revision [[Special:Diff/79061|79061]] by [[Special:Contributions/PythonshellDebugwindow|PythonshellDebugwindow]] ([[User talk:PythonshellDebugwindow|talk]]) complexity class and computational class are different concepts, and this section is primarily talking about t
04:42:01 <esolangs> [[User talk:Ais523]] https://esolangs.org/w/index.php?diff=134197&oldid=134074 * BoundedBeans * (+1468) Funge98 C-INTERCAL encoding bug while linking
05:05:27 <HackEso> U+1DFF4 - No such unicode character name in database \ UTF-8: f0 9d bf b4 UTF-16BE: d837dff4 Decimal: 𝿴 \ () \ Uppercase: U+1DFF4 \ Category: Cn (Other, Not Assigned)
05:07:49 <salpynx> the Unicode character I want was provisionally assigned a code point 5 days ago MODIFIER LETTER SMALL GREEK OMEGA
05:09:28 <esolangs> [[User talk:Ais523]] https://esolangs.org/w/index.php?diff=134198&oldid=134197 * Ais523 * (+1033) /* C-INTERCAL with Funge-98 bug */ some ideas
05:13:10 <salpynx> the proposal is for IPA usage, I want a superscript to denote an infinite string: a<sup>ω</sup> infintely many repetitions of a
05:24:00 -!- tromp has joined.
05:30:03 -!- Sgeo has quit (Read error: Connection reset by peer).
05:32:18 <esolangs> [[OISC]] M https://esolangs.org/w/index.php?diff=134199&oldid=134109 * TheCanon2 * (+148) Added Ichi, but the info may be wrong
05:33:38 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
05:35:35 <zzo38> Another alternative would be to use a different character set, although that will not be applicable if it is a document that does not use that character set, of course. Another another alternative would be to use HTML (or other rich formats) like you had described so t hat the character is not needed, I suppose.
05:39:58 <esolangs> [[OISC]] M https://esolangs.org/w/index.php?diff=134200&oldid=134199 * TheCanon2 * (-16) cleaned up
05:59:00 -!- tromp has joined.
06:49:46 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
07:16:12 <esolangs> [[Xx]] N https://esolangs.org/w/index.php?oldid=134201 * Gggfr * (+1155) Created page with "'''Xx''' is a minimalist esolang inspired by [[underload]] === memory === memory is stored in a tape starting with only one cell containing the letter <code>A</code>. the tape is circular so going to the end of the tape will bring you back to the start === syntax === Command
07:17:02 <esolangs> [[Xx]] https://esolangs.org/w/index.php?diff=134202&oldid=134201 * Gggfr * (+14)
07:20:05 -!- tromp has joined.
07:38:08 <esolangs> [[Genera Tag]] M https://esolangs.org/w/index.php?diff=134203&oldid=125981 * PkmnQ * (+2) /* Semantics */ Probably better wording
07:45:15 <esolangs> [[Python but it's trash]] https://esolangs.org/w/index.php?diff=134204&oldid=134157 * PkmnQ * (-141) No need for factorials
07:46:37 -!- __monty__ has joined.
07:58:57 -!- X-Scale has quit (Ping timeout: 256 seconds).
08:29:08 -!- mtm_ has joined.
08:29:33 -!- mtm has quit (Ping timeout: 245 seconds).
08:37:31 -!- X-Scale has joined.
09:03:50 -!- X-Scale66 has joined.
09:05:15 -!- X-Scale has quit (Ping timeout: 256 seconds).
09:14:21 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
09:14:53 -!- X-Scale66 has quit (Ping timeout: 256 seconds).
09:49:12 -!- tromp has joined.
10:02:10 -!- salpynx has quit (Quit: Leaving).
10:12:42 -!- Raoof has joined.
10:25:13 -!- wib_jonas has joined.
10:46:41 -!- Raoof has quit (Ping timeout: 256 seconds).
10:47:15 -!- wib_jonas has quit (Ping timeout: 256 seconds).
11:05:14 -!- X-Scale has joined.
11:13:10 -!- Noisytoot has quit (Ping timeout: 260 seconds).
11:21:03 -!- Noisytoot has joined.
11:34:04 -!- visilii has joined.
11:38:46 -!- visilii has quit (Ping timeout: 272 seconds).
11:40:32 -!- Raoof has joined.
11:41:28 -!- visilii has joined.
11:49:01 -!- X-Scale has quit (Ping timeout: 256 seconds).
11:55:17 <Raoof> 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
11:55:17 <Raoof> using this function
11:58:15 <Raoof> you can find the source code of Ar2 [here](https://github.com/raoofha/Ar/blob/main/Ar2.py)
12:04:28 -!- mtm_ has quit (Ping timeout: 265 seconds).
12:06:06 -!- mtm has joined.
12:26:13 -!- X-Scale has joined.
12:38:13 -!- Raoof2 has joined.
12:38:19 -!- Raoof has quit (Ping timeout: 256 seconds).
12:38:24 -!- Raoof2 has quit (Client Quit).
12:38:35 -!- Raoof has joined.
12:42:32 -!- visilii_ has joined.
12:45:54 -!- visilii has quit (Ping timeout: 272 seconds).
12:50:04 -!- Raoof has quit (Quit: Client closed).
12:58:47 -!- amby has joined.
13:07:51 -!- visilii has joined.
13:08:06 -!- X-Scale has quit (Quit: Client closed).
13:11:31 -!- visilii_ has quit (Ping timeout: 264 seconds).
13:18:36 -!- visilii_ has joined.
13:20:18 -!- visilii- has joined.
13:21:13 -!- visilii has quit (Ping timeout: 252 seconds).
13:23:21 -!- visilii has joined.
13:23:49 -!- visilii_ has quit (Ping timeout: 260 seconds).
13:26:00 -!- visilii- has quit (Ping timeout: 252 seconds).
13:34:07 -!- visilii_ has joined.
13:35:46 -!- visilii- has joined.
13:37:44 -!- visilii has quit (Ping timeout: 252 seconds).
13:39:12 -!- visilii_ has quit (Ping timeout: 252 seconds).
13:41:38 -!- visilii has joined.
13:41:39 -!- visilii- has quit (Read error: Connection reset by peer).
13:48:07 -!- visilii_ has joined.
13:51:43 -!- visilii has quit (Ping timeout: 264 seconds).
13:59:38 -!- visilii has joined.
14:02:31 -!- visilii_ has quit (Ping timeout: 264 seconds).
14:06:24 -!- visilii_ has joined.
14:08:40 -!- visilii- has joined.
14:09:37 -!- visilii has quit (Ping timeout: 252 seconds).
14:12:11 -!- visilii_ has quit (Ping timeout: 252 seconds).
14:22:50 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
14:23:50 -!- X-Scale has joined.
14:24:15 <esolangs> [[Xx]] https://esolangs.org/w/index.php?diff=134205&oldid=134202 * Gggfr * (+70) /* syntax */
14:31:05 -!- X-Scale has quit (Ping timeout: 256 seconds).
14:44:54 -!- tromp has joined.
14:45:38 -!- X-Scale has joined.
14:51:26 -!- visilii- has quit (Ping timeout: 252 seconds).
14:51:31 -!- ais523 has joined.
14:55:34 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
15:00:23 -!- wib_jonas has joined.
15:02:39 -!- Raoof has joined.
15:06:13 -!- X-Scale has quit (Ping timeout: 256 seconds).
15:06:21 <Raoof> ais523 have you looked at Ar2 ?
15:08:52 <ais523> that general approach is usually capable of creating a TC language
15:09:31 <ais523> although I can't immediately see a way to create a control structure capable of looping
15:11:03 <ais523> 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
15:11:51 -!- visilii has joined.
15:11:56 <ais523> but, if you're looking for counterexamples, pick a function that requires TCness to calculate, such as a Spiral Rise interpreter
15:17:10 -!- visilii_ has joined.
15:17:38 <esolangs> [[User:TheCanon2]] M https://esolangs.org/w/index.php?diff=134206&oldid=134184 * TheCanon2 * (+12) Subleq
15:18:26 <wib_jonas> (see https://logs.esolangs.org/libera-esolangs/2024-07-02.html#lDb for previous discussion)
15:19:40 -!- visilii has quit (Ping timeout: 252 seconds).
15:20:50 -!- ais523 has quit (Remote host closed the connection).
15:22:04 -!- ais523 has joined.
15:22:07 <Raoof> 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
15:28:18 <wib_jonas> 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
15:28:19 <wib_jonas> 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
15:28:19 <wib_jonas> 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?
15:40:56 -!- visilii_ has quit (Ping timeout: 252 seconds).
15:47:45 -!- FreeFull has quit (Quit: rebooting).
15:49:42 -!- FreeFull has joined.
15:49:50 <esolangs> [[Ichi]] M https://esolangs.org/w/index.php?diff=134207&oldid=134194 * TheCanon2 * (+158) noted that divmeq is still better for tcness despite ichi being simpler
15:55:36 <wib_jonas> I guess this is why inheritance sucks
15:59:02 <ais523> Raoof: ah – it is impossible in general to create a computable language that implements all total functions but is total itself
15:59:11 <ais523> because that would let you solve the halting problem
16:00:28 -!- tromp has joined.
16:04:28 <Raoof> 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
16:05:59 <Raoof> I also think that Ar1 aka Ar has a good chance of being a total model of computation
16:09:07 -!- ais523 has quit (Ping timeout: 264 seconds).
16:09:23 -!- ais523 has joined.
16:12:43 <esolangs> [[$+-?]] M https://esolangs.org/w/index.php?diff=134208&oldid=134004 * TheCanon2 * (-3) Register, not accumulator
16:15:25 <Raoof> ais523 notice that an anti-diagonal function is definable in Ar,Ar2 and Ar3
16:26:30 <ais523> 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
16:27:19 <ais523> 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)
16:27:59 <ais523> 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
16:28:34 <ais523> actually, hmm, I think I have that backwards
16:29:20 <ais523> 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
16:29:33 <ais523> it would not be useful, because you would have to run the programs already to construct the trace
16:30:05 <ais523> as for total *functions*, though, I think it's still impossible
16:30:12 <ais523> because the same workaround doesn't wrk
16:30:29 <ais523> please don't pressure me into doing this sort of complicated computational class proof when I'm not fully awake :-)
16:32:46 <wib_jonas> 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?
16:33:13 <ais523> 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"
16:33:38 <ais523> 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
16:34:10 <ais523> 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
16:34:59 -!- sprout has quit (Ping timeout: 260 seconds).
16:35:59 <wib_jonas> 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.
16:36:19 <ais523> 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"
16:36:20 -!- sprout has joined.
16:36:52 <ais523> 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)
16:38:56 <wib_jonas> (and ideally write it without string-eval)
16:40:39 <ais523> 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
16:41:03 <int-e> AFAICS that particular thing can't even do primitive recursion.
16:42:57 <Raoof> ais523 isn't the program itself the proof that it is total ?
16:43:59 <ais523> 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
16:46:04 <wib_jonas> 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
16:46:05 <Raoof> wib_jonas I didn't think anybody wants to read that I add some documentation later
16:46:19 <ais523> 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"
16:46:31 <ais523> (this works because Agda is powerful enough to prove that your program is total)
16:46:59 <ais523> (and the function itself is total if Agda is consistent)
16:48:40 <wib_jonas> 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
16:54:23 <esolangs> [[Talk:Divmeq]] https://esolangs.org/w/index.php?diff=134209&oldid=134183 * TheCanon2 * (+679) Added a section for algorithms
16:54:28 <Raoof> 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
16:55:04 <ais523> because this was already proved ages ago, it's a standard result in computability theory
16:55:17 <ais523> there are lots of total functions that can be proved total, but (for any given proof language) some that can't be
16:55:49 <ais523> 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
16:56:32 <ais523> (I should clarify – inconsistent languages prove false statements, but some consistent languages prove false statements too)
16:56:52 <ais523> let's say "consistent and correct"
16:57:35 -!- wib_jonas has quit (Quit: Client closed).
16:57:37 <ais523> 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
16:58:32 <Raoof> ais523 how do you prove the proof language to be total ?
16:59:49 <ais523> 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
17:00:23 <ais523> 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
17:00:59 -!- visilii has joined.
17:01:35 <ais523> btw, if you get to use uncomputable functions, it is much easier to show that no language can compute all total functions
17:01:55 <ais523> 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
17:02:50 -!- visilii_ has joined.
17:02:53 <ais523> 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
17:04:00 <Raoof> ais523 why not think of Ar as a proof language ? you have to start somewhere
17:04:18 <ais523> Raoof: because the thing you are trying to accomplish is known to be impossible
17:04:39 <ais523> if you try to write, say, the busy beaver function in Ar or Ar2, you will probably not even figure out how to start
17:04:53 <ais523> it's just a totally different level of abstraction
17:05:23 <Raoof> ais523 can you write busy beaver in agda or peano arithmetic ?
17:05:43 <ais523> you can't even write it in C or Python or lambda calculus
17:06:39 -!- visilii has quit (Ping timeout: 252 seconds).
17:07:06 <Raoof> 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
17:07:26 <ais523> oh, you need a different example if you want to compute all total computable functions
17:07:41 <ais523> such as the function that typechecks agda programs and enters an infinite loop if they prove false without containing type errors
17:08:32 <ais523> that one *should* be total if agda is consistent, because the situation that enters an infinite loop would require an inconsistency
17:08:35 <ais523> and it's clearly computable
17:08:40 <ais523> but how do you prove it?
17:09:41 <ais523> 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
17:12:26 <Raoof> how can a function that enters an infinite loop be total ?
17:13:14 <ais523> because the situation where it enters the infinte loop cannot occur
17:15:17 <ais523> the problem basically reduces to dead code analysis: "given this program, prove that this particular line of the program never runs"
17:15:25 <ais523> and in general you can't do that, even if it does in fact never run
17:17:45 <Raoof> but that is a non-computable function
17:18:42 -!- visilii_ has quit (Ping timeout: 276 seconds).
17:18:43 <ais523> well, you can have computable functions that work similarly
17:18:53 <ais523> you're confusing two levels, I think
17:19:18 <ais523> 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
17:19:31 <ais523> function A can be trivially computable, if the property can be checked by brute force
17:19:40 <ais523> function B is usually uncomputable
17:20:13 <ais523> now, your language implementation is function B, but it's computable, which means there are some function As it can't handle
17:21:02 <ais523> because the property in question could be anything that's checkable by brute force
17:27:42 <Raoof> 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(...)
17:29:45 <korvo> Raoof: Let's back up for a moment. Do you see how your Ar approach is similar to Kleene's definition of primitive recursion?
17:29:54 <Raoof> let me add that u() == 0 and u(x) == x+1 so you can define all integer using u alone
17:31:11 <korvo> 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.
17:32:27 <korvo> Sadly, the literature on this sort of construction is not great. The magic search phrase is "primitive recursive functional".
17:35:18 <korvo> 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.
17:35:18 <ais523> 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
17:35:20 <int-e> 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
17:35:49 <korvo> (Also I'm going to say "PRF" for these functionals and consider them on N* → N instead of Z* → Z for simplicity.)
17:36:00 <ais523> 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
17:37:01 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
17:37:14 <korvo> 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.
17:37:42 <korvo> Raoof: Okay, let's take a breath. How does all of this sound so far?
17:38:52 <ais523> 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
17:40:24 <Raoof> 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
17:40:44 <korvo> 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.
17:41:27 <ais523> 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
17:41:58 <korvo> 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.
17:42:40 <korvo> 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
17:43:10 <ais523> 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
17:43:39 <korvo> 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.
17:44:17 <korvo> Maybe you can take some inspiration or proofs from his work.
17:45:15 <korvo> 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.
17:46:03 <korvo> 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.
17:46:56 <ais523> oh, I see, examples like the Goldbach Conjecture can be expressed as a PRF equivalence problem
17:46:57 <Raoof> korvo thanks I sure do
17:47:43 <korvo> ais523: Bingo. Jaw-dropping, right? It's like realizing that Gödel sentences are undetectable because they're all equivalent to fairly vacuous truthhoods.
17:47:45 <ais523> because "is number X a counterexample?" can be checked by a PRF
17:48:22 <ais523> now I'm wondering how low computational class can become before equivalence becomes decidable
17:48:40 <ais523> FSAs have decidable equivalence, for example
17:49:17 <korvo> I want to say it's an open question, but it can't be *that* open. CFGs have undecidable equivalence.
17:49:43 <esolangs> [[Chicken]] M https://esolangs.org/w/index.php?diff=134210&oldid=132289 * TheCanon2 * (+11) /* See also */ H
17:49:48 <korvo> (Because CFGs can encode Turing-machine traces as productions, kind of like Post correspondence machines.)
17:51:19 <ais523> yep – CFG equivalence is one of my favourite Turing-complete (i.e. semi-decidable) problems
17:51:48 <ais523> but, I don't think that necessarily implies that DPDA equivalence is undecidable; does it immediately imply that NPDA equivalence is undecidable?
17:53:25 -!- iovoid has quit (Ping timeout: 248 seconds).
17:53:41 <ais523> actually my favourite related problem is CFG intersection, rather than CFG equivalence
17:54:24 -!- iovoid has joined.
17:58:58 <korvo> I'm not sure about PDAs. I only know the CFG stuff offhand from writing so many parsers.
17:59:55 <korvo> 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.
18:02:10 <Raoof> korvo I meant to say of course I need more intution
18:03:49 -!- FreeFull has quit (Quit: New kernel version).
18:04:15 <korvo> 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.
18:05:03 <korvo> 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?
18:05:52 <korvo> 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.
18:06:47 <korvo> 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.
18:14:35 <ais523> on an unrelated topic, I feel like I should report a combinator-related discovery I made recently
18:15:02 <ais523> BCKW combinator calculus is Turing-complete: its combinators are (in Haskell notation) flip, (.), const, and \f \x -> f x x
18:15:13 <ais523> but I have been experimenting with replacing flip by (flip id)
18:15:42 <Raoof> korvo I didn't get your point about totality vs computability
18:16:11 <ais523> 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
18:16:25 <ais523> and the remaining combinators have enough power to both construct that expression, and do the recursion
18:17:00 <ais523> so, you end up with (flip id), (.), and \f \x -> f x x as your three combinators
18:17:15 <ais523> this probably doesn't have any or many advantages over SK combinator calculus but I thought it was interesting
18:17:28 -!- FreeFull has joined.
18:18:09 <korvo> ais523: That's...actually a really big deal IMO. Congratulations. What do we call (flip id)? Is it a bird?
18:18:09 <ais523> err, I mean \f x -> f x x, sorry for the notational errors
18:18:52 <ais523> korvo: I have been calling it V, initially for "inverse" or "reverse"
18:18:54 <korvo> 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.
18:19:04 <ais523> it is \x y -> y x which is an intuitively simple combinator
18:20:17 * korvo fetches their Smullyan
18:20:51 <ais523> 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))
18:21:09 <esolangs> [[Talk:Divmeq]] M https://esolangs.org/w/index.php?diff=134211&oldid=134209 * TheCanon2 * (+427) Added OR
18:21:40 <korvo> 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?
18:22:10 <ais523> korvo: I was considering trying to find a copy of To Mock a Mockingbird just to see if it had been named alreayd
18:22:18 <ais523> I've never actually read the book, although of course I know of it
18:23:02 <esolangs> [[MIRROR]] https://esolangs.org/w/index.php?diff=134212&oldid=133994 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+32)
18:23:06 <b_jonas> 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
18:23:12 <b_jonas> (also the implementation is very slow).
18:23:50 <b_jonas> ais523: I have a translation of Smullyan's To Mock a Mockingbird on my shelf, what did you want to know?
18:24:34 <esolangs> [[MIRROR]] https://esolangs.org/w/index.php?diff=134213&oldid=134212 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+3) /* Compiler */
18:24:41 <korvo> 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.
18:25:11 <korvo> He does that so that the SKI notation works correctly; it's not just for play.
18:25:21 <ais523> 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)
18:25:40 <ais523> the two degenerate cases are \x.(A B) and \x.(A x), where x is not free in A or B
18:25:56 <b_jonas> ais523: there's a list of most of the named birds at https://esolangs.org/wiki/Bird_sociology#Non-primitives
18:26:07 <ais523> ah, this will probably do
18:26:33 <ais523> although the notation is going to be a pain to read because I am used to lambda-calculus definitions of combinators
18:26:52 <b_jonas> let me see who put that list there
18:27:06 <lambdabot> (a1 -> a2 -> b) -> (b -> c) -> a1 -> a2 -> c
18:27:27 <ais523> that one seems to come up often enough that I was wondering if it had a name, too
18:27:44 <b_jonas> hppavilion1 added the list
18:27:45 <ais523> it seems to map the result of a 2-argument function
18:28:50 <ais523> 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)
18:31:03 <ais523> 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
18:31:22 <b_jonas> 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
18:31:38 <b_jonas> but of course it's possible that some birds are mentioned in the main text but not in that table
18:32:44 <esolangs> [[Talk:Divmeq]] M https://esolangs.org/w/index.php?diff=134214&oldid=134211 * TheCanon2 * (+885) added two inequalities
18:33:00 <b_jonas> but also that table gives fewer names than the one on the wiki
18:33:16 <ais523> 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
18:33:24 <b_jonas> which is strange because the wiki specifically says these are the named birds from the book
18:33:35 <Raoof> 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 ?
18:34:55 <ais523> but you need to write it in continuation-passing-style to make it work
18:35:27 <ais523> e.g. if you have a "stack action" f, you apply it to a stack as call/cc \c.((f c) stack)
18:37:20 <ais523> 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
18:37:25 <ais523> a and * don't implement as neatly, though
18:37:42 <esolangs> [[Talk:Divmeq]] M https://esolangs.org/w/index.php?diff=134215&oldid=134214 * TheCanon2 * (+1) /* X == Y */ typo
18:37:53 <ais523> 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
18:38:00 <esolangs> [[Talk:Divmeq]] M https://esolangs.org/w/index.php?diff=134216&oldid=134215 * TheCanon2 * (+1) /* X != Y */ capitalisation
18:38:58 <b_jonas> 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?
18:39:53 <Raoof> b_jonas Ar3 is just Ar2 where mul function replaced by hyperoperation function as one of the basis
18:45:37 <b_jonas> Raoof: what does "hyperoperation" mean there?
18:46:30 <Raoof> b_jonas https://en.wikipedia.org/wiki/Hyperoperation
18:46:43 <int-e> tetration I'd think
18:46:50 <korvo> It's the standard tower: addition, multiplication, exponentiation, tetration, pentation, etc.
18:49:57 <b_jonas> 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)
18:51:30 <korvo> 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.
18:53:02 <Raoof> I don't get your points, are you saying that u(f,...) := f(...) is not computable or I poorly described it ?
18:53:39 <int-e> you haven't said how exactly your scheme extends to a three-argument function
18:56:05 <b_jonas> 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
18:56:13 <int-e> 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.
18:56:53 <int-e> b_jonas: that was before we threw in a relatively fast growing base function
18:57:16 <korvo> 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.
18:57:34 <b_jonas> 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
18:58:15 <korvo> 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.
18:59:55 <esolangs> [[Turtle just want to dig]] https://esolangs.org/w/index.php?diff=134217&oldid=133918 * Gggfr * (-54)
19:00:05 <Raoof> 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
19:00:06 <Raoof> argument of hyperoperation
19:01:19 <Raoof> 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
19:01:21 <korvo> Sure. That's using Python's implementation of Parameters. It turns out that PRFs have the responsibility of doing it themselves.
19:01:53 <int-e> Raoof: u/n is notation for an n-ary function from Prolog, so I did model the variadic part
19:02:43 <esolangs> [[Turtle just want to dig]] https://esolangs.org/w/index.php?diff=134218&oldid=134217 * Gggfr * (-62)
19:04:30 -!- tromp has joined.
19:11:59 <esolangs> [[$]] https://esolangs.org/w/index.php?diff=134219&oldid=118408 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+4)
19:12:07 <esolangs> [[$]] https://esolangs.org/w/index.php?diff=134220&oldid=134219 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (-4)
19:14:09 <esolangs> [[Turtle just want to dig]] https://esolangs.org/w/index.php?diff=134221&oldid=134218 * Gggfr * (+173) /* how it works */
19:16:57 <esolangs> [[Turtle just want to dig]] https://esolangs.org/w/index.php?diff=134222&oldid=134221 * Gggfr * (-4)
19:17:25 <esolangs> [[Turtle just want to dig]] https://esolangs.org/w/index.php?diff=134223&oldid=134222 * Gggfr * (+22)
19:24:00 <esolangs> [[Turtle just want to dig]] https://esolangs.org/w/index.php?diff=134224&oldid=134223 * Gggfr * (+43) /* examples */
19:35:05 -!- X-Scale has joined.
19:37:54 <esolangs> [[Turtle just want to dig]] https://esolangs.org/w/index.php?diff=134225&oldid=134224 * Gggfr * (+0) /* examples */
19:52:04 -!- Guest81 has joined.
19:53:07 -!- Guest81 has quit (Client Quit).
19:55:31 -!- dawids has joined.
20:01:31 -!- dawids has quit (Ping timeout: 265 seconds).
20:04:12 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
20:20:49 -!- tromp has joined.
21:02:39 -!- Raoof has quit (Ping timeout: 256 seconds).
21:02:41 <esolangs> [[Talk:Divmeq]] M https://esolangs.org/w/index.php?diff=134226&oldid=134216 * TheCanon2 * (+0) typo
21:05:29 -!- X-Scale has quit (Ping timeout: 256 seconds).
21:11:43 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
21:17:32 <fizzie> 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.
21:18:16 <korvo> 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.
21:26:18 <fizzie> Page popularity over time, in what I think are requests/second: https://zem.fi/tmp/lambda.png (mostly programs rather than people).
21:26:42 -!- salpynx has joined.
21:33:12 <b_jonas> 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
21:33:18 <b_jonas> arguments of the u function. LTG has a similarly annoying restriction on how you compose functions.
21:33:44 <ais523> 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
21:33:49 <ais523> (which is an intentional restriction to stop it being TC)
21:34:53 <b_jonas> 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.
21:37:08 <korvo> 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.
21:39:59 -!- lutherann has joined.
21:53:04 <b_jonas> "1683 different Mastodon instances fetched that same page." => ah, clients that automatically preview links, so great, especially when the previewer has vulnerabilities
22:03:56 <fizzie> "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."
22:04:02 <fizzie> Thanks, MySQL, that's not confusing at all.
22:09:07 <ais523> isn't it fairly well established that mysql is a disaster? :-D
22:09:10 <b_jonas> 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
22:12:44 <fizzie> 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.
22:13:34 <b_jonas> 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
22:13:47 <b_jonas> gnu coreutils does that in particular
22:15:25 <ais523> Rust sometimes has - and _ as interchangeable in package names, sometimes it doesn't, depending on context
22:15:36 <ais523> I think they should probably have banned - in all contexts to avoid the confusion
22:20:46 <b_jonas> 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
22:21:25 <b_jonas> so that's also one of those things where the case difference sometimes matters and sometimes doesn't
22:24:15 <ais523> 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
22:24:38 <ais523> 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
22:25:51 -!- __monty__ has quit (Quit: leaving).
22:26:26 <b_jonas> 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
22:27:04 <b_jonas> of course that can cause problems if you copy the source code elsewhere
22:27:09 <ais523> b_jonas: I would expect that at least in Turkey, Windows would use Turkic casefolding for its case-insensitive file systems
22:27:33 <b_jonas> 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
22:28:28 <b_jonas> 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
22:30:20 <salpynx> 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
22:31:18 <ais523> it isn't that rare for people to make false claims of TCness on the wiki
22:31:40 <ais523> although, it also isn't that rare for people to doubt correct TCness proofs
22:31:51 <salpynx> .. 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.
22:32:33 <b_jonas> that reminds me of https://logs.esolangs.org/libera-esolangs/2023-07-18.html#lkb
22:34:40 <ais523> b_jonas: I selected .... as the file extension for Incident fully in the knowledge that it would probably break something
22:34:44 <ais523> but I didn't expect it to be this recent
22:34:59 * ais523 is tempted to make a language whose file extension is a period followed by a newline
22:36:48 <ais523> files are traditionally supposed to end with newlines, right? :-)
22:36:52 <b_jonas> .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.
22:37:04 <ais523> b_jonas: Perl, Prolog, and?
22:37:32 <ais523> 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
22:38:10 <esolangs> [[Neoff]] M https://esolangs.org/w/index.php?diff=134227&oldid=134102 * RainbowDash * (+83)
22:38:11 <esolangs> [[Talk:Z3]] https://esolangs.org/w/index.php?diff=134228&oldid=61228 * Salpynx * (+293) /* instruction set with load, store, increment, zero and unconditional branching */
22:41:20 -!- X-Scale has joined.
22:45:01 <esolangs> [[Neoff]] M https://esolangs.org/w/index.php?diff=134229&oldid=134227 * RainbowDash * (+15)
22:45:10 <salpynx> From the linked Raul Rojas paper on Z3: "The Z3 is therefore no universal computer in the sense of Turing". p.5
22:50:57 <esolangs> [[Rnadom]] N https://esolangs.org/w/index.php?oldid=134230 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+971) Created 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
22:51:18 <esolangs> [[Rnadom]] https://esolangs.org/w/index.php?diff=134231&oldid=134230 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (-183)
22:51:34 <esolangs> [[Rnadom]] https://esolangs.org/w/index.php?diff=134232&oldid=134231 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (-3) /* Actual Random Number */
22:52:08 <esolangs> [[Rnadom]] https://esolangs.org/w/index.php?diff=134233&oldid=134232 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+28) /* programs */
22:52:21 <esolangs> [[Rnadom]] https://esolangs.org/w/index.php?diff=134234&oldid=134233 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+0) /* Random number generator */
22:52:50 -!- Sgeo has joined.
23:03:39 -!- ais523 has quit (Quit: quit).
23:13:43 <esolangs> [[Rnadom]] https://esolangs.org/w/index.php?diff=134235&oldid=134234 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+147)
23:14:31 <esolangs> [[Rnadom]] https://esolangs.org/w/index.php?diff=134236&oldid=134235 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+38) /* polyglot */
23:15:24 <esolangs> [[Z3]] https://esolangs.org/w/index.php?diff=134237&oldid=96084 * Salpynx * (+170) attempt to clarify the conditions under which Z3 can be made TC, and link to relevant papers
23:20:02 <salpynx> 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?
23:21:18 <salpynx> 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
23:26:11 <esolangs> [[Rnadom]] https://esolangs.org/w/index.php?diff=134238&oldid=134236 * Fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff * (+30) /* polyglot */
23:27:22 <esolangs> [[Neoff]] M https://esolangs.org/w/index.php?diff=134239&oldid=134229 * RainbowDash * (+106) Points added
23:28:51 -!- X-Scale has quit (Ping timeout: 256 seconds).
23:31:37 -!- Raoof has joined.
23:33:55 <salpynx> hi Raoof, not sure if you saw the logs of my msg above about Ar?
23:35:10 <Raoof> 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
23:35:12 <zzo38> Using the same file name extensions for multiple purposes is not so uncommon anyways though.
23:38:28 <salpynx> Without having read much on Blindfolded Arithmetic, I think that's safely TC, mainly because it says "you can use arbitrary control flow"
23:38:40 <b_jonas> 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.
23:39:03 <b_jonas> salpynx: no, Blindfolded arithmetic specifically cannot use arbitrary control flow
23:39:14 <b_jonas> its main restriction is the no control flow
23:40:26 <korvo> 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.
23:41:03 <korvo> 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.
23:42:43 <salpynx> 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
23:43:40 <salpynx> 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?
23:45:34 <salpynx> 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
23:50:43 <salpynx> 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?
23:51:11 <Raoof> korvo do you this that there is a simple algorithm that computes 2**n for a practically finite number using only Ar or Ar2
23:53:25 <korvo> 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.
23:54:08 <Raoof> 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
23:54:40 <korvo> 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.
23:55:34 <salpynx> 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)
23:55:57 <korvo> 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.)
23:56:39 <korvo> 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.
23:57:33 <salpynx> 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?
23:58:37 <korvo> 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.
23:59:21 <korvo> Raoof: So, let's start at the beginning again: *why* do you want to work around diagonalization?
23:59:23 <int-e> 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.