What Does “Without Loss of Generality” Mean (And How Do We Detect It) James H. Davenport University of Bath Department of Computer Science, Bath, BA2 7AY, U.K. Email: J.H.Davenport@bath.ac.uk Abstract—When one goes from a geometrical statement to B: exploitation of symmetry: as in [Har09]’s opening ex- an algebraic statement, the immediate translation is to replace ample of Schur’s inequality ∀a, b, c ∈ R, k ∈ N, every point by a pair of coordinates, if in the plane (or more as required). A statement with N points is then a statement with 0 ≤ak (a−b)(a−c)+bk (b−a)(b−c)+ck (c−a)(c−b), (1) 2N (or 3N or more) variables, and the complexity of tools like cylindrical algebraic decomposition is doubly exponential in the where a typical proof might begin: “Without loss of number of variables. Hence one says “without loss of generality, generality, let a ≤ b ≤ c”. A is at (0,0)” and so on. How might one automate this, or turn This paper is essentially concerned with the second case, it into a procedure (and possibly even a formal proof)? though, as we shall see, it is not possible to ignore the first, and indeed a given statement might combine both in practice. I. I NTRODUCTION This is a very powerful form of human reasoning. [Har09] Symmetry is at once a familiar concept (we asks, and substantially answers, the question of how it can recognize it when we see it!) and a profoundly deep be incorporated into formal proof: here we ask the same mathematical subject. At its most basic, a symmetry question for computation, notably in the context of Symboic is some transformation of an object that leaves the Computation and Satisfiability Checking [ABB+ 16]. object (or some aspect of the object) unchanged. II. E XPLOITATION OF S YMMETRY — D ISCRETE [Sak09] [Har09] explains the example above as follows. That quotation comes from a major survey of symmetry If asked to spell this out in more detail, we might in purely Boolean satisfiability problems, but our setting is say something like: Since ≤ is a total order, the “Satisfiability Modulo Theories” over the real numbers, and three numbers must be ordered somehow, i.e. we the desire to enhance this with techniques from Computer must have (at least) one of a ≤ b ≤ c, a ≤ c ≤ b, Algebra, notably Cylindrical Algebraic Decomposition. See b ≤ a ≤ c, b ≤ c ≤ a, c ≤ a ≤ b or c ≤ b ≤ a. [Á15], [ABB+ 16]. Here the situation is different in two, But the theorem is completely symmetric between complementary, respects. a, b and c, so each of these cases is just a version 1) It is not legitimate to discard a part of the Boolean of the other with a change of variables, and we may search space on the grounds that it is symmetric to as well just consider one of them. another, already searched, space, unless we know that He then offers two possible formalisms: this symmetry carries through to the underlying theory. • The phrase may be an informal shorthand saying 2) Conversely, symmetries in the underlying theory may ‘we should really do 6 very similar proofs here, exist, which either do not appear directly in the Boolean but if we do one, all the others are exactly formulation, or indeed are irrelevant to the Boolean for- analogous and can be left to the reader’. mulation, but may greatly simplify the underlying theory. • The phrase may be asserting that ‘by a general More specifically, it is the second kind of symmetry that this logical principle, the apparently more general case paper is concerned with. and the special WLOG case are in fact equivalent Many proofs, particularly of the more computational kind, (or at least the special case implies the general in mathematics contain a line of the form “without loss of one)’. generality, we may assume . . . ” (often abbreviated w.l.o.g). He then argues that the second interpretation is closer to the This is discussed in [Har09], who claims, we believe correctly, informal mathematics, and shows how to implement this as a that this means one of two, rather different, things: HOL-Light theorem, more precisely A: non-degeneracy: for example “w.l.o.g. α 6= 0”, really ` (∀xyz.P xyz ⇒ P yxz ∧ P xzy)∧ means1 “α = 0 is a special case, which you can easily (∀xyz.x <= y ∧ y <= z ⇒ P xyz) (2) see for yourself, so I am not going to bother with it here”; ⇒ (∀xyz.P xyz) 1 However, it may also mean C: “α = 0 renders the result meaningless, so Note 1: There’s a subtlety here: in fact the statement is we shall not consider it further”. invariant under S3 , the symmetric group on {x, y, z}, but the Copyright c by the paper’s authors. Copying permitted for private and academic purposes. In: E. Ábrahám, J. Davenport, P. Fontaine, (eds.): Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation (SC2 ), Timisoara, Romania, 02-07-2016, published at http://ceur-ws.org TABLE I Theorem 1 (Simson’s Theorem, [Wan96], [Mou16]): Let D C ELLS SATISFYING a ≤ b ≤ c be on the circumcircle of the triangle ABC, let P , Q and R be the points of AB, AC and BC where the line to D is c<0 b0 b<0 all sation2 of this is (4). b=0 a 0 similarly, and c = 0 having 2 xA 2 yB − xA 2 yC − xB 2 yA + xB 2 yC +  a three-way split on b, each having a three-way split on a. Of these, the 14 listed in Table I satisfy a ≤ b ≤ c, either  xC 2 yA − xC 2 yB + yA 2 yB − yA 2 yC −  2 2 2 2    totally, or, where underlined, only partially. Not only is this xA − 1 yA yB + yA yC + yB yC − yB yC  −  ratio of 14/31 ≈ 45% disappointing compared with the naı̈ve   2 D   (not allowing for equality) 1/6 one might expect: if we split   the underlined cells to get precisely the cells with a ≤ b ≤ c,   2 −xA xB 2 + yB 2 + xA xC 2 + yC 2 +  the ratio would be 18/39 ≈ 46%.  xA 2 (xB − xC ) + yA 2 (xB − xC ) −  B. How might we detect it?   x B x C 2 + yC 2 + x C x B 2 + yB 2   yA + 1  The most obvious generalisation of Note 1 is the following   2 D   well-known result.   Proposition 1: The permutations (1, 2, . . . , n) and (1, 2) generate Sn as a group acting on {1, 2, . . . , n}. D := xA yB − xA yC − xB yA + xB yC + xC yA − xC yB Corollary 1: Hence, if a statement P (x1 , x2 , . . . , xn ) (4) is given, and P (x1 , x2 , . . . , xn ) is logically equivalent to It is relatively easy (for a computer algebra system) to verify P (x2 , x1 , . . . , xn ) and to P (x2 , . . . , xn , x1 ), it is sufficient to that (4) is invariant if we replace all variables z by z + c. prove Hence it is legitimate to choose yA = 0, which gives us (5). P (x1 , x2 , . . . , xn ) ∧ x1 ≤ x2 ∧ x2 ≤ x3 ∧ · · · . (3) xD xA 2 yB − xA 2 yC + xB 2 yC − xC 2 yB + yB 2 yC − yB yC 2 Note 2: We have said “logically equivalent to”, rather than xD 2 + yD 2 = + xA yB − xA yC + xB yC − xC yB  2 2 2 2 just “equal to”, as we needed the laws of algebra (at least yD − xA xB + yB + xA  xC + yC +  commutativity of addition and multiplication) to show that (1) xA 2 (xB − xC ) − xB xC 2 + yC 2 + xC xB 2 + yB 2 was actually invariant. yD + xA yB − xA yC + xB yC − xC yB  2 III. E XPLOITATION OF S YMMETRY — C ONTINUOUS xA 2 yB − xA 2 yC + xB 2 yC − xC 2 yB + yB 2 yC − yB yC 2 2 One of the most important ways in which such in- 4 (xA yB − xA yC + xB yC − xC yB ) 2 xA 2 yB − xA 2 yC + xB 2 yC − xC 2 yB +  variances are used in proofs is to make a convenient choice of coordinate system. [Har09]  1 yB 2 yC − yB yC 2  −x A −  If a problmis intrinsically geometric, then the precise coordi-  2 xA yB − xA yC + xB yC − xC yB  nate system is irrelevant to the truth of the statement. It is this (5) sort of symmetry that we will look for in this section. Let us consider the following example 2 Obtained with Maple’s geometry[circumcircle] command. TABLE II yB < − 7420725 4194304 , and hence the author hoped that rescaling CAD OF Rn FOR NUMERATORS OF (4)–(7) would reduce this problem. The effect is in fact negligeable: 303093 [CM14] [McC84], [EWBD14] in (6)|xB =16 the same cell has − 131072 < yC < − 2424743 1048576 , Equation Cells Time Memory Cells Time Memory and in (6)|xB =256 we have − 1048576 < yC < − 13752053 27504107 524288 . (secs) MiB (secs) MiB As can be seen, the overall effect on memory and time of (7)|xA =1 37 0.14 11 245 1.86 108 (7) 107 0.47 26 589* 3.89 303 changing the scaling was for the worse. (6)|xB =1 319 3.48 256 30803* 433.20 31460 The second set of timings were produced using the software (6)|xB =16 319 3.53 290 in [EWBD14], but with no special declarations, hence effec- (6)|xB =256 319 4.24 318 (6) 591 2.29 188 36531* 807.00 55000 tively the projection of [McC84]. In several cases, this warned (5) 591 2.80 235 — > 9000 that the projection was not well-oriented. Since the McCallum (4) 591 4.12 341 projection is a superset of the Lazard projection, and this has The timings and memory usage come from Maple’s CodeTools[Usage], and hence both have (up to) four significant figures. been recently [MPP16] been proved unconditionally correct, ∗ Warning that the input is not well-oriented. we can ignore these. We observe that detecting the rotational symmetry ((7) rather than (6)) had a much greater effect here than it did for the [CM14] method. Again, it is relatively easy (for a computer algebra system) The really surprising effect was the difference between (6)) to verify that (5) is invariant if we replace all variables z ∈ and (5)). As far as the author could tell, the code was still {xA , xB , xC , xD } by z + c. Hence it is legitimate to choose projecting when interrupted after 2 21 hours: at least is had xA = 0, which gives us (6). produced no warnings about orientation. This needs further  2 2 xD xB 2 yC − xC 2 yB + yB 2 yC − yB yC 2 investigation. xD + yD = + xB yC − xC yB  B. How might we detect it? yD −xB xC 2 + yC 2 + xC xB 2 + yB 2 The question of detection comes in several forms. xB yC − xC yB (6) 1D Invariance by translation by R can be detected, as In fact, both [Wan96], [Mou16] coordinatise with A = (xA , 0) we did in going from (4) to (5), by checking that and B = (−xA , 0), taking (implicit) advantage of the fact that adding c to all variables leaves the equation (or the problem is invariant under translation (so we can place the system of equations) invariant. This will fail, of midpoint of AB at (0, 0)) and rotation (so we can place A and course, if there are variables other than the results B on the x-axis). Then (4) becomes the simpler (7). of coordinatisation.  2D Having detected invariance by translation by R, we 2 2 yD −xA 2 + xC 2 + yC 2 can look for invariance by translation by R2 as xD + yD = + xA 2 (7) yC we did in going from (5) to (6), by checking that One further step, which [Wan96], [Mou16] could have done, adding c to a proper subset of the variables leaves and a computer system could certainly spot, is that the the equation (or system of equations) invariant. Of equation is homogeneous, and hence we can pick, say, xA = 1. course, the author “cheated” and translated all the x However, whilst appearing to be a type B w.l.o.g., exploiting variables based on variable name, but in practice one symmetry under dilation, it is also asserting xA 6= 0, thus a would have to try all subsets (but not a subset and type A, or even type C, w.l.o.g. as well. its complement) of the set of variables. 3+D Though not present in our example, we could then A. Does this help SC2 ? go on to detect invariance by translation by R3 , and The non-vanishing of the denominators in (4)–(7) essentially so on. As we see in the discussion of rotation, it is corresponds to the non-degeneracy of the triangle ABC, so important to do so. it is legitimate to consider just the numerators. The resource Scaling This is a consequence of homogeneity, and can consumptions of Cylindrical Algebraic Decomposition, com- easily be detected. The problem is that this is also a puting a complete CAD of Rn on these are shown in Table type A (or even C) w.l.o.g. as well as type B one, and, II. having chosen xi as our dehonogenising variable, we Let us consider first the [CM14] timings. These show, ought in principle to consider the two cases xi = 1 somewhat to the author’s surprise, that Cylindrical Algebraic and xi = 0. The second case, if it does not collapse, Decomposition is, at least in this example, unaffected in terms is also homogeneous in the remaining variables, so of cell count by the translation w.l.o.g.s, though rotation ((7) we can recurse. rather than (6)) and scaling (the substitution lines) help, at 2D Rot. If we know that we have 2D translation symmetry, least in terms of cell count. we might hope for 2D rotational symmetry as well. We solved (6) with variable ordering x  y  xC  Let us call the set of variables translated by c yB  yC (i.e. yC is the first variable to be eliminated). The in the search for 2D symmetry the “x” variables, different scalings were applied to (6) after (6)|xB =1 showed and its complement the set of “y” variables, and quite large denominators, e.g. cell (1,1,1,2,1) has − 3710363 2097152 < assume that there are no more “x” variables than “y” variables, which will occur if we do a breadth- R EFERENCES first search for such a set. If the problem comes from [Á15] E. Ábrahám. Building Bridges between Symbolic Computation coordinatisation of a 2D geometrical problem, there and Satisfiability Checking. In D. Robertz, editor, Proceedings should be as many “x” as “y” variables — of couse ISSAC 2015, pages 1–6, 2015. [ABB+ 16] E. Ábrahám, B. Becker, A. Bigatti, B. Buchberger, C. Cimatti, whether these correspond to the original x and y J.H. Davenport, M. England, P. Fontaine, S. Forrest, D. Kroening, or vice versa is a matter of chance, but from now W. Seiler, and T. Sturm. SC2 : Satisfiability Checking meets on we shall drop the quotes, implicitly assuming the Symbolic Computation (Project Paper). In Proceedings CICM 2016, 2016. correspondence, not that it matters. [CM14] C. Chen and M. Moreno Maza. An Incremental Algorithm for Then the question comes: which yj ∈ {y1 , . . . , ym } Computing Cylindrical Algebraic Decompositions. In Ruyong corresponds to which xi ∈ {x1 , . . . , xn }? Here we Feng, Wen-shin Lee, and Yosuke Sato, editors, Computer Math- ematics, pages 199–221. Springer Berlin Heidelberg, 2014. know of no better answer than trying all m!/(m−n)! [EWBD14] M. England, D.J. Wilson, R. Bradford, and J.H. Davenport. possibilities for a complete assignment σ. We then Using the Regular Chains Library to build cylindrical algebraic replace all pairs (xi , yσ(i) ) by (cxi − syσ(i) , cyσ(i) + decompositions by projecting and lifting. In Proceedings ICMS 2014, pages 458–465, 2014. sxi ) to practice a rotation3 by θ with c = cos θ, [Har09] J. Harrison. Without Loss of Generality. International Confer- s = sin θ, and apply c2 + s2 = 1. For the correct ence on Theorem Proving in Higher Order Logics, pages 43–59, assignment in our example, it is relatively easy 2009. [McC84] S. McCallum. An Improved Projection Operation for Cylindrical to demonstrate equality (in particular the result is Algebraic Decomposition. PhD thesis, University of Wisconsin- independent of c and s), and for incorrect examples Madison Computer Science, 1984. we get results that still contain c and s. [Mou16] C. Mou. ”software library for triangular decompositions”. Talk at ICMS 2016, 2016. 3D Rot. We have no examples of this, but the principles [MPP16] S. McCallum, A. Parusinski, and L. Paunescu. Validity proof are the same as above. Note that, if there really is of Lazard’s method for CAD construction. https://arxiv.org/abs/ 3D symmetry, we should identify it, and then choose 1607.00264, 2016. [Sak09] K.A. Sakallah. Symmetry and Satisfiability. Chapter 10 of triples (xi , yσ(i) , zτ (i) ), as assuming we have merely Handbook of Satisfiability, pages 289–338, 2009. 2D symetry, and rotating the x and y but not the z, [Wan96] D. Wang. GEOTHER: A geometry theorem prover. International will fail. Conference on Automated Deduction, pages 166–170, 1996. IV. C ONCLUSION We have only considered one example so far, but intend to study others. It is a “natural” example in that it comes from 2D geometry. It would be possible to build artificial examples that had, for example, rotational symmetry but no translational symmetry, but, in the spirit of [ABB+ 16], we have started with natural problems. From the basis of this limited analysis, we draw the following provisional conclusions. It is possible to detect certain forms of symmetry simply from the equations (though it would clearly be better to detect them before coordinatisation if at all possible). For the method of [CM14], detecting translational symmetry has no effect on the cell count (and a modest effect on runtime and memory), but seems to be a pre-requisite to efficient detection of rotational symmetry, which is extremely helpful. The method of [McC84] seems much more susceptible to the number of variables, and hence all symmetry detection and “w.l.o.g.” specialisation are helpful. Acknowledgements. The author is grateful to Julien Nar- boux for references, and to Matthew England and the referees and Programme Committee of the SC2 2016 workshop for useful comments. This work was performed as part of the H2020-FETOPEN-2016-2017-CSA project SC2 (712689). The dataset supporting these computations is stored at http://doi. org/10.5281/zenodo.305441. 3 The reader may object that this is a rotation about the origin. But we have already demonstrated 2D translational invariance, so one centre is as good as another.