"Supercompilation" vs. a "supercompiler"
Sergei Romanenko
"supercompiler".
Supercompilation is a well-defined program-manipulation technique,
based on the following procedures:
(1) The construction of a labeled "process tree" that represents all
possible traces of a computation process, the label (=
"configuration") being a representation the possible states of the
computation.
(2) Decomposing and/or generalizing the configurations in order to
turn the (possibly) infinite process tree into a finite graph.
(3) Generating the target graph from the graph.
So, "supercompilation" is a _technique_ that can be used by some
software tools. And a "supercompiler" is, evidently, a software tool
that is mainly based on supercompilation, but, in addition, may use
any other techniques (program transformation, program manipulation,
program optimization, etc.) while generating a target program.
Therefore, if we want to compare the power of various program
manipulation techniques (for example, the power of "supercompilation"
and "distillation"), we cannot do it by just submitting test programs
to the software tools, each tool being based on a heterogeneous
collection of techniques/methods! Because, the results thus obtained
would show the comparative power of the tools, rather than the
comparative power of the "core techniques" the tools are based upon.
Andrei Nemytykh
exists no subject for our research in the filed of supercompilation
at all. We have to declare that the technology is closed for further
development. What is more we have to demand that nobody is allowed to
create new ideas in this technology. I do not see both theoretical and
practical benefits in accepting such a point of view. To me, that
looks like follows: we have proved a good theorem in Euclid's
geometry. We declare the theorem is the last.
Geoff W. Hamilton
has the consequences stated by Andrei.
I would like to come up with a relative comparison of supercompilation
and distillation, but this is actually rather
difficult to do - do I mean the supercompilation performed by SCP4 on
Refal, or do I mean supercompilation
with a pure functional language as presented by Sorensen? If I compare
with Sorensen's supercompilation,
then the distinction is quite clear - this can achieve no better than
a linear improvement as opposed to the super-
linear improvement with distillation. However, if I compare with the
supercompilation of SCP4, then the distinction
is less clear - the use of associative pattern matching also allows
super-linear improvements such as the transformation
of naive quadratic reverse into the linear accumulating one. The
associative pattern matching is a peculiar property
of the Refal language (which is not found in many other programming
languages) - not a property of supercompilation
itself.
Sergei Romanenko
> Sergei! If we will accept your opinion without any doubts, then there
> exists no subject for our research in the filed of supercompilation
> at all.
supercompilation (for example, "higher-order supercompilation", and
(2) to invent various improvements to the "classical"
supercompilation.
Concerning (1). Even if we remain withing the framework of the
"classical" supercompilation, the field for study and research is
immense and boundless!
(a) The possible sets of states of the computation process has to be
described in a "constructive" way. So the languages used for this
description can be infinitely improved and refined.
(b) The data a supercompiler is working with may be much more
sophisticated as compared to Refal expressions.
(c) The ways of comparing and generalizing configurations depend on
the language the configurations are formulated in. Hence, the "algebra
of configurations" can take different forms and can be refined "ad
infinitum".
(d) And so forth...
Concerning (2). Refal Plus is a first-order functional language, while
Standard ML is a higher-order functional language. Nevertheless, Refal
Plus possesses some specific features that are absent from Standard
ML: associative pattern matching, backtracking. By the way, the theory
of associative pattern matching, the Refal compilers are based upon is
sufficiently interesning (but not published in English)...
But it would be silly to insist that Refal is a "higher-order"
functional language... This would be not true.
> We have to declare that the technology is closed for further
> development. What is more we have to demand that nobody is allowed to
> create new ideas in this technology.
> I do not see both theoretical and
> practical benefits in accepting such a point of view.
but rather to various bureaucratic games. For example, if there is a
possibility of getting a grant, but the pre-condition is that "X"
should be called as "Y" in a grant application, hence a researcher is
usually forced to flexibly "adjust" her point of view.
In some cases inventing new names for old things may be "beneficial",
but in other situations it is using old names for new things may be
more advantageous. This is a very "concrete" question... :-)
> To me, that looks like follows: we have proved a good theorem
> in Euclid's geometry. We declare the theorem is the last.
be "a fool", nobody stopped teaching and learning the Euclidean
geometry. And the research in the Euclidean geometry didn't stop. For
example, the research by Hilbert in the axiomatic of the Euclidean
geometry was after the invention of Lobachevsky's geometry.
Nevertheless, it would be incorrect to straightforwardly claim that
Lobachevsky's geometry IS Euclid's geometry!
Andrei Nemytykh
> I would like to come up with a relative comparison of supercompilation
> and distillation, but this is actually rather difficult to do
--- I agree with you that a relative comparison of supercompilation
and distillation difficult to do.
In fact, I hope, that my discussion will be considered just as an
occasion to make things clear rather than an occasion to balk like a
mule. :-)
I do not want to balk like a mule. :-)
I am remembering a classical Wadler's paper on deforestation. The
reason why I very like the paper is as follows:
Wadler formulated a small class of programs and proved a theorem
how the programs will be improved when they will be transformed by an
algorithm defined in the theorem. I see some contradictions in my
motivation :-) ...
I fact, that is well known, I do not like the name
"supercompilation". But still I do not like (but have no objections
:-) ) to produce new names for old conceptions.
In my opinion, it will be much more better if we just introduce new
names for new ideas inside supercompilation technology. Let me recall,
that partial evaluation technology was developed in such a way.
Let me give an example, the supercompiler SCP4 constructs output
formats of partially constructed graphs in an online fashion. The
graphs already are not input programs but still are not residual
program. Constructing the output formats is one of the reasons why
SCP4 sometimes produces super-linear improvements.
I recognized that such constructing of the output formats is very
important, when I was analyzing a result supercompilation of the
driving. That is to say, when the supercompiler SCP4 supercompiled the
driving algorithm taken from the SCP4 itself.
If I will say that supercompilation have not to construct such
output formats, then I am sure, I have to add any self-application of
supercompilation can not be achieved, provided that we mean in some
sense good optimal properties of a result of the self-application.
Another subject: the generalization algorithm is enough simple for the
LISP's structures, and Morten Sorensen declared his supercompilation
only in LISP's terms.
Following Sergei's logic I have to say that Turchin never developed
supercompilation technology, because all Turchin's papers uses REFAL's
data. But for REFAL's data the generalization algorithm much more
complicated, but sometimes gives new possibilities to improve
programs.
Thus the question is as follows:
Did V.T. Turchin ever take part in development the supercompilation
technology, did not he?
Sincerely,
Andrei Nemytykh.
2008/3/12, Geoff W. Hamilton <hami...@computing.dcu.ie>:
Andrei Nemytykh
Thank you very much for your very interesting message!
-1-
>Nevertheless, it would be incorrect to straightforwardly claim that
>Lobachevsky's geometry IS Euclid's geometry!
But it is still geometry! Here I have a remark on Russian live
concerning geometry, but I prefer to omit it. The remark is not
understandable for foreign people ...
It looks like REFAL ... :-)
-2-
Could you, please, consider the arguments from my previous message as
reply on you notes. I would like to say once again what is concerning
the new names.
I have no objections, but I do not like.
Despite on opinion the foreign members of this mail-group I am a free
human living in a free country. :-)
Sincerely,
Andrei Nemytykh.
2008/3/13, Sergei Romanenko <sergei.r...@gmail.com>:
Sergei Romanenko
> -1->Nevertheless, it would be incorrect to straightforwardly claim that
> >Lobachevsky's geometry IS Euclid's geometry!
>
> But it is still geometry! Here I have a remark on Russian live
> concerning geometry, but I prefer to omit it. The remark is not
> understandable for foreign people ...
> It looks like REFAL ... :-)
Supercompilation = Euclidean geometry
Sergei Romanenko
> Let me give an example, the supercompiler SCP4 constructs output
> formats of partially constructed graphs in an online fashion. The
> graphs already are not input programs but still are not residual
> program. Constructing the output formats is one of the reasons why
> SCP4 sometimes produces super-linear improvements.
us to see why the output format inference (= "co-arity raising"?) is
beneficial in some cases.
I've got a strong suspicion that Geoff's distiller solves this problem
in another way: the distiller deals with typed programs (in the
Hindley-Milner style). Hence, the type of values returned by a
function in known in advance.
But this is only a guess of mine. I'm looking forward to seeing the
results of a comparison between the distiller and SCP4 concerning this
point.
Andrei Nemytykh
Today I leave for Moscow.
2008/3/13, Sergei Romanenko <sergei.r...@gmail.com>:
Geoff Hamilton
were applied
to the same language. This is why I prefer to compare distillation to
Sorensen's formulation
of supercompilation rather than Turchin's. Refal has some rather
non-standard features
such as associative pattern matching. For a similar feature within other
functional languages,
we would need to appeal to a law of the associativity of concatenation.
This is not to say
that Turchin did not invent supercompilation, just that comparison with
Sorensen's formulation
provides a more informative comparison of the transformation techniques
themselves.
I am not sure in exactly what way you construct output formats and how
this can produce
super-linear improvements. I would be very interested to know more about
this. I have
not seen this mentioned in any of Turchin's work.
I do not believe that distillation is just a new name for an old
conception. I would be happy
to say that it was an instance of supercompilation if I thought this was
the case. I believe that
the way in which distillation performs metasystem transitions to further
analyse graphs of
configurations achieves more powerful improvements than can be achieved
by repeated
applications of supercompilation.
Geoff.
Geoff Hamilton
currently self-applicable -
this is one of many directions for future work!! I would be interested
to know exactly why
the output format inference is considered to be necessary, and how
exactly it can cause
super-linear improvements.
Sergei Romanenko
Dear colleagues,
> I do not believe that distillation is just a new name for an old
> conception. I would be happy
> to say that it was an instance of supercompilation if I thought this was
> the case. I believe that
> the way in which distillation performs metasystem transitions to further
> analyse graphs of
> configurations achieves more powerful improvements than can be achieved
> by repeated
> applications of supercompilation.
(modification?, mutation?) with respect to Sørensen's
supercompilation. The problem is that Sørensen's supercompilation
seems to be a simplified version of Turchin's supercompilation.
M.H.Sørensen, R.Glück, and N.D.Jones did an excellent job at making
Turchin's ideas accessible to the public. For this purpose they had to
create a simplified "projection" of Turchin's original ideas,
mercilessly throwing away what they considered to be "less important",
"too specific", or "too difficult" for the public.
And this tactic was absolutely rational, justified and efficient!
But now we should realize that Sørensen's supercompilation is not
identical to Turchin's supercompilation. Hence, there is a good time
to re-read some of Turching's papers/reports. Not just for the sake of
showing our respect for V.F.Turchin, but "for the sake of
pillage"! :-)
I suspect that there still remain some interesting ideas of Turchin
that are waiting for somebody to simplify, formailze and implement
them.
But the problem is that some of Turchin's papers/reports are not
readily accessible now. In particular, I'v got a paper copy of the
report
Valentin F.Turchin. The Language REFAL -- The Theory of Compilation
and Metasystem Analysis. - Courant Computer Science Report #2,
February 1980.
Since the report doesn't seem to be easy to find, I've got the
intention of digitizing it. I've already have put the volume to
separate pages, for the stuff to be easier to scan. :-)
Perhaps, I'll start with the last chapters, because they are the most
interesting, for them to become accessible as soon as possible...
Andrei Nemytykh
> But now we should realize that Sørensen's supercompilation is not
> identical to Turchin's supercompilation. Hence, there is a good time
> to re-read some of Turching's papers/reports. Not just for the sake of
> showing our respect for V.F.Turchin, but "for the sake of
> pillage"! :-)
>
> I suspect that there still remain some interesting ideas of Turchin
> that are waiting for somebody to simplify, formailze and implement
> them.
-- I absolutely agree with you concerning the estimation of the
excellent paper written by Morten Sorensen.
It seems here is a good occasion to indicate still another very
important property of the Turchn's supercompilation, which was dropped
at all in the Sorensen's paper.
I mean that the Turchin's supercompilation, by definition, allows to
extend the domain of the program to be transformed. As a consequence,
still another possibility to improve order of the time complexity of
the programs to be supercompiled are open. That is very easy to see.
If a program implements just a partial identity function and the
program contains a loop, then if we will require to save the domain of
the program, then we are not allowed to remove the loop (i.e. to
improve the order of the time complexity).
But the Turchin's supercompilation allows to remove such a loop!
And the supercompiler SCP4 sometimes do that!
-2-
Concerning the Turchin's report mentioned by Sergei: I have to say
that is not a easy work to read the paper, :-) especially for people,
who do not know REFAL.
To me, the exists the only decision of the problem. The decision is to
study REFAL language.
I have to say, that China has started to do that! :-)
Sincerely,
Andrei Nemytykh.
Sergei Romanenko
> I mean that the Turchin's supercompilation, by definition, allows to
> extend the domain of the program to be transformed. As a consequence,
> still another possibility to improve order of the time complexity of
> the programs to be supercompiled are open. That is very easy to see.
>
> If a program implements just a partial identity function and the
> program contains a loop, then if we will require to save the domain of
> the program, then we are not allowed to remove the loop (i.e. to
> improve the order of the time complexity).
That's right. But the usefulness of such an optimization depends on
the purpose the metacomputation is used for.
It can be used for, at least, two different purposes: "program
optimization" (to speed up a program) and "program analysis" (to infer
and prove some non-trivial facts about a program).
If we are interested in "program optimization", then extending the
domain of a program is OK. But, if we are interested in "program
analysis", then extending the domain of a program may result in
additional problems, because supercompiling/distilling a program is
only the first stage. The program obtained at this step is used as the
input to further stages. And the fact that the supercompiled program
is not equivalent to the original program may "discredit" the final
result of the analysis.
If we say: "P is equivalent to P' and the fact X is true about P'",
then, undoubtedly, X is true about P. But if we say: "P is not
equivalent to P' and the fact X is true about P'", we can't
immediately conclude that X is true about P (without some additional
fuss and investigation).
I'd like also to note, that the optimization that replaces a "partial
identity function" with the "total identity function" is useful and
important when dealing with a dynamically typed language. But, in the
case of a statically typed language, we usually don't have to deal
with functions defined "for all inputs", but rather the domain of a
functions is known in advance, before the start supercompiling the
program. Hence, usually there is no need to replace an identity
function
f : a -> b
with a "universal identity function" of the type Anything -> Anything.
Sergei
Andrei Nemytykh
> I am not sure in exactly what way you construct output formats and how
> this can produce
> super-linear improvements. I would be very interested to know more about
> this. I have not seen this mentioned in any of Turchin's work.
--- As far as I know, there is no Turchin's works concerning output formats.
I thought necessary of on-line constructing such formats, when I
was developing the supercompiler SCP4 and analyzing the residual
programs produced by SCP4.
As far as I know, I was not a pioner who was thinking on such a
problem in the context of supercompilation, but I was the first who
turn the problem into a real algorithm in a real supercompiler.
The algorithm implemented in the supercompiler SCP4 is simple and must
be improved and I have some ideas how to do that, but already a simple
algorithm gives very interesting results in the context of
supercompilation.
How I promised in one my previous message, below I gives a very simple
example demonstrating new possibilities.
It is very interesting question: can distillation do such
transformation, cannot it?
The example standing alone does not demonstrate very significance of
using the on-line constructed output formats.
The reason is like the follows:
partial evaluation separates biding time analysis and the main stage
of specialization. As a result, such partial evaluation is weaker than
supercompilation, where everything is being done on-line. (And
generalization is an analog of the biding time analysis.)
The main point is as follows: the output formats depend not only on
the input program standing alone, but also on the context of
specialization.
Below I give the simplest example written in Refal, after that I will
translate it in LISP's terms.
I am ready to show more complicated example, but in Refal's term.
It is very interesting can your distillation do such transformation, cannot it?
So the example written in Refal is as follows:
$ENTRY Go {
t.xs (Cons t.ys) = <append t.xs (Cons t.ys)>;
}
append {
Nil t.vs = t.vs;
(Cons t.u t.us) t.vs = (Cons t.u <append t.us t.vs>);
}
That means we have to specialise the entry point.
The residual program constructed by the supercompiler SCP4 is:
$ENTRY Go {
t.101 (Cons t.102) = (Cons <F7 t.101 t.102>) ;
}
F7 {
Nil t.102 = t.102 ;
(Cons t.104 t.105) t.102 = t.104 (Cons <F7 t.105 t.102>) ;
}
So what we see here: the SCP4 did recognize that the result of the
call for append will sure be not Nil, and Cons was drawn out of the
call. It is easy to see that such a kind of propagation of information
may lead to super-linear improvement.
Now the example given above we informally translate in LISP's terms:
Honestly, I am not sure that is a pure LISP :-), but something like that.
Sorry, I am a Refalist. :-)
The input program:
Go {
xs, (Cons ys) = append(xs, (Cons ys));
}
append {
Nil, vs = vs;
(Cons u us), vs = (Cons u append(us, vs));
}
The residual program:
Go {
xs, (Cons ys) = (Cons F7(xs, ys));
}
F7 {
Nil, ys = ys;
(Cons x xs), ys = x :: (Cons F7(xs, ys)) ;
}
Sincerely,
Andrei Nemytykh.
Andrei Nemytykh
> Actually, I have not tackled this problem at all. My distiller is not
> currently self-applicable -
> this is one of many directions for future work!!
The supercompiler SCP4 is not currently self-applicable as well.
But I did some experiments in this directions.
There exist a number of simple experiments on self-application with
another supercompiler (named by Turchin as SCP3), which reported in
the following paper:
Nemytykh A.P., Pinchuk V.A., Turchin V.F. A Self-Applicable
Supercompiler. Partial Evaluation, Lecture Notes in Computer Science,
vol. 1110 (1996) pp: pp. 322-337.
Sincerely,
Andrei Nemytykh.
Andrei Nemytykh
> The supercompiler SCP4 is not currently self-applicable as well.
Andrei Nemytykh.
Sergei Romanenko
A short examination of the report
Turchin V. F., The language Refal - the theory of compilation and
metasystem analysis. Courant Institute of Mathematical Sciences.
Courant Computer Science Report No. 20, 1980.
shows that Turchin's "supercompilation" is, certainly, something much
more general than Sørensen's "supercompilation" (but still a
"concretization" or an "implementation" of more general ideas, like
"metasystem transition" and "metacomputation").
This is especially evident if we look into Chapter 5.
It would be interesting to investigate, does Turchin sketch some
techniques similar to distillation? In any case Geoff don't have to
"lose sleep" over this point. Geoff's distillation is a carefully
elaborated, formalized and implemented technique, while Turchin
describes some "higher-order" approaches in a "sketchy" form, as
"directions for further research".
Sergei
Geoff Hamilton
A Happy St. Patrick's day to you!
The example which you give does not actually type-check in my language:
Cons is a constructor of arity 2, but you have used it with both arities
1 and 2!
I guess what you are trying to do in this example is to show that the
constructor
at the head of the second argument will always appear at the head of the
result.
This would not actually be the case if the constructor were of arity 2:
the head
of the second list argument to append will not be the head of the list
result.
I guess the nearest I could get to your example in my language would be
something
like the following:
go x Succ(y)
where
go = %x y.add x y
add = %x y.case x of
Zero => y
| Succ(x') => Succ(add x' y)
Which would be equivalent to something like the following in Refal:
$ENTRY Go {
t.x (Succ t.y) = <add t.x (Succ t.y)>;
}
add {
Zero t.y = t.y;
(Succ t.x) t.y = (Succ <add t.x t.y>);
}
Which I guess would be transformed by SCP4 to give a residual program
similar to the following:
Go {
x, (Succ y) = (Succ F7(x, y));
}
F7 {
Zero, y = y;
(Succ x), y = (Succ F7(x, y)) ;
}
Distillation does not extract constructors from inside functions in this
way. Is it not possible
that if you extract a constructor from an infinite loop that you will
actually alter the termination
characteristics of the program? The above example program would be
transformed to the
following using distillation:
f x y
where f = %x y.case x of
Zero => Succ(y)
| Succ(x) => Succ(f x y)
However, the original function would be transformed in a different way
depending on the
context within which it appears - perhaps this is why I have no need to
perform the output
format encoding.
It is still not clear to me how a transformation such as the given one
can result in a super-linear
improvement. Do you have an example of this?
I had thought that the output format encoding was something similar to
co-arity raising, but this
does not appear to be the case.
Regards,
Geoff.
Geoff Hamilton
optimizations should not
extend the domain of the program, and should be totally semantics
preserving.
Regards,
Geoff.
Geoff Hamilton
Thank you very much for making this available. I have skimmed through
it, and it looks
very interesting stuff. I look forward to reading it in detail. I agree
with you that Sørensen's
formulation is a simplification of Turchin's. I do not wish to do a
disservice or to disrespect
the work of Turchin - I am a great fan of his work which I believe to be
way ahead of its
time.
I will not lose any sleep over the comparison between distillation and
Turchin's work!
I believe that distillation does do something different, but if it does
not, then I would be
happy to have come up with a formulation of it which is more accessible
to a mainstream
audience - this is what Sørensen's work also did.
Regards,
Geoff.
Sergei Romanenko
Dear Geoff,
> I do not wish to do a disservice or to disrespect
> the work of Turchin - I am a great fan of his work which I believe to be
> way ahead of its time.
the USA. But the report describes ideas that Turchin had developed
while in the USSR. The point is that the USSR authorities prevented
Turchin from publishing anything after 1977. And, upon coming to the
USA, Turchin "dumped" in the report
Turchin V. F., The language Refal - the theory of compilation and
metasystem analysis. Courant Institute of Mathematical Sciences.
Courant Computer Science Report No. 20, 1980.
> I believe that distillation does do something different, but if it does
> not, then I would be happy to have come up with a formulation of it
> which is more accessible to a mainstream
> audience - this is what Sørensen's work also did.
reports. In any case, you may well find there something interesting
and inspiring.
Sergei
Andrei Nemytykh
> A Happy St. Patrick's day to you!
Like most of Russian people I am an orthodox christian using
Julian church calendar.
This time is Lent by Julian church calendar.
Happy St. Patrick's day to you!
> I guess the nearest I could get to your example in my language would be
> something like the following:
-- Yes, you are right.
> I had thought that the output format encoding was something similar to
> co-arity raising, but this does not appear to be the case.
-- Sergei was quite right in his message concerning co-arity raising.
But in the point of view of the supercompiler SCP4, output
formats are something more, than only co-arity raising.
And the first my example demonstrates that.
> It is still not clear to me how a transformation such as the given one
> can result in a super-linear improvement. Do you have an example of this?
The example is as follows.
===== Input program. =======
$ENTRY Go { t.ls = <last <append t.ls (Succ A)>>; }
last {
(Succ t.x) = (Succ t.x);
(Cons t.x t.ls) = <last t.ls>;
}
append {
(Cons t.x t.ls) t.ys = (Cons t.x <append t.ls t.ys>);
(Nil) t.ys = t.ys;
}
==== The residual program produced by SCP4 =======
$ENTRY Go {
(Cons t.x (s.n e.ys)) = (Succ A) ;
(Nil ) = (Succ A) ;
}
The residual program contains some new Refal's concepts.
The following program is a version of this residual program.
The version was produced by my hands,which still are not worse than SCP4.
At least in this example :-) .
This version is not quite correct, but it looks closely to LISP.
$ENTRY Go {
(Cons t.x t.ys) = (Succ A) ;
(Nil ) = (Succ A) ;
}
===== Input program written in "LISP's style". =======
$ENTRY Go { ls = last( (append ls, (Succ A))); }
last {
(Succ x) = (Succ x);
(Cons x ls) = last(ls);
}
append {
(Cons x ls), ys = (Cons x append(ls, ys));
(Nil) ys = ys;
}
===================================
> Is it not possible
> that if you extract a constructor from an infinite loop that you will
> actually alter the termination characteristics of the program?
How I wrote in one my previous message, the Turchin's
supercompilation allows to exdend the domain of the program to be
transformed.
Honestly, if we use supercompilation for program optimization, I do
not understand why we have to refuse any possibility to improve a
program.
With point of view of a user, does not matter how his a program
behaves outside its domain. I do not see reasons to prefer an abnormal
stop of the program (or an infinite loop) to producing a new result by
the program.
I guess Turchin followed the same logic.
Sincerely,
Andrei Nemytykh.
Geoff Hamilton
The example which you give also does not type-check in my language as
the Succ constructor
builds naturals rather than lists. I guess the closest equivalent
program I can come up with is the
following:
go xs
where
go = %xs.last (append xs Cons(A,Nil))
last = %xs.case xs of
Cons(x',xs') => case xs' of
Nil => x'
| Cons(x'',xs'') =>
last xs'
append = %xs ys.case xs of
Nil => ys
| Cons(x',xs') => Cons(x',append xs' ys)
Which would probably look something like the following in Refal:
$ENTRY Go { t.ls = <last <append t.ls (Cons (A) (Nil))>>; }
last {
(Cons t.x (Nil)) = t.x;
I guess this program would be transformed to something like the
following using SCP4:
$ENTRY Go {
(Cons t.x t.ys) = (A);
(Nil) = (A);
}
which has a constant time complexity.
The original program is transformed to the following using distillation:
f xs
where
f = %xs.case xs of
Nil => A
| Cons(x',xs') => f xs'
I guess this would look as follows in Refal:
$ENTRY Go { t.ls = <f t.ls>; }
f {
(Nil) = (A)
(Cons t.x t.ls) = <f t.ls>;
This has the same termination characteristics as the original program
and is linear with respect to the size of the input list, but is still
more efficient than the original program. We therefore have not "refused
any possibility to improve the program".
I believe that it quite often does matter to a user how their program behaves
outside its domain. If a program behaves differently depending on whether or
not it is optimized, it can be very confusing for a user. It is better if the
user is aware that they have written a non-terminating program, and correct it,
than to rely on the non-termination of the program being removed by optimization.
Also, some users may actually want their code to be non-terminating and this may
be removed!
Finally, as Sergei has already pointed out, if we wish to perform program
analysis, or to use our program transformation in a theorem prover, it is
absolutely essential that there is a total equivalence between the input
and output to the program transformation.
Regards,
Geoff.
Andrei Nemytykh
Thank you very much for your explanation.
I think the programs given by you as the examples demonstrating
possibilities of the distillation algorithm are more complicated than
the example shown by me.
I hope I will be able to understand your distillation algorithm and
implement it in Refal terms. That is very interesting which new
possibilities will be created in the context more complicated Refal
data.
Thank you again for your very interesting papers.
> I believe that it quite often does matter to a user how their program behaves
> outside its domain. If a program behaves differently depending on whether or
> not it is optimized, it can be very confusing for a user. It is better if the
> user is aware that they have written a non-terminating program, and correct it,
> than to rely on the non-termination of the program being removed by optimization.
> Also, some users may actually want their code to be non-terminating and this may be removed!
-- When I am speaking about extension of the domain of a program to
be transformed, I mean pure functional language.
-- If we have a "side-effect procedure", then it is certainly we
cannot extend the domain.
> Finally, as Sergei has already pointed out, if we wish to perform program
> analysis, or to use our program transformation in a theorem prover, it is
> absolutely essential that there is a total equivalence between the input
> and output to the program transformation.
-- The supercompiler SCP4 still can be used as a theorem prover.
But, of course, we have take more care of the properties of the
logical programs. That is to say the programs encoding conjectures.
For, example, a number of experiments on successful verification
of cache coherence protocols can be found on the following web-page:
http://refal.botik.ru/protocols/
Sincerely,
Andrei Nemytykh.
Andrei Nemytykh
> I believe that it quite often does matter to a user how their program behaves
> outside its domain. If a program behaves differently depending on whether or
> not it is optimized, it can be very confusing for a user. It is better if the
> user is aware that they have written a non-terminating program, and correct it,
> than to rely on the non-termination of the program being removed by optimization.
> Also, some users may actually want their code to be non-terminating and this may be removed!
--- In my opinion, any deep optimisation (like supercompilation and
distillation) must be done as a final step of the user in developing
his program.
-- We do not need any optimisation on the debugging stage. So the
debugging stage will save behavior of the program to be debugged. In
my opinion, on this stage just a simple compiler must be used.
Sincerely,
Andrei Nemytykh.
Andrei Klimov
From: "Sergei Romanenko" <sergei.r...@gmail.com>
Sent: 17 Mar 2008 22:57
> Yes, the report was written in 1980, just after Turchin had come to
> the USA. But the report describes ideas that Turchin had developed
> while in the USSR. The point is that the USSR authorities prevented
> Turchin from publishing anything after 1977.
Turchin was fired for political reasons and became jobless in Summer _1974_. Since then he has no opportunity to publish scientific papers until his emigration in October 1977 and coming to USA in 1978.
In this "period of silence" only one his result was published, but without the author's name. In 1976-77 we prepared a book on Refal which includes chapters on Refal written by Turchin together with chapters on Refal implementations written by their authors. Additionally several pages on what was later called "Futamura projections" formulated in Refal were inserted. Since Turchin's name could not be put on the title of the book, it was published without the authors at all.
BTW Turchin was unfamiliar with the Futamura's 1971 paper at that time. Futamura mentioned only 2 "projection" in the paper, while in the 1977 book Turchin mentioned the third one as well -- the generation of compiler compiler by double self-application of a specializer / supercompiler. This is why we prefer to say "Futamura-Turchin projections" implying 3 ones rather than "Futamura projections" which should refer to only 2 ones.
Andrei