Plane Affine Algebra (III)

See also Part I and Part II.

Finally, a theorem, in the style of the Elements:

To trisect a segment. Let the endpoints of the segment be P, Q. Let R be any point not on PQ. Let M be the midpoint of PR, N be the midpoint of QR, O the midpoint of PQ. Then let S be the midpoint of MO, and T be the midpoint of NO. Produce the line RS to PQ in X; similarly, produce the line RT to PQ in Y. Then PX, XY, YZ are equal to one-third of PQ.

Proof: We begin by calculating S and T:

   S
= { definition with M, O := ray.P.R.½, ray.P.Q.½ }
   ray.(ray.P.R.½).(ray.P.Q.½).½
= { (18), twice }
   ray.(P → ½·‹R−P›).(P → ½·‹Q−P›).½
= { (18) }
   P → ½·‹R−P› → ½·‹(P → ½·‹Q−P›)−(P → ½·‹R−P›)›
= { (3); linearity }
   P → ½·(‹R−P› + ‹(P → ½·‹Q−P›)−(P → ½·‹R−P›)›)
= { (9) }
   P → ½·(‹R−P› + ‹P−P› + ½·‹Q−P› − ½·‹R−P›)
= { (6); linearity }
   P → ¼·(‹R−P› + ‹Q−P›)

From considerations of symmetry, T = S[P, Q := Q, P]. We have:

(21)  S = P → ¼·(‹R−P› + ‹Q−P›)
(22)  T = Q → ¼·(‹R−Q› + ‹P−Q›)

Finally, we calculate X and Y:

 X
= { definition }
 meet.P.Q.R.S
= { (20); (18) }
 P → (‹S−R›⊥⋅‹R−P›)/(‹S−R›⊥⋅‹Q−P›)·‹Q−P›
= { (21) }
 P → (‹(P → ¼·(‹R−P› + ‹Q−P›))−R›⊥⋅‹R−P›)/(‹(P → ¼·(‹R−P› + ‹Q−P›))−R›⊥⋅‹Q−P›)·‹Q−P›
= { (2), twice }
 P → ((‹P−R› + ¼·(‹R−P› + ‹Q−P›))⊥⋅‹R−P›)/((‹P−R› + ¼·(‹R−P› + ‹Q−P›))⊥⋅‹Q−P›)·‹Q−P›
= { (5), twice; linearity throughout }
 P → ((¼·‹Q−P› − ¾·‹R−P›)⊥⋅‹R−P›)/((¼·‹Q−P› − ¾·‹R−P›)⊥⋅‹Q−P›)·‹Q−P›
= { (10) and (11), twice }
 P → ((¼·‹Q−P›⊥ − ¾·‹R−P›⊥)⋅‹R−P›)/((¼·‹Q−P›⊥ − ¾·‹R−P›⊥)⋅‹Q−P›)·‹Q−P›
= { linearity of inner product, twice }
 P → (¼·‹Q−P›⊥⋅‹R−P› − ¾·‹R−P›⊥⋅‹R−P›)/(¼·‹Q−P›⊥·‹Q−P› − ¾·‹R−P›⊥⋅‹Q−P›)·‹Q−P›
= { (14), twice }
 P → (¼·‹Q−P›⊥⋅‹R−P›)/(−¾·‹R−P›⊥⋅‹Q−P›)·‹Q−P›
= { (12) }
 P → (¼·‹Q−P›⊥⋅‹R−P›)/(¾·‹Q−P›⊥⋅‹R−P›)·‹Q−P›
= { algebra }
 P → ⅓·‹Q−P›

To finalize, from considerations of symmetry, Y = meet.Q.P.R.T = (meet.P.Q.R.S)[P, Q := Q, P]. Hence:

(23)  X = P → ⅓·‹Q−P›
(24)  Y = Q → ⅓·‹P−Q›

Plane Affine Algebra (II)

See also Part I and Part III.

As noted before, the algebra permits us to calculate proofs without resorting to coordinate manipulations. As a demonstration, I'll present a very simple calculation, and then a theorem that I didn't know (and I would be very hard-pressed to come up with a classical proof).

Given points P, Q, R, the altitude of the triangle PQR through the vertex Q is the segment QH perpendicular to the base PR. Denoting hgt.P.Q.R = |Q−H| (we write |•−•| = |‹•−•›| per abusum linguae), it is:

(17)  hgt.P.Q.R = (‹R−P›⊥⋅‹Q−P›)/|R−P|

Proof:

   hgt.P.Q.R
= { definition }
   |Q−H|
= { definition of the sine line }
   |Q−P|·sin.(θ.‹R−P›.‹Q−P›)
= { (16) with u, v := ‹R−P›, ‹Q−P› }
   (‹R−P›⊥⋅‹Q−P›)/|R−P|

The line through point P with direction vector v is the set of points P⇒v that, in the words of Euclid, "lies equally on the points of itself":

(18.0)  Q ∈ P⇒v ≡ |v|⋅‹Q − P› = |Q − P|⋅v

The following are theorems:

(18.1)  P ∈ P⇒v
(18.2)  ⟨∀ k : k ≠ 0 : P⇒(k⋅v) = P⇒v ⟩
(18.2)  P⇒v = ⟨k ∈ R | P → k⋅v⟩

The parametric line through points P and Q is defined as the real function:

(18)  ray.P.Q.k = P → k·‹Q−P›

From (18.2), it is immediate that ray.P.Q maps R to the line P⇒‹Q−P›.

As a special case, the midpoint of the segment PQ is:

(19)  ray.P.Q.½ = P → ½·‹Q−P›

Given points P, Q, R and S, the intersection of the lines containing the segments PQ and RS is:

(20)  meet.P.Q.R.S = ray.P.Q.((‹S−R›⊥⋅‹R−P›)/(‹S−R›⊥⋅‹Q−P›))

Proof: At the intersection point meet.P.Q.R.S, for some k, l ∈ R:

   ray.P.Q.k = ray.R.S.l
= { (18) }
   P → k·‹Q−P› = R → l·‹S−R›
= { (6) }
   ‹(P → k·‹Q−P›) − (R → l·‹S−R›)› = 0
= { (9) }
   ‹P−R› + k·‹Q−P› − l·‹S−R› = 0
= { heading towards eliminating l; inner product }
   ‹S−R›⊥⋅(‹P−R› + k·‹Q−P› − l·‹S−R›) = 0
= { linearity of inner product }
   ‹S−R›⊥⋅‹P−R› + k·‹S−R›⊥⋅‹Q−P› − l·‹S−R›⊥⋅‹S−R› = 0
= { (14) }
   ‹S−R›⊥⋅‹P−R› + k·‹S−R›⊥⋅‹Q−P› = 0
= { (5); algebra }
   k = (‹S−R›⊥⋅‹R−P›)/(‹S−R›⊥⋅‹Q−P›)

In Part III, the theorem.

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

On Borges' "Spinoza"

Or rather, on just its fourth verse:

(Las tardes a las tardes son iguales.)

and the problem of translating it into English while trying to preserve some of its quality.

Why I find this verse so striking? First, it's an example of a perfect Spanish hendecasyllable, the so-called endecasílabo propio (proper hendecasyllable), with the least number of stressed syllables: the second, the sixth and the tenth, the last two obligatory. Second, the anastrophic antimetabole is masterful. It carries by itself the bleak melancholy of the entire poem, using just two distinct words.

First problem: how to translate "tardes"? In Buenos Aires, tarde is the time of day that stretches from just after noon (1 PM local time) to dusk (5:30 PM to 8:00 PM, local time), with subdivisions like "tardecita" (before 3 PM), "siesta" (3 PM to 5 PM) and "tarde tarde" (6 to 7 PM in summer). Let me try with the generic English "afternoon". Of course, I strive for a iambic pentameter:

The afternoons are equal to themselves.

I dare say it is viable, given the constraints: it is a translation, and it is a iambic pentameter. However, I find it unacceptable: I did preserve none of the qualities of the original. In particular, I miss its sense of "perpetual sameness", the circularity, the eternal return. Second try, a slight variation:

The afternoons are equal one another.

Well, some alliteration here, and to me the nasals are melancholic (No one, Nothing, Never is one of Juan José Saer's novels); however, there is an extra unstressed syllable now that marrs the pentameter. If I drop the requirement of preserving the plural "tardes":

One afternoon is equal to another.

which has a more regular syntax but is definitely a step backwards, and doesn't solve the problem of the extra syllable.

And, besides, the distinct image I have of "tardes" is of dusks, a sun that is forever gone, or rather, the recurrent evidence of the disappearing sun. So how about:

The dusks are equal one another.

Now I'm one syllable short. Again:

The dusks to dusks themselves are equal.

Better, but still short of a syllable. On the other hand, it is not clear if the dusks are equal to themselves (that is, identical as individual dusks), or if they are equal one another, as in the original. Also, I don't like to mix English words of Germanic and Latin origin: I like better using "same" than "equal". So:

The dusks to every other dusk are same.

I badly mangled the syntax (I've found English usage for "is same", mainly journalistic, so I don't think it's unjustifiable, but then); this could be a dead end.

The dusks to dusks are equal and the same.

This attempt leaves me with a sense of accomplishment. Now I understand what Borges meant: it is the days, dusk to dusk, that are equal, not the afternoons themselves. The Jews count days as starting with the first star, that is, at dusk; this sense is nicely conveyed by the English "dusk to dusk". The antimetabole is preserved, and "equal and the same" makes clear that days are not only compared one to another, but confused and confounded into one, unchanging day.

(Un)Expected Symmetries

There is an obvious isomorphism between depth-first and breadth-first traversals: perform one, but keeping enough information to reconstruct the tree from the traversal; do so, and finally perform the other.

Of course this isomorphism is not constructive; and it doesn't sound like it would be the simplest one possible. One thing the usual presentations of the algorithms do is obscure the parallels between both traversal strategies. Let's recall the type of rose trees:

type 'a tree = L of 'a | N of 'a tree list

and at their DFS traversal:

let rec fold_dfs f e = function
| L x -> f e x
| N t -> List.fold_left (fold_dfs f) e t

The last case in fold_dfs is a left fold over the list t of children: first visit the first child, then proceed with the rest of the tree. This makes the function distinctly non-tail-recursive. We can use an explicit stack to manage the children pending of being visited:

let fold_dfs f e t =
  let rec fold e = function
  | []       -> e
  | L x :: s -> fold (f e x) s
  | N t :: s -> fold e (t @ s)
  in fold e [t]

Contrast this with the BFS traversal we've seen before:

let fold_bfs f e t =
  let rec fold e = function
  | []       -> e
  | L x :: q -> fold (f e x) q
  | N t :: q -> fold e (q @ t)
  in fold e [t]

The isomorphism couldn't be clearer.