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.

In-Place Reversal... of Trees

We've seen before that we can traverse a tree in constant stack space; that is, we've come up with a tail-recursive BFS traversal:

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 (List.rev_append (List.rev q) t)
  in fold e [t]

Unfortunately, this version is rather inefficient, as it copies the "queue" of nodes already waiting to be visited just to reverse it, and then copies it again to prepend it to the current node's children, finally discarding both the original and its reverse. This generates two garbage nodes per tree node processed. This outer copy is absolutely local to the traversal, since the first argument to rev_append is fresh. We can thus replace it by an in-place reversal of q.

Suppose we had a function rplacd that, given two lists l ≠ [] and m, physically modified the tail of l to be m, while returning l's old tail:

val rplacd : 'a list -> 'a list -> 'a list

With it we can write an in-place reversing function as:

let rec ip_revappend l v =
   if l == [] then v else
   let t = rplacd l v in
   ip_revappend t l

(I use a let-binding to make explicit the sequencing between the replacement and the recursive invocation). Compare this with the purely functional version:

let rec revappend l v = match l with
| []     -> v
| h :: t -> revappend t (h :: v)

In OCaml, we can use the module Obj to (carefully!) write replacd:

let rplacd : 'a list -> 'a list -> 'a list = fun l m ->
   let o = Obj.repr l in
   let t = Obj.field o 1 in
   Obj.set_field o 1 (Obj.repr m);
   Obj.obj t

(the type annotations are essential for OCaml to infer the correct types for Obj.obj). Putting it all together, and inlining rplacd in ip_revappend to avoid the call:

let rec ip_revappend (l : 'a list) v =
    if l == [] then v else
    let o = Obj.repr l in
    let t = Obj.obj (Obj.field o 1) in
    Obj.set_field o 1 (Obj.repr v);
    ip_revappend t l

(again, the type annotation is essential). In the absence of sharing, ip_revappend is observationally equivalent to revappend. Since, as explained above, the outer list is free, the following traversal is unconditionally observationally equivalent to the previous version:

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 (ip_revappend (List.rev q) t)
  in fold e [t]

Even so, it differs from it in that it produces just one garbage node per tree node traversed. This is optimal if we want to preserve the tree: concretely, q is the list of younger siblings, so as a part of the tree it should be preserved. If the tree is ephemeral, however, we can also replace the inner rev q by an ip_revappend q [] to recruit the nodes of the tree to serve as the tail of the traversal queue.

So, by stepwise, mechanical refinement, we arrive at an in-place ip_fold_bfs that uses constant stack and heap space:

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

This is the main point of Sobel and Friedman's paper.