Computational Origami:
Interaction of Solving, Proving and Computing

Bruno (Buchberger^1), Tetsuo (Ida^2)

\(TraditionalForm\`\(*\^1\)\)Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria,
\(TraditionalForm\`\(*\^2\)\)Symbolic Computation Research Group (SCORE), University of Tsukuba, Japan.

Copyright Bruno Buchberger, T. Ida  2004.

Copyright Note: This file can be printed, stored and distributed under the following conditions:

- the file is kept unchanged
- this copyright note is included
- a message is sent to Bruno.Buchberger@RISC.Uni-Linz.ac.at or Tetsuo.Ida@acm.org.


If you use the material, please, cite this  talk appropriately.

Acknowledgement: Sponsored by Austrian FWF (Austrian Science Foundation), Project 1302 in the frame of the SFB (Special Research Area) 013 "Scientific Computing".

Abstract

Origami paper folding has a long tradition in Japan's culture and education. The second author has recently developed a software system, based on functional logic programming and web-technology, for simulating origami paper folding on the computer (the "origami computing problem" or the "forward origami problem"). This system is based on the implementation of the six fundamental origami folding steps ("origami axioms") formulated by Huzita. In this paper, we consider the problem of automatically proving general theorems on the result of origami folding sequences (the "origami proving problem") using algebraic methods, in particular the first author's Gröbner bases method. We also give some comments on finding origami folding steps that result in a desired object (the "origami solving problem" or "inverse origami problem").

Introduction

The current computational origami system under development by  the second author  allows to study the effect of sequences of origami folding steps on the computer [Ida 2003a, 200b].  It is implemented in Mathematica and can be accessed via  Mathematica notebook as well as via a standard  web browser such as Internet explorer. The system can simulate and visualize, by algebraic calculations, the effect of any origami folding sequence. Namely, it solves what we call the "origami computing problem". In this paper we will  discuss the expansion of the capability of the system into the following two natural directions:

The  origami solving problem: For a given initial origami shape and a  final origami shape with certain desired properties, find a sequence of origami steps that transforms the initial into the final shape (or report "not origami solvable" if such a sequence does not exist).

The origami proving problem:  For a given sequence of origami steps and a given property (out of a certain class of properties), prove that the resulting shape will satisfy the property (or disprove the property).

We will give an answer to the origami proving problem (for a well-defined wide class of theorems) and some preliminary remarks on the origami solving problem.

The algorithmics of origami is an excellent example of the fundamental and general three algorithmic aspects "computing (simplifying, forward solving, equivalence transforming, ...)", "solving (inverse computing, existential proving,...)", and "proving (universal proving, truth deciding, ...)".
This paper is the abridged version of the project report  [Buchberger 2003].

A Simple Solve Problem and a Simple Prove Problem

We start with the following simple origami solving problem: Given a square ABCD, find a sequence of origami steps such that, finally, we arrive at an equilateral triangle.  Here is a first solution to the problem.  In Fig. 1 we show an array of graphics outputs generated by our system.

Fig. 1   Construction of  Equilateral Triangle by Origami

At Step 1, we first define the origami as a 10 x 10 square with the four  corner points marked as A, B, C and D.

step1 = 
        NewOrigami[
          Square[10, 
            MarkPoints -> {"A", "B", "C", "D"}], 
          Context -> "EquilateralTriangle`", 
          FigureCaption -> "Step. ", 
          Show -> {ShowFrame -> True}];

\(At\ Step\ 2, \ 
    we\ \ fold\ the\ square\ to\ bring\ the\ point\ A\ to\ point\ \(\(B\)\(.\)\(\ \)\)\)

step2 = 
        FoldBring[A, B, MarkCrease -> True, 
          Show -> {ShowFrame -> True, 
              ImageSize -> 200}];

At Step 3,  we unfold the origami .  This makes the middle line\(EF\&_\).

step3 = 
        Unfold[Show -> {ShowFrame -> True, 
              ImageSize -> 200}];

Similarly,  we  create the crease \(JG\&_\) by folding (Step 4) and unfolding (Step5).

step4 = 
        FoldBring[A, D, MarkCrease -> True, 
          Show -> {ShowFrame -> True, 
              ImageSize -> 200}];

step5 = 
        Unfold[Show -> {ShowFrame -> True, 
              ImageSize -> 200}];

At Step 6,  \(we\ fix\ the\ point\ A\ and\ make\ a\ fold\ along\ the\ line\ passing\ through\ the\ point\ A\),so that point D will lie on line\(EF\&_\). The function FoldBrTh  \((read\ as\ \*"""Fold\ by\ Bring\ Through\)")  is the function that implements one of  the Huzita's  six  origami axioms, \(and\ hence\ \ is\ a\ legal\ origami\ \(\(operation\)\(.\)\)\)

\(\(step6 = 
        FoldBrTh[D, \(E\ F\)\&_, A, MarkCrease -> True, 
          Show -> {ShowFrame -> True, 
              ImageSize -> 200}];\)\)

Now we do the same construction once more, this time starting from the edge \(AB\&_\).

\(\(step7 = 
        FoldBrTh[B, \(G\ L\)\&_, A, MarkCrease -> True, 
          Show -> {ShowFrame -> True, 
              ImageSize -> 200}];\)\)

By folding along the line  \(MO\&_\), we obtain the desired triangle.

step8 = 
        FoldThru[O, M, C, 
          Show -> {ShowFrame ->  True, ImageSize -> 200, 
              ShowMarkPoints ->  {"A", "O", "M"}, 
              ShowCreases -> False}];

\(The\ final\ image\ is\ generated\ by\ turning\ over\ the\ image\ at\ Step\ 8. \)

step9 = 
        TurnOver[
          Show -> {ShowFrame ->  True, 
              ShowMarkPoints ->  {"A", "O", "M"}, 
              ShowCreases -> False}];

ExitOrigami[];

The triangle AOM is an equilateral triangle with edge length \(TraditionalForm\`AB\&_\).  Of course this statement has to be verified, which is the topic of discussion of the next section.  In fact this triangle is the maximum equilateral triangle embedded in the given origami.

Translation into a Prove Problem on Equalities

For deciding whether, for all ABCD, the constructed origami AOM  is equilateral, we first translate the question into a statement consisting of equalities:

First, note that \(TraditionalForm\`AB\&_\) = \(TraditionalForm\`BC\&_\) = \(TraditionalForm\`CD\&_\) = \(TraditionalForm\`DA\&_\), since we start from a square. Hence, whenever the length of one of these four edges occurs, we replace it by \(TraditionalForm\`AB\&_\).

Now observe from the origami shape at step 6 that

\(DE\&_\^2 = \(AD\&_\^2 - AE\&_\^2 = \(AB\&_\^2 - \((AB\&_/2)\)\^2 = 
          3/4 \(\( AB\&_\^2\)\(.\)\)\)\)\)

\(MD\&_\^2 = \(MF\&_\^2 + 
          FD\&_\^2 = \((AB\&_/2 - MD\&_)\)\^2 + \(\(\((AB\&_ - 
                    DE\&_)\)\^2\)\(.\)\)\)\)

For abbreviation, let's write

\(a = AB\&_, \ b = MD\&_, f = \(\(DE\&_\)\(.\)\)\)

We want to decide whether, under these assumptions,   triangle AMO is  equilateral, i.e. that \(AM\&_\)=\(MO\&_ = OA\&_\). For this, it suffices to prove that

(a^2) + (b^2) = 2 (((a - b))^2).

Then, what we want to prove is

(Underscript[∀ , a, f, b])({({{(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}})}\[Implies](a^2) + (b^2)=2 (((a - b))^2)),

where the variables a, f, b range over the real numbers.

A Proof by Gröbner Bases

In this easy example, it can be easily verified by a sequence of simplification steps that the conclusion is a consequence of the premises (with the exception of the case a=0). However, for proceeding towards a general (and completely automated) proving method for such theorems, let us formulate the proving steps in a more general setting by saying that the theorem would be proved if we could show that the polynomial

(a^2) + (b^2) = 2 (((a - b))^2)

was in the ideal generated by the two polynomials:

(f^2) - 3/4  (a^2)

(b^2) - (((a/2 - b))^2) - (((a - f))^2),

because if this is true then the conclusion polynomial is a linear combination of the two premise polynomials and, hence, the conclusion polynomial vanishes for all values of a, b, f, for which the premise polynomials vanish.

Questions about polynomial ideal membership can be answered by the Gröbner bases method [Buchberger 1970].

The Gröbner bases method by now is implemented in all computer algebra systems. For example, in Mathematica we can execute the necessary steps in the following way. We first compute the Gröbner basis for the two premise polynomials (w.r.t. to the lexical ordering of the variables b, f,  a) :

G = 
      GroebnerBasis[{(f^2) - 3/4  (a^2), 
          (b^2) - (((a/2 - b))^2) - (((a - f))^2)}, {b, f, a}]

Now, by Gröbner bases theory, for checking whether the conclusion polynomial is in the ideal generated by the hypothesis polynomials, it suffices to check whether the conclusion polynomials can be reduced to zero by using the polynomials in the Gröbner basis G. In fact,

(a^2) + (b^2) - 2 (((a - b))^2)

is irreducible modulo G because its leading power product b is neither a multiple of the leading power product (f^2) of -3 (a^2) + 4 (f^2) nor of the leading power product a b of -2 (a^2) + a b + 2 a f. (Note that we are working over the pure lexical ordering determined by b>f>a.)  Hence, the conclusion polynomial is not in the ideal generated by the premise polynomials and we cannot conclude that the theorem is true.

However, under the assumption that a≠0, the Gröbner basis G can be brought into the form

G0 = {-3 (a^2) + 4 (f^2), -2 a +  b + 
            2 f}.

Now we see that substituting 2a - 2f  for all the occurrences of b  in the polynomial and simplifying the result polynomial,

(a^2) + (b^2) - 2 (((a - b))^2)

is reduced to 3 (a^2) - 4 (f^2).

This polynomial is reduced to zero modulo G0. This means that we have proved the following slightly  restricted form of the theorem:

(Underscript[∀ , a ≠ 0, f, b])({({{(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}})}\[Implies](a^2) + (b^2)=2 (((a - b))^2)).

A Decision by Gröbner Bases

The above approach gave us a sufficient condition (expressed in terms of Gröbner bases computation and reduction) that guaranteed that the theorem was true. One can go one step further for obtaining a sufficient and necessary condition (expressed in terms of Gröbner bases) for deciding whether the theorem is true. For this we transform the theorem in the following way:

(Underscript[∀ , a, f, b])({({{(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}})}\[Implies](a^2) + (b^2)=2 (((a - b))^2))

is equivalent to

(Underscript[(¬ ∃ ), a, f, b])({({{(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}, {(a^2) + (b^2) ≠ 2 (((a - b))^2)}})}),

which is equivalent to

(Underscript[(¬ ∃ ), a, f, b, ξ])({({{(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}, {((a^2) + (b^2) - 2 (((a - b))^2)) ξ = 1}})}),

Now, this question can be decided by computing the (reduced) Gröbner basis

H = 
      GroebnerBasis[{(f^2) - 3/4  (a^2), 
          (b^2) - (((a/2 - b))^2) - (((a - f))^2), ((a^2) + (b^2) - 
                  2 (((a - b))^2)) ξ - 1}, {ξ, b, f, 
          a}]

and to check whether or not this Gröbner basis is equal to {1}. Since this is not the case, we know that the above version of the theorem is not true.

However, if we restrict a to be non-zero, we come up with the following theorem

(Underscript[(¬ ∃ ), a, f, b, ξ, η])({({{a η = 1}, {(f^2) = 3/4  (a^2)}, {(b^2) = (((a/2 - b))^2) + (((a - f))^2)}, {((a^2) + (b^2) - 2 (((a - b))^2)) ξ = 1}})}).

Now, again, this question can be decided by computing the (reduced) Gröbner basis and checking  whether or not this Gröbner basis is equal to {1}.

J = 
      GroebnerBasis[{a η - 1, (f^2) - 3/4  (a^2), 
          (b^2) - (((a/2 - b))^2) - (((a - f))^2), ((a^2) + (b^2) - 
                  2 (((a - b))^2)) ξ - 1}, {ξ, η, b, f, 
          a}]

Since this is the case, we know that the restricted version of the theorem is true.

A General Decision Algorithm for the Origami Proving Problem and Its Implementation in Mathematica / Theorema

The Decision Problem

Once again we want to emphasize that for the easy example theorem, the proof can be established straightforwardly by high-school mathematics. Similarly, the proof of many such theorems could be given by ad hoc invention of appropriate proof steps.

The point is that we can provide a general algorithm which, for any such proposition about the result of a sequence of origami steps, decides whether or not the proposition is true and, in case it is true, establishes a proof. The algorithm can already be read from the above example.

First of all, let us specify which class of propositions are in the scope of the decision algorithm:

It is clear that the result of any of the admissible six origami operations (according to the origami axiom system by Huzita [Huzita 89]) can be described by a polynomial equality in the coordinates of the points in an origami construction. Now let 𝒪 be the class of propositions of the following structure:

(Underscript[∀ , a, b, c,  ... ])(C \[Implies] (p = q))

where C is a conjunction of equalities between arithmetical expressions in numerical constants and the variables a, b, c, ... that denote coordinates of points corresponding to the operations in an origami construction and p and q are also arithmetical expressions.

Thus, for example, the above two theorems are in 𝒪. Note, however, that the proposition stating that the above construction yields the equilateral triangle of maximum length inscribed in the initial square is not in 𝒪 because the maximum operation cannot be described in a purely equational theory. Still, 𝒪 is a very big class of statements that includes a huge class of interesting properties of the result of origami constructions.

In fact, it is known, see e.g. [Buchberger 1998], that the following class ℬ of statements that contains 𝒪 as a proper subclass admits a decision algorithm: ℬ is the class of statements of the form

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

or of the form

(Underscript[∃ , a, b, c,  ... ])M

where M is a Boolean combination of equalities between arithmetical expressions in numerical constants and the variables a, b, c, ...

A Decision Algorithm for the Class ℬ

The decision algorithm is implemented within Theorema [Buchberger et al. 2000] using the implementation of  Buchberger's Gröbner bases algorithm in Mathematica. In the Theorema implementation, one can call the algorithm by, first, specifying the formula which one wants to prove

Formula["Origami Theorem",any[a, f, b],
	({{(Underscript[∀, b,f,a])(a≠0∧((a^2)-(f^2)-((((a/2)))^2)=0)∧((b^2)-((((a/2)-b))^2)-(((a-f))^2)=0)
\[Implies]((a^2)+(b^2)=2 (((a - b))^2))),  "(1)"}})]

and then calling the Gröbner bases prover by

Prove[Formula["Origami Theorem"], using -> {}, 
      by -> GroebnerBasesProver]

In the following we show the output of the proof generated by Theorema.

The output from Theorema

The proof automatically generated by the Gröbner bases prover of Theorema also contains the explanation of the method and does not  give only the "yes" or "no" decision. This is desirable for didactical purposes so that each call of the prover for a concrete example proposition also explains the general strategy in the concrete example. We do not show, in the proof text, the individual steps of the Gröbner bases computation, which corresponds to the didactic and logical principle that a proof in some area of mathematics should only contain the proof steps on the highest level, specific to the particular area, and should leave out the details on lower levels, which at this stage are considered to be "routine".  In our case, the actual computation of the Gröbner basis could consist of thousands and even millions of steps depending on the proposition to be decided.

An Implementation of Origami Proving in Theorema / Mathematica

Combining the Computational Origami System of the second author,  the implementation of the Gröbner bases algorithm in Mathematica, the implementation of the above decision algorithm in Theorema , and a new tool in Theorema, which can translate geometrical descriptions of configurations into the corresponding polynomial equalities, developed in the recent PhD thesis [Robu 2002], all  implemented in Mathematica, we will soon be able to offer a coherent tool  that can

simulate arbitrary origami sequences both algebraically and graphically,

translate conjectures about properties of the results of origami sequences into statements in the form of universally quantified boolean combinations of polynomial equalities,

decide the truth of such conjectures and produce a proof or refutation of the conjecture fully automatically.

Concluding Remarks

We did not yet study the origami solving problem, which asks for  automatically  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 compass and ruler.

Note that the two problems - origami construction and compass / ruler construction - are not equivalent. In fact origami operations are more powerful than compass / ruler operations [Geretschläger 2002]. For example, trisection of angles is possible by origami but not by compass / ruler [Chen 1996]. In analogy to the compass / ruler construction problem, Galois theory suggests itself as the main approach to solving the general  origami construction problem.

References

[Buchberger . 2003] B. Buchberger and T. Ida
Origami Theorem Proving, SFB Scientific Computing Technical Report 2003-23-Oct 2003, Johanne Kepler University RISC, 2003

[Buchberger 1970] B. Buchberger.
Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems (An Algorithmical Criterion for the Solvability of Algebraic Systems of Equations). 
Aequationes mathematicae 4/3, 1970, pp. 374-383. 
(English translation in: B. Buchberger, F. Winkler (eds.), Gröbner Bases and Applications, Proceedings of the International Conference "33 Years of Groebner Bases", 1998, RISC, Austria, London Mathematical Society Lecture Note Series, Vol. 251, Cambridge University Press, 1998, pp. 535 -545.)

[Buchberger 1998] B. Buchberger.
Introduction to Groebner Bases.
In: Groebner Bases and Applications (B. Buchberger, F. Winkler, eds.),
Cambridge University Press, 1998, pp.3-31.

[Buchberger et al. 2000] B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, Koji Nakagawa, D. Vasaru, W. Windsteiger. 
The Theorema Project: A Progress Report.
In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, August 6-7, 2000, St. Andrews, Scotland), M. Kerber and M. Kohlhase (eds.), A.K. Peters, Natick, Massachusetts, pp. 98-113.

[Ida 2003a] T. Ida.
Constructing Origami on the Internet.
In: D. Petcu, V. Negru, D. Zaharic, T. Jebelean (eds.), Symbolic and Numeric Algorithms for Scientific Computing (Proc. of the 5th International SYNASC Workshop, Oct. 1-3, 2003, Timisoara, Romania), Mirton Publishing Company, ISBN 973-661-104-3, p. 40.

[Ida 2003b] T. Ida,  M. Marin and H. Takahashi.
Constraint Functional Logic Programming for Origami Construction,  Proceedings of the First Asian Symposium on Programming Languages and Systems
(APLAS2003),  Lecture Notes in Computer Science, Vol. 2895, pp 73 - 88, 2003.

[Robu 2002] J. Robu.
Automated Geometric Theorem Proving.
PhD Thesis, RISC (Research Institute for Symbolic Computation), Johannes Kepler University Linz, Austria, 2002.

[Wolfram 1999] S. Wolfram.
The Mathematica Book.
Wolfram Media and Cambridge University Press, 4th edition, 1999.

[Geretschläger 2002] R. Geretschläger,  
Geometric Constructions in Origami (in Japanese,  translation by Hidetoshi Fukagawa), Morikita Publising Co., 2002.

[Huzita 1989] H. Huzita.
Axiomatic Development of Origami Geometry,  Axiomatic Development of Origami Geometry, Proceedings of the First International Meeting of Origami Science and Technology, pp. 143--158, 1989.

[Chen 1996] T. L. Chen.
Proof of the Impossibility of Trisecting an Angle with Euclidean Tools, Mathematics Magazine, Vol. 39, pp.239-241,1966.