Edsger W. Dijkstra on Reasoning about Processes
To see why this video is well worth watching and listening to carefully, consider the following question.
Imagine a process which, given a list containing a number of tasks, each of which is one of two different types, call them odd or even, chooses two at random, and if they both turn out to be the same type, adds an even task to the list, otherwise it adds an odd task to the list. This process then repeats until there are fewer than two tasks on the list, at which point it returns the list of the remaining tasks as its result. How many tasks will this process produce as a result?
At 42 minutes 20 seconds on functions of a permutation, see How to Be A Genius Part II. And on the application of these ideas to determinants and solving systems of linear equations, see Charles Lutwidge Dodgson's book An Elementary Treatise on Determinants: With Their Application to Simultaneous Linear Equations.
See this for how to construct bijections on partial orders.
At 51 minutes 20 seconds, on the animistic connotations of the term "bug" ... do you often hear people at, say Google or Microsoft, saying "Another bug got into my program! We need to fumigate this fucking building, ... it's full of bugs!" ...
Now see Ben Eater on Running a Breadboard at 1MHz and watch this lecture:
Then see Patrick Cousot & Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.
This paper: Systematic design of program analysis frameworks gives a more general algorithm for lattice completion using a Galois Connection as a fixpoint operator, but the paper is not available from the link on the author's web page. This reference is from A Standard Basis for Standard Bases.
Laura Pausini on Galois Connections:
Imagine a process which, given a list containing a number of tasks, each of which is one of two different types, call them odd or even, chooses two at random, and if they both turn out to be the same type, adds an even task to the list, otherwise it adds an odd task to the list. This process then repeats until there are fewer than two tasks on the list, at which point it returns the list of the remaining tasks as its result. How many tasks will this process produce as a result?
At 42 minutes 20 seconds on functions of a permutation, see How to Be A Genius Part II. And on the application of these ideas to determinants and solving systems of linear equations, see Charles Lutwidge Dodgson's book An Elementary Treatise on Determinants: With Their Application to Simultaneous Linear Equations.
See this for how to construct bijections on partial orders.
At 51 minutes 20 seconds, on the animistic connotations of the term "bug" ... do you often hear people at, say Google or Microsoft, saying "Another bug got into my program! We need to fumigate this fucking building, ... it's full of bugs!" ...
Now see Ben Eater on Running a Breadboard at 1MHz and watch this lecture:
Then see Patrick Cousot & Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.
This paper: Systematic design of program analysis frameworks gives a more general algorithm for lattice completion using a Galois Connection as a fixpoint operator, but the paper is not available from the link on the author's web page. This reference is from A Standard Basis for Standard Bases.
Laura Pausini on Galois Connections:
Comments
Post a Comment