Taking conjuncts as invariant 0

Our derivation of Euclid's algorithm was pretty involved. Let's spend some time practicing some simpler derivations.

Continued

Euclid, via Knuth

The very first algorithm we encounter in The Art of Computer Programming is Euclid's formula for the greatest common divisor. Euclid's algorithm is actually a family of algorithms, one of which Knuth describes below.

Algorithm E ( Euclid's algorithm). Given two positive integers m and n,
find their greatest common divisor, that is, the largest positive integer that
evenly divides both m and n.

E1 [Find remainder.] Divide m by n and let r be the remainder.
(We will have 0 ≤ r < n)
E2 [Is it zero?] If r=0, the algorithm terminates: n is the answer.
E3 [Reduce.] Set m← n, n&larr r, and go back to step E1.


Knuth's presentation is somewhat unfortunate, as it begs the question - where did it come from? In his preface to volume one Knuth writes `... I am not trying to teach the reader how to use somebody else's software. I am concerned rather with teaching people how to write better software themselves.'
In that spirit, let us see how we might produce this algorithm ourselves.

Continued

An open note to Craig Laughton

Dear Craig,

In your journal entry dated 11/12/04 you express discomfort with the operator ≥. I'm not sure how you feel about it now, but just in case you're still unsure about it I thought I'd write this little note.

I think the first thing getting you into trouble is your pronunciation. ≥ is best pronounced 'at least'. The problem with `greater than or equal to' is that it leaves one with the mistaken impression that ≥ is a special case of > (as the commenter on your entry demonstrates). In fact it is better the other way round. We define > in terms of ≥ i.e.

x > y   ≡   x ≥ y  ∧  ¬(y ≥ x)

≥, of course has a counterpart, ≤, pronounced `at most' and you can find a nice little note about it here.

One property of ≥ is that it is reflexive i.e. x ≥ x for all x. Thus expressions like 14≥14 and 9≥9 are perfectly fine.

Regards,


Eric M.

The Σ calculus Part 4

Let us conclude (for now) our exploration of the Σ calculus by introducing
one new postulate and one more theorem.

Continued

The Σ calculus Part 3

Associativity and symmetry reveal themselves again in another postulate
- referred to by `interchange of quantifications'.

Continued

The Σ calculus Part 2

Formulae (3) and (4) relate quantifications with the same range. (4) has an analogue for different ranges.

Continued

The Σ calculus Part 1

In analogy to addition's symmetry and associativity, we postulate that summation distributes over addition.

Continued