A Historical Account of My Early
Research Interests ^††thanks: This work has been partially supported by GNCS-INdAM, Italy.

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 $\lambda o\gamma\acute{\iota}\zeta o\mu\alpha\iota$ 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 [46]. 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 (1939–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 [47]. 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 [38], Yanov [75], and Martynuk [40]. 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 [33] 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 [28, 29]. 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) [4].

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 [31] 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: $Xx_{\_}{1}x_{\_}{2}x_{\_}{3}x_{\_}{4}x_{\_}{5}x_{\_}{6}\ >^{*}\ x_{\_}{1}(x_{\_}{2}(x_{\_}{3}x_{\_}{4}))(x_{\_}{5}x_{\_}{6})$.

During 1975, while attending in Rome the conference on $\lambda$-calculus and Computer Science Theory, where our results on subbases were presented [4], I heard from Professor Henk Barendregt of an open problem concerning the existence of a combinator $\widetilde{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^{\prime}$ exists such that $T\!>\!T^{\prime}$. $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 $\widetilde{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 $\lambda$-calculus [3, page 162].

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 [49]. That definition uses the notion of a sampling function $s$ which is a total function from the set of natural numbers to $\{\mathit{true},\mathit{false}\}$, which from an infinite sequence $\sigma\!=\!\langle w_{\_}{0},w_{\_}{1},w_{\_}{2},\ldots\rangle$ of finite words constructed by an infinite computation, selects an infinite subsequence $\sigma\!_{\_}{s}$ whose words are the elements of a (finite or infinite) language $L_{\_}{s}$. We state that $L_{\_}{s}=_{\_}{\mathit{def}}\{w_{\_}{j}\mid j\!\geq\!0\wedge w_{\_}{j}\leavevmode\nobreak\ \mathit{occurs\leavevmode\nobreak\ in}\leavevmode\nobreak\ \sigma\wedge s(j)\!=\!\mathit{true}\}$. Let us assume that $L_{\_}{s}$ is generated by a grammar $G_{\_}{s}$. In this case we say that also the subsequence $\sigma\!_{\_}{s}$ is generated by the grammar $G_{\_}{s}$. Given a sequence $\sigma$, 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 $\sigma$ is of type $i$ if there exists a sampling function $s$ selecting a subsequence $\sigma\!_{\_}{s}$ generated by a grammar of type $i$, and no sampling function $s^{\prime}$ exists such that the subsequence selected by $s^{\prime}$ is generated by a grammar of type $(i\!+\!1)$.

For instance, let us consider the following program $P$ :

$w=``a$”$\,;\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ {\mathtt{while}}\leavevmode\nobreak\ true\leavevmode\nobreak\ {\mathtt{do}}\leavevmode\nobreak\ {\mathit{print\leavevmode\nobreak\ w\,;}}\leavevmode\nobreak\ \leavevmode\nobreak\ w=``b$”$\,w\,``c$”$\,;\leavevmode\nobreak\ \leavevmode\nobreak\ \pi_{\_}{0}\leavevmode\nobreak\ {\mathtt{od}}$

When I first presented this hierarchy definition at a conference, I met my dear colleague Philippe Flajolet (1948-2011) and he said to me: “I have already studied these topics [25]. You should look at the immune sets.” That remark motivated my first encounter with Roger’s book on recursivity [67] 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 [50]. 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 [51]. 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 [21]. 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)\rightarrow f(y,z,x)$ is a left linear rule, while $f(x,y,x)\rightarrow g(y,x)$ is not. During a conference coffee-break, Jean-Jacques showed me a simple inductive proof of Fact 1 [51, pages 436–437] using bounded lexicographic orderings (actually, that proof is based on a non-predicative definition of the non-ascending rewriting rules).

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,$\ldots$”. 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 [10] he was developing at that time. The language NPL later evolved into Hope [12]. While at Edinburgh, I wrote a paper [48] 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 [11]. Some time before, Rod had received a letter from Professor Edger W. Dijkstra (1930-2002) proposing the following ‘exercise’ in program transformation: the derivation of an iterative program for the fusc function [23, pages 215–216, 230–232]:

${\mathtt{fusc(0)=0}}$ ${\mathtt{fusc(1)=1}}$

${\mathtt{fusc(2n)=fusc(n)}}$ ${\mathtt{fusc(2n\!+\!1)=fusc(n\!+\!1)+fusc(n)}}$     for ${\mathtt{n\!\geq\!0}}$

To do the same exercise Bauer and Wössner [5, page 288] use an embedding into a linear combination, that is, they define the function ${\mathtt{F(n,a,b)=_{\_}{\mathit{def}}}}$ $\mathtt{a\!\times\!{\mathtt{fusc}}(n)+b\!\times\!fusc(n\!+\!1)}$. Using that function, they are able to derive for fusc a program that is linear recursive and also tail-recursive. 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 [11] 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 $\mathtt{fusc}$, we introduce the tuple function $\mathtt{t(n)=_{\_}{def}\langle fusc(n),\leavevmode\nobreak\ fusc(n\!+\!1)\rangle}$ and we get the following recursive equations for $\mathtt{fusc}$:

${\mathtt{fusc(n)=u}}$ ${\mathtt{where\leavevmode\nobreak\ \langle u,v\rangle=t(n)}}$   for ${\mathtt{n\!\geq\!0}}$

${\mathtt{t(0)=}}$ {by unfolding} $\mathtt{=\langle fusc(0),\leavevmode\nobreak\ fusc(1)\rangle=}$ {by unfolding} $\mathtt{=\langle 0,1\rangle}$

${\mathtt{t(2n)=}}${by unfolding} $\mathtt{=\langle fusc(2n),\ fusc(2n\!+\!1)\rangle=}$ {by unfolding} =
$\mathtt{=\leavevmode\nobreak\ \langle fusc(n),\ fusc(n\!+\!1)\!+\!fusc(n)\rangle=}$ {by $\mathtt{where}$ abstraction [11]} =
$\mathtt{=\leavevmode\nobreak\ \langle u,u\!+\!v\rangle}$$\mathtt{where\langle u,v\rangle=\langle fusc(n),\leavevmode\nobreak\ fusc(n\!+\!1)\rangle}$ = {by folding} =
${\mathtt{=\leavevmode\nobreak\ \langle u,u\!+\!v\rangle}}$where ${\mathtt{\langle u,v\rangle=t(n)}}$   for ${\mathtt{n\!>\!0}}$

${\mathtt{t(2n\!+\!1)\!=\!\langle u\!+\!v,v\rangle}}$ where ${\mathtt{\langle u,v\rangle=t(n)}}$   for ${\mathtt{n\!\geq\!0}}$ (by a derivation similar to that of $\mathtt{t(2n)}$)  

I used the following schema equivalence (such as the ones in [70]) stating that $\mathtt{t(n)}$ defined by the non-tail recursive equations:

$\mathtt{t(0)=a}$

$\mathtt{t(2n)=b(t(n))}$ for $\mathtt{n\!>\!0}$

$\mathtt{t(2n+1)=c(t(n))}$ for $\mathtt{n\!\geq\!0}$

${\mathtt{res\!=\!a;\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ p\!=\!\ell;}}$ ${\mathtt{while\leavevmode\nobreak\ p\!\geq\!0\leavevmode\nobreak\ do\leavevmode\nobreak\ if\leavevmode\nobreak\ \leavevmode\nobreak\ B[p]\!=\!0\leavevmode\nobreak\ \leavevmode\nobreak\ then\leavevmode\nobreak\ \leavevmode\nobreak\ res\!=\!b(res)\leavevmode\nobreak\ \leavevmode\nobreak\ else\leavevmode\nobreak\ \leavevmode\nobreak\ res\!=\!c(res)\,;\leavevmode\nobreak\ \leavevmode\nobreak\ p=p\!-\!1\leavevmode\nobreak\ \leavevmode\nobreak\ od}}$

${\mathtt{\{n\!\geq\!0}}\leavevmode\nobreak\ \leavevmode\nobreak\ \wedge\leavevmode\nobreak\$ $\mathtt{n=\sum_{\_}{p=0}^{\ell}B[p]\cdot 2^{p}}$}

${\mathtt{\langle u,v\rangle=\langle 0,1\rangle;}}$      ${\mathtt{p=\ell;}}$

${\mathtt{while\leavevmode\nobreak\ p\!\geq\!0}}$ ${\mathtt{do\leavevmode\nobreak\ }}$${\mathtt{if\leavevmode\nobreak\ \leavevmode\nobreak\ B[p]\!=\!0\leavevmode\nobreak\ \leavevmode\nobreak\ then\leavevmode\nobreak\ \leavevmode\nobreak\ v=u\!+\!v\leavevmode\nobreak\ \leavevmode\nobreak\ else\leavevmode\nobreak\ \leavevmode\nobreak\ u=u\!+\!v\,;}}$${\mathtt{p=p\!-\!1\leavevmode\nobreak\ od}}$

$\{{\mathtt{\langle u,v\rangle\!=\!t(n)}}\leavevmode\nobreak\ \leavevmode\nobreak\ \wedge\leavevmode\nobreak\ \leavevmode\nobreak\ {\mathtt{u\!=\!fusc(n)}}\}$

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 [42], which computes the Fibonacci function $\mathtt{fib(n)}$ using an $O(\log$ $\mathtt{n}$$)$ number of arithmetic operations. Here is the definition of the Fibonacci function:

${\mathtt{fib(0)\!=\!0\hskip 56.9055ptfib(1)\!=\!1}}$

${\mathtt{fib(n\!+\!2)=fib(n\!+\!1)+fib(n)}}$  for ${\mathtt{n\!\geq\!0}}$ $(\dagger 1)$ 

${\mathtt{fib(0)\!=\!0\hskip 56.9055ptfib(1)\!=\!1}}$

${\mathtt{fib(n\!+\!2)\!=\!u}}$   where ${\mathtt{\langle u,v\rangle=g(n\!+\!2)}}$            for ${\mathtt{n\!\geq\!0}}$

${\mathtt{g(1)=}}$ $\mathtt{\langle 1,0\rangle}$

${\mathtt{g(n\!+\!2)\!=\!\langle u\!+\!v,u\rangle}}$ where ${\mathtt{\langle u,v\rangle=g(n\!+\!1)}}$       for ${\mathtt{n\!\geq\!0}}$

${\mathtt{g(0)\!=\!a}}$ ${\mathtt{g(n\!+\!1)\!=\!b(g(n))}}$  for ${\mathtt{n\!\geq\!0}}$

${\mathtt{res\!=\!a;}}$ ${\mathtt{while\leavevmode\nobreak\ n\!>\!0\leavevmode\nobreak\ do\leavevmode\nobreak\ \leavevmode\nobreak\ res=b(res)\,;\leavevmode\nobreak\ \leavevmode\nobreak\ n=n\!-\!1\leavevmode\nobreak\ \leavevmode\nobreak\ od}}$

${\mathtt{\{n\!\geq\!0}}\}$

${\mathtt{if\leavevmode\nobreak\ n\!=\!0\leavevmode\nobreak\ then\leavevmode\nobreak\ u\!=\!0\leavevmode\nobreak\ else}}$

${\mathtt{if\leavevmode\nobreak\ n\!=\!1\leavevmode\nobreak\ then\leavevmode\nobreak\ u\!=\!1\leavevmode\nobreak\ else}}$

${\mathtt{begin\leavevmode\nobreak\ p=n\!-\!1;\leavevmode\nobreak\ \langle u,v\rangle\!=\!\langle 1,0\rangle;\leavevmode\nobreak\ }}{\mathtt{\leavevmode\nobreak\ while\leavevmode\nobreak\ p\!>\!0\leavevmode\nobreak\ do\leavevmode\nobreak\ \langle u,v\rangle\!=\!\langle u\!+\!v,u\rangle\,;\leavevmode\nobreak\ \leavevmode\nobreak\ p=p\!-\!1\leavevmode\nobreak\ od\leavevmode\nobreak\ end}}$

$\{{\mathtt{u\!=\!fib(n)}}\}$

${\mathtt{fib(n\!+\!2)}}$${\mathtt{=fib(n\!+\!1)+fib(n)=}}$ {by unfolding ${\mathtt{fib(n\!+\!1)}}$} =

${\mathtt{=2\cdot fib(n)+fib(n\!-\!1)=}}$ {by unfolding ${\mathtt{fib(n)}}$} =

${\mathtt{=3\cdot fib(n\!-\!1)+2\cdot fib(n\!-\!2)}}$ $(\dagger 2)$ 

In our case the invention of the multiplication operation is reduced to three generalization steps [56]. First, we generalize the initial values 0 and 1 of the function ${\mathtt{fib}}$ to two variables ${\mathtt{a_{\_}{0}}}$ and ${\mathtt{a_{\_}{1}}}$, respectively. (This kind of generalization step is usually done when mechanically proving theorems about functions [8].) By promoting those new variables to arguments, we get the following new function $\mathtt{G}$:

${\mathtt{G(a_{\_}{0},\!a_{\_}{1},\!0)\!=\!a_{\_}{0}\hskip 56.9055ptG(a_{\_}{0},\!a_{\_}{1},\!1)\!=\!a_{\_}{1}}}$

${\mathtt{G(a_{\_}{0},\!a_{\_}{1},\!n\!+\!2)=G(a_{\_}{0},\!a_{\_}{1},\!n\!+\!1)+G(a_{\_}{0},\!a_{\_}{1},\!n)}}$            for ${\mathtt{n\!\geq\!0}}$ $(\dagger 3)$ 

${\mathtt{G(a_{\_}{0},a_{\_}{1},n\!+\!2)\!=\!3\cdot G(a_{\_}{0},a_{\_}{1},n\!-\!1)+2\cdot G(a_{\_}{0},a_{\_}{1},n\!-\!2)}}$ $(\dagger 4)$ 

The third, final generalization consists in generalizing the argument $\mathtt{n\!+\!2}$ on the left hand side of Equation $(\dagger 4)$ to ${\mathtt{n\!+\!k}}$ and promoting the new variable $\mathtt{k}$ to an argument of a new function defined as follows: $\mathtt{F(a_{\_}{0},a_{\_}{1},n,k)=_{\_}{def}G(a_{\_}{0},a_{\_}{1},n\!+\!k)}$.

From the equations defining $\mathtt{F(a_{\_}{0},a_{\_}{1},n,k)}$ we get (the details are in [56, pages 184–185]):

${\mathtt{G(a_{\_}{0},a_{\_}{1},n\!+\!k)=G(0,1,k)\cdot G(a_{\_}{0},a_{\_}{1},n\!+\!1)+G(1,0,k)\cdot G(a_{\_}{0},a_{\_}{1},n)}}$

${\mathtt{G(a_{\_}{0},a_{\_}{1},2k)=G(0,1,k)\cdot G(a_{\_}{0},a_{\_}{1},k\!+\!1)+G(1,0,k)\cdot G(a_{\_}{0},a_{\_}{1},k)}}$ for $\mathtt{k>0}$

${\mathtt{G(a_{\_}{0},a_{\_}{1},2k\!+\!1)=G(0,1,k)\cdot G(a_{\_}{0},a_{\_}{1},k\!+\!2)+G(1,0,k)\cdot G(a_{\_}{0},a_{\_}{1},k\!+\!1)}}$ for $\mathtt{k\geq 0}$

${\mathtt{fib(0)=0\hskip 56.9055ptfib(1)=1}}$

${\mathtt{fib(n\!+\!2)\!=\!u\!+\!v\leavevmode\nobreak\ \leavevmode\nobreak\ where\leavevmode\nobreak\ \langle u,v\rangle=r(n\!+\!1)}}$  for ${\mathtt{n\!\geq\!0}}$

${\mathtt{r(0)=\langle 1,0\rangle}}$

${\mathtt{r(2k)=\langle u^{2}\!+\!v^{2},\ 2uv\!+\!v^{2}\rangle}}$ where ${\mathtt{\langle u,v\rangle=r(k)}}$   for ${\mathtt{k\!>\!0}}$

${\mathtt{r(2k\!+\!1)=\langle 2uv\!+\!v^{2},\ (u\!+\!v)^{2}\!+\!v^{2}\rangle}}$ where ${\mathtt{\langle u,v\rangle=r(k)}}$   for ${\mathtt{k\!\geq\!0}}$

In the paper with Rod Burstall [56] 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 ${\mathtt{fib(n)=(A^{n}-B^{n})/sqrt(5)}}$, where ${\mathtt{A=(1\!+\!sqrt(5))/2}}$ and ${\mathtt{B=(1\!-\!sqrt(5))/2}}$.

From September 1977 to June 1978, I visited the School of Computer and Information Science at Syracuse University, N.Y., USA. I attended courses taught by Professor Alan Robinson, John Reynolds, Lockwood Morris, and Robert Kowalski (at that time a visiting professor from Imperial College, London, UK). It was a splendid occasion for deepening my knowledge about many aspects of Computer Science from such illustrious teachers.

In Syracuse I had the opportunity of reading more carefully some parts of the book Automata Theory, Languages, and Computation by Hopcroft and Ullman [31] and the book Introduction to Mathematical Logic by Mendelson [41]. 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 [36]. I remember the stress put by Kowalski on Keith Clark’s negation as failure semantics for logic programs [13]. 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 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 [53]. While giving a seminar on those results at the University of Warsaw (Poland) Professor Helena Rasiowa²²2Helena Rasiowa and Roman Sikorski gave in 1950 a first algebraic proof of Gödel Completeness Theorem for first-order predicate calculus. 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, [27, page 285]), and the derivation I proposed is also easily mechanizable.

The following Hanoi function ${\mathtt{h(n,A,B,C)}}$ computes the shortest sequence of moves in the free monoid $\mathtt{\{AB,BC,CA,BA,CB,AC\}^{*}}$ to move ${\mathtt{n\,(\geq\!0)}}$ disks from peg ${\mathtt{A}}$ to peg ${\mathtt{B}}$ using peg ${\mathtt{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 $\mathtt{\{A,B,C\}}$. Every disk is of a different size and over any disk only smaller disks can be placed. $\varepsilon$ denotes the empty sequence of moves, and ${\mathtt{::}}$ denotes the concatenation of sequences of moves.

${\mathtt{h(0,A,B,C)=\varepsilon}}$

${\mathtt{h(n\!+\!1,A,B,C)=h(n,A,C,B)::AB::h(n,C,B,A)}}$   for ${\mathtt{n\!\geq\!0}}$ $(\dagger 5)$ 

We get:

${\mathtt{h(0,A,B,C)=\varepsilon}}$ ${\mathtt{h(1,A,B,C)=AB}}$

${\mathtt{h(n\!+\!2,A,B,C)=u::AC::v::AB::w::CB::u}}$${\mathtt{where\leavevmode\nobreak\ \langle u,v,w\rangle=t(n)}}$   for ${\mathtt{n\!\geq\!0}}$

${\mathtt{t(0)=\langle\varepsilon,\varepsilon,\varepsilon\rangle}}$ ${\mathtt{t(1)=\langle AB,BC,CA\rangle}}$

${\mathtt{t(n\!+\!2)=\langle}}$${\mathtt{u::AC::v::AB::w::CB::u,}}$ ${\mathtt{v::BA::w::BC::u::AC::v,}}$

${\mathtt{w::CB::u::CA::v::BA::w\,\rangle}}$${\mathtt{where\leavevmode\nobreak\ \langle u,v,w\rangle=t(n)}}$   for ${\mathtt{n\!\geq\!0}}$

${\mathtt{g(0)\!=\!a}}$       ${\mathtt{g(1)\!=\!b}}$                 ${\mathtt{g(n\!+\!2)\!=\!c(g(n))}}$    for ${\mathtt{n\!\geq\!0}}$

${\mathtt{if\leavevmode\nobreak\ even(n)\leavevmode\nobreak\ \leavevmode\nobreak\ then\leavevmode\nobreak\ \leavevmode\nobreak\ res\!=\!a\leavevmode\nobreak\ \leavevmode\nobreak\ else\leavevmode\nobreak\ \leavevmode\nobreak\ res\!=\!b;}}$

${\mathtt{while\leavevmode\nobreak\ n\!>\!1\leavevmode\nobreak\ do\leavevmode\nobreak\ \leavevmode\nobreak\ res=c(res)\,;\leavevmode\nobreak\ \leavevmode\nobreak\ n=n\!-\!2\leavevmode\nobreak\ \leavevmode\nobreak\ od}}$

${\mathtt{\{n\!\geq\!0}}\}$

${\mathtt{if\leavevmode\nobreak\ \leavevmode\nobreak\ n\!=\!0\leavevmode\nobreak\ \leavevmode\nobreak\ then\leavevmode\nobreak\ \leavevmode\nobreak\ Hanoi\!=\!\varepsilon\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ else}}$

${\mathtt{if\leavevmode\nobreak\ \leavevmode\nobreak\ n\!=\!1\leavevmode\nobreak\ \leavevmode\nobreak\ then\leavevmode\nobreak\ \leavevmode\nobreak\ Hanoi\!=\!AB\leavevmode\nobreak\ \leavevmode\nobreak\ else}}$

${\mathtt{begin\leavevmode\nobreak\ \leavevmode\nobreak\ n\!=\!n\!-\!2;\leavevmode\nobreak\ \leavevmode\nobreak\ if\leavevmode\nobreak\ even(n)\leavevmode\nobreak\ \leavevmode\nobreak\ then\leavevmode\nobreak\ \leavevmode\nobreak\ T\!=\!\langle\varepsilon,\varepsilon,\varepsilon\rangle\leavevmode\nobreak\ \leavevmode\nobreak\ else\leavevmode\nobreak\ \leavevmode\nobreak\ T\!=\!\langle AB,BC,CA\rangle\,;}}$

    ${\mathtt{while\leavevmode\nobreak\ n\!>\!1\leavevmode\nobreak\ do\leavevmode\nobreak\ \leavevmode\nobreak\ T\!=\!\langle\,}}$${\mathtt{T1\!::\!AC\!::\!T2\!::\!AB\!::\!T3\!::\!CB\!::\!T1,}}$ ${\mathtt{T2\!::\!BA\!::\!T3\!::\!BC\!::\!T1\!::\!AC\!::\!T2,}}$

${\mathtt{T3\!::\!CB\!::\!T1\!::\!CA\!::\!T2\!::\!BA\!::\!T3\,\rangle;\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ n\!=\!n\!-\!2\leavevmode\nobreak\ \leavevmode\nobreak\ od\,;}}$

$\mathtt{Hanoi=T1\!::\!AC\!::\!T2\!::\!AB\!::\!T3\!::\!CB\!::\!T1}$

$\mathtt{end}$

$\{\,{\mathtt{Hanoi=h(n,A,B,C)}}\,\}$

In a later paper I addressed the problem of finding the $\mathtt{m}$-th move of algorithms which compute sequences of moves without computing any other move [55]. 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 $\mathtt{m}$-th move without computing any other move. For the case of the Hanoi function $\mathtt{h(n,A,B,C)}$ we have that the length $\mathtt{Lh(n)}$ of the sequence of moves for $\mathtt{n}$ disks, satisfies the following equations: ${\mathtt{Lh(0)=0\hskip 28.45274ptLh(n\!+\!1)=2\cdot Lh(n)\!+\!1}}$   for ${\mathtt{n\!\geq\!0}}$

One can show [55] that the $\mathtt{m}$-th move of $\mathtt{h(n,A,B,C)}$, for $\mathtt{1\!\leq\!m\!\leq\!2^{n}\!-\!1}$ and $\mathtt{n\!\geq\!0}$, can be computed using the deterministic finite automaton of Figure 2. We assume that $\mathtt{M[\ell..0]}$ is the binary expansion of $\mathtt{m}$, the most significant bit being at the leftmost position $\mathtt{\ell}$. Thus, $\mathtt{m=\sum_{\_}{i=0}^{\ell}M[i]\cdot 2^{i}}$ and $\mathtt{m}$ is not a power of $\mathtt{2}$ iff $\mathtt{M[\ell..0]\not\in 10^{*}}$. Let $\mathtt{trans(X,p)}$ denotes the state $\mathtt{Y}$ such that in the finite automaton of Figure 2 there is an arc from state $\mathtt{X}$ to state $\mathtt{Y}$ with label $\mathtt{p}$.

$\mathtt{i\!=\!\ell;\leavevmode\nobreak\ \leavevmode\nobreak\ state\!=\!AB;}$

$\mathtt{while\leavevmode\nobreak\ M[i..0]\not\in 10^{*}\leavevmode\nobreak\ do\leavevmode\nobreak\ }$ $\mathtt{begin\leavevmode\nobreak\ \leavevmode\nobreak\ state=trans(state,M[i]);\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ i=i\!-\!1\leavevmode\nobreak\ \leavevmode\nobreak\ end\leavevmode\nobreak\ od}$

Suppose that we want to compute the $\mathtt{44}$-th move of $\mathtt{h(6,A,B,C)}$. The binary expansion of $\mathtt{44}$ is $\mathtt{101100}$. Starting from the left, we take the prefix $\mathtt{101}$ up to (and excluding) the suffix in $\mathtt{10^{*}}$ (in our case $\mathtt{100}$). We perform the transitions on the automaton of Figure 2 starting from state $\mathtt{AB}$ according to that prefix (from left to right) and we get to state $\mathtt{CA}$. Since the length of the prefix is odd (it is indeed $\mathtt{3}$), the move to be computed is $\mathtt{BA}$, that is, $\mathtt{CA}$ with $\mathtt{B}$ and $\mathtt{C}$ interchanged.

In a subsequent paper with Maurizio Proietti [58] 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 [31]), 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 $\mathtt{t(n\!-\!1)}$ and $\mathtt{t(n\!-\!3)}$. Both of them are of size $\mathtt{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 [45] can be found in my Ph.D. thesis [52].

We used the list introduction strategy for deriving a program for computing the binomial coefficients: $\binom{n+1}{k+1}\!=\!\binom{n}{k}\!+\!\binom{n}{k+1}$. In this case the sequence of cuts from the root to the leaves is of increasing size. Indeed, $\binom{n+1}{k+1}$ requires the computations of $\binom{n}{k}$ and $\binom{n}{k+1}$, which in turns, require the computations of $\binom{n-1}{k-1}$, $\binom{n-1}{k}$, $\binom{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 [58]. An $n\!\times\!n$ board configuration Qs is represented by a list of pairs of the form: $[\langle R_{\_}1,C_{\_}1\rangle,\ldots,\langle R_{\_}n,C_{\_}n\rangle]$, where for $i\!=\!1,\ldots,n$, $\langle R_{\_}i,C_{\_}i\rangle$ denotes a queen placed in row $R_{\_}i$ and column $C_{\_}i$. For $i\!=\!1,\ldots,n$, the values of $R_{\_}i$ and $C_{\_}i$ belong to the list $[1,\ldots,n]$.

We start from the following initial program Queens:

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{1.}&{\it queens}({\it Ns},{\it Qs})\leftarrow{\it placequeens}({\it Ns},{\it Qs}),\ {\it safeboard}({\it Qs})\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{2.}&{\it placequeens}([\,],[\,])\leftarrow\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{3.}&{\it placequeens}({\it Ns},[Q|{\it Qs}])\leftarrow{\it select}(Q,{\it Ns},{\it Ns}1),\ {\it placequeens}({\it Ns}1,{\it Qs})\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{4.}&{\it safeboard}([\,])\leftarrow\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{5.}&{\it safeboard}([Q|{\it Qs}])\leftarrow{\it safequeen}(Q,{\it Qs}),\ {\it safeboard}({\it Qs})\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{6.}&{\it safequeen}(Q,[\,])\leftarrow\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{7.}&{\it safequeen}(Q1,[Q2|{\it Qs}])\leftarrow{\it notattack}(Q1,Q2),\ {\it safequeen}(Q1,{\it Qs})\end{array}$

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 [68, 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 [58]. 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 [6, 16]).

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{8.}&{\it queens}([\,],[\,])\leftarrow\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{9.}&{\it queens}({\it Ns},[Q|{\it Qs}])\leftarrow{\it select\/}(Q,{\it Ns},{\it Ns}1),\ {\it genlist}1({\it Ns}1,{\it Qs},[Q])\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{10.}&{\it genlist}1([\,],[\,],{\it Ps})\leftarrow\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{11.}&{\it genlist}1({\it Ns},[Q1|{\it Qs}],[\,])\leftarrow{\it select}(Q1,{\it Ns},{\it Ns}1),\ {\it genlist\/}1({\it Ns}1,{\it Qs},[Q1])\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{12.}&{\it genlist}1({\it Ns},[Q1|{\it Qs}],[P1|{\it Ps}])\leftarrow{\it select}(Q1,{\it Ns},{\it Ns}1),\ {\it notattack}(P1,Q1),\par\par\end{array}$

$\begin{array}[]{rlll}\hskip 166.44861pt{\it genlist\/}2({\it Ns}1,{\it Qs},[P1],{\it Ps},Q1)\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{13.}&{\it genlist}2({\it Ns}1,{\it Qs},{\it Ps}1,[\,],Q1)\leftarrow{\it genlist\/}1({\it Ns}1,{\it Qs},[Q1|{\it Ps}1])\end{array}$

$\begin{array}[]{rlll}\makebox[22.76228pt][r]{14.}&{\it genlist}2({\it Ns}1,{\it Qs},{\it Ps}1,[P2|{\it Ps}2],Q1)\leftarrow{\it notattack}(P2,Q1),\\ \end{array}$

$\begin{array}[]{rlll}\hskip 193.47873pt{\it genlist\/}2({\it Ns}1,{\it Qs},[P2|{\it Ps}1],{\it Ps}2,Q1)\end{array}$

The explanation which we have just given about the derived program (clauses 8–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.

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 $\mathtt{where}$ abstraction as shown in Section 3 for the $\mathtt{fusc}$ function), you need to fold.” This need for folding [17] 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 [63]. This is done by replacing the expression $\mathtt{E[e]}$ where the subexpression $\mathtt{e}$ occurs, by the application $\mathtt{(\lambda 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 [63]. The first example refers to the following program Reverse for reversing a list, where $\mathtt{[\,]}$, $\mathtt{:}$, and $\mathtt{@}$ denote the empty list, cons, and append on lists, respectively.