00:15:43 -!- Lord_of_Life has quit (Ping timeout: 244 seconds).
00:16:30 -!- Lord_of_Life has joined.
06:30:39 <nakilon> just realised that ttyrec is similar to gif in the way that it encodes timestamped regions
06:30:45 <nakilon> there should be ttyrec compressors
08:05:46 -!- hendursa1 has joined.
08:08:30 -!- hendursaga has quit (Ping timeout: 276 seconds).
08:37:17 <esolangs> [[Broken Calculator]] M https://esolangs.org/w/index.php?diff=89020&oldid=89008 * Iamn00b * (+3) minor change
08:57:29 -!- Sgeo has quit (Read error: Connection reset by peer).
10:29:24 -!- SGautam has joined.
11:49:12 -!- oerjan has joined.
11:51:21 -!- Noisytoot has quit (Quit: ZNC 1.8.2 - https://znc.in).
12:02:40 -!- Noisytoot has joined.
12:11:57 -!- sprout_ has joined.
12:15:20 -!- sprout has quit (Ping timeout: 260 seconds).
12:27:41 <esolangs> [[Special:Log/upload]] upload * Dominicentek * uploaded "[[File:ImagePath - Hello World.png]]"
13:15:50 -!- Thelie has joined.
13:36:47 <Taneb> I've been trying to construct the real numbers in Agda
13:54:36 <shachaf> Taneb: With what sort of construction?
13:55:31 <Taneb> Cauchy sequences with explicit moduli of conversion
13:56:43 <Taneb> I went with Cauchy sequences mostly because it's what I was in the mood for
13:59:23 <b_jonas> I believe Dedekind cuts are a trap, don't use them. They sound like they're easier because the definition of the set of reals itself is simpler. But once you actually try to define arithmetic and prove all its nice properties, Cauchy sequences behave nicer.
14:01:27 <Taneb> b_jonas: are you speaking from experience?
14:03:20 <riv> im no fan of dedekind cuts either
14:03:42 <riv> i read some interesting discussion about how dedekind cuts vs cauchy sequences are actually different in some way, in constructive logic
14:04:14 <Taneb> Yeah, you can turn a Cauchy sequence into a dedekind cut but not the other way around, I think
14:04:37 <Taneb> (constructively, at least. They're classically equivalent)
14:06:57 <Taneb> I couldn't immediately see how to prove that multiplication converges, so I'm taking a little break. I'm normally best at this sort of thing just after I wake up, I think
14:13:12 <sprout_> uh, my intution would be that reals just aren't pat of constructive mathematics, period?
14:13:37 <Franciman> |a_n * b_n - a*b| = |a_n * b_n - a * b_n + a * b_n - a * b|
14:13:42 <Taneb> sprout_: why do you think that?
14:13:43 <Franciman> then argue by triangular inequality
14:14:11 <Franciman> |a_n * b_n - a * b_n| + |a * b_n - a * b|
14:14:23 <Franciman> first member must be argued about twice
14:14:40 <Franciman> ah no ok, you use that convergent series are limited
14:14:54 <sprout_> Taneb: no idea. because? infinite approximations and all that. probably not well founded when you observe it mathematically
14:15:26 <Taneb> sprout_: in practice, you can define pretty much all of it, but you can't compute whether two arbitrary reals are equal
14:15:28 <Franciman> sprout_: constructively reals are indeed on demand fractional numbers
14:15:31 <sprout_> any approximation is wf, but the thing itself isn't
14:15:43 <Franciman> the more fractional numbers you can get
14:15:51 <Franciman> that's why cauchy sequences is a good model
14:15:58 <shachaf> In fact no nontrivial property of the reals is decidable.
14:16:12 <Franciman> you can get as far as you want in the sequence for getting a better approximation of reals
14:21:08 <Taneb> Franciman: ah, I've not yet proven that convergent series are limited
14:23:04 <Taneb> seq is convergent iff forall positive rational epsilon, there exists an N such that for all m, n > N, |seq[m]-seq[n]| < epsilon
14:25:29 <Taneb> Oh, I think I see how to do it
14:25:52 <Taneb> I can ask how far I need to go before it's all within epsilon = 1 (say), then take the max up to then and add 1
14:36:22 <esolangs> [[User:Hakerh400/How to solve Slitherlink using SAT solver]] https://esolangs.org/w/index.php?diff=89022&oldid=89015 * Hakerh400 * (+4)
14:45:44 -!- Thelie has quit (Remote host closed the connection).
15:12:30 -!- arseniiv has joined.
15:37:05 <Corbin> "Real Analysis in Reverse" https://arxiv.org/abs/1204.4483 is a fun paper which compares different ways of constructing reals.
16:11:10 <nakilon> got suspended on reddit for saying that they suspend for reasons not stated in their rules
16:13:00 <nakilon> (of course there is no rule against saying what I said)
16:19:15 -!- arseniiv has quit (Ping timeout: 265 seconds).
16:27:41 <esolangs> [[Special:Log/upload]] upload * Dominicentek * uploaded "[[File:ImagePath - Truth Machine.png]]"
16:28:13 <esolangs> [[Special:Log/upload]] upload * Dominicentek * uploaded "[[File:ImagePath - Cat Program.png]]"
16:29:45 <esolangs> [[ImagePath]] N https://esolangs.org/w/index.php?oldid=89025 * Dominicentek * (+2595) Created page with "ImagePath is an esoteric programming language created by Dominicentek for Truttle1's Visuals Esojam. It has a pointer that executes pixels in an image as instructions. Path is..."
16:30:55 <esolangs> [[User:Dominicentek]] https://esolangs.org/w/index.php?diff=89026&oldid=87955 * Dominicentek * (+26)
16:32:00 <esolangs> [[Language list]] https://esolangs.org/w/index.php?diff=89027&oldid=88948 * Dominicentek * (+16) /* I */
16:42:45 -!- arseniiv has joined.
17:19:01 -!- Sgeo has joined.
17:22:48 <esolangs> [[User:Hakerh400/Ideal programming language]] N https://esolangs.org/w/index.php?oldid=89028 * Hakerh400 * (+9570) Created page with "== Requirements == The more requirements from this list a language satisfies, the better language it is (more useful). Below is my opinion about some popular programming lang..."
17:23:53 <esolangs> [[User:Hakerh400]] https://esolangs.org/w/index.php?diff=89029&oldid=89016 * Hakerh400 * (+89)
17:27:47 <esolangs> [[Composite]] M https://esolangs.org/w/index.php?diff=89030&oldid=88486 * ArthroStar11 * (-43) fixed typo and updated interpreter link
17:28:48 <esolangs> [[User:ArthroStar11]] M https://esolangs.org/w/index.php?diff=89031&oldid=88966 * ArthroStar11 * (-41) updated link to Composite
17:36:32 <esolangs> [[User:Hakerh400/Ideal programming language]] https://esolangs.org/w/index.php?diff=89032&oldid=89028 * Hakerh400 * (+163) Add Java
17:37:33 <esolangs> [[User:Hakerh400/Ideal programming language]] https://esolangs.org/w/index.php?diff=89033&oldid=89032 * Hakerh400 * (+21)
17:55:40 <b_jonas> Taneb: not from experience, in that I never tried to formalize reals in Agda or other proof systems.
17:57:28 <b_jonas> (also not from experience in that I didn't invent real numbers, you did)
18:00:54 <b_jonas> "ah, I've not yet proven that convergent series are limitedah, I've not yet proven that convergent series are limited" => no, what you need is that Cauchy sequences are bounded. you don't need to even define convergent sequences until later, when you have real numbers.
18:01:10 <Corbin> One can get pretty far with functions N -> 2 or N -> N depending on what one wants. To get good convergence, use something like continued logarithms (for N -> 2) or continued fractions (for N -> N).
18:01:16 <b_jonas> "seq is convergent iff forall positive rational epsilon, there exists an N such that"for all m, n > N, |seq[m]-seq[n]| < epsilon" => yeah, that's a Cauchy sequence
18:01:41 <Corbin> Actually *writing* a formal library that proves facts and is correct is hard, but the conceptual part is straightforward enough.
18:01:57 <b_jonas> "continued logarithms" => what?
18:03:19 <Corbin> Like continued fractions, but with multiplication and division. They were described by Gosper in the same memo as their algorithms for continued fractions.
18:03:41 <Corbin> https://carma.newcastle.edu.au/resources/jon/clogs.pdf is an example fun paper about them.
18:04:39 <Corbin> Actually, this paper's great because it shows one way to build a correspondence between the N -> 2 and N -> N spaces by using the latter as run-length-encoding of the former.
18:08:17 <Taneb> b_jonas: I was keeping the same vocabulary as Franciman there
18:12:52 <Corbin> sprout_: It can be taken as an axiom (the "Turing axiom" IIRC?) that the reals are computable. IIUC the resulting real numbers are sufficiently smooth for typical work, but I'm not sure; looking for references.
18:14:49 <Corbin> Ah, https://en.wikipedia.org/wiki/Church%27s_thesis_(constructive_mathematics) is the axiom. We must give up LEM, but that's fine constructively.
18:20:12 -!- arseniiv has quit (Ping timeout: 244 seconds).
18:38:14 -!- zegalch has quit (Remote host closed the connection).
18:38:40 -!- zegalch has joined.
19:02:15 <myname> today i learned about the rado graph. surely, there is an esolang just hiding in there
19:19:55 <nakilon> https://www.youtube.com/watch?v=4y_nmpv-9lI
19:20:56 <nakilon> I'm not sure how the sqrt method works but I see another method that has no rejection and has only two random() calls, not three, like the rest of the methods he showed
19:28:17 <nakilon> a = rand(); b = rand(); if (a < b) then { r = b; angle = a / b } else { r = 1 - b; angle = (1 - a) / b }
19:34:43 <nakilon> oh, angle *= 2*pi after that
19:34:48 <riv> never seen this way
19:38:16 <nakilon> and / (1 - b), not / b , in the second branch
20:05:30 -!- zzo38 has quit (Ping timeout: 258 seconds).
20:06:33 -!- zzo38 has joined.
20:08:59 -!- SGautam has quit (Quit: Connection closed for inactivity).
20:25:44 -!- zzo38 has quit (Ping timeout: 244 seconds).
20:27:36 -!- Lykaina has joined.
20:29:29 -!- zzo38 has joined.
21:12:45 <imode> can you do an if/else if/else if/.../else structure in brainfuck?
21:13:11 <imode> I feel like I've had this answered before..
21:15:23 -!- earendel has joined.
21:16:09 <imode> I know you can do if/else pairs and by extension if/else chains.
21:16:31 <oerjan> imode: hm i did a case match when i wrote mbfi the other day, that's pretty close.
21:16:32 <imode> but I feel like you can't just arbitrarily insert new conditions without having continual nesting.
21:17:04 <HackEso> https://esolangs.org/wiki/mbfi
21:17:35 <oerjan> although i borrowed the method from cgbfi
21:18:03 <oerjan> basically you set a flag first, and the first condition to match clears it.
21:18:25 <imode> how is that phrased generally? it looks like nested if/else chains to me.
21:18:47 <imode> ah. yeah.. I was hoping something like...
21:19:24 <oerjan> you want to avoid increasing nesting level?
21:19:26 <imode> <condition> if <b1> else <condition> if <b2> else if ... else <false> end
21:19:33 <imode> just straight linear.
21:19:59 <oerjan> well you can do that with flags too, i should think
21:20:00 <imode> you can do it if you add an additional conditional "break" instruction but that's cheating.
21:20:16 <imode> I don't think you can, because there always has to be some check, and checking induces nesting.
21:20:37 <imode> i.e "if this didn't run, run that".
21:20:44 <imode> "and if _that_ didn't run, run that."
21:21:00 <oerjan> no, you still need just a flag
21:21:11 <imode> fwiw I'm working in a different language but the structural syntax is the same (looping).
21:21:27 <oerjan> "if the flag wasn't cleared, run that." "if it's _still_ not cleared, run that."
21:22:14 <imode> so in FV3 this looks like (condition) 1[<[0<] (true) 00<]<[ (false) 0<]
21:23:28 <oerjan> dbfi the super golfed one doesn't nest. although it uses a loop to get started.
21:23:29 <imode> we enqueue the flag as a 1 for later, we check the condition, if it's true, recall the flag, drop it (that's [0<]), do the body, then push a 0.
21:23:48 <imode> then the latter loop recalls the flag and then does the normal conditional check.
21:23:59 <imode> i.e if it's 1 then enter the loop otherwise it's don't.
21:24:18 <imode> I guess you could have a double-loop inside of every else-if case..
21:24:47 <oerjan> well you need _some_ nesting, just not an arbitrary amount.
21:27:12 <imode> (cond_1) 1[<[0<] (true_1) 00<]<[ (cond_2) 1[<[0<] (true_2) 00<]]<[ (cond_3) 1[<[0<] (true_3) 00<]]<[ ...
21:27:23 <oerjan> you may have some additional inefficiency if i understand that you need to go around the queue to recheck the flag
21:27:47 <imode> think of the queue as a tape. < and > move it left and right, you just insert to the left of the head when you do 0 and 1.
21:27:53 <imode> to recall it, just move the tape to the left.
21:28:12 <imode> so you need two levels of nesting.
21:28:22 <imode> that's better than arbitrary.
21:28:49 <imode> ehhhhhhh that won't work.
21:29:00 <imode> you still need if/else because what happens if the first branch is 0.
21:29:14 <imode> you'll consume the flag and end up with a 'tape underflow'.
21:31:04 <imode> what if you used two flags at the start and swapped between them. that could work.
21:31:34 <imode> ehh no it wouldn't.. you need some kind of `dup-bit` between everything.
21:32:19 <imode> which is easy. it's just 1[<[0<]1<1<00<]<[0<0<0<]
21:33:36 <imode> 1[<[0<]11<00<]<[00<0<] would be better as it leaves the bit under the tape head and the copy to the left of it.
21:34:36 <imode> so you'd compute the condition, the initial branch would either fire or not, and if it did, it'd leave a 0, which signals the rest of the branches to not fire.
21:35:19 <oerjan> well you should leave a 0 or a 1, always, until you're through the branches
21:35:54 <imode> and from there you could do else-if chaining by duping the bit, doing a [ (condition) [... 0<] 0<]
21:36:38 <imode> ehhh I need to think about that a little more.
21:37:21 <imode> first branch sends "yes I fired", rest of the branches should get and propagate a 0 until the terminal branch chomps it.
21:38:14 <imode> first branch sends "I failed to fire", next branch gets a "1", computes the condition, if the condition is true, rest of the branches get a "0", otherwise it passes a "1" flag onto the next branch.
21:42:29 <imode> https://hastebin.com/raw/zejamacaxa
21:42:31 <imode> somethin' like this.
21:43:12 <imode> need to add the point where you drop the bit, but.
21:46:20 <oerjan> this is in some sense the opposite of something i noticed when writing mbfi
21:47:20 <oerjan> that often in brainfuck it is more efficient to encode your status by your position relative to a flag than by changing the flag itself.
21:47:42 <imode> that makes sense, because you have a fixed background of cells.
21:48:15 <imode> you can litter the background with 1s and then move there.
21:48:25 <oerjan> (i noticed that cgbfi spent a lot of time calculating flags, while i could avoid that because i had better spacing of temporary cells)
21:49:20 <imode> yeah. this is a deque automata though, so the background is "variable". I don't have fixed positions unless I make them.
21:50:31 <imode> https://hastebin.com/raw/piyozagako
21:50:33 <imode> this should be it.
21:50:41 <oerjan> ok maybe "i noticed" is the wrong word, because the parser of dbfi also used that method heavily.
21:51:48 <oerjan> if you say so. i cannot really read it :P
21:52:01 <imode> sorry I'm in matrix-mode. "I don't even see the code".
21:52:32 <imode> "<1[<[0<]1<1<0<]<[0<0<0<]" <-- this bit recalls the flag and leaves two copies of it at top of the queue.
21:53:26 <imode> the [ ... 0<] around each of the conditions and branches checks that. if it's a 1, we drop the copy of the flag, compute whatever condition fired..
21:53:49 <imode> ...and if that condition was _true_, then we do the branch associated with that condition and then set the flag to 0, _otherwise_ we do nothing and we set the flag to 1.
21:54:03 <imode> then it moves to the next branch and we dup the flag... etc. etc. until else.
21:54:14 <imode> which is branch_false.
22:06:18 <imode> though I'll say that this is far more code to do the same thing...
22:11:51 <imode> tbf I'd probably just do the nesting. if it's a switch/case I imagine you could work out a far more general form from that.
22:12:39 <imode> like just do the equality check for every branch ahead of time and then just compute boom boom boom boom boom.
22:14:31 <imode> like the general form would be (value) (dup-value) (const_1) (equal) (right) (dup-value) (const_2) (equal) (right) ... (dup-value) (const_N) (equal) (right) <[ (branch_1) 0<] <[ (branch_2) 0<] ... <[ (branch_N) 0<]
22:14:45 <imode> so you'd generate something like 0000001000000 and each branch would grab a bit.
22:14:58 <imode> and which ever branch got the 1 gets to execute.
22:15:21 <imode> you can generate that because the switch/case form is always constant equality.
22:15:37 <imode> so you could even replace (equal) with a piece of code to recognize the value bit-for-bit.
22:16:54 <oerjan> this is in some sense closer to what dbfi did, although without nesting.
22:17:07 <imode> precomputing conditions?
22:18:14 <oerjan> it makes the length of a field of padding longer by the value tested
22:18:53 <oerjan> then goes to the end, and goes left one step with each branch
22:19:06 <imode> yeah, that sounds closer to the above.
22:21:35 -!- Melvar has quit (Ping timeout: 258 seconds).
22:24:12 -!- Lykaina has left (Leaving).
22:44:53 <esolangs> [[Special:Log/newusers]] create * Squidmanescape * New user account
22:52:23 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=89034&oldid=89017 * Squidmanescape * (+544) /* Introductions */
22:53:28 <esolangs> [[User:Squidmanescape]] N https://esolangs.org/w/index.php?oldid=89035 * Squidmanescape * (+108) Created page with "Hello! I am Squidmanescape, and I like Gray Snail! ==Accounts== *[https://github.com/Ramanuj-Sarkar Github]"
23:00:21 -!- Melvar has joined.
23:10:55 <esolangs> [[JSMeth]] https://esolangs.org/w/index.php?diff=89036&oldid=78899 * CoffeeHax17 * (-69)
23:13:03 -!- arseniiv has joined.
23:14:04 -!- oerjan has quit (Quit: Nite).
23:17:16 -!- arseniiv has quit (Ping timeout: 244 seconds).
23:34:45 <esolangs> [[ImagePath]] M https://esolangs.org/w/index.php?diff=89037&oldid=89025 * PythonshellDebugwindow * (+35) /* Examples */ make images clearer
23:52:39 <esolangs> [[Greg]] M https://esolangs.org/w/index.php?diff=89038&oldid=88919 * TheJonyMyster * (-8)
23:58:05 <esolangs> [[Gray Snail]] https://esolangs.org/w/index.php?diff=89039&oldid=75313 * Squidmanescape * (+2725) I wrote some stuff. I hope to write more.