←2019-01-28 2019-01-29 2019-01-30→ ↑2019 ↑all
00:10:07 -!- FreeFull has quit (Ping timeout: 240 seconds).
00:10:29 <esowiki> [[ElemScript]] M https://esolangs.org/w/index.php?diff=59498&oldid=59495 * Arseniiv * (-26) [1] no need in plain links to itself, [2] user page links should be explicit, by starting with User:, [3] really please elaborate what you mean there
00:19:13 -!- arseniiv has quit (Ping timeout: 245 seconds).
00:20:45 -!- FreeFull has joined.
00:24:42 <shachaf> kmc: does it gotta go
00:25:46 -!- 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:27:56 <kmc> refusing to let time pass?
00:28:47 -!- Remavas has changed nick to Remavas[ZzZz].
00:30:06 -!- Remavas[ZzZz] has quit (Read error: Connection reset by peer).
00:57:38 <esowiki> [[Special:Log/newusers]] create * EsoLangUser11 * New user account
01:16:03 <shachaf> Do you know any type systems or whatevers that are really linear, not just affine?
01:20:46 <shachaf> Taking the string diagram thing I was thinking about, maybe it'd look like this: Every "function" has some number of input arguments and some number of output arguments, and you have to use each output exactly once.
01:21:39 <shachaf> Maybe you can use uppercase for output and lowercase for input or something.
01:22:25 <shachaf> Seems a bit like a logic language?
01:22:44 <shachaf> The way you can compose things in general is to create new variables for the intermediate values.
01:23:34 <shachaf> Say you have add which has two inputs and one output. You could write something like "add(a, b, X) add(x, c, R)"
01:23:45 <shachaf> Which has three inputs and one output, a,b,c,R
01:24:15 <shachaf> For data/comonoids, you have dup(x, Y, Z) and del(x)
01:25:15 <esowiki> [[Special:Log/newusers]] create * Something Fawful * New user account
01:25:22 <shachaf> Or maybe it's just dup(x, ...) which lets you produce zero or more copies of the input.
01:26:37 <shachaf> Anyway you have to use each variable exactly once each of lowercase and uppercase.
01:26:46 <shachaf> I mean each name.
01:30:33 <shachaf> ski: Seems similar to the mode thing you were talking about the other day, though I think that's not linear.
01:40:03 -!- leonheart has quit (Ping timeout: 256 seconds).
01:48:10 -!- xkapastel has joined.
01:48:16 -!- imode has joined.
01:50:22 -!- leonheart has joined.
02:04:25 -!- leonheart has quit (Ping timeout: 256 seconds).
02:04:59 -!- dauie_ has quit (Ping timeout: 246 seconds).
02:11:00 -!- leonheart has joined.
02:13:38 -!- dauie_ has joined.
02:15:37 -!- dauie_ has quit (Client Quit).
02:15:53 -!- dauie_ has joined.
02:19:01 <esowiki> [[@NUM]] https://esolangs.org/w/index.php?diff=59499&oldid=59478 * KrystosTheOverlord * (+10)
02:24:52 <esowiki> [[@NUM]] https://esolangs.org/w/index.php?diff=59500&oldid=59499 * KrystosTheOverlord * (-10)
02:46:38 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=59501&oldid=59487 * Something Fawful * (+313) /* Introductions */
02:51:30 <esowiki> [[User talk:TuxCrafting]] https://esolangs.org/w/index.php?diff=59502&oldid=49876 * Sigfb05 * (+661)
02:55:43 <esowiki> [[@NUM]] https://esolangs.org/w/index.php?diff=59503&oldid=59500 * KrystosTheOverlord * (+3628)
03:01:39 -!- leonheart has quit (Ping timeout: 256 seconds).
03:17:06 <esowiki> [[@NUM]] https://esolangs.org/w/index.php?diff=59504&oldid=59503 * KrystosTheOverlord * (+15)
03:50:20 -!- APic has quit (Ping timeout: 250 seconds).
03:57:51 -!- APic has joined.
04:23:49 -!- hexfive has joined.
05:08:20 -!- dauie_ has quit (Ping timeout: 250 seconds).
05:24:28 <esowiki> [[Brainfuck algorithms]] https://esolangs.org/w/index.php?diff=59505&oldid=58016 * FSHelix * (+306) /* Divmod algorithm */
05:28:16 -!- myname has quit (Ping timeout: 250 seconds).
05:29:44 -!- myname has joined.
06:00:47 -!- hexfive has quit (Quit: WeeChat 2.3).
06:02:58 -!- sprocklem has quit (Read error: Connection reset by peer).
06:03:22 -!- sprocklem has joined.
06:32:38 -!- FreeFull has quit.
07:45:36 -!- xkapastel has quit (Quit: Connection closed for inactivity).
09:41:31 <shachaf> `? tanebventions: math
09:41:32 <HackEso> Mathematical tanebventions include D-modules, Chu spaces, the torus, Stephen Wolfram, Klein bottles, string diagrams, linear logic, the reals, Lambek's lemma, Curry's paradox, Stone spaces, algebraic geometry, locales, and histograms.
09:41:54 <shachaf> Taneb: You invented string diagrams, maybe you have some idea? This seems pretty neat.
09:42:08 <shachaf> What kind of weird category is this?
09:42:28 <Taneb> What kind of weird category is what?
09:44:16 <shachaf> I'm not sure exactly.
09:44:32 <Taneb> Is it a dagger compact category?
09:44:34 <rain1> `? boost
09:44:35 <HackEso> boost? ¯\(°​_o)/¯
09:44:36 <shachaf> Possibly!
09:45:25 <shachaf> So if you have to be explicit about all inputs and outputs, you might write "f(x) = g(h(x))" as f(x,Z) = f(x,Y) g(y,Z)
09:46:12 <rain1> typo?
09:46:26 <shachaf> Possibly?
09:46:50 <Taneb> f(x,Z) = g(x,Y) h(y,Z)?
09:46:57 <shachaf> Oh, yes.
09:47:26 <Taneb> Well, it definitely feels like a category, I'll start with that
09:47:26 <shachaf> This just corresponds to connecting up strings. Every name must be used twice, once as input (lowercase) and once as output (uppercase).
09:47:52 <shachaf> Except for the ones that are used only once, which are the inputs and outputs to the thing you're defining.
09:48:14 <shachaf> Of course, what do you do when you have something more complicated than composition?
09:48:47 <shachaf> Say you have a sum type that you want to match on.
09:49:10 <shachaf> Do you use something like +, like with tensors?
09:49:42 <shachaf> You could say that some operators can be used in multiple modes. For example cons(x,xs,L) constructs a list, and cons(X,XS,l) matches on a list.
09:50:25 <Taneb> Maybe everything winds up reversible like that?
09:50:45 <Taneb> Depends on your primitives, of course
09:50:59 <shachaf> Then maybe you can write: append(l,ys,ZS) = ( cons(X, XS, l) cons(x, tmp, ZS) append(xs, ys, TMP) ) + ( nil(l) id(ys,ZS) )
09:51:13 <rain1> f(x,Z) = g(x,Y) h(y,Z)
09:51:20 <rain1> how does this work
09:51:23 <shachaf> In "e1 + e2", e1 and e2 must have the same free variables in the same modes.
09:51:29 <rain1> oh right
09:51:34 <rain1> an n-arg function becomes an n+1 arg function
09:51:38 <rain1> and the extra arg is the output
09:51:58 <shachaf> Yes
09:52:01 <rain1> so f(x,Z) = g(x,Y) h(y,Z) means f(x) = h(g(x))
09:52:39 <shachaf> Oh, yes. That one.
09:52:40 <rain1> so this is just prolog!
09:52:52 <shachaf> It's pretty prology the way I'm describing it.
09:53:20 <shachaf> Of course, I think it's more interesting when the things you're dealing with aren't just data (i.e. not comonoids).
09:53:38 <shachaf> So you can't just drop a thing. You must use it exactly once in general.
09:54:46 <shachaf> For example, if you're using this to talk about (multi)linear algebra, you might write f(X,Y) to represent f being a (2,0)-tensor
09:57:18 <shachaf> int-e: got any good chains of block i can get in on twh
09:59:13 <shachaf> Anyway maybe it is prolog-related. What's the category theory of prolog?
10:01:36 <int-e> shachaf: https://www.theguardian.com/world/2017/dec/01/belgian-artist-rescued-from-installation-representing-inescapable-burden-of-history is a pretty good example
10:02:25 <int-e> (unfortunately I didn't find any actual block chains... I would have expected that linked concrete blocks would make a good barricade. maybe I should have used "linked" as a keyword in my search)
10:02:57 <int-e> but lunch first.
10:03:07 <shachaf> @time int-e
10:03:08 <lambdabot> Local time for int-e is Tue Jan 29 11:03:07 2019
10:07:42 -!- arseniiv has joined.
10:09:04 <shachaf> Hmm, maybe an alternative would be producing
10:09:24 <shachaf> one output for each summand, or something?
10:09:38 <shachaf> I don't think that'd work, if you only have one tensor.
10:10:08 <shachaf> Hmm.
10:11:03 <shachaf> For handling a summand, you could have something like:
10:11:33 <arseniiv> (oh, tensors here! I should see the logs)
10:11:55 <shachaf> They're not tensor tensors yet but I hope to connect them.
10:12:43 -!- atslash has joined.
10:12:58 <shachaf> Say you have e.g. data Blah = Left String | Right Int; foo (Left s) = length s; foo (Right x) = twice x
10:13:25 <shachaf> That might turn into something like
10:13:30 <shachaf> foo : (in Blah, out Int)
10:14:24 <shachaf> foo(b, OUT) = left(b, S) length(s, OUT) + right(b, X) twice(x, OUT)
10:14:28 <shachaf> With the + scheme
10:15:13 <shachaf> Oh, I was thinking of something like: foo(b, OUT) = blah(b, L, R) length(l, OUT) twice(r, OUT)
10:15:17 <shachaf> But of course that doesn't work at all.
10:15:27 -!- MDude has quit (Ping timeout: 240 seconds).
10:15:50 <rain1> how about f(a,b,c:x,y) instead of lower/uppercase
10:16:36 <shachaf> Not sure about the exact syntax yet. I'm trying to match index notation with upper/lower indices.
10:17:21 <shachaf> It's important (?) that every letter is used once as input and once as output. Is there a Prolog variant that does that?
10:19:06 -!- arseniiv has quit (Read error: Connection reset by peer).
10:19:15 -!- arseniiv has joined.
10:20:51 <rain1> no
10:21:03 -!- AnotherTest has joined.
10:21:13 <shachaf> If you have a traced monoidal category, you can implement something like recursion with something like foo(x,X)
10:21:19 <shachaf> s/implement/do/
10:24:33 <shachaf> Of course for single-output things you could support a shorthand like f(g(x))
10:24:58 <shachaf> This is more interesting for things with nontrivial graphs.
10:25:59 -!- salpynx has quit (Ping timeout: 256 seconds).
10:33:26 -!- arseniiv_ has joined.
10:36:20 -!- arseniiv has quit (Ping timeout: 246 seconds).
10:41:23 -!- imode has quit (Ping timeout: 268 seconds).
10:43:01 <shachaf> So, presumably true(X) true(x) is just 1
10:43:08 <shachaf> Not sure how the scalars work here exactly.
10:43:21 <shachaf> A scalar is a thing with no inputs and no outputs.
10:43:28 <shachaf> Is there a good meaning for something like (left(a, X) + left(b, X)) ?
10:43:35 <shachaf> Is it just backtracking or something?
10:44:14 <shachaf> true(X) false(x) = 0
10:45:21 <shachaf> whoa, this could be tg
10:53:26 <shachaf> whoa, this is literally prolog
11:03:23 <shachaf> Man, this is TG
11:38:44 -!- Lord_of_Life has quit (Ping timeout: 268 seconds).
11:40:21 -!- Lord_of_Life has joined.
11:56:10 <esowiki> [[Difficult]] N https://esolangs.org/w/index.php?oldid=59506 * A * (+268) Save
12:05:07 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59507&oldid=59506 * A * (+730)
12:05:37 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59508&oldid=59507 * A * (+3)
12:10:01 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59509&oldid=59508 * A * (+444)
12:15:01 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59510&oldid=59509 * A * (+499) /* Setting variables */
12:15:37 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59511&oldid=59510 * A * (+31) /* Other operators */
12:18:20 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59512&oldid=59511 * A * (+86) /* Other operators */
12:19:04 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59513&oldid=59512 * A * (-10)
12:19:44 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59514&oldid=59513 * A * (-68) /* Documentation (actually a tutorial) */
12:20:22 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59515&oldid=59514 * A * (+41) /* =Hello world */
12:20:32 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59516&oldid=59515 * A * (-8) /* Hello World! program */
12:24:44 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59517&oldid=59516 * A * (+162) /* Other operators */
12:27:23 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59518&oldid=59517 * A * (+51)
12:27:46 <esowiki> [[Difficult]] https://esolangs.org/w/index.php?diff=59519&oldid=59518 * A * (-6)
13:02:54 -!- Deewiant has quit (Remote host closed the connection).
13:03:10 -!- Deewiant has joined.
13:27:53 -!- LKoen has joined.
13:28:38 -!- leonheart has joined.
13:30:04 -!- xkapastel has joined.
13:36:21 -!- wob_jonas has joined.
13:37:38 <wob_jonas> oerjan: I blame izabera https://esolangs.org/logs/2016-06-09.html#lNl
13:39:52 <wob_jonas> oerjan: not really a flamewar yet, but there were short exchanges where other people claimed that I make certain pronoun errors for certain deliberate purposes
13:40:08 <wob_jonas> oerjan: as for this case, I think I just wrote "Taneb invented it." because so many wisdoms say that
13:40:45 <wob_jonas> ``` grep -RlF "Taneb invented it." wisdom
13:40:46 <HackEso> wisdom/bbc \ wisdom/sand \ wisdom/diagram chasing \ wisdom/sanity \ wisdom/taneb consistency \ wisdom/shannon \ wisdom/this sentence
13:40:50 <wob_jonas> `? bbc
13:40:51 <HackEso> The BBC is the BreadBox Corporation. Its inventions include, without limitation, Muppets, tiny elfs, villages in Norway, and inventors of all things. Taneb invented it.
13:40:51 <wob_jonas> ` ?sand
13:40:52 <HackEso> ​/srv/hackeso-code/multibot_cmds/lib/limits: line 5: exec: : not found
13:40:55 <wob_jonas> `? sanity
13:40:56 <HackEso> Sanity is the defining property of boily. Taneb invented it.
13:41:01 <wob_jonas> `? diagram chasing
13:41:02 <HackEso> Diagram chasing is a technique used to prove integer lemmas. Taneb invented it.
13:41:03 <wob_jonas> `? sand
13:41:04 <HackEso> Sand is what microprocessors are made of. Taneb invented it.
13:43:04 <wob_jonas> Hmm, not that many apparently. Only like four.
13:44:19 <Taneb> Using "it" to refer to a person in English is incorrect and prone to cause offense in virtually all circumstances
13:45:20 <Taneb> Even if they're a person I invented
13:45:35 <wob_jonas> Taneb: I'm not sure if it's supposed to refer to a person there.
13:45:38 <wob_jonas> `? shannon
13:45:39 <HackEso> Shannon forbade non mathematically minded people from reading his research papers. Taneb invented it.
13:45:48 <Taneb> wob_jonas: it reads to me as referring to Shannon himself
13:45:50 <wob_jonas> It probably refers to the research papers
13:46:15 <FireFly> `? taneb consistency
13:46:16 <HackEso> Taneb consistency is a consistency that is weaker than all other consistencies. Taneb invented it.
13:46:21 <wob_jonas> or perhaps refers to the idea of forbidding non-mathematically minded people from reading papers
13:46:48 <wob_jonas> Hmm, and one of them is probably mine
13:46:52 <wob_jonas> `? it
13:46:53 <HackEso> It would have been certainly so, but `8ball refused to coöperate.
13:47:02 <wob_jonas> ``` hg cat -r 8422 wisdom/it | tail -n+2
13:47:03 <HackEso> Taneb invented it.
13:47:26 <wob_jonas> ^ That was me too, and it may have been another inappropriate use of "it"
13:48:03 <Taneb> `? learn Shannon forbade non mathematically minded people from reading his resarch papers. Taneb invented Shannon, his research papers, and Shannon's prohibition.
13:48:06 <HackEso> learn Shannon forbade non mathematically minded people from reading his resarch papers. Taneb invented Shannon, his research papers, and Shannon's prohibition.? ¯\(°​_o)/¯
13:48:08 <Taneb> `learn Shannon forbade non mathematically minded people from reading his resarch papers. Taneb invented Shannon, his research papers, and Shannon's prohibition.
13:48:11 <HackEso> Relearned 'shannon': Shannon forbade non mathematically minded people from reading his resarch papers. Taneb invented Shannon, his research papers, and Shannon's prohibition.
13:48:22 <Taneb> That's somewhat less ambiguous
13:49:50 <int-e> `grWp tanea
13:49:51 <HackEso> tanea:Tanea plays Minecrafs, Dware Fortresr, and lives in Cambridgd.
13:50:01 <wob_jonas> ``` hg grep -l -r ":8422" 'Taneb invented it' wisdom
13:50:16 <HackEso> wisdom/this sentence:4396 \ wisdom/torus:5763 \ wisdom/bbc:7823 \ wisdom/it:8397 \ wisdom/underwater jousting:8405 \ wisdom/necessity:8408
13:50:23 <wob_jonas> ^ and of those, "it" and "underwater jousting" are my own, so they don't count
13:50:24 <wob_jonas> hmm
13:50:38 * int-e wonders whether "Cambridgd" is still up-to-date.
13:51:02 <int-e> (Not that it's really any of our business.)
13:56:22 <wob_jonas> `? submarine jousting
13:56:23 <HackEso> Submarine jousting is unexplainable.
13:56:26 <wob_jonas> `? underwater jousting
13:56:27 <HackEso> underwater jousting? ¯\(°​_o)/¯
13:56:52 <wob_jonas> hmm, did Taneb invent submarine jousting?
13:57:04 <wob_jonas> ah yes
13:57:06 <wob_jonas> `? tanebventions
13:57:07 <HackEso> Tanebventions include necessity, Go, submarine jousting, Fueue, the universe, metar, sand, dragons, persistence, the BBC, _46bit, progress, sanity, Italian, the grace period, the limerick, ruin, and this sentence. See also tanebventions: maths or tanebventions: foods. He never invents anything involving sex.
13:57:07 <wob_jonas> says so
14:03:09 <wob_jonas> ``` hg log -r "7042" -T "{rev}:{date|shortdate}:{desc}\n" wisdom/tanebvention # ed? seriously?
14:03:10 <HackEso> 7042:2016-02-28:<b_jonas> `` ed wisdom/tanebvention <<<$\'1s/ Go, /&submarine jousting, /\\nwq\'
14:10:16 <wob_jonas> my hon. and learned friend fungot, do you watch submarine jousting?
14:10:16 <fungot> wob_jonas: what we have the important conclusions, the report notes the irony of the governments two working days forward, that the necessary, even if the government are
14:34:36 <Taneb> wob_jonas: I may have invented submarine jousting but Phantom_Hoover is the undisputed world champion
14:35:21 <arseniiv_> btw where could I read about ‘data ~ comonoids’? (I’m reading about that tensory shachaf thing finally, yay)
14:35:27 -!- arseniiv_ has changed nick to arseniiv.
14:35:45 <arseniiv> aaah
14:36:02 <arseniiv> it’s about that deleting and copying, I’ve got it
14:36:42 <arseniiv> counit deletes, cothatotherthing duplicates
14:36:53 <arseniiv> neat
14:38:33 <wob_jonas> no, not really
14:38:43 <arseniiv> also sigfpe have written several times about tensory things in Haskell (and used do notation, how couldn’t it be)
14:38:47 <arseniiv> wob_jonas: huh?
14:39:07 <int-e> ^style
14:39:07 <fungot> Available: agora alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp ukparl* youtube
14:39:24 <int-e> fungot: do *you* want to deliver the brexit?
14:39:25 <fungot> int-e: the right to a review of it. on the commitment to the bill and the other is the reckless. the eu insists that the government take to make that a reality, and that
14:39:41 <wob_jonas> arseniiv: well, I don't really know, but what you wrote sounds suspicious, so my guess is that it's wrong
14:40:24 <arseniiv> it’s the only way a data ~ comonoid makes sense to me yet :)
14:41:13 <arseniiv> maybe shachaf would say in what sense it should be understood, then
14:41:34 <int-e> "Labour has been absolutely clear from the start..." <laughter>
14:42:00 <arseniiv> as I get it, it’s not data vs. codata but data vs. something hardly copyable/destructible
14:42:31 <arseniiv> if it’s the case with the suspicion
14:43:18 -!- MDude has joined.
14:45:55 <arseniiv> also I’m intrigued if there could be an analog of metric tensor, say, commutative functions f(x, y) and f(X, Y) canonical in some way and such that f(x, y) f(Y, Z) = id(x, Z) etc.
15:00:22 <wob_jonas> argh
15:00:37 <wob_jonas> darn you, unpredictable 1-indexing
15:11:27 -!- Essadon has joined.
15:11:44 -!- Essadon has quit (Max SendQ exceeded).
15:22:45 -!- sleepnap has joined.
15:23:49 <arseniiv> shachaf> Oh, I was thinking of something like: foo(b, OUT) = blah(b, L, R) length(l, OUT) twice(r, OUT) => oh, could we make some abstraction of argument lists, too? for example (,) is like conjunction/product, and we could add something like disjunction/sum, and then one should be able to write blah(b, (L ; R)), where (;) is that one “disjunctional separator”
15:24:28 <arseniiv> hm it suddenly reminds me of sequent calculus
15:24:51 <arseniiv> and those traditional formulations of linear logic based on it
15:30:52 <arseniiv> shachaf> something like recursion with something like foo(x,X) => wait wait, what should foo(x, X) mean? Shouldn’t these isolated “scalars” be in a sense unobservable? We can’t interact with them, there’s no strings dangling…
15:32:37 <arseniiv> at least id(x, X) should not add anything, so maybe other scalar terms shouldn’t too… hm but a zero scalar should fail, or that nice addition semantics wouldn’t work
15:33:44 <arseniiv> (also what is TG?)
15:34:19 <Taneb> arseniiv: an acronym shachaf uses, I think to mean "too good"
15:34:46 <wob_jonas> `? tg
15:34:47 <HackEso> TG is short for Turing-Gödel, the highest possible level of difficulty for a multiplayer game. At this level, it's undecidable whether you can manage to halt before losing or not.
15:35:10 <LKoen> tell me you made that up
15:35:40 <arseniiv> “TG is f^W Turing good and too Gödel for me”
15:36:09 <arseniiv> maybe 1 + 1 should be nondeterministic
15:36:53 <wob_jonas> that wasn't me. that was oerjan and int-e.
15:37:42 <wob_jonas> or so the logs claim
15:37:52 <int-e> `cwlprits tg
15:37:54 <HackEso> int-̈e int-̈e oerjän oerjän oerjän oerjän oerjän
15:38:14 <int-e> `dwag tg
15:38:15 <HackEso> ​/srv/hackeso-code/multibot_cmds/lib/limits: line 5: exec: dwag: not found
15:38:24 <Taneb> How does cwlprits handle people with single-character nicks?
15:38:24 * int-e can't remember that command
15:39:11 <Taneb> dowg?
15:39:18 <int-e> `dowg tg
15:39:20 <HackEso> 8822:2016-07-16 <int-̈e> revert \ 8821:2016-07-16 <int-̈e> learn_append tg This gizmo talks gibberish too garbled to grasp. \ 7314:2016-03-29 <oerjän> sedlast s/quit/halt/ \ 7313:2016-03-29 <oerjän> learn_append tg At this level, it\'s undecidable whether you can manage to quit before losing or not. \ 7257:2016-03-21 <oerjän> learn TG is short for Turing-G\xc3\xb6del, the highest possible level of difficulty for a multiplayer game. \ 7256:2016-03-2
15:40:25 <int-e> Oh. I forgot.
16:09:10 -!- 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.”).
16:10:54 <arseniiv> maybe we could add something like subtyping to that tensorial system to be able to control whether an expression is total and/or deterministic
16:10:54 <arseniiv> for example cons(X, XS, l) : (out a, out list a, in cons a), nil(l) : (in nil), and (A : (Γ, in t, Δ), B : (Γ, in u, Δ)) |- A + B : (Γ, in t + u, Δ), and list a = cons a + nil, and we mark list a and other ADTs as “total types” and any non-ADT sums of constructor types as either partial or indeterministic or neither (like cons a + cons a)
16:11:37 <arseniiv> s/neither/both
16:13:32 <arseniiv> and also please forget what I said about 0, it seems it shouldn’t be considered as a fail
16:15:38 <arseniiv> a Prolog analogy suggests it transparently
16:16:56 <arseniiv> also maybe we indeed really deal there with linear logic, and then there should be two kinds of scalars and two different zeros, one is this unconditional success and the other I can’t remember what it is
16:17:44 <arseniiv> its category is monoidal too
16:30:23 -!- arseniiv has changed nick to arseniiv_.
16:30:40 -!- arseniiv_ has changed nick to arseniiv.
16:33:16 <arseniiv> five months ago I @told myself with and underscore some thing and today was very confused when saw and read that message
16:34:27 -!- sleepnap has left.
16:36:41 <Taneb> What was the message
16:42:47 <wob_jonas> the message was "five months ago I @told myself with and underscore some thing and today was very confused when saw and read that message "
16:54:36 <shachaf> arseniiv: Yes, by comonoid I mean copy+delete
16:55:19 <arseniiv> Taneb: it was “why did you add an underscore?”
16:56:47 <shachaf> arseniiv: Yes, sequent composition/the cut rule is the same sort of thing as tensor contraction.
16:57:54 <shachaf> arseniiv: I think there's probably some analog of a metric at least in some contexts.
17:01:15 <shachaf> Why shouldn't 0 be fail? I think it is fail.
17:05:53 <shachaf> Maybe you can do a full classical linear logic thing, in which case it'd be one of the additive units, I guess.
17:14:14 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client).
17:18:02 <arseniiv> shachaf: consider this Prolog code: succeeds() :- . If I get it right, there’s 0 in rhs
17:18:37 <shachaf> I think that should be a 1?
17:19:09 <arseniiv> I’m unsure too
17:19:14 <shachaf> I'm pretty sure.
17:19:32 <shachaf> "foo(X) :- bar(X)." is the same as "foo(X) :- bar(X), succeeds()."
17:20:22 <arseniiv> still, it’s strange in light of that scalars are “uninteracting”
17:20:36 <shachaf> What do you mean?
17:21:06 <arseniiv> we don’t send to, nor recieve from them anything
17:21:20 <arseniiv> how could they change something, then?
17:21:25 <shachaf> Scalars are something like the count of ways to satisfy a program.
17:21:58 <shachaf> There's one way to satisfy succeeds(), and zero ways to satisfy fails().
17:22:10 <shachaf> + adds and , multiplies.
17:22:18 <arseniiv> maybe I just haven’t understood what foo(x, X) should mean
17:22:37 <shachaf> Oh, trace? I'm not sure how it should work either.
17:23:38 <shachaf> But I do know that if you say "foo(x, Y) :- bar(x), vaz(Y)", then foo(x, X) = bar(x) vaz(X)
17:23:53 <shachaf> I'm only not sure about the behavior when they're connected.
17:25:11 <Taneb> Is there such a thing as a completely disconnected category?
17:25:18 <Taneb> Which would just be a collection of monoids, I guess
17:25:37 <arseniiv> hm maybe we must think in a prology way further, then it succeeds iff x is a fixed point of foo
17:26:06 <shachaf> Right, that's trace, of course.
17:26:15 <arseniiv> Taneb: surely it should have a name and maybe even this name
17:26:17 <shachaf> If you represent rules as tensors, trace adds up the diagonals.
17:26:31 <Taneb> arseniiv: eh, as I was typing I realised just how uninteresting it is
17:27:15 <shachaf> Taneb: There are totally disconnected topological spaces which are at least somewhat interesting.
17:29:42 <arseniiv> it’s strange that we get fixed point checking predicates seemingly out of the blue; it should be impossible for some types, but if we don’t trace any “complementary” variable pairs, then it doesn’t appear. How do one constraints that on a level of categories?
17:30:03 <arseniiv> it should be impossible for some types => I mean, equality
17:30:46 <shachaf> I guess these could be infinite-dimensional vector spaces which would mean a lot of my intuition about tensors stops working.
17:31:22 <arseniiv> on the other hand, special properties of id allow us have id(x, X) even if x isn’t equatable, it’s just 1 regardless
17:31:52 <shachaf> Why is id(x, X) 1?
17:32:06 <shachaf> In linera algebra trace(id_V) is the dimension of V
17:32:23 <shachaf> Here it seems like it could be the number of inhabitants of a type or something.
17:32:30 <arseniiv> hm… ow
17:32:34 <shachaf> Which is indeed the number of fixed points.
17:33:34 <arseniiv> this makes some sense, it seems for types without equality we can’t sensibly define a number of inhabitants
17:33:50 <arseniiv> then we can’t allow writing id(x, X) for x of that type
17:33:58 <arseniiv> and we have regularity again
17:34:28 <shachaf> Well, it might still be workable.
17:34:49 <arseniiv> maybe we even can’t have id of these types at all! :o
17:34:59 <arseniiv> then we can’t have foo(x, X) too
17:35:26 <arseniiv> as it should be equal to foo(x, Y) id(y, X), and id(y, X) for that type doesn’t exist
17:35:43 <shachaf> I guess it's possible for some types to have trace and others not.
17:36:12 <arseniiv> trace too?
17:36:19 <shachaf> You can say that, like in Haskell or whatever, trace allows you to write arbitrary recursion.
17:36:42 <shachaf> So things that use trace might not halt.
17:36:44 <shachaf> Trace is the thing that lets you can write foo(x, X)
17:37:06 <arseniiv> I think disallowing id is sufficient
17:37:14 <arseniiv> hm
17:37:28 <arseniiv> yeah, technically it’s the trace
17:39:37 <arseniiv> maybe one should simply ban any expressions with loops
17:40:09 <shachaf> Or only allow them for some types.
17:40:16 <shachaf> In particular for finite types they could be OK?
17:40:49 <shachaf> Also general recursion is probably fine too, who cares.
17:41:01 <shachaf> Can you write recursive rules with trace instead of explicit recursion?
17:42:36 <arseniiv> In particular for finite types they could be OK? => consider boolean not(x, X') dup(x', X, Y)
17:44:34 <shachaf> whoa, if you're allowing duplications that's a different story
17:44:42 <shachaf> Not representable as tensors anymore (?)
17:45:06 <arseniiv> shouldn’t be the category still monoidal? (IDK too)
17:45:35 <shachaf> Sure, but if it's a tensor I know how to contract it, just sum along the diagonal.
17:45:50 <shachaf> In other cases it's less obvious.
17:46:06 <shachaf> Hmm.
17:46:22 <shachaf> If you make + saturating, so 1 + 1 = 1, then I think this may be the category Rel?
17:49:28 <arseniiv> about recursion: let’s take e. g. fact(n, F) = zero(n) one(F) + dup(n, N', N'') succ(M, n') times(n'', f1, F) fact(m, f1)
17:49:43 <arseniiv> I think it isn’t possible without fixed-point combinator
17:50:43 <arseniiv> oh I should’ve written it tail-recursively
17:50:57 <shachaf> I think you should take a simpler recursive function. :-)
17:51:18 <shachaf> What's the simplest recursive definition?
17:51:28 <arseniiv> maybe. Let’s take list length maybe
17:52:55 <shachaf> Maybe doubling a number. That's pretty simple, and even primitive recursion.
17:53:22 <arseniiv> neat!
17:53:35 <shachaf> double(n, OUT) = zero(n) zero(OUT) + succ(M, n) double(m, M2) succ(m2, M2P1) succ(m2p1, OUT)
17:53:38 <shachaf> Right?
17:53:58 <shachaf> This style is so awkward. But I think you can introduce a shorthand to make it easier.
17:54:13 <arseniiv> I’ll write my one from scratch, it’s easier to check then
17:56:24 <arseniiv> ah yes of course it’s all right
17:57:30 <arseniiv> I’ll beter write a tail-recursive one for comparison in plain Haskell first
17:58:16 <shachaf> You think tail recursion will be easier?
17:58:40 <arseniiv> I hope it will connect somehow better
17:59:02 <shachaf> double Z acc = acc; double (S n) acc = double n (S (S acc))
18:00:17 <arseniiv> in these two non-tail-recursive definitions no argument in the definition and in the recursive call does match, let’s see for tail-recursive
18:00:25 <shachaf> double(n, acc, OUT) = zero(n) id(acc, OUT) + succ(M, n) succ(acc, ACCP1) succ(accp1, ACCP2) double(m, ACCP2, OUT)
18:01:22 <arseniiv> at least OUT matches (obviously :D)
18:01:30 <arseniiv> hm I hoped for something more
18:01:31 <shachaf> One of the shorthands I was using before was that you can drop the last argument if it's out-only, and just use a thing as an expression.
18:01:35 <shachaf> Anyway.
18:02:21 <arseniiv> I think we do still need fixed-poind combinator, IDK
18:02:26 <shachaf> The way I think of trace is like https://arxiv.org/pdf/1401.5113.pdf , going around the loop repeatedly until it halts.
18:03:45 <shachaf> Hmm.
18:05:24 <shachaf> Yes, it's tricky
18:08:42 <shachaf> I bet if I was thinking about it more declaratively I could figure it out.
18:09:49 <arseniiv> from another perspective, shouldn’t it then be possible in Prolog or its some known modifiaction?
18:10:03 <arseniiv> modification*
18:10:27 <shachaf> What about something like:
18:10:34 <shachaf> double(n, OUT) = trace_acc { zero(n) id(acc, OUT) + succ(M, n) succ(acc, ACCP1) succ(accp1, ACCp2) id(, OUT) }
18:11:07 <shachaf> I meant id(acc, OUT)
18:11:12 <shachaf> But that's not even outputing ACC, it's nonsense.
18:13:06 <shachaf> double(n, OUT) = real_double(n, OUT, x, X)
18:16:29 <arseniiv> real_double(n, OUT, x, Y) = zero(n) … id(x, Y) + succ(…, n) … succ(x, Y)?
18:19:32 <arseniiv> with such trace semantics, in some other cases it could be troublesome that we start with an unknown x in foo(…, x, X)
18:20:05 <arseniiv> and in this one too, if x could be such that succ(x, X) :o
18:20:34 <arseniiv> so this language shouldn’t be unmarked-lazy
18:27:40 <shachaf> Hmm.
18:32:10 <shachaf> arseniiv: I don't think succ(x, Y) makes sense because then there just aren't going to be any fixed points.
18:38:56 <shachaf> You could maybe use a different style of trace:
18:38:59 <arseniiv> I mean x is not acc, it’s another accumulator solely for the sake of deciding when to stop tracing, and we could eliminate acc afterwards with dup(acc)
18:39:01 <shachaf> (Either e a -> Either e b) -> a -> b
18:39:32 <shachaf> x isn't acc, but your second case should just always be 0, shouldn't it?
18:39:49 <shachaf> When you take the fixed point it'll give you succ(x, X) which should just always fail.
18:40:55 <arseniiv> it seems I didn’t understand what you’ve said about repeating applications then :D
18:41:28 <arseniiv> but your second case should just always be 0, shouldn't it? => at least for n nonzero it would fail too
18:44:08 <shachaf> I don't follow.
18:44:21 <shachaf> When would the right side ever not fail?
18:45:40 <shachaf> Hmm, maybe what you said about dropping n makes sense.
18:45:56 <shachaf> I mean dropping acc
18:46:43 -!- MDude has quit (Ping timeout: 245 seconds).
18:47:14 -!- MDude has joined.
18:49:45 -!- xkapastel has quit (Quit: Connection closed for inactivity).
18:53:01 <shachaf> This is tricky.
19:02:09 -!- imode has joined.
19:03:42 -!- b_jonas has joined.
19:08:40 <b_jonas> Do you know a lottery or stock market where I can get data that is hard to tamper with, hard to guess in advance, is released in a regular schedule and gives new data at least every hour all around the clock, and for which I can be sure people will be able to check the values and these properties even two decades from now?
19:09:46 <b_jonas> I want such a thing for making a nothing-in-my-sleeve proof, where I want to prove something, but for practical reasons my proof requires randomness, so I publish the exact method in advance and perform the proof an hour later based on the publically verifiable randomness that I couldn't have tampered with.
19:10:13 <imode> there are "test" stock markets that do stuff like this.
19:10:47 <b_jonas> imode: '"test" stock market' doesn't sound well. the whole point of a _real_ stock market is that if I could predict the results, I'd be rich.
19:11:01 <b_jonas> and that they probably live for long.
19:11:25 <kmc> something something blockchain
19:11:34 <b_jonas> oh yeah, blockchain could work
19:11:36 <kmc> I know there are Bitcoin lotteries which function like that?
19:12:00 <kmc> like, the random result is based on the next block or something so that it's impossible to predict but also impossible for the lottery people to lie
19:12:05 <b_jonas> someone will hopefully archive the full bitcoin blockchain even if people implement a proper cutting functionality so that clients don't have to store all the chain
19:12:20 <b_jonas> kmc: yes, that should probably work
19:12:48 <b_jonas> today's bitcoin will probably have enough publically accessible mirrored copies twenty years from now
19:13:02 <b_jonas> only
19:13:08 <b_jonas> I don't think that has a one hour turnaround
19:13:18 <b_jonas> I can't get my verified numbers in our hour from now
19:13:49 <b_jonas> or can I? how fast are blocks these days, and how many block do I have to wait in practice?
19:15:26 <kmc> i don't think you need to wait any blocks
19:15:27 <b_jonas> also, isn't a single block still possible to tamper with with a non-vanishing chance if I have enough computing power, so that, say, I can buy a large botnet and have 1/1000 chance of my prediction to go my way, and then do 1000 proofs one of which seems to prove whatever I want?
19:15:38 <b_jonas> kmc: that seems unlikely to me, for bitcoin at least
19:15:42 <kmc> the goal here is not to prevent double spend
19:15:44 -!- oerjan has joined.
19:15:47 <kmc> though I guess
19:15:53 <kmc> it's still bad if a block gets kicked out of the chain later
19:15:57 <kmc> after you've used it as a rng
19:16:29 <kmc> b_jonas: if you have enough compute power you could cherry-pick transactions in order to have some control over the block hash, but you couldn't control all 256 bits feasibly
19:16:37 <kmc> you might want to extract a low amount of entropy per block
19:16:47 <kmc> idk, these are just some off the cuff thoughts not having thought about it deeply
19:19:52 <b_jonas> ah, bitcoin blocks are one per 10 minutes, so one hour might be a bit too short but the idea doesn't seem unrealistic at least
19:20:44 <b_jonas> it could work if I don't insist on hourly
19:21:00 <b_jonas> and bitcoin is much less often closed for days than stock markets
19:21:35 <kmc> I remember reading that mob-run illegal lotteries back in the day would use the stock market closing price
19:22:26 <kmc> b_jonas: do you know about non-interactive zero knowledge proofs?
19:22:43 <kmc> they also involve agreed-on methods for producing 'nothing up my sleeve' randomness
19:26:08 -!- xkapastel has joined.
19:26:48 <shachaf> kmc: Do you like the Fiat-Shamir heuristic?
19:26:51 <shachaf> it's tg
19:27:05 <kmc> what's that
19:27:23 <b_jonas> kmc: um, as far as I know, zero knowledge is different, and the proof I want isn't (necessarily) zero-knowledge. it might be zero-knowledge, but that's somewhat orthogonal to what I want.
19:27:42 <shachaf> The thing where you hash your input to get challenges for your ZKP prover.
19:27:43 <kmc> b_jonas: yes but it might have a similar component
19:28:25 <kmc> b_jonas: traditional ZKP's are interactive protocols where the challenger provides randomness, but you can make them noninteractive by providing an algorithm for the prover to generate randomness, which the challenger can verify isn't cooked somehow
19:28:29 <kmc> like what shachaf just said
19:28:33 <kmc> how secure is that one?
19:28:42 -!- FreeFull has joined.
19:28:51 <b_jonas> in fact, zero-knowledge usually means a non-transferable proof, one where I have a target and I prove something to them based on data they give, but they can't prove to anyone that I proved that thing to them because anyone else could believe that they chose the right data
19:28:58 <b_jonas> that's sort of the opposite of what I want
19:29:00 <shachaf> As far as I can tell it's great.
19:29:18 <shachaf> Also I invented it and then found out it was a standard thing.
19:29:22 <kmc> b_jonas: yes, I am not saying that what you have is a zero knowledge proof system
19:29:25 <kmc> b_jonas: you might want to ask ##crypto too
19:29:33 <shachaf> Blockchain people don't use it because they don't like Fiat.
19:29:50 <b_jonas> oh, I think I see what you mean. what I perform, other than getting the verifiable randomness itself, is sort of a zero-knowledge proof
19:30:06 <b_jonas> except that I can rely on that the input data itself isn't manipulated
19:30:20 <b_jonas> but that's not too big of a difference, you can bridge that gap with a crypto commitment
19:31:13 <shachaf> I think kmc just means "ZKPs use randomness, you use randomness, let's all get along hth"
19:31:21 <b_jonas> let me look up lotteries, there are probably some well-known long-lived ones drawn more often than once a week on the west of the wall
19:31:47 <b_jonas> and hopefully not ones like we have here that take breaks on certain days of a year
19:32:00 <b_jonas> I mean what the heck? why would you close a _lottery_ for a holiday?
19:33:39 <arseniiv> shachaf> This is tricky. => fully agree
19:36:25 <esowiki> [[Talk:Difficult]] N https://esolangs.org/w/index.php?oldid=59520 * Salpynx * (+260) Some "missing characteristics"?
19:40:46 <b_jonas> ok, I probably want something with the stock market, not lottery
19:41:02 <b_jonas> I don't know how the stock market works, but I can probably find out from the internet
19:41:13 <b_jonas> but the problem with the stock market is that I hear sometimes they close for days
19:41:26 <b_jonas> and the closing is often not even planned
19:41:33 <b_jonas> plus they have planned closures for holidays
19:41:43 <b_jonas> and closures every night for several hours
19:41:47 <b_jonas> still, it's better than nothing
19:43:34 <b_jonas> kjm: I don't think that hashing multiple blocks helps. all blocks depend on all the previous blocks as far as I know, so if I can generate one block with my own info, then at that point I know the previous blocks, so I can make the entire hash to come out the way I want.
19:44:08 <b_jonas> for a similar reason, hashing wikipedia edits or IRC lines can't work, because I can take the last edit or the last line of the given period
19:44:32 <b_jonas> it gets a bit tricky because of lag, mind you
19:44:38 <kmc> b l o c k c h a i n
19:44:39 <b_jonas> but still possible
19:45:00 <kmc> also I'm not sure I understand the security model here. is it bad if others can predict in advance the randomness used for a given proof?
19:45:56 <b_jonas> kmc: if "others" can predict in advance, then I can't prove that I'm not one of those "others"
19:45:59 <b_jonas> so yes, it's bad
19:46:05 <kmc> ok
19:46:16 <kmc> can't you prove your identity separately? like with a digital signature
19:46:28 <b_jonas> unless that "others" thing is a really well trusted third party, but those things don't exist
19:46:30 <kmc> I think we need a better description of the overall problem
19:46:35 <kmc> also, maybe we should take this to ##crypto
19:46:38 <kmc> some very knowledgable people there
19:46:49 <b_jonas> here too
19:51:19 <kmc> Riastradh isn't here :)
19:55:40 -!- FreeFull has quit (Quit: Rebooting).
19:56:43 -!- FreeFull has joined.
19:59:26 <shachaf> kmc: me reading an article nominally about ZKPs and then it suddenly starts talking about blockchains: https://blog.openai.com/content/images/2017/04/low_res_maybe_faster.gif
20:00:05 <kmc> lol
20:02:05 -!- Phantom_Hoover has joined.
20:02:06 -!- Phantom_Hoover has quit (Changing host).
20:02:06 -!- Phantom_Hoover has joined.
20:03:44 -!- salpynx has joined.
20:09:02 <b_jonas> hmm wait, how often does Trump tweet, and how reliable is the best pre-trained model that tells what's tweeted by him and what by his campaign manager?
20:09:03 <salpynx> b_jonas: couldn't you achieve the thing by using a standard psuedo-random alogrithim, with a verified distribution, and use a real world source of randomness to provide a seed in the future?
20:09:57 <b_jonas> salpynx: yes, the hard part is the real world source of randomness. I know about cryptographically secure digest that can shuffle the seed so I get a uniform distribution no matter what distribution the input has, if it has enough entropy
20:09:58 <esowiki> [[Talk:Difficult]] M https://esolangs.org/w/index.php?diff=59521&oldid=59520 * Arseniiv * (+317) moar
20:10:40 <b_jonas> salpynx: the question is what's the real world source that has the properties I listed above, verifable long in the future, releasing enough bits approximately every hour, and provably impossible to tamper
20:11:32 <b_jonas> if I only wanted a turnaround of about one week, then certain lotteries would work
20:11:50 <b_jonas> but I want something with shorter wait time, and ideally a bit more entropy, though I can mix two lotteries to get enough entropy
20:12:02 <salpynx> Either way, stock market or blockchain, you could still have some influence over each, or be accused of it. Isn't the only protection against that sort of thing by publishing your method and allowing others to reproduce using any comparable source of randomness of their own?
20:12:19 <b_jonas> salpynx: I am publishing my method in advance, that's the point
20:12:40 <b_jonas> but the question is, what tamper-proof input should the method use?
20:12:57 <b_jonas> stock market is likely close to the answer, I just don't know enough details about it
20:13:01 <arseniiv> b_jonas: how bad is random.org?
20:13:03 <salpynx> Your peers are an unbiased(?) random source
20:13:20 <b_jonas> arseniiv: random.org doesn't provide verifiable (logged in the long term) random numbers as far as I know
20:13:24 <b_jonas> but let me recheck
20:13:59 <arseniiv> hope it would be at least of some use
20:14:23 <shachaf> b_jonas: There's no standard stock market that is open every hour as far as I know.
20:14:47 <shachaf> Forex is the closest but it stil closes for a couple of hours a week, I think.
20:14:49 <b_jonas> shachaf: it can be a combination of multiple stock markets, and even if I can't literally get what I'm asking for, I'd like at least an approximation
20:15:09 <b_jonas> shachaf: even if you give me a method that works any time except Christmas, that would be useful
20:15:13 <shachaf> Also I don't know that there's a canonical hourly price. Though you might be able to figure out something.
20:17:13 <b_jonas> hmm... random.org says they do provide verified random numbers, but only as a paid service https://www.random.org/draws/
20:17:35 -!- salpynx has quit (Ping timeout: 256 seconds).
20:17:45 <b_jonas> that might work
20:18:32 <b_jonas> shachaf: it doesn't need to be "canonical", in the sense that I can publish the exact method in advance, but that method has to be clearly impossible to tamper with
20:19:16 -!- salpynx has joined.
20:19:18 <b_jonas> hmm, no good
20:19:35 <b_jonas> the random.org payed service deliberately provides very little entropy
20:19:51 -!- dauie_ has joined.
20:20:45 <salpynx> Sunspot data, or some other large scale scientific data source that is logged? Might not be very random, but there could be enough in the precision for a seed?
20:21:08 <b_jonas> 0.5 USD per bit... could be worth for an important enough proof, but I'd prefer a lower price
20:21:33 <salpynx> Someone probably has sun activity hourly
20:21:35 <b_jonas> salpynx: oh, that could work
20:21:40 <b_jonas> NASA releases astronomical data
20:21:46 <b_jonas> though I don't think it has a one hour turnaround
20:21:49 <b_jonas> I think there's more lag
20:22:25 <b_jonas> mind you, it's not easy to prove that I'm not working there hiding "copyright bits" in their data
20:22:50 <b_jonas> as in, bits that are such low order that they are effectively noise, not verifiable astronomical data
20:23:14 <b_jonas> still, that's not a bad idea, might perhaps work
20:23:38 <salpynx> Would be interesting to investigate what kind of sources like that exist. On earth metereological might be too easy to "predict"
20:24:03 <salpynx> hth
20:24:13 <b_jonas> the problem with meteorology is the same, I could be working at the computer tech of the meteorological institute whose data I use
20:24:33 <b_jonas> it's hard to prove that I don't work there, nor do any of my friends
20:24:49 <b_jonas> friends in a wide enough sense
20:25:43 <b_jonas> also, meteorological data archives are guarded behind paywalls, they're usually not easy to verify two decades later
20:25:47 <b_jonas> so it probably won't work
20:25:53 <b_jonas> NASA might actually be better
20:26:55 <kmc> b_jonas: blockchain sounds like by far the best solution here, why do you keep dismissing it
20:26:56 <b_jonas> but a lottery or stock market would be the best, because there enough money is riding on enough bits that even a friend probably can't modify the bits the way they want
20:27:14 <b_jonas> kmc: I'm not dismissing it, I'm just not convinced that it works, I'd like more details than just "blockchain"
20:27:18 <kmc> ok
20:27:46 <shachaf> imo invent a blockchain specifically for randomness
20:27:49 <b_jonas> at least it actually sound relevant here, unlike in some of the dozen things where "blockchain" is used as a marketing word
20:28:21 -!- salpynx has quit (Ping timeout: 256 seconds).
20:28:36 <b_jonas> shachaf: or found my own country that isn't destroyed by a war for decades and has a state lottery every hour
20:28:37 <shachaf> Every hour, everyone can submit commitments to integers, and the results are all xored together.
20:28:52 <kmc> well what's wrong with taking the most recent bitcoin block hash
20:29:08 <kmc> perhaps it can be influenced somewhat, but can you counter that by using fewer bits, somehow?
20:29:42 <b_jonas> shachaf: hmm. how do you get it popular enough though, to make enough people interested and committed to run it on their computers?
20:30:03 <shachaf> You don't need that many people.
20:30:24 <shachaf> Each participant can submit their own data if they don't trust it.
20:30:28 <b_jonas> I wonder if one of these old distributed computing projects that search for Mersenne-primes or signals from space or protein folding happens to provide this as a side effect
20:30:34 <shachaf> What's the use of this thing anyway?
20:30:41 <b_jonas> shachaf: see logs above
20:31:34 <shachaf> I don't see it.
20:31:39 <b_jonas> shachaf: yes, but I'd have to convince people that it's worth first, make it one of the few protocols that are really ran by many people, rather than one that's abandonned and a year from now nobody will know that anyone but my friends have even ran it
20:31:44 <b_jonas> one that I couldn't really fake it
20:31:46 <shachaf> Other than the "for making a nothing-in-my-sleeve proof" bit.
20:31:54 <b_jonas> shachaf: that, yes
20:32:03 <shachaf> OK, that seems to underspecify it.
20:32:09 <b_jonas> let me try to give an example
20:38:07 <b_jonas> hmm... you might be right, it's not so easy to give a convincing example without also giving a solution
20:38:17 <b_jonas> still, I'm thinking
20:55:46 <oerjan> @tell fizzie https://esolangs.org/logs/2016-06-09.html#lNl leads me to the wrong message in IE, although the correct one is colored. checking the source shows that i'm actually going to #lnl, IE's anchors are case insensitive.
20:55:46 <lambdabot> Consider it noted.
20:59:18 <b_jonas> shachaf: I think I can give a fictional example that works if I want one day of lag in the randomness. I think I can't really argue that I need as little as one hour of lag.
20:59:22 <b_jonas> shachaf: would that work?
21:00:13 <b_jonas> it's probably possible to get verifiably hard to tamper randomness from stock markets, or by combining multiple lotteries that draw on different days
21:01:46 <oerjan> @tell fizzie trying to google seems to imply there's some html 4 vs 5 thing involved
21:01:46 <lambdabot> Consider it noted.
21:08:34 <kmc> b_jonas: what are you ACTUALLY trying to do
21:08:59 <b_jonas> kmc: nothing yet, I'm just thinking about this as an exercise
21:09:24 <oerjan> `? shannon
21:09:25 <HackEso> Shannon forbade non mathematically minded people from reading his resarch papers. Taneb invented Shannon, his research papers, and Shannon's prohibition.
21:10:01 <oerjan> `slwd shannon//s,resa,resea,
21:10:08 <HackEso> shannon//Shannon forbade non mathematically minded people from reading his research papers. Taneb invented Shannon, his research papers, and Shannon's prohibition.
21:10:21 <b_jonas> oh great, you're fixing that
21:10:43 <oerjan> . o O ( Taneb did not invent correct spelling )
21:14:03 -!- salpynx has joined.
21:17:18 <salpynx> Something "blockchain" could work, depending on a clever algorithm and what the actual requirements, but seems to me that for any specifed hour you could automate some kind of influence into the 'randomness', which depending on the goal and how important it is to you, you could do. Feels like there is still room for sleeve hiding with blockchain
21:17:56 <salpynx> Fictional example would be interesting though to see
21:18:02 <oerjan> @tell Taneb <Taneb> How does cwlprits handle people with single-character nicks? <-- it lets them have the mess they deserve hth
21:18:03 <lambdabot> Consider it noted.
21:18:14 -!- imode has quit (Ping timeout: 246 seconds).
21:19:09 <kmc> salpynx: there definitely is
21:19:16 <kmc> it's a question of how much influence you can have vs. effort
21:19:19 <kmc> whether that can be made practical
21:19:20 <kmc> idk
21:19:53 <salpynx> b_jonas: another idea I just had: micro-quake data combined / averaged from multiple independent sources globally, to remove posdibilty that you work at the sole data source. Should be frequent, and have multiple confirmations fir same events
21:20:34 <kmc> what if I go setting off nuclear bombs to create artificial quakes and influence the data?
21:20:37 <kmc> WHAT THEN??
21:20:43 <oerjan> ^
21:21:07 <b_jonas> salpynx: I certainly don't know enough about who measures and publishes micro-quake data and how to tell if that can work
21:21:56 -!- sprocklem has quit (Ping timeout: 240 seconds).
21:22:10 <oerjan> have you considered LIGO and VIRGO data
21:22:22 <salpynx> kmc: hrm, that's pretty much my argument against blockchain :( At least the nuclear tampering is mire noticable than blockchain manipulation?
21:22:33 <b_jonas> oerjan: hmm, now that's interesting. I'll have to look up how that's published
21:22:45 <oerjan> i'm not sure myself
21:23:31 <b_jonas> hmm, perhaps there's GPS data that is definite and logged
21:23:51 <b_jonas> I mean, data of the GPS satellites and network itself
21:23:59 -!- sprocklem has joined.
21:24:02 <b_jonas> that stuff that the GPS satellites themselves broadcast
21:24:02 <kmc> yes, but satellites are mostly predictable
21:24:20 <b_jonas> kmc: that's not a problem
21:24:46 <b_jonas> I think
21:24:52 <b_jonas> I don't really know how all that GPS stuff works
21:25:11 <oerjan> hm i guess LIGO and VIRGO also have the problem of long downtime periods. although that might get better with more detectors.
21:25:14 <salpynx> Sorry, the sudden outbreak of global nuclear war on the very hour if your "randomness proof" invalidates tour results. Please try again...
21:25:44 <kmc> b_jonas: er, I thought the whole point was to have globally agreed random numbers that can't be predicted in advance
21:26:08 <b_jonas> kmc: yeah, but I mean, I think there's probably enough randomness in the GPS satellite data, as in, they're not too predicatble for this
21:26:23 <b_jonas> but I'm not sure it's broadcast in a single version and logged long time properly
21:26:42 <kmc> orbital mechanics is pretty predictable
21:31:49 -!- salpynx has quit (Ping timeout: 256 seconds).
21:58:50 <b_jonas> thanks for the ideas, I might think or look up more about these
22:30:10 -!- moei has quit (Quit: Leaving...).
23:05:20 -!- TheKing01 has joined.
23:05:39 <TheKing01> Hello all!
23:05:45 <TheKing01> Anything fun your working on?
23:08:03 -!- TheKing01 has quit (Client Quit).
23:08:43 -!- TheKing01 has joined.
23:21:14 -!- TheKing01 has quit (Remote host closed the connection).
23:21:41 -!- AnotherTest has quit (Ping timeout: 250 seconds).
23:21:46 -!- dauie_ has quit (Ping timeout: 244 seconds).
23:31:41 -!- TheKing01 has joined.
23:31:53 -!- imode has joined.
23:32:33 <TheKing01> Hi imode.
23:33:26 <imode> hi TheKing01.
23:35:51 <TheKing01> Anyone working on anything fun?
23:38:34 -!- Lord_of_Life_ has joined.
23:39:16 <kmc> not esolang related
23:39:21 <kmc> i'm learning about ham radio antennas
23:39:46 -!- Lord_of_Life has quit (Ping timeout: 246 seconds).
23:40:55 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
23:41:09 <TheKing01> Oh, cool.
23:41:23 <TheKing01> And I think you mean not esolang related *yet*.
23:41:34 <imode> working on the correspondance between networks of queue automata and physical fields.
23:41:53 <kmc> hehe
23:42:04 <kmc> well, that could be interesting
23:42:04 -!- TheKing01 has quit (Read error: Connection reset by peer).
23:42:16 -!- TheKing01 has joined.
23:47:30 <fizzie> I managed to do my first work-blessed open source thing, which was fun enough, but it's not going to be esolang-related now or later.
23:47:43 <kmc> hi fizzie
23:47:54 <fizzie> Hello.
23:48:03 -!- TheKing01 has quit (Quit: has left the premise).
23:48:11 <kmc> what's new?
23:48:13 -!- Sgeo_ has joined.
23:48:41 -!- TheKing01 has joined.
23:48:47 -!- TheKing01 has quit (Client Quit).
23:49:49 <fizzie> kmc: Not much. Had I already moved to London when you were still around here?
23:49:55 <fizzie> If not, well, I moved to London.
23:50:08 <kmc> we've talked about it in #trains a few times
23:50:15 <kmc> do you like it?
23:50:57 -!- TheKing01 has joined.
23:50:59 <fizzie> The average is positive. Cycling infrastructure could be better, and Brexit's a big mess. But there's a lot going on, and less snow.
23:51:23 <kmc> cool
23:51:57 -!- Sgeo has quit (Ping timeout: 268 seconds).
23:54:10 <rain1> I wonder what you could just if you just had something that reads into a JIT buffer and executes it
23:54:26 <fizzie> We got a UK hosting/VPS company to sponsor the wiki machine (and #esolangs logs + HackEso), that's kind of new.
23:54:37 <kmc> neat
23:55:52 <fizzie> (It used to be on Gregor's shady one-time-fee "Cloud at Cost" box, which was So Flaky.)
23:56:13 -!- Phantom_Hoover has quit (Remote host closed the connection).
23:56:24 <b_jonas> fizzie: is it a short bug report to an open source project that you're depending on at work, without a patch?
23:57:50 <b_jonas> hmm no, that probably wouldn't require a blessing
23:57:54 <TheKing01> Here's a fun idea for an irc related esolang. We have one which uses IRC syntax and one which uses IRC users. How about one that you program over IRC?
23:58:14 <b_jonas> unless you're working under a very strict non-disclosure agreement...
23:58:23 <fizzie> b_jonas: No, it's something standalone I whittled together on my spare time, I just released it under the company copyright because I don't really care, and the review for that is faster than the review for getting a decision that they don't own it.
23:58:27 <fizzie> b_jonas: https://opensource.google.com/projects/nano-exporter
23:59:02 <b_jonas> I see
←2019-01-28 2019-01-29 2019-01-30→ ↑2019 ↑all