boxfire

371 karmajoined há 11 anos

she/her Opinions my own

comments

anteontemdiscuss

This is not bidirectional. The Davis-Putnam-Robinson-Matiyasevich theorem shows we can make a Diophantine equation that acts as a universal Turing machine, but there’s Diophantine equations that cannot be solved by Turing machines:

https://www.nlp-kyle.com/post/number_computability/

The smallest known Diophantine equation that cannot be solved by any Turing machine last I checked had ~8000 states as a Turing machine. This Turing machine cannot be decided to halt, and if it does halt in finite time then an (outer) Turing machine could execute it to predict that, so this lives beyond decidability:

https://scottaaronson.blog/?p=2725

I find it annoying that the response to this from the Chaitain perspective is to throw your hands in the air and say not all of math is predictable and let “equivalent to halting decidability” be the death of effort. There’s a richer field of ‘hypercomputation’ sitting beyond the pale, and I believe it will be topological applications that untwist this knot [pun intended]. I’m excited for the post Turing world but i dare say I won’t live to see it.

mês passadodiscuss

It actually took only 9 months to work around, and the new method is actually quite effective. After fixing some early bugs it’s as effective as the original drill technique.

mês passadodiscuss

Mars 2020 has a microphone. You can probably find audio out there but here’s some:

https://science.nasa.gov/mission/mars-2020-perseverance/soun...

há 3 mesesdiscuss

So yeah topological sorting is one element, but that global stack is a data race! You need to test set inclusion AND insert into it in an ordered way. Global mutex is gross. To do so lock-free could maybe be done with a lock free concurrent priority queue with a pair of monatomic generation counters for the priorities processed then next, then some memo of updates so that the conflicting re-update is invalidated by violation the generation constraint. I see no less than 3 CAS, so updates across a highly contentious system get fairly hairy. But still, a naive approach is good enough for the 99% so let there be glitches!

há 4 mesesdiscuss

Very cool! Just wanna point out that Mirror + Rotate is really just 3 different mirrors. Of course it may be more interesting to try to characterize the visual domains in terms of those 3 mirrors rather than trying to do so obfuscated between mirror and rotate.

há 5 mesesdiscuss

I am a huge fan of the work towards putting this in kanren as λKanren:

https://www.proquest.com/openview/2a5f2e00e8df7ea3f1fd3e8619...

A few of my own experiments in this time with unification over the binders as variables themselves shows there’s almost always a post HM inference sitting there but likely not one that works in total generality.

To me that spot of trying to binding unification in higher order logic constraint equations is the most challenging and interesting problem since it’s almost always decidable or decidably undecidable in specific instances, but provably undecidable in general.

So what gives? Where is this boundary and does it give a clue to bigger gains in higher order unification? Is a more topological approach sitting just behind the veil for a much wider class of higher order inference?

And what of optimal sharing in the presence of backtracking? Lampings algorithm when the unification variables is in the binder has to have purely binding attached path contexts like closures. How does that get shared?

Fun to poke at, maybe just enough modern interest in logic programming to get there too…

há 7 mesesdiscuss

It’s also funny because it’s a small, incomplete, incompatible subset of c++… seems like a perfect LLVM / clang rewriter case too, it would be easy to convert and be pure c++. Hell even a clang plugin to put the compile time into one process wouldn’t be awful. But i wonder looking at the rewrites if there’s not a terribly janky way to not need a compiler, if at some runtime cost of contextual control flow info.

há 8 mesesdiscuss

It’s exactly the same to try to use pixel buds on an Apple phone too. I don’t blame Apple or Google so much as the ridiculous pissing matches of a society that refuses to find ways to cooperate efficiently. So much energy is wasted in the name of vendor lock-in and related. Would it take more energy for Google and Apple to share in expanding into the Bluetooth capabilities in a shared way? Sure for their developers, in the short run. In less than a year the society wide savings far outweighs that. Apple people might cross pollinate and buy pixel buds. Android people will get airpods. Both companies could make even more money and save us all sanity. But we are organized for short term gains. Gradient descent without knowing or using the topology of the global complex. This isn’t Apple or Google’s job to fix, not even the government. it’s an issue at the social fabric level to have deep conscientiousness… so none of this is ever gonna change in our lives.

ano passadodiscuss

No one is really mentioning this article in from a highschooler. Awesome job! I'm happy to read this today and really hope she will continue to see such inspiring stories and maybe some day make some.

ano passadodiscuss

Is there any succinct publication of his observations?

ano passadodiscuss

That's the only part I care about dang. I still use WSL1 and have done a number of interesting hacks to cross the ABI and tunnel windows into "Linux" userspace and I'd like to make that easier/more direct

ano passadodiscuss

Definitely out of date, e.g. the 3SUM subquadratic conjecture (probably 11) has been solved and improved on [1].

If it's not been already there's immediate application, e.g. problem 41.

[1]:https://link.springer.com/article/10.1007/s00453-015-0079-6

ano passadodiscuss

There's a book that's explicitly about this, "Program = Proof", and though it's not beginner and needs maybe a light version for earlier learners, is an excellent example.

ano passadodiscuss

My story: it's a joke to be a grad student. Salary in 2012: $10,800 per year without housing.

ano passadodiscuss

Nice! Glad to see. Huge quality of life improvement

há 2 anosdiscuss

I've really had a pet peeve about footnotes on mobile and this does the crime. If you click a footnote and it jumps very far away and doesn't have a return navigation, I have left your page usually after the second time I see a footnote and didn't note my exact scroll. A small thing but pretty please don't make me have to hunt for where I was...

há 2 anosdiscuss

Elliott Conal has to covered there: http://conal.net/papers/convolution/

há 2 anosdiscuss

I liked the way Pearl phrased it originally. A calculus of anti-correlations implies causation. That makes the nature of the analysis clear and doesn't set of the classic minds alarm bells.

há 2 anosdiscuss

Yeah I work in an FFRDC, pushing the frontier of our exploration of space. I'm quite passionate both about the employer and (most of the time) my work. If I didn't care about my employer at that level I woulda been out the door after two years. I think to myself sometimes about the other side of that though, like if I didn't care for them but the money was good.

My home hobbies resemble work within my area, but not my current job function, but I'm keenly aware my employer may try to take advantage of my other talents and do I guess the only thing that saves having an alternative hobby is that I'm so diversified that whatever my work task is I can work on an orthogonal hobby at home. It's kinda nice, I've got both really.

In my mind if I "sell out" (in terms of trading in for that sense of purpose in my work), and just work for the paycheck, then I would go for max. Work an HFT quant firm as a senior or principal engineer or research analyst. $$$. Or some other juicy gig. But I would hate myself if that became a slog and I had no time for my interests at home.

há 2 anosdiscuss

and probably no where to hide if you want to just rest and vest.

"Rest and vest". What a luxury. Some of us are trying to tread water with an anvil chained to the waist. That's what I get for choosing to work for something I'm passionate about. What a world