100
Fund. Thm. of Algebra
functions are simply slices of the bivariate function
x
y
.
In ACL2(r), we introduce the continuous function
ccfn
using
encapsulate
as
(ccfn context
z)
, where the argument
z
is the one that is allowed to vary, whereas
context
is the argument that is held
fixed. The nonstandard definition of continuity that we use here requires that close points be mapped to
close values, but only for standard
z
. Similarly, we require that close points are mapped to close values
only when both
z
and
context
are standard.
The
context
argument plays an important role, which can be illustrated by the continuity of poly
nomials. Consider, for example, a proof that the function
x
n
is continuous. This would appear to be easy
to prove by induction as follows:
1.
x
0
is a constant function, so it is definitely continuous.
2.
x
n
=
x
n

1
·
x
, and
x
n

1
is continuous from the induction hypothesis, and so is the product of con
tinuous functions.
However, this does not work. The formal definition of continuity uses the nonclassical notions of
close
:
standard
(
x
)
∧
close
(
x
,
x
0
)
→
close
(
x
n
,
x
n
0
)
. But ACL2(r) restricts induction on nonclassical functions to
standard values of the arguments. In this particular case, we could prove that
x
n
is continuous, but only
for standard values of
n
, as was done in [10].
Setting that aside for now, we can imagine what would happen if we could establish (somehow) that
complex polynomials are continuous. The next step in the proof would be to show that since
p
(
z
)
is
continuous in the complex plane, then

p
(
z
)

is continuous from
C
to
R
, and this could be done by
functionally instantiating the previous result about norms of continuous functions. Once more, however,
we run into a major complication. The problem is that we want to say this about
all
polynomials, not
just about a specific polynomial
p
. For example, we could use this approach to show that the norm of the
following polynomial is continuous:
(defun
p(z)
(+
1
(*
#c(0
1)
z)
(*
3
z
z)))
But that would lead to a proof that the polynomial
p
has a root, not that all polynomials have roots. To
reason about all polynomials, we use a data structure that can represent any polynomial and an evaluator
function that can compute the value of a given polynomial at a given point. For example, the polynomial
above is represented with the list
(1 #c(0 1) 3)
, and the function
evalpolynomial
is defined so
that
(evalpolynomial '(1 #c(0 1) 3) z) = (p z)
. But we cannot use functional instantiation
to show that the norm of
evalpolynomial
is continuous, because the formal statement of continuity
uses the nonclassical notion of
close
. ACL2(r) restricts functional instantiation so that pseudolambda
expressions cannot be used in place of functions when the theorem to be proved uses nonclassical
functions.
It should be noted that both of these restrictions are necessary!
For example,
x
n
is "obviously"
continuous, but what happens when
n
is large? Suppose that
x
=
1
+
ε
, where
ε
is small, so that 1 and
1
+
ε
are close. From the binomial theorem,
(
1
+
ε
)
n
=
1
+
n
ε
+
···
. The thing is that if
n
is large,
n
ε
is not necessarily small. For instance, if
n
=
1
/
ε
, then
n
ε
=
1, and
(
1
+
ε
)
n
>
2, so it is not close to
1
n
=
1. Yes,
x
n
is continuous, but the nonstandard definition of continuity only applies when
x and n
are
standard.
Similarly, the restriction for pseudolambda expressions is crucial. Consider, for example, the theo
rem that
f
(
x
)
is standard when
x
is standard. This is true, but we could not use it to show that
x
+
y
is
standard when
x
is standard by functionally instantiating
λ
x
.
x
+
y
for
f
. The proposed theorem is just
not true when, for example,
x
=
0 and
y
=
ε
.