Posts by jix@mathstodon.xyz
(DIR) Post #A5jFex7rcteiVRXCfQ by jix@mathstodon.xyz
2021-03-19T13:25:51Z
0 likes, 0 repeats
@11011110 @christianp I'm not sure whether Mastodon relies on that mitigation. I would certainly consider it bad practice to do so, but it does provide an extra layer of defense in case of bugs in the Mastodon code base, so disabling it might not be desirable either.In theory the 'nonce-*' policy would allow passing the nonce to MathJax, allowing it to tag the inline CSS as permitted, but in general that does not work for style attributes, only for style tags, and MathJax uses attributes.
(DIR) Post #A5jFez9M6K2MmeFQGm by jix@mathstodon.xyz
2021-03-30T07:41:41Z
0 likes, 1 repeats
@christianp @mwt @11011110 I think you would also need to modify it to put all inline styles in <style> tags and not use any <other-element style="..."> attributes which don't support nonce values AFAICT. That's why I said passing the nonce value to MathJax would work only in theory... I assumed it would require too many changes to be practical.
(DIR) Post #A84xdSJDvsRbvRGRaC by jix@mathstodon.xyz
2020-12-09T08:29:06Z
0 likes, 0 repeats
My paper where I prove the optimality of the smallest known sorting networks with 11 and 12 channels is out on arXiv: https://arxiv.org/abs/2012.04400Those were known since 1969, but whether smaller exist was an open problem since. 1/n
(DIR) Post #A84xdSnM7qXzQtMVY8 by jix@mathstodon.xyz
2020-12-09T08:31:26Z
0 likes, 0 repeats
This is also known as the Bose-Nelson Sorting Problem. For up to 7 channels, Floyd & Knuth determined the optimal sizes in 1966. In 1972 Van Voorhis published a result (which I'll mention again) that extends this to 8. Solving 9 and 10 took quite a bit longer... 2/n
(DIR) Post #A84xdTGQNlnct2xirI by jix@mathstodon.xyz
2020-12-09T08:31:26Z
0 likes, 0 repeats
In 2014 Codish, Cruz-Filipe, Frank & Schneider-Kamp used a new approach to compute the optimal size for 9 channels. This took over a week on a cluster. Van Voorhis's result, again, extends this to 10 channels. Later Cruz-Filipe & Schneider-Kamp formally verified this result. 3/n
(DIR) Post #A84xdThMlbLmEbZEqu by jix@mathstodon.xyz
2020-12-09T08:31:27Z
0 likes, 0 repeats
I'd been using sorting networks for encoding some problems for SAT solving. Last year I wondered whether I could find smaller ones. This lead me to the work of Codish et al. and I improved a subroutine that is the bottleneck in their approach: https://github.com/jix/sortnetopt-gnp 4/n
(DIR) Post #A84xdU7xAkcLZ40TIG by jix@mathstodon.xyz
2020-12-09T08:33:41Z
0 likes, 0 repeats
Frăsinaru and Răschip had already improved that subroutine, reducing the overall time to a few hours. My improvements got it down to under one hour. Scaling this up to 11 channels seemed impossible though. The memory requirements alone would be prohibitive. 5/n
(DIR) Post #A84xdUafRzaP07RP3A by jix@mathstodon.xyz
2020-12-09T08:33:42Z
0 likes, 0 repeats
I couldn't stop thinking about this: Van Voorhis's result is that s(n) ≥ s(n - 1) + ⌈log₂ n⌉ where s(n) is the optimal size for n channels. It happens to be strict for n = 8 and n = 10, even though the algorithm used to compute s(9) doesn't practically scale to s(10). 6/n
(DIR) Post #A84xdUz7z39UDyswAy by jix@mathstodon.xyz
2020-12-09T08:33:43Z
0 likes, 0 repeats
This lead me to believe that there is a structure that is exploited by Van Voorhis's bound that's completely unused by previous algorithms for computing s(n). After a lot of experiments I managed to generalize Van Voorhis's bound to what I call partial sorting networks. 7/n
(DIR) Post #A84xdVP0QpqtWEzbVo by jix@mathstodon.xyz
2020-12-09T08:36:02Z
0 likes, 0 repeats
These only have to sort a given subset of input sequences. Looking at a subset is not a new idea per se, but this definition allowed me to generalize Van Voorhis's bound and provided the basis for a new dynamic programming algorithm for computing s(n). 8/n
(DIR) Post #A84xdVrii4owxIQXGi by jix@mathstodon.xyz
2020-12-09T08:36:02Z
0 likes, 0 repeats
Since my generalization results in a bound that involves Huffman's algorithm I've been calling it the Huffman bound for partial sorting networks. Huffman's not only data compression ;) Using this in my dynamic programming algorithm then allowed me to compute s(9) in seconds! 9/n
(DIR) Post #A84xdWJN3GwGL3McMq by jix@mathstodon.xyz
2020-12-09T08:38:16Z
0 likes, 0 repeats
After some more optimization and fine tuning I was able to compute s(11) a bit over a year ago. Again, Van Voorhis's bound produced s(12) for free. I wasn't confident enough that my result is correct though, so I decided to also formally verify my result. 10/n
(DIR) Post #A84xdWn9GYl3pPIOmW by jix@mathstodon.xyz
2020-12-09T08:38:16Z
0 likes, 0 repeats
Formally verifying an optimized implementation of my algorithm seemed too hard, so like Cruz-Filipe & Schneider-Kamp I decided to instead have the algorithm produce a certificate and formally verify a checker for that. That's an approach I've also known from SAT solving. 11/n
(DIR) Post #A84xdXERd4anC44CKO by jix@mathstodon.xyz
2020-12-09T08:38:17Z
0 likes, 0 repeats
My initial attempts would have produced a certificate that is too large and slow to check with such a checker. Here I noticed that I could get a smaller certificate by reusing the routine of Codish et al. that I had previously optimized. 12/n
(DIR) Post #A84xdXh9uJYqd7V85I by jix@mathstodon.xyz
2020-12-09T08:40:36Z
0 likes, 0 repeats
This worked, but I still had to formally verify my certificate checker. For this I looked at several proof assistants and went with Isabelle/HOL. End of last year I then had a fully formally verified certificate checker and was certain that my result holds. 13/n
(DIR) Post #A84xdY9AEBxk1ybUjg by jix@mathstodon.xyz
2020-12-09T08:40:37Z
0 likes, 1 repeats
I pushed all my source code and formal proofs to GitHub (https://github.com/jix/sortnetopt), but hadn't written anything suitable for human consumption yet. Over the course of this year, with some breaks, I then wrote the paper with all the details, that I just put on arXiv. 14/n
(DIR) Post #A84xdYZOeewjLKsRcm by jix@mathstodon.xyz
2020-12-09T08:45:24Z
0 likes, 1 repeats
And since I forgot to include them with my first tweet, (https://twitter.com/jix_/status/1336588447902011393) here are some figures to look at :) 15/15
(DIR) Post #A85FoM8L22518HWIj2 by jix@mathstodon.xyz
2021-06-08T11:20:55Z
0 likes, 0 repeats
Does anyone know an efficiently implementable area-preserving homeomorphism between the n+1-cube boundary and the n-sphere? Not finding anything, and what I came up with, I don't know how to compute yet. Wouldn't be surprised if I just don't know the right keywords to find sth...
(DIR) Post #A85FoMZHPrdATq7oie by jix@mathstodon.xyz
2021-06-08T11:26:54Z
0 likes, 0 repeats
This would also give you one between the n-cube and the n-ball by mapping concentric cube boundaries to concentric spheres. I'm interested in this for low-discrepancy/quasirandom sequences on n-spheres and n-balls, which is also something where I'd have expected to find more...
(DIR) Post #A85FoN1diQJdtnOSvI by jix@mathstodon.xyz
2021-06-08T11:38:54Z
0 likes, 0 repeats
Ideally for that use case, the mapping should also approximately preserve distances locally, e.g. bounded by a constant factor (depending on n, I think there's no way around that).