Proving and Solving in Computational Origami

Tetsuo Ida\(TraditionalForm\`\^1\) and Bruno Buchberger\(TraditionalForm\`\^2\)

Abstract.
Origami (paper folding) has a long tradition in Japan's culture and education. We are developing a computational origami system, based on symbolic computation system Mathematica, for performing and reasoning about origami on the computer. This system is based on the implementation of the six fundamental origami folding steps (origami axioms) formulated by Huzita. In this paper, we show how our system performs origami folds by constraint solving, visualizes each step of origami construction, and automatically proves general theorems on the result of origami construction using algebraic methods. We illustrate this by a simple example of trisecting an angle by origami. The trisection of an angle is known to be impossible by means of a ruler and a compass. The entire process of computational origami shows nontrivial combination of symbolic constraint solving, theorem proving and graphical processing.

Introduction

Origami is a Japanese traditional art of paper folding. The word origami is a combined word coming from ori (fold) and kami (paper). For several centuries, origami has been popular among Japanese common people as an art, as a playing toy, and teaching material for children. Over a decade, origami is also receiving wide interest among mathematicians, mathematics educators and computer scientists, as well as origami artists, as origami poses interesting fundamental geometrical questions.

We are proposing computational origami, as part of a discipline of origami science (also coined origamics by Haga, a pioneer in Japanese origami research [Haga 1999]). We believe that the rigor of paper folding and the beauty of origami artworks enhance greatly when the paper folding is supported by a computer. In the earlier work of the first author [Ida 2003], computational origami performs paper folding by solving both symbolically and numerically certain geometrical constraints, followed by the visualization of origami by computer graphics tools. In this paper we extend the system for proving the correctness of the origami constructions, as proposed in our previous paper [Buchberger 2003].

Origami is easy to practice. Origami is made even easier with a computer: we can construct an origami by calling a sequence of origami a folding function on the Mathematica Notebook [Wolfram 2004] or by the interaction with our system, running in the computing server, using the standard web browser. The constructed final result, as well as the results of the intermediate steps, can be visualized and manipulated. Moreover, in cases where a proof is needed, the system will produce the proof of the correctness of the construction. Namely, for a given sequence of origami construction steps and a given property, the system proves that the resulting shape will satisfy the property (or disprove the property).

The rest of this paper is organized as follows. In section 2 we explain the principles of origami construction developed from Huzita's origami axioms.  In section 3 we discuss a method for trisecting an angle by origami, which cannot be made using the traditional ruler-and-compass method. The construction is followed by the proof of the correctness of the construction in section 4. In section 5 we summarize our contributions and point out some directions for future research.

Principles of Origami Construction

An origami is to be folded along a specified line on the origami called fold line. The line segment of a fold line on the origami is called a crease, since the consecutive operations of a fold and an unfold along the same fold line makes a crease on the origami.  A fold line can be determined by the points it passes through or by the points (and/or lines) it brings together. As in Euclidean geometry, by specifying points, lines and their configuration, we have the following six basic fold operations called origami axioms of Huzita [Huzita 1989, Hull 1997].  It is known that Huzita's origami axiom set is more powerful than the ruler-and-compass method in Euclidean geometry  [Geretschlaeger 2002].  Origami can construct objects that are impossible by the ruler-and-compass method [Chen 1966].  One of them is trisecting an angle, which we will show in this paper, as an example of origami proving and solving.

Origami Axioms

Huzita's origami axioms are described in term of  fold operations as follows:

Algorithmically, these axioms suggest two operations; finding crease(s) and folding the origami along the crease. The former amounts to solving equations that describe the constraints of geometrical objects. It can be shown easily that finding the creases is reduced to solving geometrical constraints (maximum 3rd degree polynomial system).

OFold (Origami Fold Function)

The fold operations of origami based on the origami axioms can be implemented by a single function OFold whose specification is given below.  Function OFold needs several points (depending on the axioms)  to compute the crease, to determine the face to be moved, and to determine the direction of the fold (mountain or valley).  The convention below is that a single capital letter denotes a point and XY denotes a line segment from point X to point Y.  Note that the types of the arguments and the keywords can discriminate  the operations to be performed unambiguously.

(O1) OFold[X,  Along ->  PQ]

(O2) OFold[P,  Q]

(O3) OFold[AB,  CD]

(O4) OFold[X,  AlongPerpendicular ->  {P,  AB}]

(O5) OFold[P,  AB,  Through ->  Q, ]

(O6) OFold[P,  AB,  Q,  CD]

OFold[X, Along-> PQ] in (O1) directs the system to make a fold along the crease PQ.  All the faces containing the values (the coordinate of the point X) are to be moved. In all the case we have hidden optional parameters which tell the system which faces of the origami should be moved (with Move keyword) and which directions (mountain or valley).  In the case of (O2) , Move  -> P is implicit,  and in the cases of (O5) and (O6) Move  -> P is implicit if  with P we can specify the faces to be moved.  Further details are omitted here, as the above specification is sufficient to understand the origami construction in section 3,

Trisecting an angle

We give an example of  trisecting an angle. This example shows a non-trivial use of Axiom (O6). The method of construction is due to H. Abe as described in [Geretschläger 2002, Fushimi 1980].   In the following we will explain the construction of trisecting a given angle using our computational origami system.

First, we define a square origami paper, whose corners are designated by the points A, B, C and D. The size may be arbitrary, but for our example, let us fix it to be 10 by 10. All the operations are performed by Mathematica function calls. Optional parameters can be specified by "keyword -> value".

NewOrigami[Square[10, 
            MarkPoints -> {"A", "B", "C", "D"}], 
          FigureCaption -> "Step "];

We then introduce an arbitrary point, say E at the coordinate (2, 10), assuming that point A is at (0, 0).

PutPoint[{"E",  Point[2,  10]}];

Our problem is to trisect an angle ∠EAB. The method consists of the following seven steps (steps 3-9) of folds and unfolds.

Step 3: We make a fold to bring point A to D, to obtain the perpendicular bisector of segment AD .  This is the application of (O2). The points F and G, which will be  the terminal points of the crease,  are automatically generated by the system.

OFold[A, D];

Step 4: We unfold the origami and obtain the crease FG .

Unfold[];

Steps 5 and 6: Likewise we obtain the crease HI.

OFold[A, G];

Unfold[];

Step 7: This step is the crucial step of  the construction. We apply (O6).  We try to superpose G  and the line  that is the extension of  the segments AE, and to superpose  A and the line  that is the extension of  the segment HI, simultaneously. There are three possible fold lines to realize this superposition. The system responds with the query of "Specify the line number" together with the lines on the origami image.

OFold[G, AE, A, HI];

Which line(1,2,3)?

Step 8: We reply to the query by the call of OFold[Along->3,Move-> A, ...], which tells the system that we choose the line number 3. This gives the fold line that we are primarily interested in.  However, readers can easily see that the other two fold lines are also solutions (which trisect different angles).

OFold[Along -> 3, Move ->  A, 
        MarkCrease ->  False];

Step 9: We will copy  the points A and I on the other face that is below the face that A and I are on, and unfold the origami. The copied points appear as L and J (the names are automatically generated).

CopyPoint[{A,  I}]; Unfold[];

Step 10: Now we see that the segments AJ and AL trisect the angle  ∠EAB.

ShowOrigamiSegment[{{{A, E}}, {{A, J}}, {{A, L}}}];

Although it is not obvious to see that equational solving is performed, our system solves a set of polynomial equations, up to the third degree, at each step. In the case of steps 7 and 8, the system solves a cubic equation. This explains why we have (at most) 3 possible fold lines at step 7.

Proof of the correctness of the trisection method

We now prove the following theorem with our system.

Theorem: The origami construction in section 3 trisects an angle.

In this simple example, the correctness of the trisection could be easily verified either by geometric reasoning or by a sequence of simplification steps of the algebraic equations representing geometric constrains. However, for proceeding towards a general (and completely automatic) proving method for origami theorems, we formulate the proving steps in a more general setting.  We prove the above theorem by showing that

∡EAB /3= ∡JAB/2 = ∡LAB.

A general proof procedure is as follows:

We first translate the above question into the algebraic form. This is done after we fix the coordinate system (in our case the Cartesian system).

We already observed that each folding steps are formulated in Axioms (O1)-(O6). The geometric properties that hold for each origami axiom are easily extracted in terms of polynomial constraints, once the representations of lines and points are fixed.

We use Gröbner bases method. We collect all the premise equalities C = {(Subscript[c, 1]),  ... , (Subscript[c, n])} (obtained at step II) and the conclusion equalities D={(Subscript[d, 1]),  ... , (Subscript[d, m])} (obtained at step I) . Let M be the boolean combinations of the equalities of the form ¬ ((Subscript[c, 1])∧ ...  ∧ 
              (Subscript[c, n])) ∨ ((Subscript[d, 1])∧ ...  ∧ 
            (Subscript[d, m])), i.e. C ⇒ D. We prove ∀ M by refutation. The decision algorithm, roughly, proceeds as follows:

Bring M into conjunctive normal form and distribute ∀ over the conjunctive parts. Treat each of the parts

(Underscript[∀ , a, b, c,  ... ])P

separately. Note that P is now a disjunction

(Subscript[E, 1])=0∨  ...  ∨ (Subscript[E, k])=0 ∨ (Subscript[N, 1]) ≠ 0 ∨   ...  ∨ (Subscript[N, l])≠0

of equalities and negations of equalities.

Then

(Underscript[∀ , a, b, c,  ... ])((Subscript[E, 1])=0∨  ...  ∨ (Subscript[E, k])=0 ∨ (Subscript[N, 1]) ≠ 0 ∨   ...  ∨ (Subscript[N, l])≠0)

is transformed into

¬(Underscript[∃ , a, b, c,  ... ])((Subscript[E, 1]) ≠ 0∧  ...  ∧ (Subscript[E, k])≠0∧(Subscript[N, 1])=0∧  ...  ∧ (Subscript[N, l])=0)

and further into

¬(Underscript[∃ , a, b, 
            c,  ... , (Subscript[ξ, 1]), …, (Subscript[ξ, k])])((Subscript[E, 1]) (Subscript[ξ, 1]) - 1=0∧  ...  ∧ (Subscript[E, k])(Subscript[ξ, k])-1=0 ∧ (Subscript[N, 1])=0∧  ...  ∧ (Subscript[N, l])=0)

with new variables (Subscript[ξ, 1]), …, (Subscript[ξ, k]) ("Rabinovich trick").

Now, our question becomes a question on the solvability of a system of polynomial equations, which can be decided by computing the reduced Gröbner basis of {(Subscript[E, 1]) (Subscript[ξ, 1]) - 1,  ... (Subscript[E, k]) (Subscript[ξ, k]) - 1, 
      (Subscript[N, 1]),   ...  ,  (Subscript[N, m])}. Namely, one of the fundamental theorems of Gröbner bases theory tells us that this Gröbner basis will be {1} iff the system is unsolvable (i.e. has no common zeros) [Buchberger 1970].

The proof steps would require laborious work of symbolic manipulation.  We  have developed a system for finding geometrical constraints generated in each step of the origami fold and for performing the above transformations completely automatically.

The following piece of programs will do all the necessary transformations and the proof as mentioned above.

Let us first view the configurations of the points on the completely unfolded paper.

ShowProofSupport[]

The subscript k on each point indicates that the positions are determined at origami folding step k.

Preparing for proof

props = GatherProperty[];

cmap = 
        CoordinateMapping[props, 
          InitialShape -> 
            SquareP[{Point[0, 0], 
                r}, {"A", "B", "C", "D"}]];

premise = ToAlgebraic[props, cmap];

Since function tangent restricted to  (0, π/2) is bijective ,   we will prove tan[β] = tan[2α] ∧ tan[γ] = tan[3α].  We compute them by:

tanγ = (Subscript[E, 1]) /. Point[x_, y_, ___] :> y/x

tanβ = (Subscript[J, 6]) /. Point[x_, y_, ___] :> y/x

tanα = (Subscript[L, 6]) /. Point[x_, y_, ___] :> y/x

Using the well-known elementary trigonometric formulas, we have:

tan3α = 
      Simplify[((3  Tan[x]- Tan[x]^3 )/(1 - 3 Tan[x]^2)) /. Tan[x] -> tanα]

tan2α = 
      Simplify[((2  Tan[x])/(1 -  Tan[x]^2)) /. 
          Tan[x] -> tanα]

The conclusion polynomial set is {Numerator[Together[tanγ-tan3α]]=0, Numerator[Together[tanβ-tan2α]]=0}, which can be translated to algebraic form as follows.  The variables were automatically generated when the coordinate mapping table was constructed.

concl = 
      ToAlgebraic[{Numerator[Together[tanβ - tan2α]], 
          Numerator[Together[tanγ - tan3α]]}]

Sending all the data to theorem prover Theorema

thma = 
        LinkCreate["50000@192.168.11.2", 
          LinkProtocol -> "TCPIP" ] ;

SendTheoremaFormula[thma, premise, 
        concl, "TrisectingAngle"];

NotebookSave[
        LinkRead[thma], "TrisectingAngleProof.nb"];

LinkClose[thma];

The Proof

The proof text is stored in file TrisectingAngleProof.nb.  Since it takes too much space to reproduce the machine generated (albeit readable) text output, we only show the highlights of the proof.  The omitted formulas are marked as  "...".

Conclusion

We have shown the computer origami construction with the example of trisecting an angle. Our computational origami system not only does the  simulation of origami folds [Ida 2003], but also proves the correctness of the construction by accessing  the implementation of the Gröbner bases algorithm [Buchberger 1970] and  the implementation of the above decision algorithm in Theorema [Buchberger 2000]. The premise polynomial set is not optimal since it contains extra geometrical constraints unnecessary for proving the theorem.  We are currently working to minimize the premise polynomial set.

As a next step of our research we plan to study origami solving problem, which asks for finding a sequence of origami steps that will lead to an origami object with a desired property. However, it is clear that this problem is analogous to the problem of finding geometric objects with desired properties using only a ruler and a compass. Note, however, that the two problems - origami construction and the ruler-and-compass construction - are not equivalent. As we have seen, the trisection of an angle is possible by origami but not by the ruler-and-compass method. For further development of origami construction,  in analogy to the ruler-and-compass construction problem, Galois theory suggests itself as the main approach to solving the origami construction problem.