An Explanation of Lengauer-Tarjan Dominators Algorithm May, 2023
This note explains the Lengauer-Tarjan dominators
algorithm given in "A Fast Algorithm for Finding Dominators in a
Flowgraph". The algorithm is ingenious; though relatively
simple to state, its underlying proofs are fairly involved. I have
tried to present the proofs in a more structured fashion in this note.
Proof of an ellipse-drawing program due to Doug
McIlroy March, 2023
Doug McIlroy has proposed a
program for drawing ellipses on a discrete raster plane, as on a
digital monitor that has pixels only at grid points, or a printed page
on which ink can be applied only at specific points. An ellipse is a
continuous curve that only rarely passes through grid points. So, only
an approximation to the ellipse can be drawn. McIlroy proposes
choosing those grid points that are near enough to certain points on
the ellipse. He establishes a number of properties of the chosen grid
points, and develops a sequence of programs through refinement.
The purpose of this note is develop an abstract version of his program
and a give a formal proof for it.
A cat, mouse puzzle. Jan. 18, 2023
There are a finite number of caves. A mouse spends a day in one of the
caves and moves to an adjacent cave next morning. A cat knows the
movement protocol of the mouse, but does not know its initial position
nor, of course, which non-deterministic choice it will make each
day. The cat can visit any one cave each day. Devise a strategy for
the cat to catch the mouse, i.e. ensure that eventually the cat and
mouse occupy the same cave. This is a nice example of sequential
program verification.
A proof of Hall's marriage theorem. Nov. 4, 2021
A proof of Fermat's little theorem. Sept. 5, 2021
Fermat's little theorem says that for any natural number n, n^p - n is a
multiple of p. Dijkstra in EWD740 gives a beautiful proof of this
result using elementary graph theory. The proof given here is based on
Dijkstra's constructions though it does not use graph theory.
A
theorem about the postorder numbers in the depth-first tree of a
directed graph. March 22, 2020
I present a
theorem that captures an important property of the postorder numbers
in a depth-first tree of a directed graph: any path in the graph
from a lower to a higher numbered node includes a node that is the
least-common ancestor in the depth-first tree of all nodes in the path. I apply this
theorem in the proof of Kosaraju's algorithm for identifying the
strongly-connected components.
A
fundamental theorem about minimum spanning
trees. May. 12, 2020
I present a theorem
that underlies all known algorithms for minimum spanning tree
construction.
Proof of an Abstract Algorithm for Graph Reachability. May. 7,
2019
We present an abstract non-deterministic algorithm
for identifying nodes of a directed graph that are reachable from
a specific node. The algorithm encompasses all known algorithms
for this problem, including breadth-first and depth-first
search. Its correctness, therefore, implies that all such
algorithms are correct.
A
Proof of a Heavy Hitters Algorithm. Feb. 7,
2018
This note is meant to teach program development and
formal proofs in an introductory computer science course. Given a
bag of items consider finding all items that occur more often than
a given fraction of the bag size. The first algorithm for this
problem, due to Misra and Gries, is used as the motivation for the
note.
First, I treat a special case, the Boyer-Moore Majority Protocol. I
start with its mathematical underpinning, then show a program with
abstract data structures, later a refinement by replacing the
abstract data structures by concrete representations. The heavy
hitters algorithm is a small generalization of the ideas
inherent in this algorithm.
Knuth-Morris-Pratt string matching algorithm. July 21, 2016
The Knuth-Morris-Pratt string matching algorithm locates all occurrences of a
pattern string in a text string in linear time. It is a refined version of a naive algorithm.
Dijkstra's
single-source shortest path algorithm. June 14, 2016
Dijkstra's single-source shortest path algorithm is explained in two
different ways, first as a discrete event simulation of a physical
system and next in a more conventional manner.
A covergence proof.
June 6, 2016
An undirected connected finite graph has a natural number initially
associated with each node. There is a distinguished node,
anchor. A non-anchor node may make a move by setting its value
to 1 + the minimum value over all its neighbors. The anchor node never
makes a move. Show that the computation eventually converges so that
no move changes any value.
Implementation of Queue with add, remove and max operations.
Oct. 08, 2014
It is required to maintain a queue that supports the traditional
"add-at-the-left" and "remove-from-the-right"
operations. Additionally, it should support a max operation that
returns the maximum value in the queue. The inclusion of max makes it
impossible to implement each operation in constant time in the worst
case. What is required is an implementation with constant amortized
running time.
Knaster-Tarski Theorem.
Sep 12, 2014, Revised Dec 16,2021
This note presents a proof of the famous Knaster-Tarski theorem. I have
opted for clarity over brevity in the proof.
Well-founded
orderings over multisets. June 09, 2014
This note gives an elementary proof of a result, due to Manna and
Dershowitz, on the well-foundedness of an order relation over
multisets.
A
Variation of Koenig's Lemma. Sept. 11, 2014
A variation of the famous infinite tree lemma that is useful in program semantics.
Guessing a Hat color out of N colors Sep. 14, 2012
The following problem was communicated to me by Mike Starbird. There
are N persons each of whom has a hat on his head. There are N
possible hat colors. Not every color appears on someone's head. Every
one can see the colors of all others' hats, but not his own. Each
person guesses the color of his hat (writing it down on a piece if
paper, say). Devise a protocol so that at least one person guesses his
hat color correctly.
Identifying
Lights with their Switches Sep. 07, 2012
Given is a set of switches and an equal number of lights where
each switch controls exactly one light and each light is
controlled by exactly one switch. The wiring diagram is
unavailable and the wiring itself is hidden. A step consists of
selecting some number of switches and turning them on, and,
presumably, noting the lights that come on as a result. It is
required to determine which switch controls which light using a
minimum number of steps.
Digital Cash Aug. 24, 2012
We propose a scheme for management of digital cash that mimics the
current physical management. In particular, any one can verify the
authenticity of a digital bill, no one can manufacture or double-spend
a bill, a transaction between two parties does not reveal the
identities of the parties to others, and the bills are maintained by a
distributed set of (trusted) servers that may belong to many financial
institutions, much like the banks of today. Additionally, failure of
any one client or server does not affect the rest of the system.
A Proof of the Infinite Ramsey Theorem July 31, 2012
Assigning
Coordinates to Events: Solving Combinatorial problems using Discrete
Event Simulation. (with David Kitchin and John
Thywissen) Nov. 1, 2011
This paper is inspired by the
"event list" mechanism in discrete event simulations. We argue that
descriptions of many combinatorial algorithms can be simplified by
casting the solution in terms of processing events according to some
order. We propose generalizations of the event list mechanism, and
show their applications in problems from graph theory and
computational geometry.
Processing
Boolean Equalities and Inequalities. Nov. 1, 2011
Given a set of boolean variables, and a set of equalities
and inequalities among those variables (called ``facts''), it is
required to determine the relationship, if any, among pairs of
variables (called ``queries''). We consider two versions of this
problems, one when the queries are given after all the facts have
been presented (off-line) and when the queries and facts are
intermingled (on-line). For the off-line version we give a linear
algorithm, and for the on-line version a quasi-linear one by
modifying the well known union-find algorithm.
Monty Hall game Aug. 10, 2011
Four short proofs for the famous Monty Hall game.
Chameleons Sept. 8, 2009, Revised 01/05/2014
There are 3 piles of chips. A step consists of removing one chip each
from two different piles and adding both chips to the third pile. The
game terminates (reaches a final state) when no more steps can be taken,
i.e., there are at least two empty piles. It is required to devise a
strategy to arrive at a terminating state, or prove that no such
strategy exists for the given initial state.
This puzzle first appeared in the Comm. of ACM in the form of
Chameleons of 3 different colors. I have made it less colorful by
converting it to piles of chips.
A puzzle from Peter Winkler July 19, 2006
A secret is a triple where each component
is a natural number below n, for some given n. A guess is a
triple of the same form. A guess has an outcome which is revealed to
the guesser: it succeeds if it matches at least two corresponding
components of the secret, and fails otherwise. What is the minimum
number of guesses required to succeed for n=8?
Unique
Prime Factorization Theorem. Feb 4, 2006, corrected
April 3, 2022
For
every positive integer there is a unique bag of primes whose product
equals that integer. The fact that there is a bag of primes
corresponding to every positive integer is readily proven using
induction. I prove the uniqueness part: distinct bags of primes have
distinct products.
(With
William Cook)
Some Facts about String Interleaving February 17, 2005
We prove commutativity, associativity and a distributivity property of
string interleaving.
Pairing Integers so that their sums are primes. January 31, 2005
For every even positive integer n, pair the
integers up to n so that the sum of each pair is prime.
A
Consensus Protocol in a Prison. February 2, 2004
A
set of prisoners --assume there are at least 2-- are asked to play
the following game by the warden. There is a room in the prison which
has two switches; initially, the switches are in arbitrary
positions. The warden will bring one prisoner at a time to the room,
and the prisoner must flip one of the switches. The prisoners do not
know the order in which they will be taken to the room, but they know
that every prisoner will visit the room over and over until the end of
the game. The game ends when some prisoner announces, ``every prisoner
has been in this room at least once''. If the announcement is
correct, all prisoners go free; if incorrect, they all are
executed. The game continues until the announcement is made.
The prisoners are allowed to confer and decide on a protocol prior to the start of the game. Once the game starts, they are not allowed to communicate, nor can they find out who is being taken to the room. The problem is to devise a protocol for the prisoners.
A Note on EWD 1312
Sep 14, 2001
Integers h and k are disjoint provided in their
binary representations no position has 1s in both h and k. (In
comparing two integers, append leading zeroes to the binary
representation of the smaller number to make their lengths identical.)
Dijkstra proved that for positive h and k, among (h, k), (h, k-1), and
(h-1, k), an even number of pairs are disjoint. In this note we prove
this result using some elementary algebraic properties of
disjointness.
Tree
Isomorphism: An Exercise in Functional Programming
Sep 10, 2001
The problem is to decide if two unordered trees are the
same.
Parities of Binomial Coefficients
May 16, 2001
We give a formula for the parity of any binomial coefficient.
A
Problem due to J Moore. Mar 28, 2001
The following problem was
posed by J Moore during the faculty lunch today. Let there be two
machines with two registers each, which can read/write a shared
counter. Initially the counter holds the value 1 and all registers are
empty. There are two atomic actions:
Computing
Spans. Jan 22, 2001
Given is a sequence of integers. For
any element, e, of the sequence, define its "span" to be the length of
the longest segment ending at e where each element of the segment is
at most e in value. This note contains development of a linear
algorithm for computing all the spans.
Enumerating
the Strings of a Regular Expression. Aug 29, 2000
We develop
an algorithm to enumerate the strings of a regular expression in
increasing order.
Locating
the Center of a Set of Points on a Curve. June 15, 2000
Given are a finite number of points on a simple closed
curve; call these points
anchors. It is required to find a point, called the
center, so that the sum of distances between the center and the
anchors is the minimum over all points.
A
proof by Erdos. Oct 1, 1999
A sequence of numbers whose
length exceeds n2 contains either an ascending or a
descending subsequence longer than n.
Permutations
Generated by a Stack Machine. Sep 28, 1999
An output
string is computed as follows from an input string using an infinite
stack. In each step either the next input symbol is added to the
stack, or the top of the stack is moved to the output. We characterize
the outputs for a given input.
Russell
Paradox, Cantor Diagonalization. Sep 28, 1999
Formal Proofs
are simpler than their informal counterparts, for Russell Paradox and
Cantor's Diagonalization argument.
A
property of Identity Function: An Exercise in Induction.
Sep 16, 1999
Let f be a function from naturals to
naturals. It is given that for all n, f2(n) <
f(n+1). Prove that f is the identity function. We will
actually prove a generalization of this result.
Minimum
Spanning Tree. Dec 12, 1998
This note develops two
well-known algorithms for finding the minimum spanning tree.
Rules
for Division by 3 and 11. Dec 2, 1998
Show that for any natural number n, n mod 3 = r.n mod 3, where r.n is
the sum of decimal digits in n. The rule for division by 11 is to start from the lowest digit of the number, and add and subtract the digits alternately.
The
Muddy Children Puzzle Oct 8, 1998
There is a finite group of children where each child is clean or
dirty. No child knows if it is clean or dirty, but it can see if
every other child is clean or dirty. It is common knowledge that there
is at least one dirty child.
In a round, (1) the children are asked: do you know if you are
dirty, and (2) each of them responds with ``NO'', ``YES, I am dirty'',
or ``YES, I am clean''. Responses are heard by all children. Rounds
are repeated ad infinitum starting at round 0.
Prove that a child who sees n dirty children, n \ge 0, will answer
YES in round n, but no earlier.
Arithmetic Mean is greater than or equal to Geometric Mean Sept. 23,
1998
A simple proof of: the arithmetic mean of a finite non-empty bag of positive real numbers
is greater than or equal to its geometric mean.
A Proof about the Harmonic Series.
Aug 13, 1998
The following problem and its solution was shown to me by Carroll
Morgan.
Knowledge, Product and Sum
Jan 30, 1998
There are two parties, Product and Sum, who are given
numbers p and s, respectively, where p = m x n and s = m+n, for some unknown
integers m and n, each between 2 and 100. The parties deduce the
values of m and n after a certain exchange. This note
explains a solution due to Dijkstra (EWD-666).
Common
Meeting Time Dec 5, 1997
We develop the appropriate conditions on the functions which are
used in the common meeting time problem.
Making
Multiple Copies under possibility of Failure April 4, 1997
It is required to copy a file N times; call each
copy a clone of the original. The file consists of a sequence of
symbols each of which is independently copied. Therefore, we consider
the problem when the file consists of a single symbol.
There
are Infinitely Many Primes Mar 21, 1997
The following proof of the classical theorem is due to Dijkstra.
Coloring
Grid Points, without Rabbits and Snakes Dec 18, 1996
For any finite set of grid points in the plane, we can
colour each of the points either red or blue such that on each grid
line the number of red points differs by at most 1 from the number of
blue points.
A
Useful Recurrence for Division June 20, 1996
We show a recurrence that is useful for division.
Reducing
Satisfiability to Quadratic Programming May 15, 1996
We show that the boolean satisfiability problem can be reduced to the
quadratic programming problem.
A puzzle on infinite sequences: An application of Koenig's Lemma April 12, 1996
Define a word to be any non-empty finite
sequence of symbols. Each word is either good or
bad. Given an infinite sequence of symbols, show that beyond some
point, the sequence can be broken into words that are all good or that
are all bad.
A puzzle on Termination April 9, 1996
Given is a 10 X 10 square grid. A cell is a square in the
grid. Two cells are neighbors if they share a side. Initially 9 cells
are chosen and colored red. Next, any cell may be colored red provided
it has two red neighbors. Prove or disprove that the entire region can
be colored red.
A
Counting Problem Communicated by Dijkstra April 9, 1996
Given that there are 25 boys and 25 girls. A
party has 12 tables, each of which seats 2 boys and 2
girls. Thus, a party is attended by 24 boys and 24 girls. A boy
sees 2 girls at his table in a party, and so do the girls. A set of
parties, P, is feasible if each boy/girl sees different
girls/boys in different parties in P. What is the size of the
largest feasible set?
Random Number Generation without Repetition Mar 27, 1996
We are given a function from naturals to
naturals, which is applied repeatedly starting at a fixed seed. Floyd
has shown how repetitions can be detected in this sequence. We give a
proof of this result.
Sorting The Rows of a Matrix Preserves the Sorted Columns Feb 19, 1996
Given is a matrix whose columns are sorted. Show
that if each row is sorted individually then the columns remain
sorted.
On
the union of well-founded relations: An application of Koenig's
Lemma Feb 16, 1996
We are given two well-founded relations
on the same set, and that their union is transitive. We show that the
union is
well-founded.