Transcript Functional programming, supercompilation and

Functional programming,
supercompilation and metacomputation theories, and
their applications to practical programming.
Program System Institute, Russian Academy of Sciences.
Functional programming
in IPS RAS.
• Supercompilation, program specialization.
• Metacomputation, semantics modifiers –
reusing “semantics components”.
• Implementation of functional programming
languages.
• Applied computer algebraic libraries.
Reasons for program
optimization.
• The methods can do almost nothing with programs that are already
carefully optimized by a professional programmer in a lower-level
language. The methods can clean a program of natural inefficiencies if
the program has been developed “inefficiently” in a structured way,
using various “high-level” techniques like
1. interpretation of specialized application-oriented languages and
2. component programming from libraries of general re-usable software,
etc.
Thus, the methods are directed to provide degrees of freedom for
new software technologies rather than to optimizing programs written
in an old style.
Specialization: the main idea
Let human be a program with two parameters knowledge and problem.
Then creating a specialist humanknowledge from human and knowledge is
a good example of specialization:
humanknowledge(problem) = human(knowledge,problem)
Specialist humanknowledge can solve problems much quicker than
an ordinary human when the problems are covered by his specific
knowledge.
A number of tasks for specialization.
<F x0, y>
The first argument of a program F is given, while the second is unknown.
<F <G x, y> , z >
Let two programs F and G be given, specialize a composition of
applications of the programs. That is specialization with respect to a
context of application.
<IntL ( Program )
e.data
>
<GO
>
An interpreter IntL of a programming language L is specialized with
respect to a given program. IntL is written in a language M, while the
program is written in L, so we expect an optimal program written in M as
a result of specialization. Thus a specializer may be used as a compiler
from L into M, where M is the subject language of the specializer.
What is supercompilation ?
•
Supercompilation is a technique of specialization of programs written in
a functional programming language. The technique was introduced in the
1970s by V. F. Turchin. He proposed a task of creating tools to observe
operational semantics of a program, when a function F that is to be computed
by the program is fixed. As a result of such observations a new algorithmic
definition of an extension of the function F must be constructed. His ideas were
studied by a number of authors for a long time.
•
The main aim of a supercompiler is to perform as many actions of a given
parameterized application of a program uniformly on the parameters as
possible.
•
Also supercompilers can be used
• as theorem provers for program verification;
• as compilers by specialization of operational specifications;
• for porting a non-standard semantics from one programming language to
another; by specialization of a semantics modifier.
The Supercompiler SCP4
•
is an experimental specializer for a functional language Refal-5.
(There are no special restrictions on the input language.) SCP4 has been
implemented once again using Refal-5. Sources of the supercompiler,
executable modules and sources of Refal-5 are available for immediate
free download: http://www.botik.ru/pub/local/scp/refal5/
Windows 98
Windows NT/2000/XP
Linux (Intel)
Specialization of interpreters.
<IntL ( Program )
e.data
<GO
>
>
An interpreter IntL of a programming language L is specialized with respect to
a given program. IntL is written in a language M, while the program is written in
L, so we expect an optimal program written in M as a result of specialization.
Thus a specializer may be used as a compiler from L into M, where M is the
subject language of the specializer.
Semantics modifiers (a class of programs that allow the development of general
and reusable “semantics components”) can be specialized alike interpreters.
Verification of parameterized systems
by the supercompiler SCP4.
• Successful experiments on verification cache coherence
protocols:
– IEEE Futurebus+, MOESI, MESI, MSI, “Illinois”, “Firefly”, “Berkeley”.
• More parameterized protocols:
– Java Meta-Locking Algorithm, Reader-Writer protocol.
References
[1] Abramov S.M., and Glueck R. From standard to non-standard semantics by semantics
modifiers. International Journal of Foundation of Computer Science, Vol. 12 No. 2,
pp:171-211, 2001.
[2] Nemytykh A.P., and Turchin V.F. The Supercompiler Scp4: sources, on-line
demonstration. http://www.botik.ru/pub/local/scp/refal5/ ,2000.
[3] Nemytykh A.P., The Supercompiler Scp4: General Structure., LNCS vol. 2890,
pp.162-170, 2003.
[4] Nemytykh A.P., A Note on Elimination of Simplest Recursions. In Proceedings of
the ACM SIGPLAN Asia-PEPM'02, 138-146. ACM Press, 2002.
[5] Korlyukov A.V., and Nemytykh A.P., Supercompilation of Double Interpretation.
(How One Hour of the Machine's Time Can Be Turned to One Second). (In English),
Vestnik natcional’nogo tekhnicheskogo universiteta “Khar’kovskogo politekhnicheskogo
instituta”, Khar’kov, No. 1, 2004.
[6] Lisitsa A., and Nemytykh A.P., Verification via Supercompilation.
http://www.csc.liv.ac.uk/~alexei/VeriSuper/ , 2005.
Thank you!