00:00:15 <pikhq> Right now I'd describe it as "I do not especially like how I look right now, but I have a goal in mind that makes me very happy"
00:02:05 -!- moony_ has quit (Read error: Connection reset by peer).
00:02:21 -!- moony_ has joined.
00:03:11 <kmc> I started noticing that I look a lot like my sister now
00:03:21 <int-e> mmm "I have a dream."
00:03:51 <kmc> i had some dreams last night
00:03:53 <kmc> i don't remember them
00:03:56 <kmc> but I think they were pretty bad
00:04:35 <pikhq> The parts I like about how I look, well, jeeze I look a lot like my mom
00:08:58 -!- moony_ has quit (Read error: Connection reset by peer).
00:26:09 <shachaf> two's complement is so good
00:26:19 <shachaf> Can you even believe how good it is?
00:26:37 <shachaf> I was, like, whoa, dude, the first person who figured out two's complement must've been so happy with it.
00:26:48 <shachaf> I looked it up and apparently it was von Neumann. Figures.
00:27:19 -!- FreeFull has quit.
00:30:06 <int-e> Always the same geniuses...
00:31:03 <kmc> is it better than UTF-8
00:31:25 <int-e> kmc: THat's a pretty low standard.
00:31:56 <kmc> what? UTF-8 is great!
00:31:58 <int-e> The ASCII subset of UTF-8 is okay.
00:32:00 <kmc> it's a really good design
00:32:13 <kmc> as far as an encoding for the Unicode character set
00:32:21 <shachaf> UTF-8 is good engineering, sure.
00:32:23 <kmc> as for the Unicode character set itself, well, it's a bit of a mess
00:32:28 <int-e> It's so Western-centric.
00:32:32 <oerjan> . o O ( but two's complement is just (mod 2^n) arithmetic )
00:32:51 <kmc> int-e: a bit, but backwards compatibility with ASCII is important
00:33:00 <int-e> (I may be contradicting myself here.)
00:33:09 <kmc> I am annoyed at how many short code units are wasted on C0 and C1 control codes that are rarely used, but that's life
00:33:18 <int-e> But I like being contrarian.
00:33:20 <kmc> Unicode made some mistakes but they also have some pretty severe constraints
00:33:26 <kmc> int-e: this is a good place for it
00:33:58 <shachaf> another fun thing is sincerely having and expressing opinions
00:34:17 <int-e> oerjan: I see what you did there. I think.
00:34:19 <kmc> I think gzipped UTF-8 is not too bad even on mostly-Chinese texts
00:34:27 <oerjan> int-e: someone had to do it.
00:34:28 <kmc> compared to, say, the 2 byte legacy chinese encodings
00:34:38 <kmc> also most things now are HTML and all the markup is ASCII
00:34:40 <int-e> oerjan: no they didn... err, we've done this already.
00:35:12 <int-e> fungot: can you loop?
00:35:12 <fungot> int-e: sherry was still nice with strawberries and whipped cream, not strawberries with sherry and whipped cream although the sun went down over the source for feeley's ring.scm?
00:35:23 <fungot> Selected style: oots (Order Of The Stick)
00:35:29 <int-e> fungot: what about now?
00:36:00 <shachaf> fungot: what's going to happen with xykon
00:36:00 <fungot> shachaf: that is by far the lowest price i have ever laid at least, that you would even suggest that i would do such as that, yes because that is what, twenty! four! the time, and there, that ought to be good.
00:36:26 <fungot> int-e: i need, a random castle self-destruct."
00:36:27 <HackEso> 10) <fungot> GregorR-L: i bet only you can prevent forest fires. basically, you know. \ 13) <fizzie after embedding some of his department research into fungot> Finally I have found some actually useful purpose for it. \ 14) <fungot> oerjan: are you a man, if there weren't evil in this kingdom to you! you shall find bekkler! executing program. please let me go... put me out! he's really a tricycle! pass him! \ 56) <fungot> i am sad ( of course
00:36:49 <HackEso> 1050) <Taneb> I would like to learn how to use a sword <Taneb> And also how to ride a unicycle <Taneb> Perhaps not at the same time
00:37:47 <oerjan> i suddenly realize that my brain must have always imagined a juggling part in that quote that isn't there
00:41:49 <HackEso> 728) <fungot> itidus21: hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, hey, h
00:43:34 <shachaf> Is there a general name for the kind of algorithm DPLL is?
00:43:46 <shachaf> I mean the kind where you guess and propagate and backtrack.
00:43:50 <HackEso> 1296) <int-e> fungot is here <fungot> int-e: may cause extreme loss of appetite! may cause severe diarrhea and vomiting!
00:43:56 <int-e> I forgot about that one
00:46:04 <int-e> shachaf: I'm not sure whether there's anything between the super generic "branch and bound" (which can involve branching heuristics including branching on something that has only one viable alternative first) and DPLL.
00:46:36 <shachaf> Branch and bound is more sophisticated than DPLL, isn't it?
00:46:57 <int-e> well, it does not have to be
00:47:10 <shachaf> Say you're solving sudoku. The obvious approach is to propagate all the constrains you can, then guess, repeat, backtrack, etc.
00:47:48 <fizzie> I didn't remember there was an oots style.
00:47:51 <int-e> the for SAT, "bound" really just means to immediately backtrack when one of the clauses becomes false.
00:48:23 <shachaf> ILP-style branch-and-bound seems pretty different from that.
00:48:41 <int-e> Yeah, SAT isn't linear
00:50:33 <int-e> I'd agree that it's a degenerate case of branch and bound. I believe the pattern still fits.
00:51:57 <int-e> (But if you insist on *linear* programming rather than more or less arbitrary optimization in a discrete search space (with some exploitable monotonicity to allow bounding), you'll have to disagree.)
00:52:47 <shachaf> Also, do all NP-complete problems have a natural algorithm analogous to that?
00:53:25 <shachaf> Say subset sum. I'm not sure offhand what propagation would look like.
00:53:46 <shachaf> Whereas it's obvious for SAT or exact cover.
00:54:28 <int-e> If the sum becomes too large, do *not* select the number. <-- propagation. Incidentally, a variant of bounding "branch and bound" style.
00:54:55 <shachaf> Is that a heuristic or a guarantee?
00:55:17 <shachaf> I guess it can be a guarantee, if you know how many negative numbers you have left.
00:56:13 <int-e> Ah, I had knapsack in mind... but anyway, a similar heuristic can be made up by taking into account all remaining numbers.
00:56:44 <int-e> You can also do something with remainders modulo prime powers.
00:57:24 <int-e> (If all but one of the remaining numbers are even, then you immediately know whether you have to pick the odd number, or not.)
00:58:14 <int-e> (Hmm, and I guess /occasionally/ one can get leverage out of doing this for moduli that are not prime powers.)
01:00:37 <int-e> shachaf: But I don't think it's inherent in NP... given an arbitrary verifier, it's pretty unreasonable to assume that you can predict its output (accept or not) early.
01:04:35 <int-e> shachaf: And in fact, pre-images of cryptographic hashes are a good example where propagation is hard to impossible.
01:07:10 <int-e> Any significant amount of propagation would weaken pre-image resistance.
01:07:18 <shachaf> One way I think of nondeterministic Turing machines is as deterministic machines with one extra "coin flip" primitive, where NP means that at least one possible sequence of coins will find an answer in polynomial time.
01:07:46 <shachaf> From this perspective the deterministic part is propagation, and the nondeterministic part is the coin flips.
01:08:24 <int-e> shachaf: Yeah but I'm focussing on the coin flips.
01:08:35 <int-e> So propagation only counts if it predicts a coin flip.
01:09:13 <shachaf> Of course SAT solvers don't necessarily guess the coin flips specifically, they just start guessing anywhere and see the consequences.
01:09:30 <int-e> The other view is tenable as well, of course. And in fact that's what happens when you reduce to SAT.
01:09:45 <shachaf> But unit propagation still corresponds to the deterministic part of evaluation, in some sense, I think.
01:17:19 <int-e> There *is* some funny interchangability phenomenon here... in order to compress certificates (the sequence of coin flips leading to acceptance), you can build propagation rules into the verifier.
01:18:10 <shachaf> You mean instead of giving the entire polynomial-size trace of execution or something?
01:18:53 <shachaf> Is there a pathological NP problem that's really hard to compress this way?
01:19:14 <int-e> But it doesn't really match how I think about a typical NP problem. I usually have a naive verifier in mind, which leads to a corresponding search tree corresponding to the coin flips. And then one can start pruning and re-ordering the search tree by propagation rules.
01:19:55 <int-e> shachaf: I'm sticking to cryptographic hashes.
01:20:36 <shachaf> Cryptograhic hashes seem very compressible to me in this sense.
01:21:11 <shachaf> You need to specify the entire preimage, but none of the computation involved in hashing it.
01:21:42 <int-e> The computations are part of the verifier, and I already said that I don't count that as propagation.
01:22:58 <shachaf> Oh, I thought "naive verifier" meant the opposite.
01:24:26 <int-e> To my mind, the naive verifier for hash function takes/guesses the pre-image, computes the hash, and compares that to the desired output.
01:26:07 <int-e> And the question is, can we get the witness size significantly below the size of the preimage. "significantly" is more than O(log(n)) where n is the problem size...
01:26:47 <b_jonas> int-e: not in the case of a cryptographic hash, if it's well-designed
01:27:00 <int-e> b_jonas: that's the claim, yes.
01:27:19 <shachaf> is this like explaining someone's joke to them
01:27:48 <int-e> it's nice to be understood
01:29:55 <int-e> Hmm, how close are random polynomial-sized boolean circuits (n inputs to n outputs) to hash functions?
01:31:16 <int-e> (Very unfamiliar territory for me. You probably have to be very careful to ensure that the functions don't become constant with non-negligible probability, for starters...)
01:31:35 <int-e> probability: what an unlikely nickname
01:31:46 <int-e> probability: how do you cope?
01:32:15 <shachaf> probability: you're non-negligible to me
01:32:41 <int-e> ...because what's the likelihood that this might come up as a topic...
01:33:42 <shachaf> that sounds too 4channy for me
01:33:42 <int-e> probability: do people ask you whether you're high or low a lot?
01:33:55 <int-e> they really should :P
01:34:08 <kmc> i do not have a halloweed nickname
01:34:11 <kmc> i meant halloween
01:34:14 <kmc> but i'm going to own the typo
01:34:28 <shachaf> So this one book takes expectation as axiomatic and defines probability as the expectation of indicator variables, rather than the usual way.
01:34:39 <int-e> kmc: it's perfectly sound grammar ;)
01:34:48 <kmc> the october Hempfest is called Halloweed
01:34:56 <shachaf> Do you like this approach?
01:35:05 -!- moony_ has joined.
01:35:15 <int-e> I mean the -ed ending :)
01:35:31 <int-e> Or suffix as educated people might call it.
01:36:03 <int-e> Hi probability indeed. (How did I miss that!)
01:36:55 <shachaf> Oh, I forgot that int-e doesn't use colors.
01:38:13 <int-e> shachaf: Well it seems I didn't miss much.
01:38:40 <int-e> (the logs have colors if you want them to)
01:39:18 <moony_> probability: ok ima go do something elsr
01:43:27 <int-e> Must be a Markov chain.
01:46:20 * pikhq doesn't like Haloween nicks
01:48:00 <int-e> I didn't realize it was even a thing until 15 minutes ago.
01:52:00 <HackEso> 1316) <shachaf> int-e does not like this [...] <int-e> shachaf: I experience heightened levels of indifference :P <shachaf> Higher than your usual? <int-e> who cares?
01:54:10 <b_jonas> wow it will be pretty cold
01:54:27 <lambdabot> KOAK 300053Z 04008KT 10SM CLR 20/M07 A2991 RMK AO2 SLP129 T02001067
01:54:46 <lambdabot> KSFO 300056Z 30011KT 10SM FEW200 18/04 A2991 RMK AO2 SLP126 T01780039
01:54:50 <lambdabot> KSJC 300053Z 32011KT 10SM FEW036 FEW090 19/M02 A2989 RMK AO2 SLP121 FU FEW036 FU FEW090 T01941017
01:54:55 <lambdabot> KDEN 300053Z 36012KT 1 1/4SM -SN BR OVC020 M13/M14 A3021 RMK AO2 TWR VIS 2 SLP290 P0001 T11281139 $
01:55:15 <pikhq> 1/4SM? Pretty good all things considered.
01:55:36 <lambdabot> LOWI 300150Z 09003KT 060V130 9999 -RA FEW005 BKN014 06/05 Q1022 TEMPO SCT010 BKN020
01:58:14 <int-e> (I had to look up FU.)
01:58:39 <int-e> (And now I'm wondering what's burning. Or is it just chimneys?)
02:00:53 <shachaf> There is a lot of burning.
02:01:00 <shachaf> https://www.nbcnews.com/news/us-news/map-how-big-are-california-fires-see-size-shape-dozens-n1073266
02:01:25 * pikhq is just really cold over here
02:01:32 <int-e> Oh maybe I should've looked up the airport.
02:01:37 <int-e> It makes sense now.
02:01:59 <lambdabot> KLAX 300153Z 21003KT 10SM CLR 18/12 A2989 RMK AO2 SLP122 T01780117 $
02:06:03 -!- b_jonas has quit (Ping timeout: 264 seconds).
02:06:36 -!- b_jonas has joined.
02:06:50 -!- moony_ has quit (Ping timeout: 240 seconds).
02:13:07 -!- oerjan has quit (Quit: Nite).
02:31:01 -!- moony_ has joined.
02:31:16 -!- moony_ has quit (Remote host closed the connection).
02:31:36 -!- moony_ has joined.
03:17:38 -!- moony_ has quit (Quit: AndroIRC - Android IRC Client ( http://www.androirc.com )).
03:30:49 <kmc> shachaf: how's the air in berkeley been
03:41:34 <shachaf> It smelled pretty smoky before but it seems better now.
03:41:55 <kmc> it looks alright on the map yeah https://www.purpleair.com/map?module=AQI&conversion=C0&average=10&layer=standard&advanced=false&inside=false&outside=true&mine=true#7.92/37.825/-122.396
03:42:08 <kmc> the bad thing about this site is that a lot of their sensors are down due to power outages :(
03:55:55 <esowiki> [[L]] https://esolangs.org/w/index.php?diff=66891&oldid=66344 * Voltage2007 * (+703)
04:08:32 -!- sprocklem has joined.
04:09:14 <shachaf> I think Windows-style import libraries actually make a lot of sense.
04:09:31 <shachaf> Though they should probably just be in header files or something?
07:20:17 -!- imode has quit (Ping timeout: 265 seconds).
08:00:16 -!- ArthurStrong has quit (Quit: leaving).
08:14:34 -!- xkapastel has joined.
08:47:56 -!- arseniiv has joined.
08:48:35 -!- cpressey has joined.
08:50:02 -!- GeekDude has quit (Ping timeout: 240 seconds).
08:51:40 -!- GeekDude has joined.
09:14:07 -!- b_jonas has quit (Remote host closed the connection).
09:14:34 <cpressey> Good morning. When we say something nondeterministic like lambda calculus or SKI-calculus is Turing-complete, we mean that there is at least one reduction strategy we know of for it that lets us simulate a deterministic Turing machine in it.
09:15:43 <cpressey> I was going somewhere with this but lost track while I was typing it out.
09:16:37 <cpressey> OK, well, I'll come back to it later.
09:22:37 <arseniiv> <int-e> I didn't realize it was even a thing until 15 minutes ago. => same
09:23:16 -!- Phantom__Hoover has joined.
09:34:45 -!- Phantom__Hoover has quit (Quit: Leaving).
09:35:34 <cpressey> OK. When we say lambda calculus (or some other thing that is per se nondeterministic) is Turing-complete, I think we usually mean there is a reduction strategy for it, under which we can show it can simulate a deterministic Turing machine.
09:37:10 <cpressey> But, you could show a direct simulation along the lines of, for every accepting path in an NTM, there's an accepting path in this nondeterministic thing.
09:39:19 <cpressey> And I'm not sure if I've ever seen a TC proof done in this way, actually.
09:41:25 <cpressey> I guess you don't ever *need* to, because a DTM can simulate a NTM and vice versa.
09:41:59 <cpressey> But what if you have some nondeterministic thing and you don't know of any reduction strategies for it that you can show let it simulate a DTM?
09:42:59 <cpressey> If you can show that it can simulate an arbitrary NTM, does that imply there is some reduction strategy for it under which it can simulate arbitrary DTMs?
09:57:17 <cpressey> I think it does, if you're willing to accept an arbitrarily complex reduction strategy (or rather, one that is potentially as complex as your simulation reduction is.)
10:42:13 -!- tswett[m] has quit (Read error: Connection reset by peer).
10:42:34 -!- wmww has quit (Write error: Connection reset by peer).
11:04:50 -!- tswett[m] has joined.
11:24:18 -!- xkapastel has quit (Quit: Connection closed for inactivity).
11:27:45 -!- wmww has joined.
11:42:11 <esowiki> [[Digital root calculator]] M https://esolangs.org/w/index.php?diff=66892&oldid=46623 * Mechafinch * (+5) Fixed modulo value to 10 for accuracy
11:42:45 <esowiki> [[Digital root calculator]] M https://esolangs.org/w/index.php?diff=66893&oldid=66892 * Mechafinch * (+1) /* Efficient calculation */ Fixed modulo value to 10 for accuracy
11:43:59 <esowiki> [[Digital root calculator]] M https://esolangs.org/w/index.php?diff=66894&oldid=66893 * Mechafinch * (-1) Undo revision 66893 by [[Special:Contributions/Mechafinch|Mechafinch]] ([[User talk:Mechafinch|talk]])
11:44:18 <esowiki> [[Digital root calculator]] https://esolangs.org/w/index.php?diff=66895&oldid=66894 * Mechafinch * (-5) Undo revision 66892 by [[Special:Contributions/Mechafinch|Mechafinch]] ([[User talk:Mechafinch|talk]])
11:49:01 <esowiki> [[Textual subleq]] N https://esolangs.org/w/index.php?oldid=66896 * Joshop * (+878) Created page with "Textual SUBLEQ is a programming language that's similar to SUBLEQ but it uses strings instead of integers. ==Operation== Each line is of the format: <pre> [words]: [word] [wor..."
13:05:29 -!- kspalaiologos has joined.
13:42:09 <cpressey> And if it does, I think it means you can say things like: Second-order logic is Turing-complete.
13:43:16 <cpressey> Or maybe even: ZFC is Turing-complete.
13:50:22 <int-e> So is the existential fragment of Peano Arithmetic: https://en.wikipedia.org/wiki/Matiyasevich%27s_theorem
13:55:03 -!- jix has quit (Ping timeout: 245 seconds).
13:58:33 <cpressey> int-e: So is relation algebra: https://en.wikipedia.org/wiki/Relation_algebra#Expressive_power
13:59:22 <int-e> Didn't we agree to call that term rewriting?
14:02:09 -!- jix has joined.
14:03:32 <cpressey> Yeah yeah. Well. That was inequational. This is equational, and seems richer, not that it matters.
14:03:39 <int-e> cpressey: The thing is, you can just directly simulate Turing machines with string rewriting systems. So this is *far* less surprising than the case Hilbert's ten's problem to me.
14:04:14 <int-e> Of course I've also studied rewriting for some time :P
14:04:46 <int-e> So maybe it's just that familiarity takes away most of the surprise.
14:06:45 <cpressey> What's surprising is that "Turing-complete" has such a heavy connotation of deterministic behaviour, statements like "Second-order logic is Turing-complete" are true, but they sound stupid. How do you "run" a "program" in 2nd-order logic?
14:07:23 <cpressey> You don't, you "search" for "proofs" instead.
14:08:35 <int-e> Loosen up and embrace nondeterminism.
14:08:49 <int-e> Or better yet, alternation.
14:09:17 <cpressey> Tell that to the CPU manufacturers!
14:09:53 <int-e> (Honestly, alternation is beyond my intuition. I have to translate it back to game trees.)
14:10:37 <int-e> cpressey: Actually I suspect CPU manufacturers would *love* more non-determinism... cache coherence is a headache. But nobody knows how to program this stuff.
14:11:52 <cpressey> Ha. Yeah. That's sort of my point (or is it? -- I'll think about it.)
14:12:46 <int-e> Of course embracing alternation is just a crazy idea... alternation is unphysical.
14:13:29 <int-e> (So is the TCS version of non-determinism unless you believe in quantum suicide.)
14:23:22 -!- jix has quit (Ping timeout: 268 seconds).
14:23:29 -!- jix has joined.
14:25:24 <cpressey> <cpressey> How do you "run" a "program" in 2nd-order logic? <-- Perform Knuth-Bendix completion on it and hope for the best?
14:28:07 <int-e> What are your critical pairs? I suppose you can attempt to treat the proof calculus as a higher order rewriting system but then you run into the problem that higher order unification is undecidable.
14:28:19 <int-e> But sure, you can still hope for the best.
14:29:49 <cpressey> I read a nice explanation of the higher-order unification algorithm a while ago. It made it sound like a bloody hack.
14:29:50 <int-e> Maybe stick to FOL? Then you have some complete formalisms... and lots of research to try to make them efficient.
14:30:18 <int-e> Hmm, by Nipkow maybe?
14:30:36 <int-e> Though many people have written papers on this... and I don't really know the topic.
14:31:09 <int-e> Colleagues struggled with this. I kept away... but I picked up bits and pieces from conversations.
14:33:56 <cpressey> I think it was https://github.com/jozefg/higher-order-unification/blob/master/explanation.md
14:34:59 <cpressey> "1. Generate a solution 2. Test it 3. If it was correct, stop 4. Else, go to 1"
14:35:04 <int-e> Hmm, flex and rigid, that sounds familiar.
14:35:55 <int-e> e.g. https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.9080
14:36:12 <int-e> (it's deplorable that neither the text nor the source file seems to refer to academic literature)
14:37:00 <int-e> (at least not where I looked... I didn't look closely)
14:38:42 <int-e> I don't have the patience to read the text, I think.
14:39:09 <lambdabot> LOWI 301420Z VRB01KT 9999 -RA FEW007 BKN017 BKN050 07/04 Q1023 NOSIG
14:39:20 <int-e> still chilly... and wet :/
14:42:00 -!- wib_jonas has joined.
14:42:27 <arseniiv> <cpressey> I think it was https://github.com/jozefg/higher-order-unification/blob/master/explanation.md => oh, unification with metavariables? that could help me with one thing
14:47:41 <int-e> arseniiv: as long as you realize it's a best effort
14:48:58 <arseniiv> better than nothing! I’m interested in cases he calls “stuck on a metavariable”, my simple system was more or less simple other than that
14:50:02 <arseniiv> the only solution I saw before was to make reduction steps explicit in inferences (that system was meant to check inferences)
14:50:46 <arseniiv> maybe this is even not that bad, but I didn’t pursue it yet, only theorized
14:53:28 <arseniiv> my favorite example with that stuck metavariable case was one of inferences using an axiom `a = b → ϕ[a] → ϕ[b]` for inferring `x = y → x = x → y = x`
14:54:17 <wib_jonas> there are so many ways to fall into infinite loops
14:54:30 <arseniiv> here one ends up with ϕ[x] ~ x = x and ϕ[y] ~ y = x and must deduce ϕ ~ z.x = z
14:55:40 <int-e> yeah, ϕ[x] ~ x = x has four solutions which is more than a bit annoying.
14:56:48 <arseniiv> at first I thought it would be feasible to add a constraint disjunction thingy but then (I don’t remember why) I wasn’t in favor of that
14:56:49 <int-e> and that's an easy case because it's merely *matching*
14:57:21 <arseniiv> (though I hoped my formalism would allow only simple cases like that)
14:57:43 <arseniiv> (I planned to restrict types of variables and constructors to a manageable subset)
14:57:58 -!- imode has joined.
14:58:13 <arseniiv> (but I didn’t saw how it would help)
14:59:01 <int-e> I suspect rewriting is preferable to matching `a = b → ϕ[a] → ϕ[b]` in practice even though logically it's the same.
15:00:17 <arseniiv> int-e: you mean, adding a special rule that a = b ⊦ …a… → …b… for formulas and …a… = …b… for terms?
15:00:46 <int-e> It doesn't solve the problem, of course because you still have to unify a particular equation's left-hand side with a subterm of your goal...
15:01:02 <arseniiv> in my case it wouldn’t work as there are no intristic = and →, it would be meant as a metalogic framework
15:01:53 <int-e> One can argue that equality is ubiquitous in most logical contexts, it deserves special treatment.
15:03:00 <arseniiv> but how would I decide for which term sorts should I allow = and for which shouldn’t, and how to know which type … = … should then have?
15:03:13 <int-e> (I'd point to paramodulation in first-order logic, which extends resolution to deal with equality.)
15:04:50 <cpressey> When the metalanguage has to be able to refer to ⊦ on the LHS of a ⊦ you start to wonder why you are even bothering with → anymore
15:05:13 <arseniiv> int-e: though I could define = or ↔ and then mark it as an “equality-like thing”
15:05:22 <arseniiv> I hadn’t considered that approach
15:10:41 -!- kspalaiologos has quit (Ping timeout: 276 seconds).
15:12:32 <cpressey> arseniiv: The issues you mention seem eerily familiar to me; I'm sure I ran into similar ones (though not the same ones) while thinking about how to design a logical metalanguage.
15:13:16 <cpressey> I really admire Gentzen now ;)
15:14:34 <cpressey> I mean, it's hard to beat either natural deduction, or sequent calculus, and hey, they were even invented by the same person.
15:17:48 <arseniiv> cpressey: hm! FTR I tried to make Metamath a system with sorted terms, then I saw that λ-calculus naturally embeds into that, when trying to represent substitutions in terms
15:18:35 <arseniiv> going from Metamath, I inherited disjointness constraints for metavariables — was it in your case too?
15:24:06 <cpressey> I never quite got into Metamath. I came from reverse-engineering The Incredible Proof Machine and eventually realizing it's basically the same as natural deduction. Then trying to square that with term rewriting.
15:25:48 <cpressey> I'd really like to know what Metamath's doing, so one day I'll look into it again, I hope.
15:26:10 <lf94> this is the best prog channel
15:28:12 <arseniiv> and a description of a concrete logic would consist of declarations of some type letters (“completr terms” occurring as steps of inferences would be allowed to have only these types), some constructors of types u1 × … × un → t, again where t is a letter and ui is t1 → … → tn → t0, all ti also letters, this would allow variable binding in the constructor’s arguments; and finally there would be inference rules, each wi
15:28:12 <arseniiv> th complete terms and disjointness constraints as hypotheses and a complete term conclusion, and that would be all. Though I contemplated also something else what I don’t remember now. Ah, something akin to subtyping or simplistic type classes for type letters, to aid against constructor explosion in complex languages
15:29:19 <arseniiv> cpressey: The Incredible Proof Machine => hm I need to look that up
15:30:13 <arseniiv> anyway natural deduction is tg, I agree. Especially when you finally understand how to write its proof trees linearly (like a simply typed λ-calculus with pairs, sums etc.)
15:30:53 <arseniiv> <cpressey> I'd really like to know what Metamath's doing, so one day I'll look into it again, I hope. => AFAIK it’s a string rewriting checker
15:31:53 <arseniiv> so you can express a variety of mathematical notation, but you also need define that with a care, to not make parsing ambiguous
15:32:12 <arseniiv> so there are ubiquitous brackets as part of notation
15:32:19 <imode> huh, metamath's being mentioned.
15:32:58 <arseniiv> I really like tree representation, moreso a typed one to aid against many many typos
15:33:33 <arseniiv> and giving helpful error reporting. I hadn’t used Metamath program but I’m afraid it’s an art
15:34:04 <arseniiv> imode: have you used it in some way?
15:34:20 <imode> I've been looking at it adjacent to what I'm already doing, with curiosity.
15:34:58 <arseniiv> I just read notes on its site and looked at many proofs and definitions from set.mm posted there and read an article about its workings though I don’t remember much from that
15:35:59 <arseniiv> I find a goal to write a minimalistic proof checker noble but personally I’d rather use something with typed trees as terms
15:37:10 <arseniiv> and maybe as proofs. Though I think that can be simulated with linear proofs using explicit ⊦, contexts etc.. But maybe natural-style proofs are easier to check, IDK at all
15:42:59 <cpressey> arseniiv: I actually didn't understand until very recently, that Milner's theorem prover LCF was actually a "DSL" in ML -- proofs are data structures, and the type system ensures you can't build an invalid proof. (Previously I thought ML was simply the implementation language instead of the "host" language like that.)
15:44:38 <cpressey> So now that I've learned that, I wonder if it would be a nicer approach for a proof checker, than designing a dedicated language. I don't know yet.
15:58:13 <cpressey> And so it goes. I wonder when I'll have enough time to turn my attention to again :)
15:58:22 -!- cpressey has quit (Quit: quietly).
15:58:40 <arseniiv> people seem to mention “Dale Miller's pattern calculus” as a decidable system with simple unification algorithm, I googled that and I see something familiar, “Abstract syntax for variable binders <…>” and inside the author talks about β₀-conversion which could be what I seek
16:01:33 <arseniiv> cpressey: proofs are data structures, and the type system ensures you can't build an invalid proof => oh, HOAS at its best; I hadn’t considered encoding proofs like that, this should demand a type system more complex than just for encoding terms
16:02:59 <arseniiv> @tell cpressey look at the logs at approx. 2019-10-30 15:58 UTC
16:04:04 <HackEso> 2019-10-30 16:04:03.252 +0000 UTC October 30 Wednesday 2019-W44-3
16:04:38 <int-e> yay for excess precision
16:07:11 <arseniiv> <cpressey> So now that I've learned that, I wonder if it would be a nicer approach for a proof checker, than designing a dedicated language. I don't know yet. => yeah, it’s nice but one constraints themselves with a basic syntax structure of the host language which can be not what’s desired, maybe not flexible enough. Though the idea of implementing the checker using a library of type inference for a complex language would both admi
16:07:12 <arseniiv> t using HOAS and making any syntax one wishes. Yes, I should consider that. Hm would Haskell’s GADTs allow me to represent inference rules for several simple systems I intended to encode…
16:09:12 <HackEso> Today is Pungenday, the 11th day of The Aftermath in the YOLD 3185 \ 714
16:22:23 <kmc> `paste bin/beat
16:22:24 <HackEso> https://hack.esolangs.org/repo/file/tip/bin/beat
16:22:52 <kmc> fizzie: apparently I am to blame you for this
16:22:55 <fizzie> Don't blame me for the code, I had a lot simpler implementation.
16:23:13 <fizzie> https://hack.esolangs.org/repo/file/dea37ae411c0/bin/beat
16:23:41 <wib_jonas> simpler and more broken. does invalid double rounding
16:24:49 -!- skyplane has quit (Quit: Connection closed for inactivity).
16:25:29 -!- kspalaiologos has joined.
16:26:44 <fizzie> You mean, first to seconds and then to .beats? Meh, it's good enough.
16:27:21 <fizzie> Also it had the @ in the output format, because Internet.
16:27:48 <kmc> ah, for a simpler time
16:28:17 <kmc> https://www.bonequest.com/1437
16:28:45 <kmc> https://www.bonequest.com/554
16:29:24 <wib_jonas> oh, it should have @ in the output format? I can fix that
16:29:45 <fizzie> TBH, I'm not sure. It's not like it's an ISO standard format.
16:30:41 <wib_jonas> yeah "@" prefix may be a bad idea. coreutils uses it to denote unix epoch times
16:30:56 <HackEso> 2019-10-30 04:00:00.000 +0000 UTC October 30 Wednesday 2019-W44-3
16:31:01 <fizzie> The watch had a @ symbol to indicate .beats, and it was often styled that way, but yeah.
16:31:26 <fizzie> "A day in internet time begins at midnight BMT (@000 Swatch .Beats) (Central European Wintertime)."
16:31:30 <HackEso> Fri Feb 13 23:31:30 UTC 2009
16:32:21 <HackEso> /bin/date: invalid date '@1234567890'
16:32:26 <HackEso> 2009-02-13 23:31:30.000 +0000 UTC February 13 Friday 2009-W07-5
16:33:06 <wib_jonas> maybe we should put some crazy unicode symbol instead of the @
16:38:17 -!- kspalaiologos has quit (Remote host closed the connection).
16:39:39 -!- zzo38 has quit (Ping timeout: 268 seconds).
16:43:25 <esowiki> [[Special:Log/newusers]] create * Ssblut * New user account
16:46:52 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=66897&oldid=66870 * Ssblut * (+250) Hello world!
16:47:14 <esowiki> [[Cool]] M https://esolangs.org/w/index.php?diff=66898&oldid=50641 * Ssblut * (-84) Improved spelling and punctuation, removed irrelevant details.
16:57:45 -!- wib_jonas has quit (Remote host closed the connection).
17:27:46 -!- LKoen has joined.
17:35:57 -!- LKoen has quit (Remote host closed the connection).
17:36:23 -!- LKoen has joined.
17:37:31 <arseniiv> “In higher-order patterns, this uncertainty is eliminated by requiring the argument list t̄ in each subterm of the form λv̄.X t̄ to be a list of distinct bound variables w̄. => now let’s see if my formula with equality suffices
17:40:17 <arseniiv> x = y → Φx → Φy. At first glance, it doesn’t have that form: x, y are free, but we can do a trick: ∀x.∀y.x = y → Φx → Φy, now they’re bound; am I missing anything?
17:54:32 <arseniiv> also a quirk of my old approach was a two different kinds of abstraction types: (t1, …, tn)t (in place of t1 × … × tn → t) for constructors and a plain t1 → t2 for things like x.y.term, and two different syntaxes for applications: c(args…) and V[arg], all for better error reporting, as these kinds of applications are pretty different here: the former for constructing terms, the latter is for subst
17:55:23 <arseniiv> normal people use only →, as I see. This simplifies algorithm specification and some types of reasoning
17:55:46 <arseniiv> but maybe this idea of refined →-types would be useful for someone!
18:03:51 <imode> I think to make any progress in any of my projects, I need to agree upon small accomplishable goals and move forward with them. writing an interpreter for my language in my language is not going to be productive. making a text adventure or something will be.
18:07:16 <imode> I should probably add some kind of random access memory to my language to ease usage.
18:07:29 <imode> I can embed it in my queue but it's just not reasonable.
18:15:30 -!- FreeFull has joined.
18:27:22 <HackEso> olist 1184: shachaf oerjan Sgeo FireFly boily nortti b_jonas
18:40:44 <arseniiv> imode: watching video on Noita I thought how would it be if a game wouldn’t be certain about its rules sometimes
18:41:27 <arseniiv> like maybe there are several gods each wanting their own and subjecting the world to their conflicting wishes
18:43:02 <arseniiv> gods and their ill wishes of course remind me A tower of something, I forget what exactly, but it’s that one with soundtrack by flashygoodness
18:44:30 <arseniiv> there the god simply gradually wants more and more, at one point even disallowing the player looking at a list of all their commandments
18:46:01 <arseniiv> imode: are you writing a game in the queue language? not that one with `?patterns`?
19:09:07 <imode> yeah, not the one with patterns.
19:09:19 <imode> also, that sounds like tower of heaven.
19:09:30 <imode> https://en.wikipedia.org/wiki/Tower_of_Heaven
19:10:20 <imode> noita is nuts. it makes me wonder why nobody's tried physics at that scale, though I haven't tried running it on my machine, so who knows if it's actually performant.
19:11:25 <shachaf> If only it wasn't Windows-only.
19:11:35 <imode> proton has worked well for me in the past.
19:12:25 <imode> I'm looking at ways of making my queue language more robust with respect to how I _want_ to program rather than how I _currently_ program. I don't have functions, just bare loops, but adding functions/subroutines seems like a waste.
19:12:46 <imode> I'm considering making concurrency a second-tier extension to the language.
19:13:34 <imode> { ... } creates a new interpreter running concurrently to the one that created it and enqueues the ID of that interpreter. you can then (via blocking sends/receives) send data to the newly spawned interpreter.
19:14:05 <imode> from there, creating things like RAM, lists, etc. is pretty trivial.
19:14:10 -!- Frater_EST has joined.
19:16:30 <imode> { V begin V drop dup ^ repeat } 5 ^ $0 ^ V $0 ^ V $0 ^ V for example.
19:17:22 <imode> the spawned interpreter just loops repeatedly after receiving a value, duplicating it and sending a copy back to whomever made the request.
19:19:19 <imode> V and ^ should consume the handle, though.
19:20:34 <imode> there should also probably be some kind of "kill" function to terminate an interpreter given a handle.
19:22:43 <imode> wasn't there a brainfuck derivative that added concurrency.
19:24:09 <imode> brainfork, that was it. if you added persistence to the whole ensemble, you essentially have an in-memory database with a wild query language.
19:27:57 -!- kspalaiologos has joined.
19:31:57 -!- kspalaiologos2 has joined.
19:32:06 -!- kspalaiologos2 has quit (Client Quit).
19:32:34 -!- kspalaiologos has quit (Client Quit).
19:32:51 -!- kspalaiologos has joined.
19:38:10 <imode> an interesting snippet is a broadcaster. the protocol would be "I send you a 0, and then I send you a handle, and you'll add it to your list of handles." and "I send you a 1, then I send you a value, and you'll run through the list of handles and send it to all of them."
19:40:33 <imode> at that point you can build process supervision structures similar to erlang.
19:42:47 <imode> a tree node could be a composition of a broadcaster and a variable.
19:47:00 <arseniiv> <imode> also, that sounds like tower of heaven. => that’s it, yeah
19:51:53 <arseniiv> <imode> you can then (via blocking sends/receives) send data to the newly spawned interpreter. => nice! coroutines aplenty!
19:53:17 <arseniiv> <imode> a tree node could be a composition of a broadcaster and a variable. => you lost me
19:54:17 -!- MDude has quit (Ping timeout: 240 seconds).
19:54:20 <imode> a variable could be a process that takes a value, then loops infinitely. upon receiving any value, it sends a copy of the value given initially to the requesting process.
19:55:13 <imode> though I guess you'd need to send the process ID that you're currently "in"... a kind of 'self'.
19:56:04 <imode> so { V begin V drop dup ^ repeat } 5 ^ self V ^ would be storing and recalling `5`.
19:56:21 <imode> s/self V ^/self ^ V
19:56:57 <imode> "^" being "send" and "V" being "receive".
20:02:50 -!- 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.”).
20:11:53 -!- MDude has joined.
20:13:33 -!- kspalaiologos has quit (Quit: Leaving).
20:19:21 -!- Frater_EST has quit (Remote host closed the connection).
20:21:39 -!- MDude has quit (Ping timeout: 268 seconds).
20:23:43 -!- tromp has quit (Remote host closed the connection).
20:25:54 -!- b_jonas has joined.
21:33:05 <b_jonas> kspalaiologos: 5 kilobytes doesn't sound too big. maybe you should try a different regex engine. do you use only the regular operations proper, or the irrational extensions like backreferences?
21:41:47 <imode> https://hatebin.com/frolcfqyqy a sketch.
21:42:18 <imode> constructing lists backward is weird. I could probably invert that to be prefix instead of postfix.
21:51:22 <imode> the way send/receive works is that receive essentially just... infloops. sends also infloop, but only if the target process' instruction isn't a receive.
21:51:49 <imode> a deadlock would be { 0 ^ } 0 ^
21:52:43 <imode> when a send matches with a receive, the sending end dequeues an item and pushes it to the receiving end's queue. both then increment their instruction pointers by one.
21:53:03 <b_jonas> this is strange. I have a distinct memory that when I saw that the new o strip was released, I invoked olist and thanked fungot, and HackEso even said "Thanks, fungot. Thungot." which means I wasn't typing it to the wrong channel
21:53:03 <fungot> b_jonas: i know, i was, uh, " child" parody so soon? we'll get sneak attacked if we go down a level and face me! ye may haf tha upper hand in it. or a pool, pal.
21:53:07 <b_jonas> yet that's not in the logs.
22:04:18 -!- tromp has joined.
22:21:23 <arseniiv> my first try of Haskell HOAS for natural deduction for first-order intuitionistic logic, at least it works for a simple zero-order example and when we don’t try to statically check what is the proof of what: https://repl.it/repls/ImpartialWaterloggedFolder
22:22:16 <arseniiv> because `:t f` gives overly general `F (a1 -> Not (Not a2))`. I’m not sure if that’s fixable
22:23:08 <arseniiv> (pf is too more general: `I (F (a -> (a -> b) -> b))`, but that’s okay, it *is* such a general proof)
22:23:38 <arseniiv> I’m not sure at all about encodings of ∀ and ∃
22:24:16 <arseniiv> if someone would interest themselves, please @tell me
22:25:09 <arseniiv> <b_jonas> yet that's not in the logs. => why, I do seem to remember thungot here several days earlier
22:27:48 <arseniiv> <imode> a variable could be a process that takes a value, then loops infinitely. upon receiving any value, it sends a copy of the value given initially to the requesting process. => only once? Isn’t that kind of too linear? :D
22:28:16 -!- MDude has joined.
22:28:18 <arseniiv> ah never mind, we could duplicate what we received of course, dumb me
22:28:45 <b_jonas> arseniiv: that may have been the previous strip, because this one went up only half a day ago
22:29:18 <arseniiv> ah so then you could be remembering that penultimate time?
22:29:45 <b_jonas> https://esolangs.org/logs/2019-10-21.html#lyb
22:31:17 <b_jonas> I guess when I joined today, I got distracted by all that talk about typechecking higher order types
22:40:13 -!- a92 has joined.
22:41:08 -!- a92 has quit (Remote host closed the connection).
22:45:54 <arseniiv> high-ordering typechecked types
22:52:56 -!- arseniiv has quit (Ping timeout: 246 seconds).
22:55:05 -!- ArthurStrong has joined.
23:08:38 -!- ARCUN has joined.
23:09:20 <ARCUN> The newly featured languages seem a bit uninteresting, don't they?
23:17:29 <int-e> do you mean Thue, or the current candidates?
23:18:17 <ARCUN> let me rephrase: the new languages mentioned in the most recent pages
23:18:30 <ARCUN> such as textual subleq
23:25:19 -!- ARCUN has quit (Remote host closed the connection).
23:25:59 <int-e> Not sure that one is all that bad... well, apart from the lack of love the page has received, and perhaps that the halting problem is trivial (if I read the description correctly).
23:28:49 <int-e> maye be should start using stub templates?
23:34:47 <esowiki> [[Textual subleq]] M https://esolangs.org/w/index.php?diff=66899&oldid=66896 * Int-e * (+4) link