{'fraction_non_alphanumeric': 0.04248163896405102, 'fraction_numerical': 0.011693080788558175, 'mean_word_length': 4.417338498586536, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 16, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 1, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Historical Account of My Early Research Interests

This paper presents a brief account of some of the my early research interests. This historical account starts from my laurea thesis on Signal Theory and my master thesis on Computation Theory. It recalls some results in Combinatory Logic and Term Rewriting Systems. Some other results concern Program Transformation, Parallel Computation, Theory of Concurrency, and Proof of Program Properties. My early research activity has been mainly done in cooperation with Andrzej Skowron, Anna Labella, and Maurizio Proietti.


From Signal Theory to Combinatory Logic
Since my childhood I very much liked Arithmetic and Mathematics. The formal reasoning always attracted my spirit and I always felt a special interest for numbers and geometrical patterns. Maybe this was due to the fact that I thought that Mathematics is a way of establishing 'truth beyond any doubt'. As Plato says: 'Truth becomes manifest in the mathematical process' (Phaedo). (The actual word used by Plato for 'mathematical process' comes from λoγίζoµαι which means: I compute, I deduce.) During my high school I attended the Classical Lyceum. Perhaps, for me the Scientific Lyceum would have been a better school to attend, but the Scientific Lyceum was located too far away from my home town.
At the age of nineteen, I began my university studies in Rome as a student of Engineering. I was in doubt whether or not to enrol myself as a Mathematics student, but eventually I followed my father's suggestion to study Engineering because, as he said: "If you study Mathematics, you will have no other choice in life than to become a teacher." My thesis work was in Telecommunication and, in particular, I studied the problem of how to pre-distort an electric signal which encodes a sequence of symbols, each one being 0 or 1, via a sequence of impulses. The pre-distortion of the electric signal should minimize the effect of a Gaussian white noise (which would require a reduction of bandwidth) and the interference between symbols (which would require an increase of bandwidth). A theoretical solution to this problem is not easy to find. Thus, I was suggested to look for a practical solution via a numerical simulation of the transmission channel and the construction of the so called eye pattern [45]. In the numerical simulation, which uses the Fast Fourier Transform algorithm, one could easily modify the various parameters of the pre-distortion for minimizing the errors in the output sequence of 0's and 1's. The thesis work was done under the patient guidance of my supervisors Professors Bruno Peroni and Paolo Mandarini.
After getting the laurea degree, I attended during 1972 at Rome University a course in Engineering of Control and Computation Systems. During that year I read the book entitled Mathematical Theory of Computation written by Professor Zohar Manna (1939Manna ( -2018 (at that time that book was nothing more than a thick technical report of Stanford University, California). I wrote my master thesis on the "Automatic Derivation of Control Flow Graphs of Fortran Programs", under the guidance of Professor Vincenzo Falzone and Professor Paolo Ercoli [46]. In particular, I wrote a Fortran program which derives control flow graphs of Fortran programs. That program ran on a UNIVAC 1108 computer with the EXEC 8 Operating System. The main memory had 128k words. The program I wrote was a bit naive, but at that time I was not familiar with efficient parsing techniques. I also studied various kinds of program schemas and, in particular, those introduced by Lavrov [37], Yanov [74], and Martynuk [39]. Having constructed the control flow graph of a given Fortran program, one could transform that program into an equivalent one with better computational properties (such as smaller time or space complexities) by applying a set of schema transformations [32] which are guaranteed to preserve semantical equivalence. Schema transformations are part of the research area in which I have been interested for some years afterwards.
During that period, which overlapped with my military service in the Italian Air Force, I also read a book on Combinatory Logic (actually, not the entire book) by J. R. Hindley, B. Lercher and J. P. Seldin [27,28]. I read the Italian edition of the book, which was emended of some inaccuracies with respect to the previous English edition (as Roger Hindley himself told me later). Under the guidance of Professor Giorgio Ausiello and the great help of my colleague Carlo Batini, I studied various properties of subbases in Weak Combinatory Logic (WCL) [3].
WCL is an applicative system whose terms, called combinators, can be defined as follows: (i) K and S are atomic terms, and (ii) if t 1 and t 2 are terms, then (t 1 t 2 ) is a term. When parentheses are missing, left associativity is assumed. A notion of reduction, denoted >, is introduced as follows: for all terms x, y, z, Sxyz > xz(yz) and Kxy > x. Thus, for instance, SKKS > KS(KS) > S. WCL is a Turing complete system as every partial recursive function can be represented as a combinator in WCL. A subbase in WCL is a set of terms which can be constructed starting a fixed set of (possibly non-atomic) combinators. For instance, the subbase {B}, where B is a combinator defined by the following reduction: Bxyz > x(yz), is made out of all terms which are constructed by B's (and parentheses) only. These terms are called B-combinators. One can show that B can be expressed in the subbase {S, K} by S(KS)K. Indeed, S(KS)Kxyz > * x(yz), where > * denotes the reflexive, transitive closure of >. The various subbases provide a way of partitioning the set of computable functions into various sets, according to the features of the combinators in the subbases. This should be contrasted with other stratifications of the set of computable functions one could define and, among them, the stratifications based on complexity classes or on the Chomsky hierarchy [30] with the type i (for i = 0, 1, 2, 3) classes of languages.
Among other subbases, we studied the subbase {B} and we showed how to construct the shortest B-combinator for constructing bracketed terms out of sequences of atomic subterms. For instance, B(B(BB)B)(BB) is the shortest B-combinator X such that: During 1975, while attending in Rome the conference on λ-calculus and Computer Science Theory, where our results on subbases were presented [3], I heard from Professor Henk Barendregt of an open problem concerning the existence of a combinator X made of only S's (and parentheses), having no weak normal form. A combinator T is said to be in weak normal form if no combinator T ′ exists such that T > T ′ . X is said to have weak normal form if there exists a combinator T such that X > * T and T is in weak normal form.
It was not hard to show that one such combinator X is SAA(SAA), where A denotes ((SS)S). I send the result to Henk Barendregt (by surface mail, of course). Some years later I was happy to see that an exercise about that problem and its solution was included in Barendregt's book on λ-calculus [2, page 162].

Finite and Infinite Computations
While studying Combinatory Logic, I became interested in terms viewed as trees and tree transformers. Indeed, combinators can be considered both as trees and tree transformers at the same time. This area was also related to the research on Term Rewriting Systems which was going to be one of my interests for a few years later. The search for a non-terminating combinator stimulated my studies on infinite, non-terminating computations.
In 1979 I introduced a hierarchy of infinite computations within WCL (and other Turing complete systems) which is related to the Chomsky hierarchy of languages [48]. That definition uses the notion of a sampling function s which is a total function from the set of natural numbers to {true, false}, which from an infinite sequence σ = w 0 , w 1 , w 2 , . . . of finite words constructed by an infinite computation, selects an infinite subsequence σ s whose words are the elements of a (finite or infinite) language L s . We state that L s = def {w j | j ≥ 0 ∧ w j occurs in σ ∧ s(j) = true}. Let us assume that L s is generated by a grammar G s . In this case we say that also the subsequence σ s is generated by the grammar G s . Given a sequence σ, by varying the sampling function s we have different languages L s and different generating grammars G s . For i = 0, 1, 2, 3, we say that the infinite computation which generates σ is of type i if there exists a sampling function s selecting a subsequence σ s generated by a grammar of type i, and no sampling function s ′ exists such that the subsequence selected by s ′ is generated by a grammar of type (i+1).
For instance, let us consider the following program P : w = "a" ; while true do print w ; w = "b" w "c" ; π 0 od where a, b, c are characters, w is a string of characters, and π 0 is a terminating program fragment associated with a type 0 language L 0 , such that: (i) L 0 is not of type 1, (ii) π 0 does not modify w, (iii) at each loop body execution, π 0 prints only one word of L 0 , and (iv) for every word v ∈ L 0 there is exactly one body execution in which π 0 prints v. We have that P evokes an infinite computation of type 2, as the grammar with axiom S and productions: S → a | b S c is a type 2 (context free) grammar.
When I first presented this hierarchy definition at a conference, I met my dear colleague Philippe Flajolet (1948Flajolet ( -2011 and he said to me: "I have already studied these topics [24]. You should look at the immune sets." That remark motivated my first encounter with Roger's book on recursivity [66] where immune sets are defined and analyzed. Then also Professor Maurice Nivat (1937-2017) came to me and said: "It is a nice piece of work,... but you should rewrite the paper in a better way!". I was very glad that Nivat showed interest in my work. He was right in asking me to rewrite it and improve it. Unfortunately, I did not follow his suggestion. Not even when, a few years later, Professor Tony Hoare told me: "I like writing and rewriting my papers." Looking for terms with infinite behaviour in WCL, in 1980 I wrote a paper on the automatic construction of combinators having no normal form by using the so called accumulation method and the pattern matching and hereditary embedding method [49]. The solutions of some equations between terms would guarantee the existence of the combinators with the desired properties.
On the other side of the camp, that is, considering the finite behaviours, many people at that time were studying properties of Term Rewriting Systems (TRSs) which would guarantee termination. Among them, Nachum Dershowitz, Samuel Kamin, Jean-Jacques Lévy, and David Plaisted. In 1981 I wrote a paper introducing the non-ascending property [50]. In that paper I related the various techniques which were proposed, including recursive path orderings, simplification ordering, and bounded lexicographic orderings. I thank Nachum for pointing out to me some errors in that paper and, in particular, a missing left-linearity hypothesis about the TRS under consideration [20]. A TRS is said to be left linear if the variable occurrences on the left hand side of every rule are all distinct. For instance, f (x, y, z) → f (y, z, x) is a left linear rule, while f (x, y, x) → g(y, x) is not. During a conference coffee-break, Jean-Jacques showed me a simple inductive proof of Fact 1 [50, pages 436-437] using bounded lexicographic orderings (actually, that proof is based on a non-predicative definition of the non-ascending rewriting rules).

Program Transformation
During the years 1977-1981 I visited Edinburgh University. I was supported by the British Council organization and the Italian National Research Council. I did my Ph.D. thesis work on program transformation under the guidance of Professor Rod Burstall and also Professor Robin Milner, during Rod's visit to Inria in Paris for some months. I met Rod in person for the first time at the Artificial Intelligence Department, in Hope Park Square at Edinburgh. I addressed him by saying: "Professor Burstall,. . .". I do not remember my subsequent words, but I do remember what he said to me in answering: "Alberto, this is the last time you call me 'professor'. Please, call me Rod." He introduced me to functional programming and he wrote 'for me', as he said, a compiler for a new functional language, called NPL [9] he was developing at that time. The language NPL later evolved into Hope [11]. While at Edinburgh, I wrote a paper [47] on the automatic annotation of functional programs for improving memory utilization. Functions could destroy the value of their arguments whenever they were no longer needed for subsequent computations. I apologize for not having Rod as co-author of that paper.
My Ph.D. thesis work was mainly on program transformation starting from the seminal paper by Rod and John Darlington [10]. Some time before, Rod had received a letter from Professor Edger W. Dijkstra (1930Dijkstra ( -2002 proposing the following 'exercise' in program transformation: the derivation of an iterative program for the fusc function [22, pages 215-216, 230-232]: In one of my scientific conversations with Rod, he told me about his research interests and he also mentioned the above exercise. The difficult part of the exercise was how to motivate the 'invention' of the new function definitions to be introduced during program transformation in the so called eureka steps [10]. To do the same exercise Bauer and Wössner [4, page 288] use an embedding into a linear combination, that is, they define the function F(n, a, b) = def a×fusc(n) + b×fusc(n+1). Using that function, they are able to derive for fusc a program that is linear recursive and also tailrecursive. Then, from that program they easily derive an iterative program. But, where the function F comes from? I wanted to do the exercise using the unfolding/folding rules only [10] and, at the same time, I wanted to give a somewhat mechanizable account of the definition the new functions to be introduced. Now, the unfolding rule allows one to unroll (upto a specified depth) the recursive calls thereby generating a directed acyclic graph of distinct calls. I called that graph the m-dag. The prefix m (short for minimal) tells us that in an m-dag identical function calls are denoted by a single node. Then, I used the so called tupling strategy that allows one to define new functions as the result of tupling together function calls which share common subcalls, that is, calls which have common descendants in the m-dag. Note that to check this sharing property requires syntactic operations only on the m-dags. By using the tupling strategy, looking at the m-dag for fusc, we introduce the tuple function t(n) = def fusc(n), fusc(n+1) and we get the following recursive equations for fusc: (by a derivation similar to that of t(2n)) Now a last step is needed to get the iterative program desired by Dijkstra's exercise. I used the following schema equivalence (such as the ones in [69]) stating that t(n) defined by the non-tail recursive equations: By using this schema equivalence we derive from the above linear, non-tail recursive program for fusc the following iterative program: Having derived an iterative program for the fusc function, I faced the problem of deriving by transformation an iterative program, such as the one suggested by [41], which computes the Fibonacci function fib(n) using an O(log n) number of arithmetic operations. Here is the definition of the Fibonacci function: By using the tupling strategy the function g(n) = def fib(n), fib(n−1) is introduced and the following program is derived: for n ≥ 0 The iterative program for fib can be obtained by applying the following schema equivalence stating that g(n) defined by the equations: is equal to the value of res returned by the program: Thus, we get: This program has a linear time complexity, in the sense that it computes the result by a linear number of additions. In order to get a program which requires O(log n) arithmetic operations when computing fib(n), we should invent the multiplication operation, which is not present in Equation ( †1). From that equation by unfolding we have: The unfolding process may continue for some more steps, but we stop here. We will not discuss here the important issue of how many unfolding steps should be performed when deriving programs by transformation. Let us simply note that more unfoldings may exhibit more patterns of function calls from which more efficient functions can be derived. In our case the invention of the multiplication operation is reduced to three generalization steps [55]. First, we generalize the initial values 0 and 1 of the function fib to two variables a 0 and a 1 , respectively. (This kind of generalization step is usually done when mechanically proving theorems about functions [7].) By promoting those new variables to arguments, we get the following new function G: This function G satisfies the following equation which is derived from Equation ( †3), as Equation ( †2) has been derived from ( †1): The second generalization consists in generalizing the coefficients 2 and 3 to two functions p(n) and q(n), respectively (and thus, multiplication is introduced). By this generalization we establish a correspondence between the value of the coefficients and the number of unfoldings performed. We can then derive the explicit definitions of the functions p(n) and q(n) as shown in [55], and we get that p(n) = G(1, 0, n) and q(n) = G(0, 1, n). The third, final generalization consists in generalizing the argument n+2 on the left hand side of Equation ( †4) to n+k and promoting the new variable k to an argument of a new function defined as follows: F(a 0 , a 1 , n, k) = def G(a 0 , a 1 , n+k).
From the equations defining F(a 0 , a 1 , n, k) we get (the details are in [55, pages 184-185]): Then, by taking n = k and n = k+1, we also get: for k ≥ 0 Eventually, by tupling together the function calls which share the same subcalls, we get the following program which computes fib(n) by performing an O(log n) number of arithmetic operations only, as desired. For all k ≥ 0, the function r(k) is the pair G(1, 0, k), G(0, 1, k) .
We leave to the reader to derive the iterative program that can be obtained by a simple schema equivalence from this program. One can say that the program we have derived is even better than the program based on 2×2 matrix multiplications [41], because it tuples together two values only, not four, as required by the use of the 2×2 matrices. Note that our derivation of the program does not rely on any knowledge of matrix theory.
In the paper with Rod Burstall [55] there is a generalization of the derivation of the logarithmic time program for fib to the case of any linear recurrence relation over any semiring structure. What remains to be done? One may want to derive a constant time program for evaluating any linear recurrence relation over a semiring. This would require the introduction of the exponentiation operation. Recall that fib(n) = (A n − B n )/sqrt(5), where A = (1+sqrt(5))/2 and B = (1−sqrt (5) In Syracuse I had the opportunity of reading more carefully some parts of the book Automata Theory, Languages, and Computation by Hopcroft and Ullman [30] and the book Introduction to Mathematical Logic by Mendelson [40]. I was exposed by Professor Kowalski for the first time to various topics of Artificial Intelligence and I read the preliminary draft of his beautiful book Logic for Problem Solving [35]. I remember the stress put by Kowalski on Keith Clark's negation as failure semantics for logic programs [12]. This Computational Logic area was going to become my main research area in the years to come, through my cooperation with Maurizio Proietti in Logic Program Transformation.

The Tupling Strategy and the List Introduction Strategy
The results of the use of tupling and generalization during program transformation were presented in a paper of the 1984 ACM Symposium on Lisp and Functional Programming, Austin, Texas, USA [52]. While giving a seminar on those results at the University of Warsaw (Poland) Professor Helena Rasiowa 2 who was in the audience, at the end kindly said to me: "Your paper is a collection of examples!". I was not surprised by that remark, but I was happy to have, among the examples, a simple derivation of an iterative program for computing the moves of the Towers of Hanoi problem. That task was considered to be very challenging by some authors (see, for instance, [26, page 285]), and the derivation I proposed is also easily mechanizable.
The following Hanoi function h(n, A, B, C) computes the shortest sequence of moves in the free monoid {AB, BC, CA, BA, CB, AC} * to move n (≥ 0) disks from peg A to peg B using peg C as an extra peg. A move of a disk from peg X to peg Y is denoted by XY, for any distinct X, Y in {A, B, C}. Every disk is of a different size and over any disk only smaller disks can be placed. ε denotes the empty sequence of moves, and :: denotes the concatenation of sequences of moves. We get: Then, we can apply the schema equivalence stating that g(n) defined by the equations: is equal to the value of res returned by the program: if even(n) then res = a else res = b; while n > 1 do res = c(res) ; n = n−2 od We get the following program, where for k = 1, 2, 3, Tk denotes the k-th component of the triple T : The technique we have presented is based only on the tupling strategy and a simple schema equivalence. That technique is successful also for the many variants of the Towers of Hanoi problem that can be found in the literature (see, among others, [23]). A different derivation for computing the Hanoi function can be done by introducing, besides the tuple t(n), also the tuple t ′ (n−2) = def h(n−2, A, C, B), h(n−2, C, B, A), h(n−2, B, A, C) corresponding to the calls of h at level n−2 (not depicted in Figure 1). We leave this derivation to the reader.
In a later paper I addressed the problem of finding the m-th move of algorithms which compute sequences of moves without computing any other move [54]. This problem arose as a generalization of the problem relative to the Towers of Hanoi. If the moves are computed by a function defined by a recurrence relation, then under suitable hypotheses, it is indeed possible to compute the m-th move without computing any other move. For the case of the Hanoi function h(n, A, B, C) we have that the length Lh(n) of the sequence of moves for n disks, satisfies the following equations: One can show [54] that the m-th move of h(n, A, B, C), for 1 ≤ m ≤ 2 n −1 and n ≥ 0, can be computed using the deterministic finite automaton of Suppose that we want to compute the 44-th move of h(6, A, B, C). The binary expansion of 44 is 101100. Starting from the left, we take the prefix 101 up to (and excluding) the suffix in 10 * (in our case 100). We perform the transitions on the automaton of Figure 2 starting from state AB according to that prefix (from left to right) and we get to state CA. Since the length of the prefix is odd (it is indeed 3), the move to be computed is BA, that is, CA with B and C interchanged.
In a subsequent paper with Maurizio Proietti [57] we want to explore the idea of introducing lists, rather than arrays (indeed, tuples being of fixed size can be seen as arrays). Originally, this idea was suggested to me by Rod Burstall. Since every recursive function can be computed by using stacks (actually, two stacks are sufficient for computing any partial recursive function on natural numbers [30]), this technique seems to me, at first, not very relevant in the practice of improving the time complexity of a program or avoiding inefficient recursions. We explored the use of this technique and, indeed, we managed to achieve good results. In particular, the list introduction strategy can be used when the recursive calls do not generate a sequence of cuts of constant size in the m-dag of the function calls, and thus it does not allow the use of the tupling strategy. A cut in an m-dag is set C of nodes such that every path from the root to a leaf intersects C. In the case of the Hanoi function (see Figure 1) we have depicted the cuts associated with t(n−1) and t(n−3). Both of them are of size 3 and thus, the tupling strategy (with three function calls) is successful. More details on cuts and their use for program transformation also in relation with pebble games [44] can be found in my Ph.D. thesis [51].
We used the list introduction strategy for deriving a program for computing the binomial coefficients: n+1 k+1 = n k + n k+1 . In this case the sequence of cuts from the root to the leaves is of increasing size. Indeed, n+1 k+1 requires the computations of n k and n k+1 , which in turns, require the computations of n−1 k−1 , n−1 k , n−1 k+1 , and so on. (Indeed, in the Pascal Triangle the basis has an increasing size when the height of the triangle increases). Therefore, the tupling strategy cannot be used. Now, in order to show the power of the list introduction strategy, let us consider the n-queens problem. Details are in [57]. An n×n board configuration Qs is represented by a list of pairs of the form: [ R 1 , C 1 , . . . , R n , C n ], where for i=1, . . . , n, R i , C i denotes a queen placed in row R i and column C i . For i = 1, . . . , n, the values of R i and C i belong to the list [1, . . . , n].
We start from the following initial program Queens: Program Queens solves the problem using the generate-and-test approach and it is not efficient. A more efficient program using an accumulator that stores the diagonals which are not safe, has been proposed in [67, page 255]. Efficiency is increased because backtracking is reduced.
By applying the list introduction strategy (which includes also some generalization steps) one can derive the following program TransfQueens whose behaviour is similar to that of the accumulator version. The various transformation steps are described in [57]. The higher efficiency of the final program is due to the fact that the test for a safe board configuration is 'promoted' into the process of generating new configurations, and the number of generated unsafe board configurations is decreased (see the filter promotion technique [5,15] This program performs much less backtracking than the Queens program 3 . By clause 9, the first queen position Q is selected and genlist1 is called with its last argument storing the current board configuration, which is the list [Q]. When a new queen is placed at position Q1 and it is not attacked by the last queen placed at position P 1 (see clause 12), genlist2 checks whether or not Q1 is attacked by the queens already present in the current configuration and whose positions are stored in Ps (see clauses 13 and 14). If Q1 is not attacked, the configuration is updated (see the last argument [Q1|P s1] of genlist1 in clause 13). Otherwise, if Q1 is attacked, by backtracking (see the atom select in clause 12), a different queen position is selected. If all positions for the new queen are under attack, then by backtracking (see the atoms select in clauses 9 and 11), the position of a previously placed queen, if there is one, is selected in a different way.
The explanation which we have just given about the derived program (clauses [8][9][10][11][12][13][14], may appear unclear to the non-expert reader, but one should note that it was not needed at all. Indeed, correctness of the derived program is guaranteed by the correctness of the transformation rules, and the efficiency improvement is due to filter promotion.

The Lambda Abstraction Strategy
While studying the tupling strategy and analyzing its power, a sentence by John Darlington, with whom I shared the office in Edinburgh, came often to my mind: "After unfolding, having done some local improvements (such as the ones obtained by the where abstraction as shown in Section 3 for the fusc function), you need to fold." This need for folding [16] is an important requirement. Folding steps make the local improvements to be become global, so that they can be replicated at each level of recursion and thus become significant.
However, folding steps need matchings between expressions and these matchings may be sometimes impossible. Generalization of constants to variables may allow matchings in some cases, but not always. In particular, when an expression should match one of its subexpressions, generalization of constant to variables does not help. In those cases we have suggested to construct functions from expressions [62]. This is done by replacing the expression E[e] where the subexpression e occurs, by the application (λx.E[x]) e. We call this technique lambda abstraction strategy (or, as in other papers, higher-order abstraction).
Let us see how lambda abstraction works in the following two examples taken from [62]. The first example refers to the following program Reverse for reversing a list, where [ ], :, and @ denote the empty list, cons, and append on lists, respectively. We want to derive a tail recursive definition of rev. We need rev to be the top operator of the right hand side of Eq. 2, that is, rev(ℓ) @ [a], and by induction we need that right hand side to be rev(ℓ). There is a subexpression mismatch between rev(ℓ) @ [a] and rev(ℓ). Then we proceed as follows: (i) instead of rev(ℓ), we consider rev(ℓ) @ [ ], (ii) we generalize the constant [ ] to the variable x, thereby deriving rev(ℓ) @ x, and (iii) we abstract rev(ℓ) @ x with respect to x, thereby deriving the function λx. rev(ℓ) @ x.
The definition of the new function f(ℓ) = def λx. rev(ℓ) @ x is as follows. We also have: The derived program (Eqs. 5-7) is more efficient than program (Eqs. [1][2][3][4] because the expensive operation append has been replaced by the cheaper operation cons. Eqs. [5][6][7] are basically equivalent to the program proposed in [31] where a new representation for list has to be invented. Note that the mechanization of the transformation we have now presented requires the use of associativity property for the append function. Thus, in general, it is important to have knowledge of the algebraic properties of the operations in use. A second example refers to a problem proposed by Richard Bird [6]. Given a binary tree t we want to construct an isomorphic binary tree t such that: (i) t and t have the same multiset of leaves, and (ii) the leaves of t, when read from left to right, are in ascending order. One should derive a program which construct t by making one traversal only of the tree t.
In order to solve this program Richard Bird uses the so called locally recursive programs whose semantics is quite complex and it is based on the call-by-need mode of evaluation. By using the tupling and lambda abstraction strategies we will get the desired program with the following advantages over Bird's solution: (i) the use of call-by-value semantics, (ii) the absence of local recursion, (iii) the leaves are sorted on the fly, and (iv) the computation of components of tuples is done only when they are required for later computations.
By tip(n) we denote a binary tree whose single leaf is the integer n, and by t1∧t2 we denote a binary tree with children t1 and t2. By hd and tl we denote, as usual, the head and tail functions on lists. Our initial program is as follows.
1. TreeSort(t) = replace(t, sort(leaves(t))) where: (i) leaves(t) returns the list of the leaves of the tree t, (ii) sort(ℓ) rearranges the list ℓ in ascending order from left to right, and (iii) replace(t, ℓ) uses in the left-to-right order the elements of the list ℓ to replace from left-to-right the leaves of the tree t.
We assume that the length of ℓ is at least the number of leaves in t. For instance, we have: (2)) ∧ tip(1)) = (tip (1)∧tip (1)) ∧ tip (2). Here is the definition of the various functions required:
Note also that since lambda expressions do not have free variables, we can operate on them by using pairs of bound variables and function bodies, instead of the more expensive closures. Thus, for instance, λz. expr can be represented by the pair z, expr .
Some years later Maurizio Proietti and I have studied the application of the lambda abstraction strategy in the area of logic programming. As in functional programs where we have lambda expressions denoting functions, in logic programming we should have terms denoting goals, and thus goals should be allowed to occur as arguments of predicates. To allow goals as arguments, we have proposed a novel logic language, we have defined its semantics, and we have provided for it a set of unfold/fold transformations rules, together with some goal replacement rules, such as the one stating the equivalence of the goal g ∧ true with the goal g [56,63]. Those rules have been proved correct.
Here is an example of efficiency improvement obtained by program transformation in this novel language. This transformation has not been mechanized, but we believe that it is not hard to do it. Details can be found in [63, Section 7.1]. Let us consider a program which given a binary tree (either l(N ) or t(L, N, R)), (i) flips all its left and right subtrees, and (ii) checks in a subsequent traversal of the tree, whether or not all labels are natural numbers.

Communications and Parallelism
While at Edinburgh I had the privilege of attending a course on the Calculus of Communicating Systems (CCS) by Professor Robin Milner (1934Milner ( -2010 [42]. I remember the day when Robin Milner and Gordon Plotkin decided the name to be given to this new calculus. As I was told, they first decided that the name should have been of three letters only! I appreciated the beauty of the calculus which resembles a development of lambda calculus. The application of a function λx. e[x] to an argument a can, indeed, be understood as a communication which takes place between: (i) the 'function agent' and (ii) the 'argument agent' through the 'port' named λ. After their communication, which is called a handshaking, the agents continue their respective activities, namely, (i) the function agent does the evaluation of e[a], that is, the body e[x] of the function where the variable x have been bound to the value a, and (ii) the argument agent does nothing, that is, it become the null-agent (indeed, for the rest of the computation, the argument has nothing left to do).
At about the same time, Professor Tony Hoare in Oxford was developing his calculus of Concurrent Sequential Programs (CSP) [29]. I remember a visit that Tony Hoare made to Robin Milner at Edinburgh and the stimulating seminar Hoare gave on CSP on that occasion.
In subsequent years, I thought of exploring the power of communications and parallelism in functional programming, also because the various components of the tuples introduced by the tupling strategy can be computed in parallel. These components can be considered as independent agents which may synchronize at the end of their computations. During those years, the notion of communicating agents was emerging quite significantly in various programming paradigms.
Andrzej Skowron and I did some work in this area and we proposed (some variants of) a functional language with communications [60,61]. Each function call is assumed to be an agent, that is, a triple of the form x, m :: expr, where x is its name, m is its message, that is, its local information, and expr is its expression, that is, the task it has to perform. The operational semantics of the language is based on the conditional rewriting of sets (or multisets) of agents, similarly to what is done in coordination languages (see, for instance, [25]).
As an example of a functional program with communications which we proposed, let us consider the following program for computing the familiar Fibonacci function.
The variable x ranges over agent names which are strings constructed from x as the following grammar indicates: x ::= ε | x.0 | x.1. The left and right son-calls of the agent whose name is x have names x.0 and x.1, respectively. By default, the name of the agent of the initial function call is the empty string ε.
In our example, the variables ms and ms1 range over the three message constants: R (for ready), R1 (for ready1), and W (for wait). Agents with messages R and R1 may make rewritings, while agents with message W cannot (see Rules 1-4 below). The variables n and val range over integers and the variable exp ranges over integer expressions. 1.
x, R :: fib(n+2) ⇒ Indeed, by our program the value of fib(n−1) which is needed for computing fib(n+1) and fib(n), is computed once only. Note, in fact, that one of the two agents which have to compute fib(n−1), has the message W and cannot make further rewritings.
We have considered the problem of how to modify the rules of the programs when acquiring knowledge of new facts about the functions to be evaluated for improving program efficiency. In the case of the Fibonacci function, one such fact may be the equality of the expressions to be computed by the agents x.0.0 and x.1.
Note that the above Rules 1-7 do not perform the on-the-fly garbage collection of the agents because right-sons are not erased. To overcome this problem one may use more complex messages [61] so that every agent knows the agents which are waiting for receiving the value it computes. If there are none, the agent may be erased once it has sent its value to the father-call.
Note also that, if instead of Rule 6, we use the simpler equation: 6.
x.1, ms :: val, x, ms1 :: +(exp, x.1) ⇒ x, ms1 :: +(exp, val) deadlock may be generated. We have also proposed a modal logic for proving correctness of our functional programs with agents and communications [59] and, in particular, the absence of deadlock. Unfortunately, no implementation of our language proposal and its modal logic has been done.
Concerning a more theoretical study of parallelism and communications, Anna Labella and I considered categorical models for calculus with handshaking communications both in the case of CCS [42] and CSP [29]. We were inspired by the definition of the cartesian closed categories for providing models of the lambda calculus.
We followed an approach different from Winskel's one [73]. We did not give an a priori definition of a categorical structure, where the embedding of the algebraic models of CCS or CSP might not be completely satisfactory. We started, instead, from the algebraic models, based on labelled trees of various kinds, and we defined suitable categories of labeled trees where one can interpret all the basic operations of CCS and CSP. In a sense, we followed the approach presented many years earlier by Rod Burstall for the description of flowchart programs [8]. The details of our categorical constructions can be found in [33,36].
In some models of ours we used enriched categories [34]. An enriched category is a category where the sets of morphisms associated with the pairs of objects, are replaced by objects from a fixed monoidal category. For lack of space we will not enter into the details here.

Transformation and Verification in Logic Programming
While studying at Edinburgh, I thought of applying the transformation methodology to CCS agents. I remember talking to Robin Milner about this idea. He did not show much interest maybe because for him it was more important to first acquire a good understanding the equivalences between terms in the CCS calculus, before applying them to the transformations of agents which, of course, should be equivalence preserving.
Then, I thought of applying program transformation to the area of logic programming which I first studied during my Ph.D. research at Edinburgh. At that time William Clocksin and Chris Mellish were writing their popular book on Prolog [13]. I remember reading some parts of a draft of the book. Also I had the chance of looking at David Warren's report on how to compile logic programs [70]. I also read his paper comparing the Prolog implementation with Lisp [72] and the later report on the Warren Abstract Machine [71]. From those days I still remember David's kindness, his cooperation with Fernando Pereira, and his love for plants and flowers.
A few years later, when back in Italy, I was introduced by Anna Labella to her former student Maurizio Proietti who, not long before, had graduated in Mathematics at Rome University 'La Sapienza', defending a thesis on Category Theory. I spoke to Maurizio and I introduced him to logic programming [38]. I also encouraged him to work in the field of logic program transformation. He kindly accepted. The basis of his work was a paper by Hisao Tamaki and Taisuke Sato [68] that soon afterwards became the standard reference for logic program transformation.
That was the beginning of Maurizio's cooperation with me. He was first funded by a research grant from the private company Enidata (Rome) and soon later, he became a researcher of the Italian National Research Council in Rome. We first considered some techniques for finding the eureka predicates, that is, the predicate definitions to be introduced during program transformation [64].
We have also introduced: (i) the class of non-ascending programs, where, among other properties, each variable should occur in an atom at most once, (ii) the synchronized descent rule (SDR) for driving the unfolding steps by selecting the atoms to be unfolded, and (iii) the loop absorption strategy for the synthesis of the eureka predicates. We have also characterized classes of programs in which that strategy is guaranteed to be successful.
Let us see a simple example of application of the loop absorption strategy. Here is a program, called Comsub, for computing common subsequences of lists.
where sub(X, Y ) holds iff X is a sublist of Y . The order of the elements should be preserved, but the elements in X need not to be consecutive in Y . For instance, [1,2] is a sublist of [1,3,2,3], while [2,1] is not. We want to derive a program where the double visit of the list X in clause 1 is avoided. First, we make the given program to be non-ascending by replacing clause 3 by the following clause: Let Comsub1 be the set {1, 2, 3.1, 4} of clauses. In Figure 3 we have depicted an upper portion of the unfolding tree for Comsub1. In that figure we have underlined the atoms which are unfolded. Solid down-arrows denote unfolding, and dashed up-arrows denote loops which suggest the definition clauses needed for folding, as we will explain. In clause 6 we unfold the atom sub([A|X], Z) which is selected by the SDR rule. Indeed, by the synchronized descent rule, in clause 6 we have to unfold that atom, because in its ancestor-clause 1 we have unfolded the other atom sub(X, Y ) occurring in the body of that ancestor. Unfolding is stopped when the recursive defined atoms in the body of a leaf-clause, say L, are subsumed by the body of an ancestor-clause, say A. In this case we say that a loop of the form A, L has been detected. Details can be found in [64]. According to the loop absorption strategy, for each detected loop A, L we introduce a new definition clause D so that the bodies of both clauses A and L can be folded using D. The loops 1, 10 and 1, 7 need not a new definition because we have clause 1 defining comsub. The loops 5, 9 and 6, 11 require the following two new predicate definitions By performing the unfolding and folding steps which correspond to the subtrees rooted in clauses 1, 5, and 6 of Figure 3, we get the explicit definitions of the predicates newsub and newcomsub.
Eventually, by simplifying the equalities, we get the following program: 11. newsub(Z)

newsub([A|Z]) ← newsub(Z)
Now clause 6 is subsumed by clause 5 and can be erased. Then, also clauses 11 and 12 can be erased and the final program is made out of the marked clauses 5, 7-10 only. This final program is equal to the one derived by Tamaki-Sato [68]. Note that our derivation does not rely on human intuition and can easily be mechanized. The computation of all solutions of the goal comsub (X, Y, Z), where X is a free variable and Y and Z are ground lists of 10 elements, is about 6 times faster when using the final program, instead of the initial one [64]. A development of the technique we have now illustrated can be found in [65].
The following example, taken from a paper of ours [58] written some years later in honor of Professor Robert Kowalski, shows an application of the program transformation methodology also to the case when clauses may have negated atoms in their body. For that kind of logic programs, called locally stratified logic programs, we have also provided the transformation rules that can be applied and we have shown that they are correct, in the sense that they preserve the perfect model semantics. The details on the rules and the definition of the perfect model semantics can be found in [58].
Let us consider the following program CFParser for deriving a word generated by a given context-free grammar over the alphabet {a, b}: In the second step, we apply the unfold-definition-folding strategy presented in [65]. We will not recall here the formal definition of this strategy. It will be enough to say that it is similar to the loop absorption strategy we have seen in action in the above derivation starting from the Comsub1 program.
For our CFParser program, at the end of the second step, we get: This program corresponds to the deterministic finite automaton of Figure 4. Each predicate of the derived program is a state, (ii) g is the initial state, (iii) a state p is final iff it has a clause of the form p([ ]) ←, (iv) a clause of the form p([ℓ|A]) ← q(A) denotes a transition with label ℓ from p to q. Note that the derivation of the final program that corresponds to a finite automaton has been possible because the context-free grammar indeed generates a regular language.
a b Figure 4: The finite automaton which accepts the words which are not generated from s by the productions: s → a x b and x → ε | a x | a b x. State g is the initial state and the final states have double circles.
Finally we present an example on how to use the transformation methodology for the verification of program properties. This example is the so called Yale Shooting Problem which is often used in temporal reasoning. This problem can be described and formalized as follows.
We have a person and a gun. Three events are possible: (e1) a load event, when the gun is loaded, (e2) a shoot event, when the gun shoots, and (e3) a wait event, when nothing happens (see clauses 1-3 below). A situation is (the result of) a sequence of events. A sequence is represented as a list. We assume that, as time progresses, the list grows 'to the left', that is, given the current list S of events, when a new event E occurs, the new list of events is [E|S]. In any situation, at least one of the following three facts holds: (f1) the person is alive, (f2) the person is dead, and (f3) the gun is loaded (see clauses 4-6 below).
We also assume the following hypotheses (see clauses 7-11 and note the presence of a negated atom in clause 11). (s1) In the initial situation denoted by the empty list, the person is alive. (s2) After a load event the gun is loaded. (s3) If the gun is loaded, then after a shoot event the person is dead. (s4) If the gun is loaded, then it is abnormal that after a shoot event the person is alive. (s5) Inertia Axiom: If a fact F holds in a situation S and it is not abnormal that F holds after the event E following S, then F holds also after the event E.
The following locally stratified program YSP formalizes the above statements. A similar formalization is in a paper by Apt and Bezem [1].

Future Developments
Reviewing my research activity when writing this paper, I realized that many topics and issues would need a more accurate analysis and study. It would be difficult to list them all, but I have been encouraged to mention at least some of them. I hope that these suggestions may be useful for researchers in the field and they may find these suggestions of some interest.
Concerning the theory of combinators and WCL presented in Section 1, one should note that the combinator X ≡ B(B(BB)B)(BB) we have presented has parentheses and one could consider to construct a B-combinator, call it B, which places those parentheses in a sequence of seven B's, so that BBBBBBBB > * B(B(BB)B)(BB). A routine construction, following [3], shows that B is, in fact, B (B(B(BB)B)B) (BB). The relation between combinators X and B could be for the reader a stimulus for studying the process of placing parentheses in a list of variables, that is, the process of constructing a binary tree from the list of its leaves.
One can start by considering, first, the use of regular combinators only. A combinator X is said to be regular if its reduction is of the form Xx 1 . . . x n > x 1 t 2 . . . t m , where t 2 , . . . , t m are terms made out of x 2 , . . . , x n only. A particular regular combinator for placing parentheses is, indeed, B. Similarly, one could study the permutative and duplicative properties of the regular combinators C (defined by Cxyz > xzy) and W (defined by W xy > xyy) and other regular (or non-regular) combinators. This study will improve the results reported in the classical book by Curry and Feys [14,Chapter 5].
For Section 2 one could develop the techniques presented in [49]. Those developments can be useful in the area of Term Rewriting Systems for constructing terms with infinite behaviour.
For the issues considered in Section 3 on Program Transformation, it will be important to investigate how to invent the multiplication operation, having at our disposal in the initial program version only the addition operation. Generalizations of various kinds can be suggested as we have done in this paper, but an interesting technique would be the one based on the idea of deriving multiplication as the iteration of additions. Then, in an analogous way, exponentiation can be invented as the iteration of multiplications, thus allowing us to derive even more efficient programs. The idea of iteration can hopefully be generated by mechanically analyzing the m-dags constructed by unfolding and looking at repeated patterns.
For Sections 4 and 5, it could be important to mechanize the techniques we have presented there, and in particular those for finding the suitable tuples of functions and suitable lambdaabstractions via the analysis of: (i) cuts and pebble games in the m-dags, and (ii) subexpression mismatchings, respectively.
For Section 6 one can provide an implementation of the functional language with communications we have proposed so that one can execute programs written in that language. One may also: (i) automate the process of adding communications to functional programs for improving their efficiency by making use of the properties of the functions to be evaluated, and (ii) automate the reasoning on the modal theories presented in [59] in which one can prove correctness of those communications. Thus, one will have a machine-checked proof of correctness of the communications which have been added.
For Section 7 a possible project is to construct a transformation system of logic programs with goals as arguments in which: (i) one can run the programs according to the operational semantics we have defined in our paper [56], and (ii) one can apply the various transformation rules (definition introduction, unfolding, folding, goal replacement) we have listed in that paper.