=Paper=
{{Paper
|id=Vol-3072/paper13
|storemode=property
|title=A Decidable Theory Treating Addition of Differentiable Real Functions
|pdfUrl=https://ceur-ws.org/Vol-3072/paper13.pdf
|volume=Vol-3072
|authors=Gabriele Buriola,Domenico Cantone,Gianluca Cincotti,Eugenio Omodeo,Gaetano Spartà
|dblpUrl=https://dblp.org/rec/conf/ictcs/BuriolaCCOS21
}}
==A Decidable Theory Treating Addition of Differentiable Real Functions==
https://ceur-ws.org/Vol-3072/paper13.pdf
A Decidable Theory Treating Addition
of Differentiable Real Functions? ??
Gabriele Buriola[0000−0002−1612−0985]1 ,
Domenico Cantone[0000−0002−1306−1166]2 ,
Gianluca Cincotti[0000−0001−8460−1708]2 ,
Eugenio G. Omodeo[0000−0003−3917−1942]3 , and
Gaetano T. Spartà[0000−0002−8993−5851]4
1
Dept. of Computer Science, University of Verona, Italy
gabriele.buriola@univr.it
2
Dept. of Mathematics and Computer Science, University of Catania, Italy
domenico.cantone@unict.it
3
Dept. of Mathematics and Earth Sciences, University of Trieste, Italy
eomodeo@units.it
4
Pontificia Università Gregoriana, Rome, Italy
g.sparta@unigre.it
Abstract. This paper enriches a pre-existing decision algorithm, which
in its turn augmented a fragment of Tarski’s elementary algebra with
one-argument real functions endowed with continuous first derivative. In
its present (still quantifier-free) version, our decidable language embodies
addition of functions; the issue we address is the one of satisfiability.
As regards real numbers, individual variables and constructs designating
the basic arithmetic operations are available, along with comparison rela-
tors. As regards functions, we have another sort of variables, out of which
compound terms are formed by means of constructs designating addition
and—outermostly—differentiation. An array of predicates designate var-
ious relationships between functions, as well as function properties, that
may hold over intervals of the real line; those are: function comparisons,
strict and non-strict monotonicity / convexity / concavity, comparisons
between the derivative of a function and a real term.
With respect to results announced in earlier papers of the same stream, a
significant effort went into designing the family of interpolating functions
so that it could meet the new constraints stemming from the presence
of function addition (along with differentiation) among the constructs of
our fragment of mathematical analysis.
Key words: Decidable theories, Tarski’s elementary algebra, Functions
of a real variable.
MS Classification 2010: 03B25, 26A06.
?
Copyright c 2021 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
??
We gratefully acknowledge partial support from project “STORAGE—Università
degli Studi di Catania, Piano della Ricerca 2020/2022, Linea di intervento 2”, and
from INdAM-GNCS 2019 and 2020 research funds.
2 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà
Introduction
This paper addresses the decision problem for a fragment of real analysis which,
besides the four operators ‘+’, ‘−’, ‘·’, ‘/’ of elementary real algebra, also pro-
vides predicates expressing strict and non-strict monotonicity, concavity, and
convexity of C 1 functions of one real variable over bounded or unbounded in-
tervals, as well as strict and non-strict comparisons ‘>’ and ‘>’ between real
numbers and between functions. Further primitive constructs available in the
language are: an operator designating pointwise addition of functions, and a dif-
ferentiation operator whose usage must be reasonably restrained.5 The language
under study, named RDF ∗ , is devoid of quantifiers; we reduce the satisfiability
problem regarding its formulas to the provability problem for purely existential
sentences in Tarski’s elementary algebra of real numbers, whose decidability is
known since long (cf. [17]). We can thus count upon improved versions of Tarski’s
original method.
Our decision method consists in preprocessing the given formula into an
equi-satisfiable quantifier-free formula of the elementary algebra of real numbers,
whose satisfiability can then be checked by means of Tarski’s decision method.
No direct reference to functions will appear in the target formula, each function
variable having been superseded by a collection of stub real variables; hence,
in order to prove that the proposed translation is satisfiability-preserving, we
must figure out a flexible-enough family of interpolating C 1 functions that can
accommodate a model for the source formula whenever the target formula turns
out to be satisfiable.
This paper is a sequel of [2] and [1]—hence, indirectly, of their antecedents
[4,6]. As for semantics, the language RM CF + studied in [2] differs from the
one treated here in that RM CF + refers to continuous functions whereas in
RDF ∗ functions are also required to be endowed with continuous derivative: in
consequence of this, as will be shown, a satisfiable RM CF + formula may cease
to be satisfiable in RDF ∗ .6 As for syntax, the sole significant difference between
RM CF + and RDF ∗ is that the former did not provide—as we now do—the
differentiation operator. A brief account of the decidability result proposed in
[2], with examples of usage of its language, can be found in [15, pp.165–177].
Our present language RDF ∗ differs from the language RDF + studied in
[1] in that its syntax is richer. We now have a construct for function addition,
whose treatment calls for an enhancement of the decision algorithm, to wit, an
enhanced reduction to Tarskian algebra. We thus get closer to a language where
one can prove the linearity of differentiation; in fact, our next extension will
permit multiplication of functions by numbers.
The paper is organized as follows. In Sec. 1 we introduce syntax and semantics
of the language of interest, and illustrate its expressive power—partly stemming
5
The differentiation operator D[ ] can only appear as the lead operator in a function
term g (which will then coincide with D[ f ]). The rationaleis that D[ f ] might not
designate a C 1 function when f does; then, e.g., D D[f] + f would be meaningless.
6
On the positive side, since the universe of functions for RM CF + is richer, any
formula judged valid by the decision algorithm for RM CF + is also valid in RDF ∗ .
A Decidable Theory Treating Addition of Differentiable Real Functions 3
from the ease with which useful derived constructs can be introduced—through
a gallery of small examples. In Sec. 2, we describe our decision algorithm: since
we cannot afford to specify it in detail, we exemplify its use by manually working
out an emulation of how it would process a specific, valid formula. Then Sec. 3
provides clues on the correctness of the proposed decision algorithm. To end, we
outline a comparison with related works, and draw conclusions.
1 The RDF ∗ theory
The augmented version RDF ∗ of the theory RDF of Reals with Differentiable
Functions, is an unquantified first-order theory dealing with reals and with real
functions of class C 1 of one real variable, namely functions with continuous first
derivative. The function symbols of RDF ∗ designate the basic operations of real
arithmetic, and pointwise addition and differentiation of functions. Its predicate
symbols designate: comparisons between reals, pointwise comparisons of func-
tions; strict and non-strict monotonicity, convexity, and concavity; comparisons
between first derivatives and real terms. This section introduces the language
underlying RDF ∗ , explains its intended meaning, and briefly illustrates its use.
Syntax and semantics
The language RDF ∗ has two infinite supplies of individual variables, belonging
to the respective sorts: numerical variables x, y, z, . . . and function variables
f, g, h, . . . . Numerical and function variables are supposed to range, respectively,
over the set R of real numbers and over the class C 1 (R) of continuous functions
with continuous derivative [the collection of functions which interests us]. Four
constants are also available:
– the symbols 0 and 1, designating the numbers 0 and 1;7
– the distinguished symbols +∞ and −∞, occurring only as ends of interval
specifications (see below).
We next specify the syntax of terms, atoms, and formulas for RDF ∗ :
Definition 1. Function terms, numerical terms, and interval specs
are so defined:
a.1) every function variable f is a function term;
a.2) if f and g are function terms, then f + g is a function term.
b.1) Numerical variables and the constants 0, 1 are numerical terms;
b.2) if s and t are numerical terms, the following also are numerical terms:
s + t , s − t , and s · t ;
7
As will turn out, the constants 0, 1 would be eliminable from our language without
loss of expressive power, since z = 0∧u = 1 is the sole solution to u = u·u > z ·z = z.
4 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà
b.3) if t is a numerical term and f is a function term, then
f(t) and D[f](t)
are numerical terms.8
c.1) An interval spec A is an expression of any of the forms
[e1 , e2 ] , [e1 , e2 [ , ]e1 , e2 ] , and ]e1 , e2 [ ,
where e1 stands for either a numerical term or −∞, and e2 for either a
numerical term or +∞;
c.2) we dub the “extended” numerical terms e1 , e2 of such an A the ends of
A. a
Definition 2. An atom of RDF ∗ is an expression of one of the forms
s=t, s>t,
(f = g)A , (f > g)A ,
Up(f)A , Strict Up(f)A ,
Down(f)A , Strict Down(f)A ,
Convex(f)A , Strict Convex(f)A ,
Concave(f)A , Strict Concave(f)A , (D[f] ./ t)A ,
where ./ ∈ {=, <, >, 6, > } and A stands for an interval spec.
A formula of RDF ∗ is any truth-functional combination of RDF ∗ atoms. a
For definiteness, we will construct the RDF ∗ formulas from RDF ∗ atoms by
means of the usual propositional connectives ¬, ∧, ∨, →, ↔.
The semantics of RDF ∗ revolves around the designation rules listed in our
next definition, with which any truth-value assignment for the formulas of RDF ∗
must comply.
Definition 3. An assignment for RDF ∗ is a mapping M whose domain con-
sists of all terms and formulas of RDF ∗ , satisfying the following conditions:
0. M 0 and M 1 are the real numbers 0 and 1.
1. For each numerical variable x, M x is a real number.
2. For each function variable f , (M f ) is an everywhere defined differentiable
real function of one real variable, endowed with continuous derivative.
3. For each function term of the form f + g, the image M (f + g) (r) of any
real number r is (M f)(r) + (M g)(r).
4. For each numerical term of the form t1 ⊗ t2 with ⊗ ∈ {+, −, ·}, M (t1 ⊗ t2 )
is the real number M t1 ⊗ M t2 .
8
Throughout, s, t and f, g stand, respectively, for numerical terms and function terms
while x, y, z and f, g, h stand, more specifically, for numerical variables and function
variables.
A Decidable Theory Treating Addition of Differentiable Real Functions 5
5. For each numerical term of the form f(t), M (f(t)) is the real number
(M f)(M t); for each numerical term D[f](t), M (D[f](t)) is the real number
D[(M f)](M t).
6. For each interval specification A, M A is an interval of R of the appropriate
kind, whose endpoints are the evaluations via M of the ends of A.9
For example, when A =]t1 , t2 ], then M A =]M t1 , M t2 ].
7. Truth values are assigned to formulas of RDF ∗ according to the following
rules, where s and t stand for numerical terms and f, g for function terms:
a) s = t (respectively s > t) is true iff M s = M t (resp. M s > M t) holds;
b) (f = g)A is true iff (M f)(x) = (M g)(x) holds for all x in M A;
c) (f > g)A is true iff (M f)(x) > (M g)(x) holds for all x in M A;
d) (D[f] ./ t)A , with ./∈ {=, <, >, 6, >}, is true iff D[(M f)](x) ./ M t holds
for all x in M A;
e) Up(f)A (respectively Strict Up(f)A ) is true iff (M f) is a monotone non-
decreasing (resp. strictly increasing) function in M A;
f) Convex(f)A (respectively Strict Convex(f)A ) is true iff (M f) is a convex
(resp. strictly convex) function in M A;
g) the truth values of Down(f)A , Concave(f)A , Strict Down(f)A , and
Strict Concave(f)A are defined in close analogy with items e) and f);
h) the truth value which M assigns to a formula whose lead symbol is any
of ¬, ∧, ∨, →, ↔ complies with the usual semantics of the propositional
connectives.
An assignment M is said to model a set Φ of formulas when M ϕ is true
for every ϕ in Φ. a
Definition 4 (Derived symbols). In light of the above semantics, we tacitly
enrich our language, much as in [1], with derived dyadic and triadic comparators
involving numerical terms t1 , t2 , and t3 ; namely t1 . t2 and t1 ./ t2 /t3 , where
. ∈ {6=, <, 6, >} and ./ ∈ {=, <, >, 6, >}.
Additional relators intermixing function terms and numerical terms, e.g. the
construct (D[f] 6= t)A , can also be introduced by means of shortening definitions.
Among others, any function of the form x 7→ q ·x+q 0 , with q and q 0 fixed rational
numbers, can be characterized by means of a formula as in [1]; in particular, we
may define h = 0 ↔Def (h = h+h)]−∞,+∞[ . Thanks to the availability of function
addition, one can now also specify the multiplication of a function f by any fixed
rational number ± m n : in fact, for n, m positive integers, we can define:
n times m times
z }| { z }| {
g=m
n · f ]−∞,+∞[ ↔Def g + ··· + g = f + ··· + f ,
m
g = − n · f ]−∞,+∞[ ↔Def g + · · · + g + f + · · · + f = 0. a
| {z } | {z }
n times m times
9
It goes without saying what is meant when M is undefined at either end of A
(actually, M (−∞) and M (+∞) are undefined).
6 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà
A gallery of examples heading to Cauchy’s mean value theorem
In sight of becoming able to express the classical Cauchy’s mean value theorem—
which calls, alas, for a syntactical extension of RDF ∗ —, we formulate in RDF ∗
many basic facts of real analysis:
I (D[f ] = t)[a,b] → Linear(f )[a,b]
If f is a function with constant derivative in the interval [a, b], then it will be
linear in the same interval. With a slight abuse of notation we can improve
the result as (D[f ] = f (b)−f
b−a
(a)
)[a,b] ↔ Linear(f )[a,b] , where an equivalence
holds when the derivative is equal to the difference quotient.
I (D[f ] > 0)]a,b[ → Strict Up(f )[a,b]
If f is a real function endowed with continuous derivative f 0 , and f 0 (x) > 0
holds for all x ∈ ]a, b[ , then f is monotone increasing in [a, b].
I b > a ∧ (b − a) · t = f (b) − f (a) → ¬ (D[f ] 6= t)]a,b[
If f is a real function endowed with continuous derivative f 0 , then to any
interval ]a, b[ with a < b there belongs a c such that f 0 (c) = f (b)−f
b−a
(a)
holds.
This is a weak version of Lagrange’s mean value theorem.
I [ Up(f )A ∧ Strict Up(g)A ] → Strict Up(f + g)A
If f and g are, over the interval A, respectively monotone non-decreasing
and monotone increasing, their sum f + g is monotone increasing on A.
I [ Up(f )A ∧ f + g = 0 ] → Down(g)A
If f is an increasing function all over the interval A, its additive inverse g
decreases over A.
I D[f ] = r A ∧ D[g] = s A → D[f + g] = r + s A
If the graphs of f and g, restricted to A, are straight lines with slopes r and
s, then the graph of f + g restricted to A is a straight line with slope r + s.
Moreover, when the interval A reduces to a single point, this formula states
the additive property of derivative over all R.
I [ Convex(f )A ∧ Convex(g)A ∧ (h + h = f + g)A ] → Convex(h)A
If f and g are two convex functions on A, also their average h = f +g
2 is
convex on A.
I [ (f > k)A ∧ (g > k)A ∧ (h + h = f + g)A ] → (h > k)A
If f and g both exceed the function k on A, so does in its turn their average.
Every instance of the formula schemes shown before can be validated by
means of the decision algorithm that will be presented. Actually, the first three
could also be handled by the simpler decision algorithm tailored for RDF + (cf.
[1]), since they do not involve sums of functions.
A Decidable Theory Treating Addition of Differentiable Real Functions 7
As announced in the Introduction, a satisfiable RM CF + formula may cease
to be satisfiable in RDF ∗ . Such a formula is (see [2]):
Convex(f )[0,1] ∧ Convex(f )[1,1+1] ∧ f (0) = f (1 + 1) = 0 ∧
f (1) = 1 ∧ Concave(f )[0,1+1] ;
as a matter of fact, no real function satisfying its subformula
Convex(f )[0,1] ∧ Convex(f )[1,1+1] ∧ f (0) = f (1 + 1) = 0 ∧ f (1) = 1
belongs to the C 1 class.
2 Clues on the decision algorithm
Establishing that an RDF ∗ formula ψ is valid amounts to establishing that its
negation ¬ψ is not satisfiable; moreover, satisfying ¬ψ amounts to satisfying
one of the disjuncts of its disjunctive normal form, hence the key issue concern-
ing the decidability of RDF ∗ is: how can we determine whether or not a given
conjunction of RDF ∗ literals (that is, RDF ∗ atoms and negations thereof) is
satisfiable? Via routinary flattening techniques and in view of some basic proper-
ties of C 1 , we can restate each instance of this problem as the one of determining
the satisfiability of an arbitrary conjunction ϕ0 of atoms of the forms
z =x+y , (h = f + g)A , Strict Up(f )A , Convex(f )A ,
z =x·y , (f = g)A , Strict Down(f )A , Concave(f )A ,
x>y, (f > g)A , (D[f ] ./ z)A , Strict Convex(f )A ,
z = f (x) , z = D[f ](x) , Strict Concave(f )A
and of literals which are the complements of atoms of these forms that involve
an interval spec. Here A stands for an interval spec whose ends can be numerical
variables, −∞, or +∞; as ever, x, y, z stand for numerical variables and f, g, h
stand for function variables. Through a process furcating at various points, ϕ0
will undergo a series ϕ0 ; ϕ1 ; ϕ2 ; ϕ3 ; ϕ4 = ϕ b of transformations, ending
in a formula ϕ b where function variables do no longer occur, so that ϕ b can be
tested for satisfiability by means of Tarski’s celebrated decision algorithm [17,7].
The proper functioning of this method relies on certain assumptions about the
detailed structure of ϕ, easy to ensure, which we must fly over.
The transformations ϕi−1 ; ϕi (i = 1, 2, 3, 4) serve the following purposes:
1. Subdivide into cases each literal of the form (f > g)A whose A is not of the
form [v, w]. E.g., (f > g)]v,w] offers two choices: f (v) > g(v), f (v) = g(v).
2. Substitute every negative literal with an implicit existential assertion. E.g.,
¬Strict Up(f )[v,w] will bring into play new variables x, y, x0 , y 0 subject to
constraints v 6 x < x0 6 w ∧ y = f (x) ∧ y 0 = f (x0 ) ∧ y > y 0 .
3. With certain salient variables vj in the domains of the functions designated
by the function variables in ϕ0 , associate new variables yjf , tfj (one for each
function variable f ) subject to the constraints yjf = f (vj ), tfj = D[f ](vj ).
8 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà
4. Get rid of all literals involving function variables, whose graphs are already
outlined by the variables yjf , tfj introduced above. This elimination phase
calls for the introduction of new variables subject to suitable algebraic con-
straints.
The decision algorithm at work
Our decision algorithm for RDF ∗ cannot be specified in full in these few pages; to
convey a feel of how it works, we consider a paradigmatic formula ψ, and carry
out one by one the key transformations leading from ψ to a formula directly
submittable to Tarski’s algorithm for elementary real algebra.
Suppose that we want to establish whether the formula ψ ,
h i
D[f ] = r [a,b] ∧ D[g] = s [a,b] → D[f + g] = r + s [a,b] ,
is true under every value assignment; equivalently, we can check whether its
negation ¬ψ is unsatisfiable. After introduction of convenient stub variables h
and p, this negation becomes the following formula ϕ:
D[f ] = r [a,b] ∧ D[g] = s [a,b] ∧ h = f + g [a,b] ∧ ¬ D[h] = p [a,b] ∧ p = r + s .
Then ϕ undergoes the following transformations:
1. Behavior at the ends: Generally speaking, function-comparison literals of the
form (f > g)A must be bestowed special care, possibly leading to a subcase
analysis. Since no such literal appears in our ϕ, this phase produces ϕ1 := ϕ .
2. Negative clause removal: This phase removes the negative literal and obtains
ϕ2 from ϕ1 by substituting the conjunction a 6 x 6 b ∧ y = D[h](x) ∧ y 6= p
for ¬ D[h] = p [a,b] inside it.
3. Explicit evaluation of function variables: This phase introduces a new variable
to designate each function-application term `(v), where ` stands for a func-
tion variable of ϕ and v for one of its so-called ‘domain’ variables. More pre-
cisely, for each function variable f and each domain variable a, we introduce
two new numerical variables yaf , tfa and two literals f (a) = yaf , D[f ](a) = tfa
evaluating, respectively, the function f and its derivative f 0 in a.
To describe evaluation more transparently, let us do the renaming: a ;
v1 , x ; v2 , b ; v3 . From the previous formula ϕ2 , we get the following ϕ3 :
D[f ] = r [v1 ,v3 ] ∧ D[g] = s [v1 ,v3 ] ∧ h = f + g [v1 ,v3 ] ∧
v1 6 v2 6 v3 ∧ D[h](v2 ) = y ∧ p=r+s ∧ y 6= p ∧
h(v1 ) = y1h ∧ h(v2 ) = y2h ∧ h(v3 ) = y3h ∧
D[h](v1 ) = th1 ∧ D[h](v2 ) = th2 ∧ D[h](v3 ) = th3 ∧ y = th2 ∧
f (v1 ) = y1f ∧ f (v2 ) = y2f ∧ f (v3 ) = y3f ∧
f f f
D[f ](v1 ) = t1 ∧ D[f ](v2 ) = t2 ∧ D[f ](v3 ) = t3 ∧
g(v1 ) = y1g ∧ g(v2 ) = y2g ∧ g(v3 ) = y3g ∧
D[g](v1 ) = t1 ∧ D[g](v2 ) = t2 ∧ D[g](v3 ) = tg3 .
g g
A Decidable Theory Treating Addition of Differentiable Real Functions 9
4. Elimination of function variables: This final phase removes all literals still
containing function variables. We get rid of them by suitable replacements
involving algebraic conditions, such as the difference quotient
for literals
regarding derivatives. For example, the literal D[f ] = r [v1 ,v3 ] becomes the
y f −y f y f −y f
conjunction tf1 = r ∧ tf2 = r ∧ tf3 = r ∧ v22 −v11 = r ∧ v33 −v22 = r, where the tfi ’s
yf −y f
represent salient values of the derivative and vi+1 i
i+1 −vi
= r the corresponding
difference quotients. To make the manner we eliminate the “function
literals”
clearer we mark with the same color the two literals D[f ] = r [v1 ,v3 ] , h =
f + g [v1 ,v3 ] and their transformations.
At the end we obtain an equisatisfiable Tarskian formula we can then test
for satisfiability by Tarski’s algorithm.
From the previous formula ϕ3 we get the following final formula ϕ4 :
v 1 6 v2 6 v3 ∧ p=r+s ∧ y 6= p ∧ y = th2 ∧
y2f −y1f y f −y f
tf1 = r ∧ tf2 = r ∧ tf3 = r ∧ v2 −v1 = r ∧ v33 −v22 = r ∧
y2g −y1g y g −y g
tg1 = s ∧ tg2 = s ∧ tg3 = s ∧ v2 −v1 = s ∧ v33 −v22 = s ∧
y1h = y1f + y1g ∧ y2h = y2f + y2g ∧ y3 = y3f + y3g
h
∧
th1 = tf1 + tg1 ∧ th2 = tf2 + tg2 ∧ th3 = tf3 + tg3 .
In particular, the unsatisfiability of this last formula is given by the conjunction:
y = th2 ∧ th2 = tf2 + tg2 ∧ tf2 = r ∧ tg2 = s ∧ p = r + s ∧ y 6= p.
3 Correctness of the algorithm
In order to prove the correctness of the algorithm, it is enough to show that each
one of the (terminating) transformations ϕ ; ϕ1 , ϕ1 ; ϕ2 , ϕ2 ; ϕ3 , ϕ3 ; ϕ4
is satisfiability preserving. Regarding the first three of them (behavior at the
endpoints, negative-clause removal, explicit evaluation of function variables),
this emerges as a rather straightforward fact.
We must focus on the equisatisfiability of the formulas ϕ3 and ϕ4 , because
the transformation ϕ3 ; ϕ4 is less transparent than the previous ones: we are, in
fact, comparing a formula whose predicates regard the behavior of functions in
real intervals with another one which only involves relations between numerical
variables. Let us sketch the idea behind the proof (the full proof is unaffordably
long for a conference paper and relies on various propositions of elementary real
analysis). As usual, the proof consists of two parts: soundness and completeness.
Recall that ϕ4 is obtained from ϕ3 by adding some formulas that involve only
numerical variables, and by removing all predicates which refer to function vari-
ables.
Soundness: If a model exists for ϕ3 , it can be extended to a model that also
verifies the numerical formulas added in ϕ4 , since these formulas reflect proper-
ties of the functions in ϕ3 at specific points of real intervals.
10 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà
Completeness: Conversely, if there exists a model for ϕ4 , it is possible to
extend it to ϕ3 by interpreting the function variables with suitable interpolating
functions. In the proof, to perform the interpolation we resort to a family of
functions, closed under addition. Each function is constructed by combination
of pieces, each of which results from a linear component affected by a so-called
‘perturbation’. In its turn, each perturbation stems from a parabola. On the
one hand, we use the linear components to satisfy pointwise properties, such as
f (vi ) = yif ; on the other hand, we use parabolic perturbations to satisfy con-
straints on derivatives, such as D[f ](vi ) = tfi . Closure under addition of the
family of interpolating functions ensures proper treatment of literals involving
the sum of functions: actually, if (h = f + g)A is one such literal and F, G, H are
the functions interpreting the symbols f, g, h, we must require H = F + G. This
non trivial condition forced us to shift from the original approach presented in
[1] (where the perturbations were based on exponential functions) to the present
one, in which the perturbation of each interpolating segment originates from the
envelope of two straight lines in the interval 0, 21 . These novel interpolating
functions, and their derivatives, comply with the properties at points and on
real intervals dictated by ϕ3 .
Sample function resulting from perturbated linear segments
To shed light upon the nature of these interpolating functions, here we give a
very simple example. Suppose that we must cope, at the end of the decision
algorithm, with the following quantifier-free formula of the elementary algebra
of real numbers:
v1 = 0 ∧ v2 = 1 ∧ y1f = 0 ∧ y2f = 3 ∧ tf1 = 1 ∧ tf2 = 0 .
Driven by this satisfiable formula, we want to construct an appropriate C 1 func-
tion f . The interpolation constraints which f must comply with are pointwise
conditions, two of which regard its derivative:
f (0) = 0, f (1) = 3, f 0 (0) = 1, f 0 (1) = 0 .
We can meet the first two with a linear segment, namely r(x) = 3 x, but in order
to satisfy the conditions on the derivative we need a suitable perturbation of this
linear segment. The basic elements out of which we build our perturbations are
envelope functions defined on the interval 0, 21 , of the form:
n
1
G[k, θ1 , θ2 ](x) := (1−4k)2 (1 − 4k)[θ2 −2k (θ1 + θ2 )]x +
√ p o
−2k(θ1 − θ2 )(1 − 2k) 2k − 2 2k 2 + (1 − 4k) x ,
where k is a shrinking parameter involved in the completeness proof and θ1 , θ2
represent the values of the derivative at endpoints. Starting with these basic
elements and through reflections, translations and dilations, we can define all
required perturbations.
A Decidable Theory Treating Addition of Differentiable Real Functions 11
In the example we are considering, after entering the right values for the deriva-
tive, we obtain the function
( √
3x + 49 x + 32
17
in 0, 12
1 − 1 + 16x
f (x) := √
3x + 11 23 1
4 (x − 1) + 32 ( 17 − 16x − 1) in 2 , 1 ,
where 3 x is the linear part and the rest specifies the parabolic perturbation.
The graph of this function (whose first half falls directly under G[k, θ1 , θ2 ](x),
while the second half results from that scheme through appropriate manipula-
tions) can be seen below.
3
3*x
f(x)
2.5
2
1.5
1
0.5
0
0 0.2 0.4 0.6 0.8 1
Fig. 1. Graph of the interpolating function with f (0) = 0, f (1) = 3, f 0 (0) = 1, f 0 (1) = 0.
4 Related works and complexity issues
The decidability of the theory RDF ∗ treated above is a follow-up of a series of
previous results, regarding the theories RM CF , RM CF + , RDF , and RDF +
[4,2,6,3,1]. A general survey on those results, save the last, can be found in [5],
where other decidability results on real analysis are also treated, in particular
the FS theory [10,11].
Since the decidability of RDF ∗ is obtained via an explicit algorithm, some
complexity issues are worth being discussed here. Tarski’s decision method en-
ters into ours, hence our algorithm inherits its complexity as a lower bound. The
first complexity amelioration w.r.t. Tarski’s historical result is due to Collins
12 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà
[7], whose procedure has doubly exponential complexity relative to the number
of variables occurring in the sentence (or just exponential, if the endowment
of variables is finite and fixed). A refinement of this result was achieved with
Grigoriev’s algorithm [12], applicable to sentences in prenex normal form, whose
complexity is doubly exponential relative to the number of quantifier alterna-
tions. If we merely focus on the existential theory of reals, the known decision
algorithms have a complexity at best exponential relative to the number n of
variables [9]; however, if one fixes beforehand how many variables can be used,
then the algorithmic complexity becomes polynomial [13].
Finally, while Tarski himself showed that decidability of his full elementary
algebra of real numbers [17] would be disrupted if the language were enriched
with certain real functions, in particular sin x, Richardson proved in [14] the
undecidability of the existential theory of reals extended with the numbers log 2
and π, and with the functions ex , sin x.
5 Conclusions and Future Works
This article has presented a decision algorithm for a syntactically delimited frag-
ment, RDF ∗ , of real analysis. RDF ∗ extends the unquantified part of Tarski’s
elementary algebra EAR of real numbers with variables designating functions
of a real variable endowed with a continuous derivative. After showing how to
add derived relators and how to specify common properties of real functions and
theorems about them in RDF ∗ , we have discussed an algorithm that translates
a generic formula ϕ of RDF ∗ into an equisatisfiable formula ψ of EAR; rather
than specifying the algorithm in gory detail, we have illustrated its functioning
through a concrete example. Proving the correctness of the decision algorithm
amounts to showing the equisatisfiability of formulas ϕ and ψ, and we have
sketched the salient points of this correctness proof. The proof relies upon the
construction of a set of C 1 functions rich enough to enable the modeling of any
satisfiable RDF ∗ formula: each function results from smoothly connecting linear
segments perturbated by means of parabolic deformations.
While working on the algorithm we glimpse further extensions. The nearest two
amount to a product operator and multi-variable functions. The product oper-
ator concerns the assembly of new function terms by multiply function terms
and numerical terms. This new construct will enable us to treat literals of the
form f = tg A and paves the way to state stronger analytic theorems, such as
Cauchy’s mean value theorem. Whereas this “syntactical scalar product” seems
easily treatable, combining product of two function terms, such as h = f · g with
function sum is likely to disrupt decidability (much as Presburger’s vs. Peano’s
arithmetic [9, p.4]), or required at least deep changes in the algorithm. By multi-
variable functions we mean the possibility to treat continuous real functions with
multiple arguments, such as f : Rn → R. A similar enrichment has already been
introduced for the RM CF in [4].
A Decidable Theory Treating Addition of Differentiable Real Functions 13
References
1. Buriola G., Cantone D., Cincotti G., Omodeo E.G., Spartà G.T., A decidable
theory of differentiable functions with convexities and concavities on real intervals.
In Francesco Calimeri, Simona Perri, and Ester Zumpano, editors, Proceedings of
the 35th Italian Conference on Computational Logic - CILC 2020, Rende, Italy,
October 13-15, 2020, volume 2710 of CEUR Workshop Proceedings, pages 231–247.
CEUR-WS.org, 2020.
2. Cantone D., Cincotti G., Gallo G., Decision algorithms for fragments of real analy-
sis. I. Continuous functions with strict convexity and concavity predicates. J. Symb.
Comput., 41(7):763-789, 2006.
3. Cantone D., Cincotti G., Decision algorithms for fragments of real analysis. II.
A theory of differentiable functions with convexity and concavity predicates. List
of CILC 2007 papers, 14 pp., 2007. https://www.programmazionelogica.it/
wp-content/uploads/2014/10/cilc2007.pdf
4. Cantone D., Ferro A., Omodeo E.G., Schwartz J.T., Decision algorithms for some
fragments of analysis and related areas. Comm. Pure Appl. Math., 40(3):281-300,
1987.
5. Cantone D., Omodeo E.G., Spartà G.T., Solvable (and unsolvable) cases of the
decision problem for fragments of analysis. Rend. Istit. Mat. Univ. Trieste, 44:313-
348, 2012.
6. Cincotti G., Decision algorithms for fragments of real analysis and graph theory,
Ph.D. Thesis, Università degli Studi di Catania, Catania, Italy, ix+136 pp., 2000.
7. Collins G., Quantifier elimination for real closed fields by cylindrical algebraic de-
composition. In: Second GI Conference on Automata Theory and Formal Lan-
guages, LNCS Vol.33, Springer-Verlag, Berlin, 1975.
8. Ferro A., Omodeo E.G., Schwartz J.T., Decision procedures for elementary sublan-
guages of set theory. I. Multi-level syllogistic and some extensions, Comm. Pure
Appl. Math, 33(5):599–608, 1980.
9. Fisher M. J. and Rabin M. O., Super-exponential complexity of Presburger arith-
metic. Complexity and Computation, Vol. VII, SIAM-AMS, Philadelphia (1974),
27–41.
10. Friedman H. and Seress Á., Decidability in elementary analysis. I, Adv. Math. 76
(1989), no. 1, 94–115.
11. Friedman H. and Seress Á., Decidability in elementary analysis. II, Adv. Math. 79
(1990), no. 1, 1–17.
12. Grigoriev D., Complexity of deciding Tarski algebra, J. Symbolic Comput. 5 (1988),
65–108.
13. Renegar J., A faster PSPACE algorithm for deciding the existential theory of the
reals, 29th Annual Symposium on Foundations of Computer Science (FOCS 1988,
Los Angeles, Ca., USA), IEEE Computer Society Press, Los Alamitos (1988), pp.
291–295.
14. Richardson D., Some undecidable problems involving elementary functions of a real
variable, J. Symbolic Logic 33 (1968), 514–520.
15. Schwartz JT, Cantone D, Omodeo EG. Computational logic and set theory: Ap-
plying formalized logic to analysis. Springer-Verlag, 2011. ISBN 978-0-85729-807-2.
https://doi.org/10.1007/978-0-85729-808-9. Foreword by M. Davis.
16. Tarski A., The completeness of elementary algebra and geometry, Institut Blaise
Pascal, Paris, 1967, iv+50 pp. (Late publication of a paper which had been sub-
mitted for publication in 1940)
14 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà
17. Tarski A., A decision method for elementary algebra and geometry, prepared for
publication by J.C.C McKinsey, U.S Air Force Project RAND, R-109, the RAND
Corporation, Santa Monica, 1948, iv+60 pp.; a second, revised edition was pub-
lished by the University of California Press, Berkeley and Los Angeles, CA, 1951,
iii+63 pp.