00:13:54 -!- imode has quit (Ping timeout: 256 seconds).
00:23:33 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
00:23:44 <arseniiv> int-e: what have you poke them with?
00:26:30 <int-e> pointy letters and rount letters
00:30:54 -!- arseniiv has quit (Ping timeout: 256 seconds).
00:32:46 <fizzie> The web thing's been a little flaky occasionally. I was meant to debug it, but haven't managed to.
00:33:45 -!- FreeFull has quit.
00:34:44 <fizzie> Well, at least it's started to hang up kind of consistently.
00:35:44 <fizzie> I think chances are there's some bug in the websocket-based stalker mode that manages to hang up the regular request processing, even though it's not supposed to.
00:36:00 -!- MTGBusyBeaver42 has joined.
00:36:30 <fizzie> When I restart it, it works for a bit, until there's a new stalker mode connection, and then it stops working again.
00:39:07 <fizzie> Might have something to do with there being two active stalkers at the same time, that's probably not something I actually tested.
00:52:25 <MTGBusyBeaver42> ais523: looking at your WiP proof for 10 waterclocks, I'm not familiar with the language you are implementing, but it looks like the idea is to use that language to implement a cyclic tag system and prove TC that way,
00:53:44 <MTGBusyBeaver42> the eso wiki says not all variants of high rise are TC, what makes this implementation one of the TC ones?
00:54:33 <ais523> it's pretty easy to implement High Rise variants in The Waterfall Model, the hard part is to aim for a TC variant
00:54:45 <ais523> I erred on the side of implementing a more powerful variant to make almost certain that it's TC
00:55:04 <ais523> (you can implement a simpler variant that /might/ be TC with 8 waterclocks, I added two extra here to more or less totally make sure)
00:55:19 -!- Lord_of_Life has quit (Ping timeout: 255 seconds).
00:55:35 <ais523> to prove this particular Waterfall machine TC, you have to do two things, prove it implements that particular High Rise variant, and prove the variant TC
00:56:01 <ais523> it's only a WIP proof because I haven't done either half yet, I'm currently working on the second half (when I'm working on something that isn't my day job)
00:56:50 <MTGBusyBeaver42> yeah, it looks like implementing it in TWM isnt asking for anything TWM has a hard time doing
00:57:17 <ais523> it's the use of the E' waterclock that makes it almost certainly TC, its purpose is to outright skip every second 2 in the High Rise data string
00:57:45 <ais523> that gives us the one bit of state that you need to add to 1-tag to make it TC, so the only remaining hurdle is to prove that the rest of the language can implement 1-tag
00:58:44 <ais523> I may as well write my thoughts on that up here, too: the only thing that determines where new 2s are added in the data string is the distance between two (non-ignored) 2s scrolling off the data string
00:59:18 <ais523> the basic idea is to use two sorts of distances, small distances which also happen to be odd numbers, and large distances which also happen to be even numbers
00:59:40 <ais523> then small distances push the corresponding large distances onto the data string, large distances push a string of small distances onto the data string
01:00:17 <ais523> for the latter, you have a block of 1s in one half of the data string that matches up to the pattern you want (made of 1s) in the other half
01:00:52 <ais523> for the former, you have a sequence 101010101010101… in one half of the data string against a 1 in the other that adds up to a 2 only if you have a small (thus odd) distance
01:01:17 <ais523> and a few sporadic 1s in both halves which match up only when using a specific small distance
01:01:40 <ais523> err, I don't mean one half of the data string, I mean one half of the geometric sequence
01:01:52 <ais523> the ratio between successive elements is a very large power of 3
01:02:01 <ais523> and the two halves are around 3^n and 3^(n+1)
01:02:11 <ais523> actually this proof uses 9 rather than 3 but it's the same principle
01:02:33 <ais523> I probably haven't explained this very well, it'll probably be better to write it up as an actual proof, or else write a compiler
01:02:36 <ais523> to make it more formal
01:04:44 <ais523> it's funny, in the early history of esolangs, people made things like INTERCAL and Malbolge which were weird on purpose, for the sake of weirdness
01:05:04 -!- Lord_of_Life has joined.
01:05:07 <ais523> and nowadays, when we look into the simplest, most fundamental available tarpits, we get just as much weirdness but it's naturally occurring
01:05:54 <MTGBusyBeaver42> Yeah I actually was looking at 3-star programmer randomly like a year ago
01:06:47 <ais523> there's a High Rise language in base 2, with carries allowed, which uses a blank sequence for 0 and a geometric (not interleaved-geometric) sequence for 1 which I'm genuinely not sure whether it's TC or not, it seems so close to being TC but I can't quite make it work
01:08:26 <ais523> it gets easier once you realise that you can set things up so that some of the addresses are constants that always point to the same place, that effectively lets you get rid of stars when you don't want them
01:08:50 <ais523> it doesn't seem that ridiculous to me that a program based on ++*k, ++**k, ++***k can be TC for constant k
01:09:27 <ais523> only having increments available for writing and only having dereferences available for reading is painful, but by keeping regimented control over the whole of memory, it's not /that/ bad
01:11:35 <MTGBusyBeaver42> yeah, it is still bizarre to think about, more common operations like XOR are a lot easier to understand why.
01:12:18 <ais523> actually I think the hardest part with Three Star Programmer (and with the I/D machine) is that every statement has to increment /something/ so you need to find a lot of useless variables to throw your increments away in
01:13:12 <ais523> the TC proof for the I/D machine goes to the effort of setting up a queue that's never read from, just so that it can write to it the same way that it writes to the queue that it does use, thus vastly reducing the number of writes that need to be special-cased to sometimes write to somewhere useless
01:13:51 <ais523> this is a common trick in esoprogramming, I think, creating a dummy data structure that's just like your real, useful data structure so that you can throw away unwanted writes without using a conditional
01:14:02 <ais523> it was invented by Donald Knuth when he was programming in INTERCAL
01:16:31 <MTGBusyBeaver42> what approximate ratio do we need in TWM to get an X state TM?
01:16:49 <ais523> let's see: a TWM program is defined by zeroing triggers and initial values
01:16:54 <ais523> and number of waterclocks
01:16:57 <ais523> the number of waterclocks is fixed
01:17:14 <ais523> the initial values could be small because 2-tag is good at bootstrapping itself
01:17:42 <ais523> (by "small" I mean in the 1000-10000 range, although you could add an additional waterclock if you needed them smaller)
01:18:06 <ais523> the zeroing triggers are mostly small but a few of them will be enormous, encoding the High Rise program that encodes the 2-tag program that encodes the TM
01:18:19 <ais523> right, that doesn't surprise me
01:19:34 <ais523> the size of the zeroing triggers will be a small multiple of the ratio of the High Rise geometric series times the base of High Rise geometric series, as a number
01:19:45 <ais523> but the 2-tag translation sees it as a string of digits
01:19:51 <ais523> which we'll be converting into a number using base 9
01:20:51 <ais523> the length of the string, I suspect is roughly quadratic in the number of colors of the 2-tag system (the length of the productions obviously also matters but it's only linear in those, so the number of colors probably dominates)
01:21:21 <ais523> so we have a number of the form 9^(2^colors)
01:21:34 <ais523> this is larger than most reasonable one-arrow numbers, but smaller than almost all two-arrow numbers
01:21:58 <ais523> it's 9^(colors^2 * constant) which is much smaller
01:22:21 <ais523> it's large as one-arrow numbers go, but perhaps in reach, and thus easily dominated by two-arrow numbers
01:22:47 <ais523> the question is, how large of a 2-tag system do you need to implement a UTM
01:23:13 <ais523> and I don't know that part because the 2-tag-from-UTM translation isn't one that I've personally worked on
01:24:34 <ais523> there's a paper covering this but it isn't publicly available
01:24:53 <ais523> so I can't just look up the complexity
01:25:07 <ais523> ofc, the simpler the UTM, the larger the encoding of its input you typically need
01:26:43 <ais523> so the busy beaver function for a given UTM will grow more slowly the simpler the UTM is (although not much more slowly because busy beaver functions grow faster than anything computable, so they're all pretty fast)
01:26:44 <MTGBusyBeaver42> wait we dont need a UTM, we can encode the TM busy beaver as the 2-tag program
01:27:22 <ais523> right; and in fact you could encode a Waterfall Model busy beaver which would probably be busier (it would have to be at least as busy)
01:27:50 <MTGBusyBeaver42> Yeah once we iterate the conversion doesn't particularly matter
01:27:57 <ais523> it's an interesting problem because you need to show that the UTM exists in order to prove that the busy beaver function grows quickly, but the busiest beaver probably won't use one at all
01:28:40 <ais523> hmm, or maybe it will? that's an interesting question in its own right
01:29:05 <ais523> (and one that's very hard to answer because finding busy beavers is almost impossible even for very small machines)
01:29:51 <ais523> hey, #esoteric regulars: if you have a language that is sub-TC, does that imply that finding busy beavers for it is computable? or can a language be sub-TC and yet have an uncomputable halting problem?
01:30:02 <MTGBusyBeaver42> Yeah, though how to define the size of a TWM busy beaver something like (Clocks, Max size)
01:30:23 <ais523> "number of Plant tokens required to set it up"
01:33:01 <MTGBusyBeaver42> if Flooding Waterfall Machines have real busy beavers then we can have a lot more freedom in the setup and probably get an extra layer of iterations too
01:33:50 <ais523> well, 10 waterclocks + a number of flooding clocks is going to give you much busier beavers, because you can write a UTM using the 10 waterclocks, and use the flooding clocks as additional storage that naturally tends to explode
01:34:11 <ais523> if all your waterclocks are flooding, I'm still unsure what happens
01:34:53 <ais523> I think the best way to think about the flooding version of the language is that the zeroing triggers actually run every cycle, but their effects don't become visible until their clock zeroes
01:35:22 <ais523> but that way of thinking about it hasn't helped me much with actually programming in the language :-D
01:37:57 <MTGBusyBeaver42> yeah, either way of thinking about it, there's not really a good way to encode the values, due to combining multiplication and addition/subtraction
02:30:58 -!- ais523 has quit (Quit: quit).
02:36:09 -!- ais523 has joined.
02:37:07 <ais523> MTGBusyBeaver42: you should point out to the thread that Battletide Alchemist doesn't work if there's any way to have it on the field when setting up a double-Arcbond (even among your own creatures); you can use the optional damage prevention to make the loop run for a set, unlimited number of iterations
02:38:11 <ais523> like, the idea is that you make the opponent gain loop each iteration but don't use it yourself, set up a trivial infinite loop, run yourself out of life via choosing not to use Battletide Alchemist after a chosen number of iterations in order to deal a chosen amount of damage to the opponent
02:39:28 <ais523> although, I think it isn't being used anyway in the current versions
02:39:29 -!- ais523 has quit (Client Quit).
02:42:20 <zzo38> "There's a reason the comprehensive rules and errata for Magic: The Gathering is hundreds of pages long and reads like a federal tax code" I don't think so; the tax code is much more confusing.
03:15:20 <MTGBusyBeaver42> Well the score is actually how negative their life goes, not the total dealt.
03:19:12 <esowiki> [[Lightlang]] https://esolangs.org/w/index.php?diff=70265&oldid=68026 * Felixcesar15 * (-2131) New instruction set
03:20:50 <esowiki> [[Lightlang]] M https://esolangs.org/w/index.php?diff=70266&oldid=70265 * Felixcesar15 * (-49)
03:25:43 <zzo38> I don't know, but that is independent.
04:17:41 -!- oerjan has quit (Quit: Nite).
04:26:47 -!- MTGBusyBeaver42 has quit (Remote host closed the connection).
05:05:11 -!- imode has joined.
05:25:46 -!- Sgeo has quit (Ping timeout: 258 seconds).
06:04:56 -!- kritixilithos has joined.
06:21:53 -!- Sgeo has joined.
06:38:49 -!- myname has quit (Quit: Lost terminal).
06:56:52 -!- imode has quit (Ping timeout: 265 seconds).
07:12:10 -!- myname has joined.
08:20:03 -!- xelxebar_ has quit (Ping timeout: 240 seconds).
08:42:49 <b_jonas> ais523: "can a language be sub-TC and yet have an uncomputable halting problem?" => certainly. just take a language that is like a normal TC language but the programs are encrypted with a random function that is very uncomputable in both directions. basically just take a random language that has no rules to it.
08:44:10 <b_jonas> like, the encryption isn't uncomputable because of some fancy complexity theory reason, only because by cardinality reasons most functions are uncomputable.
08:51:51 -!- b_jonas has quit (Quit: leaving).
08:58:52 -!- xelxebar has joined.
09:45:05 <Cale> Can an actually-implementable language be sub-TC and have an uncomputable halting problem?
09:45:59 <Cale> It seems likely to me
09:46:38 <Cale> Just saying "this thing has an uncomputable halting problem" doesn't feel like it should get you Turing completeness for free.
09:47:19 <Taneb> A program p in Language P does no computation and halts if and only if p doesn't halt
09:49:25 <Cale> That sounds more like a description of a language with no correct implementation.
09:49:42 <Cale> But I can see what you're trying to do :)
09:53:09 <Cale> Maybe just take a single Turing machine whose halting already can't be decided... say it searches for a proof of a contradiction in our metatheory, and then define a language with but a single program whose implementation is that machine.
09:57:12 <kritixilithos> maybe for a particular program of this language, it runs the input as a TM, and after the completion of execution (if it does halt), the program returns 0
09:57:33 <Cale> Oh, that's a good one
09:58:29 <Cale> Just take any ordinary Turing complete language and make sure it can't produce any interesting output other than whether it terminated.
10:00:34 <Taneb> I think that might be too easy to argue it's not turing complete
10:00:40 <Taneb> It can semi-decide any semi-decidable language
10:01:01 <Cale> Well, it's supposed to not be Turing complete
10:01:17 <Cale> But have an uncomputable halting problem
10:02:00 <Cale> Of course, you might be able to also hope for a more practical language that could be used to solve a wider range of problems...
10:02:58 <Cale> Like, it should maybe contain a consistent type theory as a sublanguage.
10:02:58 <Taneb> I mean, argue it is turing complete
10:04:03 <Cale> Well, you can't solve most ordinary decision problems
10:04:15 <Cale> Like, the problem of whether the number on input is even
10:04:22 <Cale> You can only semi-decide it
10:27:43 -!- atslash has quit (Ping timeout: 255 seconds).
10:33:31 -!- wib_jonas has joined.
10:41:35 -!- cpressey has joined.
10:51:46 -!- LKoen has joined.
10:58:16 -!- arseniiv has joined.
10:58:43 -!- kritixilithos has quit (Ping timeout: 240 seconds).
11:10:21 -!- Felixcesar15 has joined.
11:12:02 -!- Felixcesar15 has quit (Remote host closed the connection).
11:27:46 -!- LKoen has quit (Remote host closed the connection).
11:28:04 <cpressey> Welcome to the international center for esoteric programming libation design, development, and deployment!
11:30:55 <cpressey> This theme and variations will continue until someone fixes the topic.
11:32:23 -!- LKoen has joined.
11:33:48 -!- sprocklem has quit (Ping timeout: 265 seconds).
11:35:09 -!- sprocklem has joined.
11:49:48 -!- kritixilithos has joined.
11:57:47 -!- sprocklem has quit (Ping timeout: 260 seconds).
11:59:19 -!- sprocklem has joined.
12:00:04 -!- LKoen has quit (Remote host closed the connection).
12:01:26 -!- LKoen has joined.
12:12:22 <esowiki> [[Function x(y)]] M https://esolangs.org/w/index.php?diff=70267&oldid=70263 * PythonshellDebugwindow * (+17) /* Syntax */
12:14:19 <HackEso> Go is a common irregular verbal game programming language invented by the Germanic Taneb tribes catching monsters in the strategic territories of East Asia.
12:18:11 <esowiki> [[Function x(y)]] M https://esolangs.org/w/index.php?diff=70268&oldid=70267 * PythonshellDebugwindow * (+271) /* Syntax */
12:19:11 <esowiki> [[Function x(y)]] M https://esolangs.org/w/index.php?diff=70269&oldid=70268 * PythonshellDebugwindow * (-22) /* Syntax */
12:27:11 <int-e> cpressey: so no incentive to change anything then
12:27:44 <HackEso> 3) <AnMaster> that's where I got it <AnMaster> rocket launch facility gift shop
12:29:44 -!- kspalaiologos has joined.
12:34:59 <arseniiv> is there a nonstandard model of natural numbers in a Heyting arithmetic (this is an intuitionistic counterpart to Peano arithmetic)
12:36:42 <int-e> arseniiv: Just take any classical non-standard model?
12:37:15 <arseniiv> though I should first find and understand what is a model of an intuitionistic first-order theory
12:38:17 <arseniiv> int-e: yeah I thought that could be the case but there’s a strange lack of mentions of nonstandard models for the case so I thought maybe there’s something interesting going on
12:38:31 <wib_jonas> arseniiv: I think there's somethink like models in intuitionistic logic but it's much more complicated than ordinary models
12:40:27 <int-e> https://en.wikipedia.org/wiki/Kripke_semantics ... but this only seems necessary if you want to capture the lack of excluded middle in the semantics, which seems unnecessary if you just want a non-standard model.
12:41:04 <int-e> (Insofar as the term makes any sense at all... I mean, what is /the/ standard model anyway if you don't have the law of excluded middle?)
12:48:35 <arseniiv> int-e: for a formula A without quantifiers, in Heyting arithmetic it’s provable A ∨ ¬A, so in particular equality of terms is decidable so the usual standard model should suffice if elevated to an intuitionistic model (in a way I don’t know yet)
12:53:18 <arseniiv> (also it makes sense that in a constructive world there should be the standard natural numbers thing: where at all if not here? Though this isn’t an argument at all as I heard in type theories there are still issues analogous to nonstandard elements, but they aren’t as visible or petrifying)
12:54:49 <int-e> so does that make the standard model of natural numbers a non-standard model :P
12:56:03 <int-e> . o O ( And just to add to the fun, it could still not be non-standard. )
12:59:58 -!- LKoen has quit (Remote host closed the connection).
13:03:37 -!- LKoen has joined.
13:09:06 -!- Lord_of_Life has quit (Ping timeout: 256 seconds).
13:15:33 -!- Lord_of_Life has joined.
13:22:57 <wib_jonas> int-e: *the* standard model is probaby still the classical logic one in which the exculded middle happens to hold, which intuitionistic logic still supports as a special case, or so this person with his traditional classical logic habits thinks
13:26:21 -!- LKoen has quit (Remote host closed the connection).
13:26:56 -!- art1 has joined.
13:29:33 -!- LKoen has joined.
13:31:10 <esowiki> [[2KWLang]] N https://esolangs.org/w/index.php?oldid=70270 * PythonshellDebugwindow * (+1102) Created page with "'''2KWLang''' (short for 2-Keyword Language) is an esolang by [[User:PythonshellDebugwindow]]. ==Syntax== There are only two keywords in this language, as the name implies, a..."
13:38:38 <esowiki> [[Truth-machine]] M https://esolangs.org/w/index.php?diff=70271&oldid=69138 * PythonshellDebugwindow * (+303) /* 2KWLang */
13:40:13 <esowiki> [[2KWLang]] M https://esolangs.org/w/index.php?diff=70272&oldid=70270 * PythonshellDebugwindow * (+540) /* Quine (maybe cheating) */
13:51:09 <cpressey> So we have lots of esolangs where we guess they are Turing-complete, and some where we even have informal proofs that they're TC. Do we have any where we have a formal, machine-checkable proof that it's TC?
13:52:35 <wib_jonas> cpressey: probably not machine-checkable, because nobody bothers to write those
13:53:01 <wib_jonas> but I can point to at least two books about theory of algorithms with formal proofs
14:00:37 <wib_jonas> cpressey: https://esolangs.org/wiki/Minsky_machine says "A proof of Turing-completeness is also given in the textbook ...", this is an important TC-ness theorem, because we often prove TC-ness by compiling Minsky machines (with a fixed number of counters) to an esolang
14:00:49 <wib_jonas> there are other similar classical computational models
14:02:59 <arseniiv> that reminds me I haven’t finished a Python module with utilities for working with generalized Minsky machines. Maybe I should start a C# module for that instead
14:06:31 <arseniiv> more like a reference implementation of the algorithm deciding whether an “algebraic type universe” is infinite and constructing a term and an unary function to realize Z and S
14:07:16 <int-e> fungot: have you stocked up on toilet paper?
14:07:16 <fungot> int-e: this is what you're trying to do, is to load it
14:16:30 -!- ais523 has joined.
14:16:55 <ais523> cpressey: the proofs have varying levels of formality, I'm not sure if any are machine-checkable
14:17:25 <ais523> I have actually started writing TC proofs for a couple of esolangs in Agda, but abandoned them pretty early
14:17:38 <int-e> cpressey: This kind of stuff is really tedious, hard to justify the effort (unless you do it just for fun).
14:17:43 <ais523> it's not an easy sort of thing to translate into Agda
14:17:43 -!- ais523 has quit (Remote host closed the connection).
14:17:55 -!- ais523 has joined.
14:18:07 <ais523> I was considering joining
14:18:17 <wib_jonas> the problem is that a lot of these proofs are really hairy, because eg. when you want to simulate a RAM machine with a turing machine, you need to be able to move all symbols on the tape to insert a space and get back to that space and copy all these move routines multiple times in the turing machine program so that you can return to the previous
14:18:31 -!- ais523 has set topic: Welcome to the international center for esoteric programming discussion, design, development, and deployment! | https://esolangs.org | logs: https://esolangs.org/logs/ http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/?C=M;O=D https://github.com/KrzysztofSzewczyk/esologs/.
14:18:36 <ais523> I felt we needed a fourth d word
14:18:54 <wib_jonas> and be able to store numbers on the tape, and copy or compare numbers between faraway palces in the tape, etc
14:19:11 <ais523> right, I was concentrating mostly on simulating one queue-based language with another
14:19:17 <ais523> but even that is hard to prove things about in Agda
14:19:47 <int-e> I have a formalization that Minsky Machines can implement recursive functions in Isabelle/HOL. That went fairly well, but it's a really nice programming model compared to many esolangs.
14:20:23 <int-e> For example it's very easy to compose Minsky machines; just rename the states apart and add a few glue transitions.
14:20:47 <wib_jonas> and then you want to prove that you can translate a structured program (with if blocks, while blocks, function definitions and non-recursive function calls) to a finite control structure (either with a state for each possible call stack in the original program, or by storing return addresses as data);
14:21:02 <wib_jonas> then you want to prove the same thing for programs with recursive calls too; etc
14:21:03 <int-e> (And I did not impose any bound on the number of registers)
14:22:15 <wib_jonas> and then that you can translate a language that has closures (like lambda expressions) to a language that doesn't have closures but has recursive calls
14:22:30 <wib_jonas> there's a step between, that you can simulate function pointers
14:22:59 <wib_jonas> there are a lot of "high-level" abstractions in real programming languages that you need to be able to prove that a simple computation model can simulate
14:24:14 <int-e> You have to consider that each of these "simple steps" probably involves defining an intermediate language, a semantics for it, a translation, and proofs that the translation preserves the semantics, all for something that we can handwave through in a couple of lines of text.
14:24:26 <int-e> (Because it's highly intuitive.)
14:25:23 <wib_jonas> you have to define the translation of the intermediate states, and prove that each step preserves that translation, translating the effect of a step of one machine to the effect of a step of the other machine
14:26:03 <wib_jonas> of course it's more likely multiple steps of one machine
14:46:21 <cpressey> Is #coq a moderated channel? I tried to ask a question there but got "Cannot send to nick/channel".
14:46:38 <ais523> you can try writing /mode #coq while you're there
14:46:50 <cpressey> afaict it's mode is [+cnt] and afaict that does not mean it's moderated
14:46:50 <ais523> that should give you full information on what channel modes might prevent you sending there
14:47:24 <ais523> hmm, perhaps you're banned from it (although you're unlikely to be banned personally, this could happen as a result of a ban that matches on characteristics other than nick/ident/IP)
14:47:52 <wib_jonas> cpressey: are you logged in to nickserv? a lot of channels ban everyone who isn't logged in to nickserv
14:48:08 <cpressey> int-e: Do you know anything about extraction in Coq?
14:48:12 <ais523> err, muted, not banned
14:48:18 <ais523> if you were banned you wouldn't be able to join it
14:48:30 <int-e> cpressey: nothing beyond the term
14:49:25 <cpressey> OK. It's a really simple question, I expect I already know the answer, it would be nice to have it confirmed but I'll just keep reading and I'll eventually know
14:49:31 <int-e> cpressey: Meaning I think I know what it is abstractly, but not how it's done.
14:51:21 <cpressey> int-e: Well, it's this: Coq is guaranteed to terminate. Are the programs extracted from Coq also guaranteed to terminate?
14:52:23 -!- kritixilithos has quit (Ping timeout: 240 seconds).
14:53:30 -!- spruit11 has joined.
14:53:58 -!- kritixilithos has joined.
14:57:16 <int-e> cpressey: I think so too (though you can mess up the setup)
15:03:35 <cpressey> Yeah, you can do some low-level things and mess it up. What I'm thinking though, is more like: you can't extract a Turing-complete interpreter from a Coq proof. You could extract a compiler, though.
15:06:29 <int-e> Uh, but there's a loophole there.
15:09:12 <int-e> (co)data Res a = Continue (Res a) | Return a
15:09:46 <int-e> Whatever that is in Coq, I haven't ventured there.
15:14:20 -!- LKoen has quit (Remote host closed the connection).
15:15:35 <cpressey> Is that a good loophole or a bad loophole
15:18:56 <esowiki> [[Function x(y)]] https://esolangs.org/w/index.php?diff=70273&oldid=70269 * Hakerh400 * (+0) Fix category link
15:19:08 <cpressey> My understanding of it is bad though
15:19:29 <int-e> The corresponding function Res a -> a is still not total.
15:20:08 <cpressey> We can't extract an big-step interpreter, but we can extract a single-step interpreter that we can iterate as much or as little as we like?
15:20:09 <int-e> The corrsponding notion to termination for codata is productivity: The outermost constructor is produced in finite time.
15:33:44 <ais523> cpressey: my Agda interpreters for TC languages had a cycle limit and got around the no-nonprovably-halting-programs restriction that way
15:34:05 <ais523> you proved two languages were equivalent by proving that if one halted after some number of cycles, the other would also halt after some number of cycles
15:48:09 <cpressey> OK. There would also seem to be a stronger definition of equivalence, where their behaviours have some correspondence regardless of whether they halt or not.
16:03:13 <wib_jonas> cpressey: yes, and you almost certainly have to use such a stronger equivalence statement in the induction part of the proof of the weaker equivalence
16:08:03 <wib_jonas> cpressey: if you want to see formal a simulation proof, I have one written down in detail at http://www.madore.org/cgi-bin/comment.pl/showcomments?href=http%3a%2f%2fwww.madore.org%2f~david%2fweblog%2f2017-08.html%23d.2017-08-18.2460#comment-23792 , and this is an easy one, because the languages it talks about ((1) with arrays and (1)) are both
16:08:03 <wib_jonas> high-level and similar, so there's no messing about with low level details like how to copy a variable length string in a one-tape Turing machine
16:08:23 -!- kritixilithos has quit (Ping timeout: 240 seconds).
16:09:53 <wib_jonas> but even then I omit a lot of fiddly details that you'd have to expand on if you wanted a machine language proof
16:22:02 <wib_jonas> and even there I'm lucky because (1) supports early function returns from inside loops, which simplifies the human-readable description a lot
16:27:16 -!- MTGBusyBeaver42 has joined.
16:29:12 <arseniiv> codata above reminded me about how I tried to invent what a coeffect should look like when I couldn’t sleep the day before. Does anybody knows if coeffects are at all considered somewhere?
16:29:49 -!- LKoen has joined.
16:31:24 <wib_jonas> is that the dual of when nsiders are effected?
16:34:05 <MTGBusyBeaver42> Regarding the non-TC halting problem I'd argue that forcing the output to be 0 is not enough to force something sub TC, as we also get how long it took to terminate.
16:34:20 <arseniiv> I thought something like: in an effectful computation, one can choose and use effect constructors as many times as they like, and in an effect handler, one “deconstructs” exactly one effect and they don’t choose which one, so a coeffectful computation may be where one uses a coeffect constructor just once and doesn’t choose which and a coeffect (co?)handler allows one to pick how many coeffects to eliminate. Looks like gibberish
16:35:52 <wib_jonas> arseniiv: sorry. stupid joke like the one about how cocoa is really just a
16:35:56 <HackEso> A is a village in Norway. The BBC invented it by not understanding things on top of letters.
16:37:05 <arseniiv> wib_jonas: ah, “considers”. I thought it’s a special spelling of “insiders” but didn’t understand why
16:38:00 <wib_jonas> no, that one is about Darth Sidious
16:38:02 <arseniiv> I like co jokes but hadn’t got this one
16:44:54 <ais523> arseniiv: IIRC coeffects are a real area of research that's quite busy
16:45:01 <ais523> I think I've met people who work on them
16:45:29 <ais523> they're the sort of thing that you use comonads to implement, just like you can use monads to implement effects
16:45:44 <ais523> and normally correspond to some sort of resource that is consumed by a computation
16:45:57 <arseniiv> ais523: do you know an expository paper or something?
16:46:12 <ais523> I was hoping there'd be a Wikipedia article but there isn't
16:46:16 <wib_jonas> .oO(if coeffects is a busy area with lots of researchers, then the coronavirus spreads there, so the ronavirus... nah, it doesn't work)
16:46:44 <arseniiv> (yeah I thought about comonads and resources/contexts but inside one head in the early morning it’s not that fruitful)
16:48:30 <arseniiv> I also imagined what it would do with a call stack but the result was of a mixed usefulness too
16:52:12 -!- kritixilithos has joined.
16:52:35 <ais523> arseniiv: try this: http://tomasp.net/blog/2014/why-coeffects-matter/
16:52:48 <ais523> sorry for not answering earlier, I was reading it first to make sure that the author actually understood the subject, but he does
16:55:29 <ais523> (it strikes me that linking a random coeffect tutorial would have had the same risks as linking a random monad tutorial, but fewer people seem to write coeffect tutorials so they're probably of higher average quality)
16:55:39 <ais523> that said, the post does remind me a lot of a monad tutorial :-D
16:56:27 <MTGBusyBeaver42> "co-" is a common prefix, so I'm confident that constant concentrated comedy (contingent on contex of course) could confound/confuse the constituents in the conversation
16:56:41 <ais523> it's a running joke in #esoteric
16:56:42 <wib_jonas> what if you link to the Typeclassopedia instead, since that's known to be a good book? https://wiki.haskell.org/Typeclassopedia#Comonad
16:57:10 <ais523> wib_jonas: that doesn't explain much about why you'd use them
16:57:22 <wib_jonas> true, but it links to references about comonads
16:58:07 <MTGBusyBeaver42> I almost posted it like this: "-" is a mmon prefix, so I'm nfident that nstant ncentrated medy (ntingent on ntex of urse) uld nfound/nfuse the nstituents in the nversation
16:59:39 <ais523> you have to be careful, if comedy is confounding constituents, then nstituents should nfound medy
16:59:50 <ais523> because the co- relationship reverses subject and object
17:00:13 <ais523> it's like a mathematical version of the "in soviet russia" jokes
17:00:29 <ais523> (does this make Soviet Russia an untry?)
17:01:20 <wib_jonas> it works well because "co" is like the thickest part of an English dictionary
17:02:08 -!- wib_jonas has quit (Remote host closed the connection).
17:20:58 <cpressey> "co" jokes are one thing, cojokes are quite another.
17:21:04 -!- cpressey has quit (Quit: A la prochaine.).
17:22:42 -!- imode has joined.
17:27:44 <kmc> ais523: :D
17:49:16 <arseniiv> <ais523> sorry for not answering earlier, I was reading it first to make sure that the author actually understood the subject, but he does => thanks! No problem, as coincidentally I was busy away from here
17:51:04 <arseniiv> <ais523> (it strikes me that linking a random coeffect tutorial would have had the same risks as linking a random monad tutorial, but fewer people seem to write coeffect tutorials so they're probably of higher average quality) => lol :D
17:55:53 <arseniiv> a cojoke is probably a thing several people say crying and an unsuspecting person nearby then feels witless
18:22:38 <ais523> I think a cojoke is something you say in the hope that someone else will cheer you up
18:23:14 -!- atslash has joined.
18:28:39 -!- atslash has quit (Ping timeout: 268 seconds).
18:29:11 -!- atslash has joined.
18:32:02 <zzo38> Does any web browser include the command to pause/rewind/fast-forward animations?
18:32:22 <ais523> I think it depends on the nature of the animations
18:32:46 <ais523> if they're based on a <video> tag, I think it's common for web browsers to offer those options if you right-click the animation (sometimes you have to do it twice, if the site has a custom right-click action defined)
18:33:05 <ais523> for animations based on an <img> tag containing an animated image, I don't think there's a common way to do that
18:34:32 <ais523> on Chromium, it appears to be right-click, right-click, "show controls"
18:34:54 <zzo38> I think it should be possible for <img> too, at least if the picture is loaded as its own document. But I also mean globalling pausing CSS animations (as well as animated pictures)
18:35:25 <ais523> it wouldn't surprise me if Firefox had a way to do that which was really obscure and almost nobody knew about; I don't know what it is if it exists
18:35:34 <ais523> it would be a useful feature, especially when debugging them
18:41:05 -!- atslash has quit (Quit: This computer has gone to sleep).
18:42:19 -!- b_jonas has joined.
18:46:11 -!- kritixilithos has quit (Quit: quit).
18:47:42 -!- atslash has joined.
19:02:32 <zzo38> What is the maximum number of scopes you can make in Italian cards?
19:02:49 -!- art1 has left ("p").
19:16:31 -!- xkapastel has joined.
19:24:31 -!- MTGBusyBeaver42 has quit (Remote host closed the connection).
19:26:36 <zzo38> (Assume that you can put the cards in your order before the cards are dealt, and that opponent can cooperate with you.)
19:29:31 -!- sprocklem has quit (Ping timeout: 260 seconds).
19:31:14 -!- sprocklem has joined.
19:40:54 <esowiki> [[Brainfunc]] M https://esolangs.org/w/index.php?diff=70274&oldid=69814 * PythonshellDebugwindow * (-18) /* Examples */ old
19:42:18 <esowiki> [[Brainfunc]] M https://esolangs.org/w/index.php?diff=70275&oldid=70274 * PythonshellDebugwindow * (-254) /* Infinite cat */ ...
19:42:32 <esowiki> [[Brainfunc]] M https://esolangs.org/w/index.php?diff=70276&oldid=70275 * PythonshellDebugwindow * (-255) /* Set the cell at the CP to 0 */
20:12:30 -!- kspalaiologos has quit (Quit: Leaving).
20:52:26 -!- arseniiv has quit (Ping timeout: 240 seconds).
21:05:37 <int-e> tromp_: did you get around to finding the first odd perfect number in binary lambda calculus? I pushed my own 288 bit version in the meantime but I expect one can do better
21:36:29 -!- MTGBusyBeaver42 has joined.
21:41:18 <MTGBusyBeaver42> zzo38: in one round of itialian cards, assuming i have the rules right, you should be able to sweep every turn by playing the same rank as your opponent (after sweeping a low board with a face card)
21:42:53 <zzo38> MTGBusyBeaver42: Yes, but then the face card played to take the initial four cards won't have a pair for it, isn't it?
21:46:16 <lambdabot> LOWI 132120Z VRB01KT CAVOK 03/M00 Q1021 NOSIG
22:01:20 <MTGBusyBeaver42> still makes for maximum sweeps, you can have the opponent go first and add an ace to 2222
22:20:19 <zzo38> If opponent plays 1 and then you play 5, and then again opponent 1 and you 5, then all of the cards will be paired, but then you won't make a scope on your first turn. Also, there is a rule that scope doesn't count for the last card.
22:23:23 <MTGBusyBeaver42> so you play 8 to sweep 2222, then sweep their card every turn and they have one last unpaired card?
22:24:04 <zzo38> Yes, that can work; they will have a left over 8.
22:27:44 <zzo38> The 8 is the low face card.
22:28:09 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
22:46:49 <tromp_> int-e: it's on my list of things to do; but I got a little sidetracked with cryptocurrency stuff in past week
22:47:28 <tromp_> i will try to find one myself before looking at yours...
22:48:53 <int-e> yeah I'd do the same
22:49:03 <int-e> it's always more fun to compare approaches
23:19:27 -!- FreeFull has joined.
23:23:08 -!- MTGBusyBeaver42 has quit (Remote host closed the connection).
23:28:15 <zzo38> Kjugobe's Pet {1} Legendary Creature - Leech (1/1) ;; Affinity for permanents named Iuckqlwviv Kjugobe ;; {4}, {T}: Remove a poison counter from target player. If you do, that player loses 1 life and put a +1/+1 counter on ~. Can be used only during your turn.
23:45:02 -!- Lord_of_Life_ has joined.
23:46:50 -!- Lord_of_Life has quit (Ping timeout: 240 seconds).
23:46:51 -!- Lord_of_Life_ has changed nick to Lord_of_Life.