1010 A much neglected mathematical object*.
Austin, 30 August. 1987. 3 pages.
EWD starts with Leibniz' rule of replacing a term by an equal term without changing the value of the whole expression. He notes the formal similarity with the definition of the equality of two functions, and introduces the "identity argument" (in analogy to the "identity function") with the property that f.i = f for all functions f. The resulting theory admits only a very trivial and uninteresting model (with only one object). This is attributed to Samson Abramsky.
*namely: the "identity argument"
—GR
1014 A monotonicity argument revisited
Austin, 22 October. 1987. 3 pages.
Deriving the formula for the length of a bisector of a triangle using monotonicity.
—ST
1015 On a problem transmitted by Doug McIlroy.
Austin, 21 November 1987. 6 pages.
A proof of the following theorem:
If a big rectangle is tiled into small rectangles, and every small rectangle has an integral side, then the big rectangle has an integral side.
Some thoughts about how the proof is derived, and how it follows quite naturally once the proper setup has been found, and why the appearance of complex numbers is then no longer a surprise. (see however EWD1025)
A postscript explains why there have been few EWD's in the past semester.
—GR
1023 On triangles being nondegenerate.
Austin, 13 June 1988. 5 pages.
A purely arithmetic proof (by manipulating expressions in the coordinates) that two criteria for degeneracy of a triangle are equivalent:
—GR
1025 Ulrich Berger's solution to the rectangle problem.
Nuenen, 12 August 1988. 2 pages.
Another charming proof of the following theorem: (see EWD1015)
If a big rectangle is tiled into small rectangles, and every small rectangle has an integral side, then the big rectangle has an integral side.
—GR
1027 My methodological blunder with grid polygons.
Nuenen, 23 August 1988. 3 pages.
Proves that a grid triangle (lattice triangle) with no grid point on the sides and exactly one interior grid point has this point as its center of gravity. On the way, he proves that all grid triangle with no interior grid points and no grid point on the sides have area 1/2 (acknowledges Wolfgang Hinderer, from Karlsruhe, for some part of the argument).
—GR
1028 Euclid, Netty*, and the prime numbers.
Austin, 19 September 1988. 5 pages.
Revisits Euclid's proof that there are infinitely many primes.
* Netty = Annette van Gasteren
—GR
1032 Decomposing an integer as sum of two squares.
Austin, 13 October 1988. 7 pages.
Derives a program for printing all pairs u,v with u2+v2=N.
(which had been a homework exercise)
Some historical thoughts about a previous (not so elegant) solution in A Discipline of Programming and about loops with more than one guarded command.
—GR
1035 On long-range planning for the CS department
Austin, 7 November 1988. 12 pages. transcription.
This is a letter written to his CS Department at the University of Texas.
Starts with discussing the future of CS as an intellectual discipline and a radical novelty. Mentions that computers can only manipulate symbols, and that programs are also created by manipulating symbols; discusses this interplay. Suggests the discipline as a whole will someday transcend formal mathematics and applied logic, and provide symbol manipulation as an alternative to human reasoning. Discusses the sources of opposition to this vision, as well as the sources of inspiration for the vision.
Continues with discussing the future of the CS department, the Amdahl strategy, and recommends that the department should differentiate themselves from the competition. The department should adopt an anti-clone strategy and teach what is both necessary and unpopular. Specific topic recommended is “the effective, large-scale application of formal methods” ( = VLSAL).
—JDA
1041 By way of introduction.
Austin, 12 February 1989. 15 pages. transcription.
This is apparently a manuscript for a speech.
A plea for the science of developing correct programs. Views programming as VLSAL ( = Very Large-Scale Application of Logic). Compares current situation to "pre-scientific" history of science, alchemy, astrology, etc. Reports about various experiences with audiences when teaching courses on programming.
—GR
1041a Factorizing the factorial.
undated, 1 page.
Proves a formula about the exponent of a prime p in the prime facturization of n!, by induction on n.
A proof of this appeared already in the article "Some beautiful arguments using mathematical induction" Algorithmica, vol. 13 (1980), pp. 1-8 (EWD697). The present proof uses slightly different notation: It makes the dependence on the induction variable n implicit and uses the Delta operator to express the difference between the situation for n and n+1, which makes the whole proof more concise.
—GR
1044 To hell with ``meaningful identifiers''!
Austin, 17 February 1989. 5 pages. transcription.
About the problem of maximizing a product of integers when their sum is given, and about the fallacy resulting from using a term ("disposable", in this case), whose meaning is "clear", without properly defining it.
—GR
1049 A somewhat open letter to Uri Leron
Austin, 12 April 1989, 5 pages.
Proves that two sets of n points in the plane in general position always have is a non-crossing matching. The proof is algorithmic, and is derived step by step, in the spirit of a related proof of Sylvester's theorem (EWD1016), and in contrast to the "usual" proof that starts with the minimum-length matching.
—GR
1063 An introductory example (Mathematical Methodology).
Austin, 12 October 1989. 12 pages.
(This is apparently an introductory chapter to a book manuscript on Mathematical Methodology.)
After introducing the notation and general notions and principles, about half of the manuscript is devoted to the detailed proof of the following theorem:
- (f.x <= y) = (x <= g.y) for all x,y;
—GR
1070 For brevity's sake.
Austin, 15 November 1989. 12 pages. transcription.
(This is apparently a chapter of a book manuscript on
Mathematical Methodology.)
At the beginning, compares two ways to present Russell's paradox. The introduction of Boolean values as "first-class citizens" by George Boole in 1858.
the slow pace at which this invention is accepted: logical expressions but no logical variables in the original FORTRAN language; programmers still write "if h==true" and similar superfluous expressions.
Among other things, introduces a nice logical riddle about two vases with a treasure, attributed to Roland C. Backhouse. The solution (by G. Wiltink) illustrates the power of using "equivalence" as a logical connective, which can be manipulated by the laws of propositional logic just like other connectives, in particular by the associative law, as opposed to just treating it as an equivalence relation.
—GR