Information Technology Reference
In-Depth Information
is an
m
+1-ary primitive recursive function
s
n
such that
φ
s
n
(
f,
x
)
=
λ
).
Partial evaluation can be characterized as the research programme to prove
Kleene's theorem under the following conditions:
y
.f
(
x
,
y
1.
φ
s
n
(
f,
x
)
is supposed to run more eciently than
f
.
2.
f
is a program from a non-trivial programming language, not merely a re-
cursive function.
3. The construction of
φ
s
n
(
f,
x
)
is ecient, i.e., its runtime should be compara-
ble to compilation of
f
-programs.
In contrast to symbolic execution the result of a partial evaluator is not the
value of output variables, but another program. The known input (named
x
above) is also called
static input
while the general part
is called
dynamic
input
. The partial evaluator or
program specializer
is often named
mix
.Fig.1
gives a schematic overview of partial evaluation.
y
static input
x
target
program
p
partial
evaluator
mix
dynamic
input
y
specialize
d
pro-
gram
p
x
specialized
program
p
x
output
Fig. 1.
Partial evaluation schema [2]
The first efforts in partial evaluation date from the mid 1960s and were targeted
towards Lisp. Due to the rise in popularity of functional and logic programming
languages the 1980s saw a large amount of research in partial evaluation of such
languages. A seminal text on partial evaluation is the topic by Jones et al. [2].
There has been relatively little research on partial evaluation of
Java
.The
paper [14] summarizes the state-of-art until 2002 and discusses the
Java
special-
izer
JSpec
which worked by cross-translation to C as an intermediate language.
JSpec
seems to be no longer maintained. We found only one other (commercial)
1
, but its capabilities and underlying theory
Java
partial evaluator called
JPE
is not documented.
The application context of partial evaluation is rather different from that of
symbolic execution: in practice, partial evaluation is not only employed to boost
the eciency of individual programs, but often used in meta-applications such
as parser/compiler generation.
We illustrate the main principles of partial evaluation by a small control circuit
PL
program depicted in Fig. 2 on the left. The program approximates the value
of variable
y
to a given
threshold
with accuracy
eps
by repeatedly increasing
or decreasing it as appropriate.
1
http://www.gradsoft.ua/products/jpe_eng.html
