Jw. Helton et M. Stankus, Computer assistance for "discovering" formulas in system engineering and operator theory, J FUNCT ANA, 161(2), 1999, pp. 289-363
The objective of this paper is two-fold. First we present a methodology for
using a combination of computer assistance and human intervention to disco
ver highly algebraic theorems in operator, matrix, and linear systems engin
eering theory. Since the methodology allows limited human intervention, it
is slightly less rigid than an algorithm. We call it a strategy. The second
objective is to illustrate the methodology by deriving four theorems. The
presentation of the methodology is carried out in three steps. The first st
ep is introducing an abstraction of the methodology which we call an ideali
zed strategy. This abstraction facilitates a high level discussion of the i
deas involved, idealized strategies cannot be implemented on a computer. Th
e second and third steps introduce approximations of there abstractions whi
ch we call prestrategy and strategy, respectively. A strategy is more gener
al than a prestrategy and, in fact, every prestrategy is a strategy. The ab
ove mentioned approximations are implemented on a computer. We stress that,
since there is a computer implementation, the reader can use these techniq
ues to attack their own algebra problems. Thus the paper might bt of both p
ractical and theoretical interest to analysts, engineers, and algebraists.
Now we give the idea of a prestrategy. A prestrategy relies almost entirely
on two commands which we call NCProcess1 and NCProcess2. These two command
s are sufficiently powerful so that, in many cases, when one applies them r
epeatedly to a complicated collection of equations, they transform the coll
ection of equations into an equivalent but substantially simpler collection
of equations. A loose description of a prestrategy applied to a list of eq
uations is:
(1) Declare which variables are known and which are unknown. At the beginni
ng of a prestrategy, the order in which the equations are listed is not imp
ortant, since NCProcess1 and NCProcess2 will reorder them so that the simpl
est ones appear first.
(2) Apply NCProcess1 to the equations; the output is a set of equations, us
ually some in fewer unknowns than before, carefully partitioned based upon
which unknowns they contain.
(3) The user must select "important equations," especially any which solve
unknown, say x. (When an equation is declared to be important or a variable
is switched from being an unknown to being a known, then the way in which
NCProcess1 and NCProcess2 reorder the equations is modified.)
(4) Switch x to being known rather than unknown. Go to (2) above or stop.
When this procedure stops, it hopefully gives the "canonical" necessary con
ditions for the original equations to have a solution. As a final step we r
un NCProcess2 which aggressively eliminates redundant equations and partiti
ons the output equations in a way which facilitates proving that the necess
ary conditions are also sufficient. Many classical theorems in analysis can
be viewed in terms of solving a collection of equations. We have found tha
t this procedure actually discovers the classic theorem in a modest collect
ion of classic cases involving factorization of engineering systems and mat
rix completion problems. One might regard the question of which classical t
heorems in analysis can be proven with a strategy as an analog of classical
Euclidean geometry where a major question was what can bi constructed with
a compass and ruler. Here the goal is to determine which theorems in syste
ms and operator theory could be discovered by repeatedly applying NCProcess
1 and NCProcess2 (or their successors) and the (human) selection of equatio
ns which are important. The major practical challenge addressed here is fin
ding operations which, when implemented in software. present the user with
crucial algebraic information about his problem while not overwhelming him
with too much redundant information. This paper consists of two parts. A de
scription of strategies, a high-level description of the algorithms, a desc
ription of the applications to operator, matrix, and linear system engineer
ing theory, and a description of how one would use a strategy to "discover"
four different theorems are presented in the first part of the paper. Thus
, one who seeks a conventional viewpoint for this rather unconventional pap
er might think of this as providing a unified proof of four different theor
ems. Thr theorems were selected fur their diverse proofs and because: they
are widely known (so that many readers should be familiar with at least one
of them). The NCProcess commands use noncommutative Grobner Basis algorith
ms which have emerged in the last decade, together with algorithms for remo
ving redundant equations and a method for assisting a mathematician in writ
ing a (noncommutative) polynomial as a composition of polynomials. The read
er needs to know nothing about Grobner Basis to understand the first part o
f this paper. Descriptions involving the theory of Grobner Basis appear in
the second part of the paper. (C) 1999 Academic Press.