Plane Affine Algebra (I)

See also Part II and Part III.

The algebra's objects are the set of points P on the plane, together with the associated Euclidean space V (that is, a vector space together with an inner product and the usual Euclidean metric), where directed line segments between points in P are identified with free vectors (in other words, V = P/∗, for ∗ ∈ P distinguished). In what follows, I denote points by P, Q, R, vectors by u, v, w and scalars by k, l, m. Functional application (of which subscription is but a special case) is denoted by a dot, it is left-associative, and it is given the highest binding power. Labeled formulas are implicitly universally quantified over their free variables, whose type is usually understood if not declared beforehand.

The point constructor:

• → •: P → V → P

and the vector constructor:

‹• − •›: P → P → V

are the only operations on points. They are related by the following axioms:

(0)  P → 0 = P
(1)  P → ‹Q − P› = Q
(2)  ‹(P → u) − Q› = ‹P − Q› + u
(3)  P → (u + v) = P → u → v

By (0) the null vector is the identity translation. By (1), the tail of an anchored vector translated by itself is its head. (2) is the parallellogram rule for adding vectors. (3) is the associative rule for vector addition.

From these, it follows as theorems that:

(4)  ⟨∑ i : 0 ≤ i < N : ‹P.((i+1) mod N) − P.i›⟩ = 0
(5)  ‹Q − P› = −‹P − Q›
(6)  ‹P − P› = 0
(7)  P → ‹Q − Q› = P
(8)  P → u → v = P → v → u
(9)  ‹(P → u) − (Q → v)› = ‹P − Q› + u − v

Formula (4), the chain rule means simply that following along a closed polygonal line returns to the starting point. By (5), segments, when considered as vectors, are oriented; and by (8) vector addition is commutative.

Proofs: (4) follows from proving:

P.0 → ⟨∑ i : 0 ≤ i < N : ‹P.((i+1) mod N) − P.i›⟩ = P.0

by induction on N with base case (0) and inductive step using (3) and (1). (5) follows from (4) with N = 2; then (6) follows from (5) by setting Q := P.

(7) follows from (6) and (0); (8) follows directly from (3); and (9) follows from (5) and (2), both twice.

The algebra is also equipped with a unary postfix operator, the perp:

•⊥: V → V

satisfying the following axioms:

(10)  (u + v)⊥ = u⊥ + v⊥
(11)  (k·v)⊥ = k·(v⊥)
(12)  u⊥⋅v = −(v⊥⋅u)
(13)  |u⊥| = |u|

From the axioms, these theorems follow:

(14)  u⊥⋅u = 0
(15)  u⊥⊥ = −u
(16)  u⊥⋅v = |u|·|v|·sin.(θ.u.v)

where -π < θ.u.v ≤ π is the CCW angle from u to v.

By (10) and (11), perp is a linear operator; by (12) it is hemi-Hermitian, and by (13) it is magnitude-preserving. From (14), u^⊥ is perpendicular to u (hence the name). There are then only two possibilities for u^⊥; the definition of θ fixes it by convention as the CCW one.

Proofs: (14) follows from (12) by setting v := u. (15) follows from (14) by setting u := u^⊥ and noting that u^⊥⊥ ≠ u. To prove (16), we note that:

   u⊥⋅v
= { inner product }
   |u⊥|·|v|·cos.(θ.u⊥.v)
= { (13) }
    |u|·|v|·cos.(θ.u⊥.v)
= { (14) }
   |u|·|v|·cos.(π/2 − θ.u.v)
= { trigonometry }
   |u|·|v|·sin.(θ.u.v)

These operations form a kind of typed domain-specific language (DSL) for doing simple plane geometry. The fact that the operators are typed greatly constrains the allowed expressions, paradoxically making proofs by uninterpreted formula manipulation much easier.

References

1. F. S. Hill, Jr. The Pleasures of Perp Dot Products. In Paul S. Heckbert ed. Graphics Gems IV