[words]: [word] [wor..."
< 1572440729 553758 :kspalaiologos!~kspalaiol@user-5-173-137-42.play-internet.pl JOIN :#esoteric
< 1572442929 242163 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :And if it does, I think it means you can say things like: Second-order logic is Turing-complete.
< 1572442996 823026 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Or maybe even: ZFC is Turing-complete.
< 1572443422 810053 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So is the existential fragment of Peano Arithmetic: https://en.wikipedia.org/wiki/Matiyasevich%27s_theorem
< 1572443703 252409 :jix!~jix@209.250.235.106 QUIT :Ping timeout: 245 seconds
< 1572443913 50092 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :int-e: So is relation algebra: https://en.wikipedia.org/wiki/Relation_algebra#Expressive_power
< 1572443962 707143 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Didn't we agree to call that term rewriting?
< 1572443965 121580 :int-e!~noone@int-e.eu PRIVMSG #esoteric ::P
< 1572444129 687327 :jix!~jix@209.250.235.106 JOIN :#esoteric
< 1572444212 970955 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Yeah yeah. Well. That was inequational. This is equational, and seems richer, not that it matters.
< 1572444219 264825 :int-e!~noone@int-e.eu PRIVMSG #esoteric :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.
< 1572444254 183772 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Of course I've also studied rewriting for some time :P
< 1572444286 635773 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So maybe it's just that familiarity takes away most of the surprise.
< 1572444405 402971 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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?
< 1572444443 141825 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :You don't, you "search" for "proofs" instead.
< 1572444515 501076 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Loosen up and embrace nondeterminism.
< 1572444529 706745 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Or better yet, alternation.
< 1572444557 926669 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Tell that to the CPU manufacturers!
< 1572444593 627351 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Honestly, alternation is beyond my intuition. I have to translate it back to game trees.)
< 1572444637 272345 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: Actually I suspect CPU manufacturers would *love* more non-determinism... cache coherence is a headache. But nobody knows how to program this stuff.
< 1572444712 148868 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Ha. Yeah. That's sort of my point (or is it? -- I'll think about it.)
< 1572444766 20178 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Of course embracing alternation is just a crazy idea... alternation is unphysical.
< 1572444809 822940 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(So is the TCS version of non-determinism unless you believe in quantum suicide.)
< 1572445402 650409 :jix!~jix@209.250.235.106 QUIT :Ping timeout: 268 seconds
< 1572445409 764169 :jix!~jix@209.250.235.106 JOIN :#esoteric
< 1572445524 457326 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric : How do you "run" a "program" in 2nd-order logic? <-- Perform Knuth-Bendix completion on it and hope for the best?
< 1572445607 434916 :int-e!~noone@int-e.eu PRIVMSG #esoteric :uh
< 1572445687 874619 :int-e!~noone@int-e.eu PRIVMSG #esoteric :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.
< 1572445699 981683 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But sure, you can still hope for the best.
< 1572445727 997895 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Oh, right.
< 1572445789 396616 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I read a nice explanation of the higher-order unification algorithm a while ago. It made it sound like a bloody hack.
< 1572445790 642744 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Maybe stick to FOL? Then you have some complete formalisms... and lots of research to try to make them efficient.
< 1572445818 324785 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hmm, by Nipkow maybe?
< 1572445836 131326 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Though many people have written papers on this... and I don't really know the topic.
< 1572445869 691793 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Colleagues struggled with this. I kept away... but I picked up bits and pieces from conversations.
< 1572446036 762024 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I think it was https://github.com/jozefg/higher-order-unification/blob/master/explanation.md
< 1572446099 590066 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :"1. Generate a solution  2. Test it  3. If it was correct, stop  4. Else, go to 1"
< 1572446104 381633 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hmm, flex and rigid, that sounds familiar.
< 1572446155 895323 :int-e!~noone@int-e.eu PRIVMSG #esoteric :e.g. https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.9080
< 1572446172 629603 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(it's deplorable that neither the text nor the source file seems to refer to academic literature)
< 1572446220 525226 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(at least not where I looked... I didn't look closely)
< 1572446322 719707 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I don't have the patience to read the text, I think.
< 1572446348 971839 :int-e!~noone@int-e.eu PRIVMSG #esoteric :@metar lowi
< 1572446349 264000 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :LOWI 301420Z VRB01KT 9999 -RA FEW007 BKN017 BKN050 07/04 Q1023 NOSIG
< 1572446360 231879 :int-e!~noone@int-e.eu PRIVMSG #esoteric :still chilly... and wet :/
< 1572446520 880474 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 JOIN :#esoteric
< 1572446547 826925 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric : 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
< 1572446861 33324 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: as long as you realize it's a best effort
< 1572446938 928745 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572447002 254243 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :the only solution I saw before was to make reduction steps explicit in inferences (that system was meant to check inferences)
< 1572447046 237731 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :maybe this is even not that bad, but I didn’t pursue it yet, only theorized
< 1572447208 93908 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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`
< 1572447257 25565 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :there are so many ways to fall into infinite loops
< 1572447270 676717 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :here one ends up with ϕ[x] ~ x = x and ϕ[y] ~ y = x and must deduce ϕ ~ z.x = z
< 1572447340 305775 :int-e!~noone@int-e.eu PRIVMSG #esoteric :yeah, ϕ[x] ~ x = x has four solutions which is more than a bit annoying.
< 1572447408 213118 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572447409 107684 :int-e!~noone@int-e.eu PRIVMSG #esoteric :and that's an easy case because it's merely *matching*
< 1572447419 403249 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :yeah
< 1572447441 135566 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :(though I hoped my formalism would allow only simple cases like that)
< 1572447463 640193 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :(I planned to restrict types of variables and constructors to a manageable subset)
< 1572447478 973900 :imode!~linear@unaffiliated/imode JOIN :#esoteric
< 1572447493 282907 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :(but I didn’t saw how it would help)
< 1572447541 290806 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I suspect rewriting is preferable to matching `a = b → ϕ[a] → ϕ[b]` in practice even though logically it's the same.
< 1572447617 734997 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: you mean, adding a special rule that a = b ⊦ …a… → …b… for formulas and …a… = …b… for terms?
< 1572447646 919092 :int-e!~noone@int-e.eu PRIVMSG #esoteric :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...
< 1572447656 1105 :int-e!~noone@int-e.eu PRIVMSG #esoteric :+,
< 1572447662 145622 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :in my case it wouldn’t work as there are no intristic = and →, it would be meant as a metalogic framework
< 1572447706 168309 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :intrinsic*
< 1572447713 923550 :int-e!~noone@int-e.eu PRIVMSG #esoteric :One can argue that equality is ubiquitous in most logical contexts, it deserves special treatment.
< 1572447780 895011 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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?
< 1572447793 527036 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(I'd point to paramodulation in first-order logic, which extends resolution to deal with equality.)
< 1572447890 846807 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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
< 1572447901 339888 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I'm exaggerating, of course
< 1572447913 658963 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: though I could define = or ↔ and then mark it as an “equality-like thing”
< 1572447922 382782 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :I hadn’t considered that approach
< 1572447934 893752 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :and still it would be risky
< 1572448241 531169 :kspalaiologos!~kspalaiol@user-5-173-137-42.play-internet.pl QUIT :Ping timeout: 276 seconds
< 1572448352 977121 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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.
< 1572448396 591415 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I really admire Gentzen now ;)
< 1572448474 249320 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I mean, it's hard to beat either natural deduction, or sequent calculus, and hey, they were even invented by the same person.
< 1572448668 500857 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572448715 252765 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :going from Metamath, I inherited disjointness constraints for metavariables — was it in your case too?
< 1572449046 258007 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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.
< 1572449148 828955 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I'd really like to know what Metamath's doing, so one day I'll look into it again, I hope.
< 1572449170 346622 :lf94!~lf94@unaffiliated/lf94 PRIVMSG #esoteric :this is the best prog channel
< 1572449292 211728 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572449292 323820 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572449359 903270 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :cpressey: The Incredible Proof Machine => hm I need to look that up
< 1572449413 513274 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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.)
< 1572449453 904231 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric : 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
< 1572449513 639147 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :so you can express a variety of mathematical notation, but you also need define that with a care, to not make parsing ambiguous
< 1572449532 88005 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :so there are ubiquitous brackets as part of notation
< 1572449539 945223 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :huh, metamath's being mentioned.
< 1572449578 297410 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :I really like tree representation, moreso a typed one to aid against many many typos
< 1572449613 808603 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :and giving helpful error reporting. I hadn’t used Metamath program but I’m afraid it’s an art
< 1572449644 103308 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :imode: have you used it in some way?
< 1572449660 797195 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :I've been looking at it adjacent to what I'm already doing, with curiosity.
< 1572449698 845850 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572449759 274723 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :I find a goal to write a minimalistic proof checker noble but personally I’d rather use something with typed trees as terms
< 1572449830 198711 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572450179 33945 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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.)
< 1572450278 874981 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :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.
< 1572451093 546166 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :And so it goes. I wonder when I'll have enough time to turn my attention to again :)
< 1572451102 368645 :cpressey!~cpressey@5.133.242.4 QUIT :Quit: quietly
< 1572451120 216123 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572451293 800348 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572451379 656692 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :@tell cpressey look at the logs at approx. 2019-10-30 15:58 UTC
< 1572451379 736426 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :Consider it noted.
< 1572451441 813047 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :`dateu
< 1572451444 293420 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :2019-10-30 16:04:03.252 +0000 UTC October 30 Wednesday 2019-W44-3
< 1572451478 393706 :int-e!~noone@int-e.eu PRIVMSG #esoteric :yay for excess precision
< 1572451631 950716 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric : 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
< 1572451632 46829 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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…
< 1572451707 396229 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :44th week already, hm
< 1572451743 149095 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :yeah
< 1572451746 540043 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :we also have 
< 1572451751 4771 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :``` ddate; beat
< 1572451752 194097 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :Today is Pungenday, the 11th day of The Aftermath in the YOLD 3185 \ 714
< 1572452543 564412 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :`paste bin/beat
< 1572452544 426406 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :https://hack.esolangs.org/repo/file/tip/bin/beat
< 1572452572 443212 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :fizzie: apparently I am to blame you for this
< 1572452575 863646 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Don't blame me for the code, I had a lot simpler implementation.
< 1572452593 930069 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :https://hack.esolangs.org/repo/file/dea37ae411c0/bin/beat
< 1572452619 779284 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :`beat -p
< 1572452620 604051 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :724.77
< 1572452621 992421 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :simpler and more broken. does invalid double rounding
< 1572452640 3383 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :s/invalid/incorrect/
< 1572452689 537213 :skyplane!uid399889@gateway/web/irccloud.com/x-sekdqeghmwwoypxo QUIT :Quit: Connection closed for inactivity
< 1572452729 578979 :kspalaiologos!b0dd7a47@176.221.122.71 JOIN :#esoteric
< 1572452804 624770 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :You mean, first to seconds and then to .beats? Meh, it's good enough.
< 1572452841 456499 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Also it had the @ in the output format, because Internet.
< 1572452868 907003 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :ah, for a simpler time
< 1572452897 613636 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :https://www.bonequest.com/1437
< 1572452925 502652 :kmc!~beehive@li521-214.members.linode.com PRIVMSG #esoteric :https://www.bonequest.com/554
< 1572452964 740013 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :oh, it should have @ in the output format? I can fix that
< 1572452985 619352 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :TBH, I'm not sure. It's not like it's an ISO standard format.
< 1572453041 132651 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :yeah "@" prefix may be a bad idea. coreutils uses it to denote unix epoch times
< 1572453055 707215 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :``` dateu -d @1234567890
< 1572453056 435442 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :2019-10-30 04:00:00.000 +0000 UTC October 30 Wednesday 2019-W44-3
< 1572453061 296249 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :The watch had a @ symbol to indicate .beats, and it was often styled that way, but yeah.
< 1572453085 199337 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :hmm, that doesn't look right
< 1572453086 419354 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :"A day in internet time begins at midnight BMT (@000 Swatch .Beats) (Central European Wintertime)."
< 1572453089 289916 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :``` /bin/date -d @1234567890
< 1572453090 21940 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :Fri Feb 13 23:31:30 UTC 2009
< 1572453131 944365 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :oh
< 1572453141 164367 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :``` /bin/date @1234567890
< 1572453141 869617 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :​/bin/date: invalid date '@1234567890'
< 1572453145 923976 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :``` dateu @1234567890
< 1572453146 651826 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :2009-02-13 23:31:30.000 +0000 UTC February 13 Friday 2009-W07-5
< 1572453186 944143 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :maybe we should put some crazy unicode symbol instead of the @ 
< 1572453245 611681 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :﹫
< 1572453497 217550 :kspalaiologos!b0dd7a47@176.221.122.71 QUIT :Remote host closed the connection
< 1572453579 728671 :zzo38!~zzo38@24-207-15-213.eastlink.ca QUIT :Ping timeout: 268 seconds
> 1572453805 51157 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03Ssblut 5*  10New user account
> 1572454012 142367 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=66897&oldid=66870 5* 03Ssblut 5* (+250) 10Hello world!
> 1572454034 120791 PRIVMSG #esoteric :14[[07Cool14]]4 M10 02https://esolangs.org/w/index.php?diff=66898&oldid=50641 5* 03Ssblut 5* (-84) 10Improved spelling and punctuation, removed irrelevant details.
< 1572454665 677664 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 QUIT :Remote host closed the connection
< 1572456466 177006 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric
< 1572456957 126551 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection
< 1572456983 277234 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric
< 1572457051 467292 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :“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
< 1572457217 142383 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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?
< 1572457230 685348 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :(∀x.t ≡ ∀(λx.t))
< 1572458072 852156 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572458123 432826 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :normal people use only →, as I see. This simplifies algorithm specification and some types of reasoning
< 1572458146 994303 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :but maybe this idea of refined →-types would be useful for someone!
< 1572458631 822749 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :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.
< 1572458663 841145 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :hm.
< 1572458836 763508 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :I should probably add some kind of random access memory to my language to ease usage.
< 1572458849 634408 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :I can embed it in my queue but it's just not reasonable.
< 1572458856 474887 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :at the moment.
< 1572459330 320817 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric
< 1572460041 901604 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`olist 1184
< 1572460042 636637 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :olist 1184: shachaf oerjan Sgeo FireFly boily nortti b_jonas
< 1572460844 383999 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :imode: watching video on Noita I thought how would it be if a game wouldn’t be certain about its rules sometimes
< 1572460887 142948 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :like maybe there are several gods each wanting their own and subjecting the world to their conflicting wishes
< 1572460982 12593 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572461070 534407 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :there the god simply gradually wants more and more, at one point even disallowing the player looking at a list of all their commandments
< 1572461161 874460 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :imode: are you writing a game in the queue language? not that one with `?patterns`?
< 1572462547 347710 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :yeah, not the one with patterns.
< 1572462559 142448 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :also, that sounds like tower of heaven.
< 1572462570 543468 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :https://en.wikipedia.org/wiki/Tower_of_Heaven
< 1572462620 706067 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :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.
< 1572462685 821166 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :If only it wasn't Windows-only.
< 1572462695 238400 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :proton has worked well for me in the past.
< 1572462745 832928 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :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.
< 1572462766 33119 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :I'm considering making concurrency a second-tier extension to the language.
< 1572462814 834247 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :{ ... } 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.
< 1572462845 263246 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :from there, creating things like RAM, lists, etc. is pretty trivial.
< 1572462850 872784 :Frater_EST!adrianbibl@172.242.0.73 JOIN :#esoteric
< 1572462990 495205 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :{ V begin V drop dup ^ repeat } 5 ^ $0 ^ V $0 ^ V $0 ^ V for example.
< 1572463042 351785 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :the spawned interpreter just loops repeatedly after receiving a value, duplicating it and sending a copy back to whomever made the request.
< 1572463159 726716 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :V and ^ should consume the handle, though.
< 1572463234 308487 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :there should also probably be some kind of "kill" function to terminate an interpreter given a handle.
< 1572463363 740492 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :wasn't there a brainfuck derivative that added concurrency.
< 1572463449 271134 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :brainfork, that was it. if you added persistence to the whole ensemble, you essentially have an in-memory database with a wild query language.
< 1572463677 754065 :kspalaiologos!~kspalaiol@176.221.122.71 JOIN :#esoteric
< 1572463695 500787 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :Anyone fancy helping with Brainfuck disassembler? 
< 1572463917 24613 :kspalaiologos2!~kspalaiol@176.221.122.71 JOIN :#esoteric
< 1572463926 68755 :kspalaiologos2!~kspalaiol@176.221.122.71 QUIT :Client Quit
< 1572463954 907513 :kspalaiologos!~kspalaiol@176.221.122.71 QUIT :Client Quit
< 1572463971 985002 :kspalaiologos!~kspalaiol@176.221.122.71 JOIN :#esoteric
< 1572464008 591556 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :switching clients
< 1572464290 370916 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :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."
< 1572464433 167016 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :at that point you can build process supervision structures similar to erlang.
< 1572464567 492847 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :a tree node could be a composition of a broadcaster and a variable.
< 1572464820 771047 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric : also, that sounds like tower of heaven. => that’s it, yeah
< 1572465113 63848 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric : you can then (via blocking sends/receives) send data to the newly spawned interpreter. => nice! coroutines aplenty!
< 1572465197 721579 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric : a tree node could be a composition of a broadcaster and a variable. => you lost me
< 1572465257 42768 :MDude!AdiIRC@c-174-55-101-236.hsd1.pa.comcast.net QUIT :Ping timeout: 240 seconds
< 1572465260 830515 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :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.
< 1572465313 626872 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :though I guess you'd need to send the process ID that you're currently "in"... a kind of 'self'.
< 1572465364 31137 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :so { V begin V drop dup ^ repeat } 5 ^ self V ^ would be storing and recalling `5`.
< 1572465381 688737 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :s/self V ^/self ^ V
< 1572465417 9575 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :"^" being "send" and "V" being "receive".
< 1572465503 694295 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :I made a 4,5 KB regex
< 1572465512 845231 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :that in theory is able to disassemble brainfuck
< 1572465532 361228 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :but the regex debugger literally died seeing this
< 1572465534 746574 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :so I'll never know
< 1572465770 755067 :LKoen!~LKoen@81.255.219.130 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.”
< 1572466313 141629 :MDude!AdiIRC@c-174-55-101-236.hsd1.pa.comcast.net JOIN :#esoteric
< 1572466413 867070 :kspalaiologos!~kspalaiol@176.221.122.71 QUIT :Quit: Leaving
< 1572466761 568280 :Frater_EST!adrianbibl@172.242.0.73 QUIT :Remote host closed the connection
< 1572466899 801475 :MDude!AdiIRC@c-174-55-101-236.hsd1.pa.comcast.net QUIT :Ping timeout: 268 seconds
< 1572467023 856678 :tromp!~tromp@2a02:a210:1585:3200:6cf7:9d98:ef9e:7345 QUIT :Remote host closed the connection
< 1572467154 464744 :b_jonas!~x@catv-176-63-14-87.catv.broadband.hu JOIN :#esoteric
< 1572471185 717228 :b_jonas!~x@catv-176-63-14-87.catv.broadband.hu PRIVMSG #esoteric :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?
< 1572471707 444945 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :https://hatebin.com/frolcfqyqy a sketch.
< 1572471738 510888 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :constructing lists backward is weird. I could probably invert that to be prefix instead of postfix.
< 1572472282 975367 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :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.
< 1572472309 543682 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :a deadlock would be { 0 ^ } 0 ^
< 1572472363 109328 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :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.
< 1572472383 504192 :b_jonas!~x@catv-176-63-14-87.catv.broadband.hu PRIVMSG #esoteric :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
< 1572472383 581963 :fungot!~fungot@unaffiliated/fizzie/bot/fungot PRIVMSG #esoteric :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.
< 1572472387 980979 :b_jonas!~x@catv-176-63-14-87.catv.broadband.hu PRIVMSG #esoteric :yet that's not in the logs.
< 1572473058 985240 :tromp!~tromp@2a02:a210:1585:3200:e89e:4bea:fa20:ece9 JOIN :#esoteric
< 1572474083 796452 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :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
< 1572474136 621013 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :because `:t f` gives overly general `F (a1 -> Not (Not a2))`. I’m not sure if that’s fixable
< 1572474188 500905 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :(pf is too more general: `I (F (a -> (a -> b) -> b))`, but that’s okay, it *is* such a general proof)
< 1572474218 316694 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :I’m not sure at all about encodings of ∀ and ∃
< 1572474256 352715 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :if someone would interest themselves, please @tell me
< 1572474309 800573 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric : yet that's not in the logs. => why, I do seem to remember thungot here several days earlier
< 1572474468 592797 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric : 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
< 1572474496 241808 :MDude!AdiIRC@c-174-55-101-236.hsd1.pa.comcast.net JOIN :#esoteric
< 1572474498 911364 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :ah never mind, we could duplicate what we received of course, dumb me
< 1572474525 160105 :b_jonas!~x@catv-176-63-14-87.catv.broadband.hu PRIVMSG #esoteric :arseniiv: that may have been the previous strip, because this one went up only half a day ago
< 1572474558 16327 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :ah so then you could be remembering that penultimate time?
< 1572474585 810588 :b_jonas!~x@catv-176-63-14-87.catv.broadband.hu PRIVMSG #esoteric :https://esolangs.org/logs/2019-10-21.html#lyb
< 1572474589 413767 :b_jonas!~x@catv-176-63-14-87.catv.broadband.hu PRIVMSG #esoteric :yes, it could be
< 1572474677 336939 :b_jonas!~x@catv-176-63-14-87.catv.broadband.hu PRIVMSG #esoteric :I guess when I joined today, I got distracted by all that talk about typechecking higher order types
< 1572475213 604265 :a92!813ff449@129.63.244.73 JOIN :#esoteric
< 1572475268 102116 :a92!813ff449@129.63.244.73 QUIT :Remote host closed the connection
< 1572475554 104687 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru PRIVMSG #esoteric :high-ordering typechecked types
< 1572475976 961931 :arseniiv!~arseniiv@94.41.13.149.dynamic.ufanet.ru QUIT :Ping timeout: 246 seconds
< 1572476105 590037 :ArthurStrong!~ArthurStr@slow.wreckage.volia.net JOIN :#esoteric
< 1572476918 574705 :ARCUN!6cf5fc98@108-245-252-152.lightspeed.miamfl.sbcglobal.net JOIN :#esoteric
< 1572476960 41074 :ARCUN!6cf5fc98@108-245-252-152.lightspeed.miamfl.sbcglobal.net PRIVMSG #esoteric :The newly featured languages seem a bit uninteresting, don't they?
< 1572477449 260192 :int-e!~noone@int-e.eu PRIVMSG #esoteric :do you mean Thue, or the current candidates?
< 1572477497 634815 :ARCUN!6cf5fc98@108-245-252-152.lightspeed.miamfl.sbcglobal.net PRIVMSG #esoteric :let me rephrase: the new languages mentioned in the most recent pages
< 1572477510 909540 :ARCUN!6cf5fc98@108-245-252-152.lightspeed.miamfl.sbcglobal.net PRIVMSG #esoteric :such as textual subleq
< 1572477919 583007 :ARCUN!6cf5fc98@108-245-252-152.lightspeed.miamfl.sbcglobal.net QUIT :Remote host closed the connection
< 1572477959 954070 :int-e!~noone@int-e.eu PRIVMSG #esoteric :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).
< 1572478129 699841 :int-e!~noone@int-e.eu PRIVMSG #esoteric :maye be should start using stub templates?
> 1572478487 913953 PRIVMSG #esoteric :14[[07Textual subleq14]]4 M10 02https://esolangs.org/w/index.php?diff=66899&oldid=66896 5* 03Int-e 5* (+4) 10link