Limits of
Computation
10 – Partial evaluation & self-referencing programs Bernhard Reus
1
So far …
• … we have seen how programs can be encoded as objects to be used as input to other programs.
• Example: self-interpreter to show semi- decidability of Halting Problem.
2
Question:
Can we write a Java program that prints itself or a While program that returns its own AST (without using its input)?
3
•Other uses of programs-as-data
public class Quine {
public static void main(String[] args) {
char q = 34; // Quotation mark character String[] l = { // Array of source code “public class Quine”,
“{“,
Partial Evaluation (Kleene’s
S-m-n Theorem)
•
” public static void
” {“,
” charq=34;
” String[] l = {
” “,
main(String[] args)”,
// Quotation mark character”, // Array of source code”,
Use of partial evaluation for Optimisation and Compiler Generation
” };”,
” for(inti=0;i < 6; i++)
" System.out.println(l[i]);",
" for(int i = 0; i < l.length; i++)
" System.out.println(l[6] + q + l[i] + q + ',');",
•
Recursion Theorem)
// Print opening code", // Print string array", // Print this code",
Self-referencing Programs (Kleene’s
" for(int i = 7; i < l.length; i++)
" System.out.println(l[i]);",
" }", "}",
•
Use of Recursion Theorem for Recursion
};
for(int i = 0; i < 6; i++)
System.out.println(l[i]); for(int i = 0; i < l.length; i++)
// Print opening code
// Print string array
System.out.println(l[6] + q + l[i] + q + ',');
for(int i = 7; i < l.length; i++) System.out.println(l[i]);
} }
// Print this code
an interesting Java program: what does it do?
4
THIS TIME
cations in its own right:
10.1 The S-m-n Theorem
The so-called “S-m-n” theorem, sometimes also called parameterization theorem,
can be regarded as justification for partial evaluation as an optimisation technique.
The reasons for the strange name will be explained soon. In terms of metaprogram-
Simple Version of S-m-n Theorem
ming (i.e. programming with programs) the theorem basically states the existence
of specialisers.
Theorem 10.1 (S-1-1 Theorem). For any programming language L with pairing
and programs-as-data there exists a program spec such that rJspecKL(p,s)zL(d) = JpKL(s,d)
(_,_) notation for generic pairing
both inputs as pair
where ( , ) denotes pairing for a general language L.3
program
with 2 inputs partial
remaining
This program spec is a specia(1lsits)eirnpfurtom L(2ntdo) Linpaust first mentioned in Chap. 6. (as pair)
Recall from Chap. 6 that a specialiser takes a program and some of its input and
It can be generalised to programs with m+1
p•roduces a new program that needs “fewer input parameters”. The above equation
(not just 2) input and providing n concrete
specifies the resulting program’s behaviour. The specialiser “applies” the one argu-
menvtatolutehse(gnivoetnjupsrotg1r)amthuthsathreqnuairmesetw(Kolaeregnuem’se)nts, using it as its first argument. IndoSi-nmg-snoTithceonrsetrmuc.tstheresultprogramwithoneremainingargument,otherwise
preserving the program’s semantics. One might say the specialiser is “freezing the
first argument of the given program”.
We can easily prove the S-1-1 theorem for L = WHILE by simply constructing
Stephen Cole Kleene (1909-1994) American mathematician
(also did regular expressions!)
the program specWHILE as given in Fig. 10.1. The program in Fig. 10.1 performs the 5
specialisation, but it does not do any partial evaluation as it does not look into the code (kept in variable code) of the given program. Such optimisations by partial evaluation are sometimes possible.
Imagine a program p to be specialised that has two arguments encoded by in- put variable XY where X has been assigned hd XY and Y been assigned hd tl
XY using the standard list encoding of tuples. After p has been “specialised” with 3 In WHILE we know how to express pairing, namely as a list via p[ , ]q since we know the
datatype is D.
S-m-n describes Specialiser
118
• The resulting program spec is a specialiser (that takes programs as input and returns a new program).
• The concrete code for spec is relatively straightforward and will be given in notes / as program on Canvas site.
• The partial input provides opportunities for optimisations in the code of program p.
6
The so-called “S-m-n” Theorem, sometimes also ca v
b r
is D.
(
H h
u t
e . p
o
c u t s
u
(
rem, can be regarded as justification for partial e technique. The reasons for the strange name will of metaprogramming (i.e. programming with prog states the existence of specializers.
S-1-1 Theorem: Optimisation Example
FmminglanguageLwithpairingan
... read XY{ A:=7
} write A
or any progra
p read XY {
X := hd XY;
xists a program
Y := hd tl XY;
A :=
}
write A
tes pairing.3 XY:= [3,XY];
newp read XY
spec is a spe X:= hd XY;
s that might
Y:= hd tl XY;
A:=
e argument to
write A
e
p
spec such that
r L zL L
JspecK (p,s) (d) = JpK where ( , ) deno
cialiser from L to L. be possible with t
the program that req
as its first argument, and produces a program wi
otherwise preserving the program’s semantics. On
“freezing the first argument of the given program” We can prove this theorem for L = While by sim
specWhile as follows in WIDE notation:
t and sec
[p,3]
This program
X:= 3;
any optimisation
A:=
“applies” the on
A := 7
7
read PS
// PS = (P.S) so compute firs
P:= hd PS;
“Efficient program
S:= tl PS;
// P = ((var i) C (var j)) so inputVar := hd P;
specialisation
code := hd tl P; outputVar := hd tl tl P;
=
// compute specialised newPr
partial evaluation”
// assignment “inputVar := c expression := (list “cons” ( newAssign := (list “:=” input newCode := (list “;” newAssig
newProgram := (list inputVar
8
write newProgram
destruct
ogram whi
ons S inp
list “quo
Var expre
n code);
newCode o
3In WHILE we know how to express pairing, namely as
Self-referencing Programs
• Can we write programs that refer to their own source or Abstract syntax tree?
• Can we give them a well-defined semantics?
• For instance, a program that prints its own source or returns its own AST?
• Try it, it’s not that simple!! What is the problem here?
9
Acceptable Prog. Language
A programming language as discussed before, defined by syntax, data type, and semantics, having also programs- as-data and pairing, is called “acceptable” iff
• it has a universal program
• it has specialisers (S-m-n theorem holds)
• all functions computed by Turing machines or While-programs are also computed by one of its programs.
10
putability and complexity we leave the exploration of partial evaluation to the reader
For instance, to compute the factorial of n, self application leads to a self-interpreter
and swiftly move on.
10.2 Kleene’s Recursion Theorem
The following theorem guarantees the existence of self-referencing programs, that
we can also call “recursive” since with the help of self-reference one can implement
Recursion Theorem
recursion. This will be discussed in more detail later. Let us first state Kleene’s
theorem[5].Recalltheforagenericlanguageweusenotation(, )forpairs.
Theorem 10.2 (Kleene’s Recursion Theorem [5]). Let L be an acceptable pro- gramming language. For any L-program p, there is a L-program q such that for all
input d 2 L-data we have
10.3. RECURSION ELIMINATION CHAPTER 10. SELF-REFERENCE
JqKL(d) = JpKL(q,d)
How does this deal with reflective programs and what is an acceptable program-
Now we simply define the program q we are looking for as another self-application, ming language? The reflective program q is defined via the help of p which has an
this time of pself.
extra parameter to represent “self”. So p may regard q as its own metadata repre-
•
q = JspecKL (pself, pself) (10.3) | {z }
sentation.
•
q is the self-referential program
self application of p
self
Definition 10.1. An acceptable programming language is a programming language This program q returns a L-program and this is actually what we will choose for the
defined by program p that has extra parameter q 4 n the sense we have already provided earlier) for which the following holds :
L (i
program required by the theorem. We have to show that it has the required property.
•
beforerwe prove it, lookzat example usage L
1. L has a self-interpreter (or universal program in the sense of Def. 7.1) and there-
fore must have programs-as-data as well as pairing;
JqKL (d) = JspecKL (pself, pself) (d) use Eq. 10.3, the definition of q
qy
2. The S-m-n theorem L(see Sect. 10.1) holds for L;
4
= f(pself,d)
= pself (pself,d)
use S-1-1 Thm. 10.1 with p and s = pself use Eq 10.2, definition pself
following Neil Jones and Rodgers
= JpKL(JspecKL(pself,pself),d) use Eq. 10.1, definition of f 11
= JpKL(q,d) 120 use Eq. 10.3, definition q backwards This is yet another neat proof achieved with self-application9, two helpings of self-
application actually.
10.3 Recursion Elimination
E
m
n
e
R
l
i
i
a
n
CHAPTER 10. SELF-REFERENCE
i
There are
ma
n
y
applic
a
tion
s of
th
t
c
r
is the
orem
So let us return to the specific language WHILE (so L := WHILE). Figure 10.2 shows
fac rFeadctno{rial
an attempt of implementing the factor
uisself- fac that
interpreter
definition
supported
if n {
makes use of a macro call to mult and
recursively:
A :=
We have seen already that in WHILE Res0:!==
directly, even in extensions of WHILE }
n! = n*(n-1)!
e
u
o
.A
cla
ssic
on
s
10.3. RECURSION ELIMINATION
e is
r
ecur
sion elimination.
ial function by a program, called
fac2 read qn {
q := hd qn;
also calls itself (fac) recursively.
n := hd tl qn;
we cannot define such a recursive
if n {
because recursive macros are not
A := [q, tl n];
ested. We first need to be able t
Res :=
else {
program (self-interpreter) for WHI
}
}
Res := 1
ursive macro as displayed in Fig. 1
s the first of which is a program, n
gram. But fac2 is not yet the fact write Res
andthuswecannotcallfacassuggocompile
else t{hemacroaway.However,withtheheesentsthe
Res := 1 programfacandusingtheuniversalLE,u,we
} factorial2 has canwriteprogramfac2withoutarec0.3.
argument [q,n] so
} Program fac2 takes two argument amely the write Res
emxetar-areparersgenutmatieonotf tqhe factorial pro orial func- tion we want. Applying Kleene’s recursion theorem, however, we obtain a program
RefcaucrRseiofnlTsuhcehothraetm gives us (existence of) facRefl such that
Fig. 10.2: Recursive fac not definable Fig. 10.3: fac2 using reflection for re- JfacReflKWHILE (d) = Jfac2KWHILE [facRefl,d]
in WHILE cursion
and this program does implement the factorial function. We have used the self-
12 10 interpreter here to make the recursion on the program source explicit.
9
TheRperaodoerfsofafmKilliaerenweit’hs ArelocnuzrosiCohnurtche’soruenmtypiesd clo-cnasltcruulucstiwveillwrehciocghnimseetahensimthialatrithyewith
the construction of the recursion operator Y f = (l x. f (x x)) (l x. f (x x)) which also uses two proof tells us how the program q actually looks like. It turns out that, despite of the
self-applications.
elegance of the proof by self application, the resulting program is not very efficient.
1st Impact of Theorem
• Any acceptable programming language is already “closed under recursion”. [Neil Jones]
• Usage in interpreted languages: needs a new self- interpreter called for each recursive call, leading to stacks of self-interpreters running each other,
• leading to exponential runtime,
• thus built-in “reflection” mechanisms to avoid this problem.
13
•
• •
• •
2nd Impact of Theorem
Reflection in compiled languages more difficult as there is no source code or AST.
So no reflection in C or C++.
But in Java as there is a ByteCode interpreter. The Reflection library allows to introspect classes/ methods.
This allows one to circumvent static type checking to
work with “unknown” classes
Frameworks like Spring heavily use reflection.
“Plug-in” technology needs reflection!
14