19 ms·
My advice: swing wide. If you don't know where to start, then judge a book by its cover and read it until you hit a knowledge gap, then slither down that gap an
by cybernautique 5y ago
My advice: swing wide. If you don't know where to start, then judge a book by its cover and read it until you hit a knowledge gap, then slither down that gap and keep digging for resources until you either get bored or achieve something.
I recommend starting with geometric algebra or topology. The aspiring selfstarter has a bevy of great options. Sidney A. Morris' "Topology Without Tears" is fine androgogy, as is the widely-acclaimed undergrad textbook "Intro to Topology: Pure and Applied" by Colin Adams.
The biggest thing, in my opinion, is to realize that there are precious few things you need permission to think, mathematically.
The fundamental mathematical advantage is abstraction. If you can manage your abstractions and approach the math as nothing more than especially pedantic philosophy- it helps.
- jhanschoo 5y agoI'm sorry, how is geometric algebra and basic topology even relevant to formal verification? Your suggestions sound more related to your own interests. The commenter is better served browsing through some introductory formal verification material like Concrete Semantics by one of the same authors as the linked document.
- namibj 5y agoNot sure about geometric algebra, but topology comes up because it studies the abstract formal structure that connects your problem with other (possibly solved) problems. For example, a couple weeks ago I was musing about optimal vertex renumberings so that "the (0/1) adjacency matrix of a non-densely-connected acyclic digraph's transitive closure" scores well according to a domain-specific compressibility metric. Specifically, at column i and row j is a 1 if and only if (using the post-remumbering indices) vertex i was reachable from vertex j in the original input graph. The compression results from only storing start and end indices of contiguous runs of 1s in a row. [Edit2: the score of a specific vertex renumbering is the the number of such runs for the complete matrix. Only uninterrupted runs of 1's count.] It is easy to see that a renumbering that results in a triangular matrix won't be terrible, and simple deepest-branch-first depth-first enumeration of the input DAG's undirected "version" (one just ignores edge direction for this step) is at least fairly good for sub-quadratic in vertex count (assuming an average degree much smaller than the number of vertices). [Edit1: I forgot to point out that this is extremely close to plain run-length-encoding of the matrix in row-major order, except for the fact that RLE cares about a row-crossing run and I don't.] But exhaustive renumbering testing is O(n!) for n vertices. I think topology could help me, but I'd need to know some topology to find me way around the literature.
- jhanschoo 5y agoI think combinatorics might be more relevant here. I'll note that I mentioned basic topology in my reply, because topology does indeed have deep connections with type theory that most formal verification systems are based on, interpreting types / theorems are spaces, terms / programs / proofs are continuous functions within them.[1] But basic undergrad topology typically studies more well-behaved (read: more like the real number line) spaces than this. [1]: https://www.andrew.cmu.edu/user/avigad/Talks/fields_hott.pdf https://www.andrew.cmu.edu/user/avigad/Talks/fields_hott.pdf
- cybernautique 5y agoSorry, you're correct, and I should have made it clearer. This is general advice for getting into math, which is what I took the parent to be seeking advice for.
- mbrodersen 5y agoThis is really bad advise. Geometric Algebra and Topology has nothing to do with proving algorithms correct. Better advise would be to learn Agda and read examples of,proving things in Agda.