"Strong typing vs. strong testing" [OT]

[Mark Wooding]

Steven D'Aprano <steve-REMOVE-THIS at cybersource.com.au> writes:

> Well, what is the definition of pi? Is it:
>
> the ratio of the circumference of a circle to twice its radius;
> the ratio of the area of a circle to the square of its radius;
> 4*arctan(1);
> the complex logarithm of -1 divided by the negative of the complex square 
> root of -1; 
> any one of many, many other formulae.
>
> None of these formulae are intuitively correct; the formula C = 2πr isn't 
> a definition in the same sense that 1+1=2 defines 2. The point that I was 
> trying to get across is that, until somebody proved the formula, it 
> wasn't clear that the ratio was constant.

There are several possible definitions of `2'.  You've given a common
one (presumably in terms of a purely algebraic definition of the
integers as being the smallest nontrivial ring with characteristic 0).
Another can be given in terms of Peano arithmetic, possibly using an
encoding of Peano arithmetic using only the Zermelo-- Fraenkel axioms of
set theory: at this point one has only a `successor' operation and must
define addition; the obvious definition of 1 and 2 are s(0) and s(s(0))
respectively, and one then has an obligation to prove that s(0) + s(0) =
s(s(0)), though this isn't very hard.

I think my preferred definition of `pi' goes like this (following Lang's
/Analysis I/).  Suppose that there exist real functions s and c, such
that s' = c and c' = -s, with s(0) = 0 and c(0) = 1.  One can prove that
a pair of such functions is unique, and periodic.  Define pi to be half
the (common) period of these functions.  (Now we notice that they factor
through the quotient ring R/(2 pi) and define `sin' and `cos' to be the
induced functions on the quotient ring.)

Would the world be a better place if we had a name for 2 pi rather than
pi itself?

-- [mdw]