By the way, I like the space-time variant of the standard proof that van Emde Boas gives in https://people.irisa.fr/Francois.Schwarzentruber/sif2_thx/articles/tiling.pdf. "Basing the proof on the space-time diagram, uniqueness of the head position is a direct consequence of local consistency throughout the diagram and does not have to be enforced explicitly."
=> More informations about this toot | View the thread
(If the tape head starts in a fixed initial position then within time T you can only access tape cells within distance T of that initial position, so there's no need to encode instances of the transition relation corresponding to machine states beyond the "light cone" emanating from the initial position.)
=> More informations about this toot | View the thread
To do the first step (encode the transition relation in propositional logic) you need to unroll in space, not just in time. In the case of Cook-Levin that relies on the usual argument that TIME(f(n)) is a subset of SPACE(f(n)) since the Turing machine's tape head starts in a fixed position, so the nondeterminism is only for the transitions. In model checking I think they usually allow an arbitrary initial-state predicate, so I guess for BMC you'd have to constrain that as well.
=> More informations about this toot | View the thread
I hadn't really thought about it in those terms, but the implementation of bounded model checking is very similar to the proof of the Cook-Levin theorem. You encode the nondeterministic transition relation of your model of computation as a formula in propositional logic, unroll it to some fixed depth (given by the polynomial-time bound in the case of Cook-Levin), and check for satisfiability of the unrolled transition relation formulas and an auxiliary formula.
=> More informations about this toot | View the thread
I wonder if having a last name with an initial letter near the start of the alphabet correlates more highly with academic success because of people assuming the author list of a paper was ordered by contribution (e.g. student first, professor last) in cases where it was ordered alphabetically.
=> More informations about this toot | View the thread
He also has a TAOCP pre-fascicle on components: https://www-cs-faculty.stanford.edu/~knuth/fasc12a+.pdf
=> More informations about this toot | View the thread
Knuth's Christmas lecture from this year is up on YouTube now: Strong and Weak Components. https://www.youtube.com/watch?v=Hi8r_63LGyg
=> More informations about this toot | View the thread
@zwarich I'd been loosely aware of F* by name only but finally got around to reading the main paper and it's very interesting. Have you looked at it at all? https://fstar-lang.org/papers/mumon/
=> More informations about this toot | View the thread
When I grew up in the 80s and early 90s, the Danish stereotype about Germans is that they had mullets. I wonder how many mullet-related national stereotypes exist nowadays. I was reminded of this because I just heard that Brazilians apparently say this about Argentinians.
=> More informations about this toot | View the thread
I finally got around to playing (and finishing) Phantom Liberty and even though it can't compete with Blood & Wine in being a perfect conclusion to a trilogy, Phantom Liberty might be the best thing CDPR has made (modulo recency bias). Crossing my fingers for their sake they don't get sucked into development hell again on the Cyberpunk sequel now that they've switched engine and rebuilt the team in the US.
=> More informations about this toot | View the thread
Asterix visits Feedback Hub: https://www.youtube.com/watch?v=4StpMBjMmlY
=> More informations about this toot | View the thread
On reporting Windows API bugs to Microsoft: "We're supposed to direct you to Feedback Hub, but you may as well transmit your message into deep space."
=> More informations about this toot | View the thread
Since I have so much muscle memory in browsers for ctrl-shift-t (reopen/unclose tab), I've started pressing it accidentally in other apps and found out others support it now too, e.g. KDE's Okular document viewer.
=> More informations about this toot | View the thread
Unfortunately even Rust can violate parametricity due to the (very limited) use of specialization in the standard library implementation to optimize certain cases. It would be nice if specialization was only allowed when you have an Any-like bound on the type parameter, which should retain parametricity. The downside is that you can't add specialization after the fact without changing the API. You could maybe salvage that by making it a default bound with an opt-out like Sized vs ?Sized.
=> More informations about this toot | View the thread
A nice example of parametricity is that a function signature like fn sort<T: Ord>(slice: &mut [T]) must be a permutation since you can't make new T values (without invoking UB). So a seemingly weak postcondition like is_sorted(slice) is actually a sufficient specification, assuming parametricity. Similarly, even if you're returning a new sequence, e.g. fn sort<T: Ord>(slice: &[T]) -> Vec, you'd only need to add result.len() == slice.len() to the postcondition.
=> More informations about this toot | View the thread
Before all the usual pundits start valorizing Carter as a saint: https://www.counterpunch.org/2015/08/18/jimmy-carters-blood-drenched-legacy/, https://www.counterpunch.org/2016/01/11/jimmy-carters-blood-drenched-legacy-2/. I assume most of this stuff is relatively common knowledge but people have short memories.
=> More informations about this toot | View the thread
Revisiting some material on model checking has made me realize that a lot of people (including myself) can be pretty sloppy when they call something a liveness property. In particular, deadlock freedom is definitely not a liveness property. It's a safety property but even more than that it's "just" an invariant property of a single system state. That's the very thing that makes deadlocks easy to dynamically detect (cycles in the waits-on graph).
=> More informations about this toot | View the thread
It would be nice if the "hold the back button to show the history" dropdown in browsers would collapse ranges of anchor links for the same page. When you have a slide deck or some other thing where you end up with a history of a hundred anchor links to the same page by the end of it, you're kind of screwed.
=> More informations about this toot | View the thread
I think this would mostly help in formal verification if you're relying on model checking of data-type invariants or something like that. If you're doing deductive verification with a proof assistant I don't think it would make really help (or hurt) the proof if your data structure carries an inverse witness as opposed to an injectivity/surjectivity property.
=> More informations about this toot | View the thread
I was idly thinking about verification for mutation-based linked structures. A nice thing about bidirectional/doubly-linked structures is that you have an inverse function to work with as opposed to merely an injectivity and surjectivity property, so you don't need a Cantor-Schröder-Bernstein-like argument to pass between the two. More prosaically this also lets you catch functional correctness/memory corruption bugs by checking local invariants like next[prev[x]] = x and prev[next[x]] = x.
=> More informations about this toot | View the thread
=> This profile with reblog | Go to pervognsen@mastodon.social account This content has been proxied by September (ba2dc).Proxy Information
text/gemini