Verifying Programs via Intermediate Interpretation
Extracted source text · arXiv 1705.06738
%-----------------------------------------------------------------------------
%
% Verifying Programs via Intermediate Interpretation
% A version for arXiv.
%
%
% Name: lisitsa_nemytykh_vpt-2017.tex
%
% Authors: Alexei P. Lisitsa
% Department of Computer Science, The University of Liverpool
% A.Lisitsa@csc.liv.ac.uk
% and
% Andrei P. Nemytykh
% Program Systems Institute of Russian Academy of Sciences
% nemytykh@math.botik.ru
%
% Version: 18 May 2017, Nemytykh
%
%-----------------------------------------------------------------------------
\documentclass[submission,copyright,creativecommons]{eptcs}
\providecommand{\event}{VPT 2017} % Name of the event you are submitting to
%\providecommand{\publicationstatus}{To appear in EPTCS.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[leqno,fleqn,intlimits]{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amstext}
\usepackage{epsfig}
\usepackage{graphicx}
\usepackage[all,2cell,knot,poly]{xy}
\newtheorem{example}{Example}
\newcommand{\zb}{\hspace{-0.5pt}}
\newcommand{\zbb}{\hspace{-1.0pt}}
\newcommand{\True}{T}
\newcommand{\False}{F}
\newcommand{\conct}{\texttt{:}}
\newcommand{\Nil}{\texttt{[]}}
\newcommand{\boxedNilL}{\boxed{\expr{\var{\Nil}}} ~~\texttt{++}}
\newcommand{\boxedNilR}{~\texttt{++}~~ \boxed{\expr{\var{\Nil}}}}
\newcommand{\append}{~\texttt{++}~}
\newcommand{\Prog}{\pi_0}
\newcommand{\Syn}{\pi_s}
\newcommand{\ccal}[2]{$\cal{#1}$#2}
\newcommand{\empt}{{\epsilon}}
\newcommand{\Nat}{\mathbb N}
\newcommand{\Int}{\mathbb Z}
\newcommand{\Fn}[1]{{\mathbb F}_{#1}}
\newcommand{\edge}{\stackrel{e}{\rightarrow}}
\newcommand{\precc}{\preccurly}
\newcommand{\precceq}{\preccurlyeq}
\newcommand{\notprecc}{\not\precceq}
\newcommand{\notprec}{\not\preceq}
\newcommand{\notpreceq}{\notprec}
\newcommand{\notprecceq}{\notprecc}
\newcommand{\proptoeq}{\;\underline{\propto}\;}
\newcommand{\notpropto}{\rlap{~{$\not$}}\proptoeq}
\newcommand{\notproptoeq}{\notpropto}
\newcommand{\tureq}{\;\trianglelefteq\;}
\newcommand{\tur}{\;\triangleleft\;}
\newcommand{\turprec}{\triangleleft\;\circ\precceq}
\newcommand{\nottureq}{\;\ntrianglelefteq\;}
\newcommand{\nottur}{\;\ntriangleleft\;}
\newcommand{\elev}[1]{_\llcorner{\hspace{-2pt}}#1{\hspace{-2pt}}_\lrcorner}
\newcommand{\ddz}{{{\texttt {\footnotesize{\#}}}\zbb}}
\newcommand{\dddz}{{{\texttt {\tiny{\#}}}\zb}}
\newcommand{\dz}{^{{\texttt {\small{\#}}}\zbb}}
\newcommand{\dzz}{^{{\texttt {\tiny{\#}}}\zbb}}
\newcommand{\rdot}{{\zb}.{\zb}}
\newcommand{\lsem}{\mbox{$\lbrack\hspace{-0.3ex}\lbrack$}}
\newcommand{\rsem}{\mbox{$\rbrack\hspace{-0.3ex}\rbrack$}}
\newcommand{\sempar}[1]{\mbox{\lsem\pgt{#1}\rsem}}
\newcommand{\semparlang}[2]{\sempar{#1}$^\pgt{#2}$}
\newcommand{\expr}[1]{#1{}}
\newcommand{\var}[2]{\mathit{#1}#2}
\newcommand{\patts}[2]{#1{,~#2}}
\newcommand{\threepatts}[3]{#1{,~#2}{,~#3}}
\newcommand{\fourpatts}[4]{#1{,~#2}{,~#3}{,~#4}}
\newcommand{\patt}[3]{#1{~#2{#3}}}
\newcommand{\app}[3]{#1{~#2{#3}}}
\newcommand{\fapp}[3]{\var{#1}(~#2\;)#3}
\newcommand{\tapp}[1]{{<}~#1~{>}}
\newcommand{\args}[2]{#1{,~#2}}
\newcommand{\threeargs}[3]{#1{,~#2}{,~#3}}
\newcommand{\fourargs}[4]{#1{,~#2}{,~#3}{,~#4}}
\newcommand{\brackets}[2]{(#1{)#2}}
\newcommand{\curly}[2]{\{#1{\}#2}}
\newcommand{\fdef}[1]{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{#1{~{\{}}} & {} & {}\end{array}}
\newcommand{\sent}[2]{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{~~} #1{} & \Rightarrow & #2{;}{}\end{array}}
\newcommand{\fend}{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{}{\}}& {} & {} \end{array}}
\newcommand{\fsent}[3]{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{\var{#1}{(~}} #2{~)} & \Rightarrow & #3{;}{}\end{array}}
\newcommand{\lfsent}[3]{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{\var{#1}{(~}} #2{~)} & &\\ {\hspace*{35pt}} \Rightarrow #3{;}{} & &\end{array}}
\newcommand{\fnew}{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}} & & \end{array}}
\newcommand{\encodfsent}[3]{{\small \underline{ \begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{\var{#1}{(~} #2{~)}} & \Rightarrow & #3{;}{} \end{array}}}}
\newcommand{\encodlfsent}[3]{{\small \begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{\underline{\var{#1}{(~} #2{~)}}} & &\\ {\hspace*{35pt}} \underline{\Rightarrow #3{;}}{} & &\end{array}}}
\newcommand{\sentshift}{\hspace{20pt}}
\newcommand{\shiftfsent}[3]{\fsent{{\sentshift}#1}{#2}{#3}}
\newcommand{\shiftshiftfsent}[3]{\fsent{{\sentshift}{\sentshift}#1}{#2}{#3}}
\newcommand{\shiftlfsent}[3]{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}\sentshift{\var{#1}{(~}} #2{~)} & &\\ {\hspace*{35pt}} \sentshift\Rightarrow #3{;}{} & &\end{array}}
\newcommand{\psent}[2]{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{{~~}} #1{~} & \rightarrow & #2{~.}{}\end{array}}
\newcommand{\pprop}[1]{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{{~~}} #1{~}\end{array}}
\newcommand{\ensent}[3]{\begin{array}[t]{@{\hspace*{1mm}}l@{\hspace*{1mm}}c@{\hspace*{1mm}}l@{\hspace*{1mm}}}{\mathfrak{{#1}{(~}}} #2{~)} & = & #3{}{}\end{array}}
\newcommand{\enapp}[3]{\mathfrak{{#1}(}~#2\;\mathfrak{)}#3}
\newtheorem{theorem}{Theorem}
\newtheorem{proposition}{Proposition}
\newtheorem{corollary}{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{note}{Note}
\newtheorem{proof}{Proof}
\newtheorem{lemma}{Lemma}
\newtheorem{remark}{Remark}
\title{Verifying Programs via Intermediate Interpretation
}
\author{Alexei P. Lisitsa
\institute{Department of Computer Science,\\ The University of Liverpool
}
\email{{a.lisitsa@liverpool.ac.uk}}
\and
Andrei P. Nemytykh
\institute{Program Systems Institute,\\ Russian Academy of Sciences\thanks{The second author was supported by RFBR, research project No. 17-07-00285\_a}
}
\email{\quad {nemytykh@math.botik.ru}}
}
\def\titlerunning{Verifying Programs via Intermediate Interpretation}
\def\authorrunning{A.\,P. Lisitsa, A.\,P. Nemytykh}
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\maketitle
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{abstract}
We explore an approach to verification of programs via program transformation applied to an interpreter of a programming language.
A specialization technique known as Turchin's supercompilation is used to specialize some interpreters with respect to the program models.
We show that several safety properties of functional programs modeling a class of cache coherence protocols can be proved by a supercompiler and compare the results with our earlier work on direct verification via supercompilation not using intermediate interpretation.
Our approach was in part inspired by an earlier work by De\,E.~Angelis et al. (2014-2015) where verification via program transformation and intermediate interpretation was studied in the context of specialization of constraint logic programs.
\noindent
\textbf{\textit{Keywords:}}
program specialization, supercompilation, program analysis, program transformation, safety verification, cache coherence protocols
\end{abstract}
\section{Introduction}\label{sec:Introduction}
We show that a well-known program specialization task called the first Futamura projection \cite{Futamura:1971, Turchin:Report20, Jones:IntSpecialisation}
can be used for indirect verifying some safety properties of functional program modeling a class of non-deterministic parameterized computing systems specified in a language
that differs from the object programming language treated by a program specializer deciding the task.
Let a specializer transforming programs written in a language ${\cal L}$ and an interpreter \texttt{Int}$_{\cal M}$ of a language ${\cal M}$, which is also implemented in ${\cal L}$, be given. Given a program \texttt{p$_0$} written in ${\cal M}$, the mentioned task is to specialize the interpreter \texttt{Int$_{\cal M}$(p$_0$,d)} with respect to its first argument, while the data \texttt{d} of the program \texttt{p$_0$} is unknown.
Our interest in this task has been inspired
by the following works \cite{FioPettProSen:Ver-IterSpec14, FioPettProSen:Ver-Linear-Fib15} especially the presentation given by the authors of these articles at the Workshop VPT-2015. The authors work in terms of \emph{constraint logic programming} (CLP), where the constraint language is the linear arithmetic inequalities imposed on integer values of variables. They use partial deduction \cite{Leuschel:04} and CLP program specialization \cite{FioPettPro:01, VeriMAP:2014} methods for specializing an interpreter of a C-like language with respect to given programs, aiming at verification of the C-like imperative specifications with respect to the postconditions defined in CLP and defining the same functions (relations) as done by the corresponding C-like programs.
Additionally to the CLP program specialization developed by De\,E.~Angelis et al. and called VeriMAP \cite{VeriMAP:2014} they also use external satisfiability modulo theories (SMT) solvers.
%
We would also refer to an earlier work by J.\,P. Gallagher et al. \cite{GH:1998} reported on a language-independent method for analyzing the imperative programs via intermediate interpretation by
a logic programming language. The success of such a method depends eventually on the analysis tools available for the logic programming languages.
%
Note that the transformation examples given in the papers \cite{GH:1998, FioPettPro:01, VeriMAP:2014} presenting the both mentioned approaches deal with neither function nor constructor application stack in the interpreted programs.
In this paper we focus our attention on
self-sufficient methods for specialization of functional programs, aiming at proving some \emph{safety} properties of the programs.
Such a property problem is a (un)rea\-cha\-bi\-li\-ty problem meaning that when a program is running, an unsafe program configuration cannot be reached from any initial configuration.
We consider a program specialization method called Turchin's supercompilation \cite{Tur:86, Turchin:Report20, SGJ:96, Jonsson_Nordlander} and study potential capabilities of the method for verifying the safety properties of the functional programs modeling a class of non-deterministic parameterized cache coherence protocols \cite{Delzanno-Param:00}.
We use an approach to functional modeling of non-deterministic computing systems, first presented by these authors in \cite{Lis_Nem:CSR07, Lis_Nem:Programming, Lis_Nem:IJFCS08}. The simple idea behind the approach is as follows. Given a program modeling a deterministic computing system, whose behavior depends on and is controlled by an input parameter value, let us call for an oracle producing the input value. Then the meta-system including both the program and the external oracle becomes non-deterministic one. And vice versa, given a non-deterministic system,
one may be concerned about the behavior of the system only along one possible path of the system evaluation. In such a case, the path of interest may be given as an additional input argument of the system, forcing the system to follow along the path. Dealing with unknown value of the additional parameter one can study any possible evolution of the non-deterministic system, for example, aiming at verifying some properties of the system.
Viability of such an approach to verification has been demonstrated in previous works using supercompilation as a program transformation and analyzing technique \cite{Lis_Nem:CSR07, Lis_Nem:Programming, Lis_Nem:IJFCS08, Lis_Nem:Protocols07,Klimov:PetriNets12}, where it was applied to safety verification of program models of parameterized protocols and Petri Nets models.
Furthermore, the functional program modeling and supercompilation have been used to specify and verify cryptographic protocols, and in the case of insecure protocols a supercompiler was utilized in an interactive search for the attacks on the protocols
\cite{AhmedLisitsaNemytykh:NSPK,ANepeivoda:PingPong}.
In these cases the supercompiler has been used for specializing the corresponding program models, aiming at moving the safety properties of interest from the semantics level of the models to simplest syntactic properties of the residual programs produced by the supercompiler. Later this approach was extended by G.\,W. Hamilton for verifying a wider class of temporal properties of reactive systems \cite{Hamilton:VPT2015, Hamilton:VPT2016}.
Given a specializer transforming the program written in a language ${\cal L}$ and used for program model verification, in order to mitigate the limitation of the specification language ${\cal L}$, in this paper we study potential abilities of the corresponding specialization method for verifying the models specified in another language ${\cal M}$, removing the intermediate interpretation overheads.
%
We analyze the supercompilation algorithms allowing us crucially to remove the interpretation layer and to verify indirectly the safety properties. The corresponding experiments succeed in verifying some safety properties of the series of parameterized cache coherence protocols specified, for example, in the imperative WHILE language by N.\,D. Jones \cite{Jones:Complex}. Nevertheless, in order to demonstrate that our method is able to deal with non-imperative interpreted programs, we consider the case when a modelling language ${\cal M}$ is a non-imperative subset of the basic language ${\cal L}$. On the other hand, that allows us to simplify the presentation.
%
In order to prove the properties of interest, some our program models used in the experiments required one additional supercompilation step (i.e., the corresponding residual programs should be supercompiled once again\footnote{Note that the method presented in the papers \cite{FioPettProSen:Ver-IterSpec14, FioPettProSen:Ver-Linear-Fib15} mentioned above sometimes requires a number of iterations of the specialization step and the number is unknown.
}).
The considered class of cache coherence protocols effectively forms a benchmark on which various methods for parameterized verification have been tried \cite{Delzanno-Param:00,Lis_Nem:Programming, Lis_Nem:IJFCS08}.
In \cite{Lis_Nem:Programming, Lis_Nem:IJFCS08} we have applied direct verification via supercompilation approach without intermediate interpretation.
The corresponding models may be very large and the automatic proofs of their safety properties may have very complicated structures.
See, for example, the structure of the corresponding proof \cite{Lis_Nem:Protocols07} produced by the supercompiler SCP4 \cite{N:03, Nemytykh:SCP4book, NT:00} for the functional program model of the parameterized Two Consumers - Two Producers (2P/2C) protocol for multithreaded Java programs \cite{Begin:BABYLON}.
Taking that into account, the experiment presented in this paper can also be considered as a partial verification of the intermediate interpreters \texttt{Int$_{\cal M}$(p,d)} used in the experiments. That is to say, a verification of the interpreters with respect to the subset of the input values of the argument \texttt{p}, being the program models of the cache coherence protocols.
A supercompiler is a program specilalizer based on the supercompilation technique. The program examples given in this paper were specialized by the supercompiler SCP4 \cite{N:03, Nemytykh:SCP4book, NT:00}.
We present our interpreter examples in a variant of a pseudocode for a functional program while real supercompilation experiments with the programs were done in the strict functional programming language Refal \cite{Turchin:Refal5}\footnote{The reader is welcome to execute several sample Refal programs and even any program written by the user directly from the electronic version of the Turchin book.},
\cite{Refal5:PZ} being both the object and implementation language of the supercompiler SCP4.
%
One of advantages of using supercompilation, instead of other forms of partial evaluation or CLP specialization, is the use of Turchin's relation \ref{subsec:Turchin} (see also \cite{Turchin:Generalization88, Nemytykh:SCP4book, AntoninaNepeivoda:VPT2016}) defined on function-call stacks, where the function calls are labeled by the times when they are generated by the unfold-fold loop. This relation is responsible for accurate generalizing the stack structures of the unfolded program configurations. It is \emph{based on global properties} of the path in the corresponding unfolded tree rather than on the structures of two given configurations in the path. Turchin's relation both stops the loop unfolding the tree and \emph{provides an evidence of how a given call-stack structure has to be generalized}. Proposition \ref{prop:Match} proven in this paper shows that a composition of the Turchin and Higman-Kruskal relations may prevent generalization of two given interpreter configurations encountered inside one big-step of the interpreter. Such a prevention from generalization is crucial for optimal specialization of any interpreter with respect to a given program.
This paper assumes that the reader has basic knowledge of concepts of functional programming, pattern matching, term rewriting systems, and program specialization.
%\vspace{-5pt}
\paragraph{The contributions of this paper are:}
(1) Developing a method aiming at uniform reasoning on properties of configurations' sequences that are encountered in specializing an interpreter of a Turing complete language.
(2) In particular, we have proved the following statement. Consider specialization of the interpreter with respect to any interpreted program from an infinite program set
that is large enough to specify a series of parameterized cache coherence protocols, controlled by a composition of the Turchin \ref{subsec:Turchin} and Higman-Kruskal \ref{subsec:Higman-Kruskal} relations. Given a big-step of the interpreter to be processed by the unfold-fold loop, we assume that no both generalization and folding actions were still done by this loop up to the moment considered. Then any two non-transitive \ref{subsec:Strategy} big-step internal configurations $C_1, C_2$ are prevented from both generalization and folding actions.
(3) We show that supercompilation controlled by the composition of the relations above is able to verify some safety properties of the series of parameterized cache coherence protocols via intermediate interpretation of their program models. Note that these program specifications include both the function call and constructor application stacks, where the size of the first one is uniformly bounded on the input parameter while the second one is not.
Unlike VeriMAP \cite{VeriMAP:2014} our indirect verification method involves no post-specialization unfold-fold.
%
The paper is organized as follows. In Section \ref{sec:Self-Interpreter} we describe the syntax and semantics of a pseudocode for a subset of the strict functional language Refal which will be used throughout this paper. We also give the operational semantics of the subset, defining its ``self-interpreter''. In Section \ref{sec:Specifying-Cache} we outline our approach for specifying non-deterministic systems by an example used through this paper.
In Section \ref{sec:Supercompilation} we shortly introduce an unfold-fold program transformation method known as Turchin's supercompilation that is used in our experiments presented in this paper. We describe the strategy controlling the unfold-fold loop. The corresponding relation is a composition of Turchin's relation and a variant of the Higman-Kruskal relation. This composition plays a central role in verifying the safety properties of the cache coherence protocols' models via intermediate interpretation.
In Section \ref{sec:Verif-Method-in-Action} we prove in a uniform way a number of properties of a huge amount of the complicated configurations generated by specialization of the self-interpreter with respect to the given program modeling a cache coherence protocol. The argumentations given in the section are applicable for the whole series of the protocols mentioned in Section \ref{sec:Conclusion}. Developing the method of such argumentations is the main aim of the paper and \emph{both Proposition \ref{prop:Match} and the proof of this proposition are the main results of the paper}. The statement given in Proposition \ref{prop:Match} can be applied to a wide class of interpreters of Turing complete programming languages. This statement is a theoretical basis to the following. Why the approach suggested in the paper does succeed in verifying the safety properties of the series of the cache coherence protocols via intermediate interpretation.
Finally, in Section \ref{sec:Conclusion} we report on some other experimental results obtained by using the approach, discuss the results presented in the paper, and compare our experiments with other ones done by existing methods.
\section{An Interpreter for a Fragment of the SCP4 Object Language}\label{sec:Self-Interpreter}
A first interpreter we consider is an interpreter of a subset {${\cal L}$} of the SCP4 object language, which we aim to put in between the supercompiler SCP4 and programs
modeling the cache coherence protocols to be verified.
%
We will refer to this interpreter as a ``self-interpreter''.
In this section, we describe the syntax and semantics of a pseudocode for the subset of the strict functional language Refal which will be used throughout this paper. We also give the operational semantics (that is, the interpreter) of the subset.
\subsection{Language}\label{subsec:Self-Int-Language}
\begin{center}
\begin{tabular}{rll}
$\expr{\var{prog}}$ ::= & $\expr{\var{def_{1}}}$ $~\ldots~$ $\expr{\var{def_{n}}}$ & Program
\\
$\expr{\var{def}}$ ::= &
${\expr{\var{f}}\expr{\brackets{~\expr{\patt{\var{ps_{1}}}}}}}\Rightarrow$ $\expr{\var{exp_{1}}};$ $~\ldots;~$
${\expr{\var{f}}\expr{\brackets{~\expr{\patt{\var{ps_{n}}}}}}}\Rightarrow$ $\expr{\var{exp_{n}}};$
& Function Definition
\\
$\expr{\var{exp}} ::=$ & $\expr{\var{v}}$ & Variable\\
$|$ & $\expr{\expr{\var{term}}}{\;:\;}\expr{\var{exp}}$ & $\expr{\var{Cons}}$ Application\\
$|$ & $\expr{\var{f}}\textbf{(}$ $\expr{\var{exp_{1}}},$ $\expr{\var{...}},$ $\expr{\var{exp_{n}}}$ $\textbf{)}$ & Function Application\\
$|$ & $\expr{\var{exp_{1}}}$ $\textbf{++}$ $\expr{\var{exp_{2}}}$ & $\expr{\var{Append}}$ Application\\
%$|$ & $\sigma$ & Symbol\\
$|$ & $\Nil$ & $\expr{\var{Nil}}$\\
%\\
$\expr{\var{term}}$ ::= & $s\textbf{.}name$ & Symbol-Type Variable \\
$|$ & $(exp)$ & Constructor Application \\
$|$ & $\sigma$ & Symbol\\
\\
$\expr{\var{ps}}$ ::= & $\expr{\var{p_{1}}},$ $\expr{\var{...}},$ $\expr{\var{p_{n}}}$ & Patterns\\
%\\
$\expr{\var{p}}$ ::= & $\expr{\var{v}}$ & \\
$|$ & ${s}\textbf{.}name{\;:\;}\expr{\expr{\var{p}}}$ & \\
$|$ & $\expr{\brackets{\expr{\var{p_{1}}}}}{\;:\;}\expr{\var{p_{2}}}$ & \\
$|$ & $\sigma{\;:\;}\expr{\var{p}}$ & \\
$|$ & $\texttt{[]}$ & \\
\\
$\expr{\var{v}}$ ::= & $s\textbf{.}name$ $|$ $e\textbf{.}name$ & Variable%\\
%\\
\end{tabular}
\end{center}
Programs in {${\cal L}$} are \emph{strict} term rewriting systems based on pattern matching.
The rules in the programs are ordered from the top to the bottom to be matched.
To be closer to Refal we use two kinds of variables: \emph{s.}variables range over \emph{symbols} (i.e., characters and identifiers, for example, $\texttt{'a'}$ and $\expr{\var{True}}$), while \emph{e.}variables range over the whole set of the \texttt{S}-expressions.\footnote{This fragment of Refal is introduced for the sake of simplicity. The reader may think that the syntactic category $\expr{\var{exp}}$ of list expressions and the parenthesis constructor are Lisp equivalents. Actually Refal does not include $\expr{\var{Cons}}$ constructor but, instead of $\expr{\var{Cons}}$, $\expr{\var{Append}}$ is used as an associative constructor. Thus the Refal data set is wider as compared with the Lisp data set: the first one is the set of finite sequences of \emph{arbitrary} trees, while the second one is the set of binary trees. See \cite{Turchin:Refal5} for details.\label{foot:append}}
Given a rule
${\expr{\var{l}}}\Rightarrow$ $\expr{\var{r}}$,
any variable of
$\expr{\var{r}}$ should appear in
${\expr{\var{l}}}$.
%
Each function ${\expr{\var{f}}}$ has a fixed arity, i.e., the arities of all left-hand sides of the rules of ${\expr{\var{f}}}$ and any expression $\expr{\var{f}}\textbf{(}~\expr{\var{exp_{1}}},\; \expr{\var{...}},\; \expr{\var{exp_{n}}}~\textbf{)}$
must equal the arity of ${\expr{\var{f}}}$.
%
The parenthesis constructor {$(\bullet)$} is used without a name. {$Cons$} constructor is used in infix notation and may be omitted.
The patterns in a function definition are not exhaustive. If no left-hand side of the function rules matches the values assigned to a call of the function, then executing the call is interrupted and its value is undefined.
In the sequel, the expression set is denoted by {$\mathbb{E}$};
{$\mathbb{D}$} and {$\mathbb{S}$} stand for
the data set, i.e., the patterns containing no variable, and the symbols set, respectively.
The name set of the functions of an arity {$n$} is denoted by {$\Fn{n}$} while {$\mathbb{F}$} stands for
{$\bigcup_{n=0}^{\infty} \Fn{n}$}.
${\cal V}_e$ and ${\cal V}_s$
stand for the \emph{e}- and \emph{s}-variable sets, respectively, and ${\cal V}$ denotes
${\cal V}_e \cup {\cal V}_s$. Let an expression {$\expr{\var{exp}}$} be given.
{${\cal V}_e(\expr{\var{exp}})$}, {${\cal V}_s(\expr{\var{exp}})$}, {${\cal V}(\expr{\var{exp}})$} denote the corresponding variable sets of {$\expr{\var{exp}}$}.
$\expr{\var{\mu_v(exp)}}$ denotes the multiplicity of $v \in {\cal V}$ in {$\expr{\var{exp}}$}, i.\,e., the number of all the occurrences of $v$ in {$\expr{\var{exp}}$}.
{$\expr{\var{exp}}$} is called passive if no function application occurs in {$\expr{\var{exp}}$} otherwise it is called an active expression.
${\cal T}$ stands for the term set, $\sigma$ stands for a symbol.
%
Given an expression $\expr{\var{exp}}$ and a variable substitution {$\theta$}, $\expr{\var{exp}}\theta$ stands for $\theta(\expr{\var{exp}})$.
\subsection{Encoding}\label{subsec:Encoding}
In our experiments considered in this paper the protocol program models have to be input values of the interpreter argument with respect to which the interpreter is specialized. Thus the program model should be encoded in the data set of the implementation language of the interpreter.
The program models used in this paper are written in a fragment of the language described in Section \ref{subsec:Self-Int-Language}, where $\append$ constructor is not allowed and only unary functions may appear.
Now we have to define the corresponding encoding function
denoted by the underline,
where the function $\mathfrak{A}$ groups the program rules belonging to the same function as it is
shown in the second definition line.
\begin{center}
\begin{tabular}{ll}
%
{$\expr{\underline{\expr{\var{prog}}}}$} $=$ {$\expr{\brackets{~~\underline{\expr{\enapp{A}{\expr{\var{prog}}}}}~~}};$}
& Program \\
%
{$\expr{\underline{{\expr{\var{f}}{\,}{\{}\expr{\var{rules}}{\}~}\expr{\var{defs}}}}}$} $=$ {$\expr{\brackets{{\var{f}~~\underline{\expr{\var{rules}}}~}}}$}{\;:\;}{$\underline{\expr{\var{defs}}};$}
& Function Definitions \\
%
{$\expr{\underline{{\expr{\var{rule;}}{~\;}\expr{\var{rules}}}}}$} $=$ {$\expr{\brackets{{~\underline{\expr{\var{rule}}}~~}}}$}{\;:\;}{$\underline{\expr{\var{rules}}};$}
& Rules \\
%
{$\expr{\underline{\fapp{\expr{\var{f}}}{\var{pattern}}{\;\Rightarrow\;}\expr{\var{exp}}}}$} $=$
{$\expr{\brackets{{~~\underline{\expr{\var{pattern}}}~~}}}$} {\;:\;}\texttt{'='}{\;:\;} {$\expr{\brackets{{~~\underline{\expr{\var{exp}}}~~}}};$}
& Rule \\
%
{$\expr{\underline{\expr{\var{term}}{\;:\;}\expr{\var{exp}}}}$} $=$
{$\expr{{\underline{\expr{\var{term}}}}}$} {\;:\;} {$\expr{{\underline{\expr{\var{exp}}}}};$}
&
%\texttt{--}
Here
$\var{term}$ ${::=}$ $(\var{exp})$ $|$ $\var{s.name}$ $|$ $\sigma$ \\
%
%Encode((expr) = ('*' Encode(expr))
{$\expr{\underline{\expr{\brackets{\expr{\var{exp}}}}}}$} $=$
{$\expr{\brackets{{\texttt{'*'}~\;\underline{\expr{\var{exp}}}~}}};$}
%
\hspace{60pt}
{$\expr{\underline{\fapp{\expr{\var{f}}}{\var{exp}}{}}}$} $=$
{$\expr{\brackets{{\var{Call}~\;\var{f}~\;\underline{\expr{\var{exp}}}~}}};$}
& Applications \\
%
% {$\expr{\underline{\fapp{\expr{\var{f}}}{\var{expr}}{}}}$} $=$
% {$\expr{\brackets{{\var{Call}~\;\var{f}~\;\underline{\expr{\var{expr}}}~~}}};$}
% & \\
%
%Encode(e.name) = (Var 'e' name)
{$\expr{\underline{\var{e.name}{}}}$} $=$
{$\expr{\brackets{\expr{\var{Var}}~\;\var{\texttt{'}e\texttt{'}}~\;\expr{\var{name}}}};$}
\hspace{25pt}
{$\expr{\underline{\var{s.name}{}}}$} $=$
{$\expr{\brackets{\expr{\var{Var}}~\;\var{\texttt{'}s\texttt{'}}~\;\expr{\var{name}}}};$}
& Variables \\
%
% {$\expr{\underline{\var{s.name}{}}}$} $=$
% {$\expr{\brackets{\expr{\var{Var}}~\;\var{\texttt{'}s\texttt{'}}~\;\expr{\var{name}}}}$}
% & \\
%
%Encode(SYMBOL) = SYMBOL
{$\expr{\underline{[]}}$} $=$ {$[];$}
\hspace{120pt}
%Encode(SYMBOL) = SYMBOL
{$\expr{\underline{\var{\sigma}{}}}$} $=$ {$\var{\sigma};$} &
{$\var{Nil}$} and Symbol\\
%
% {$\expr{\underline{[]}}$} $=$ {$[];$} &
%\ensent{M}{[]}{[]} &
%
%\end{center}
\end{tabular}\label{Encoding}
\end{center}
Note that any pattern is an expression.
Supercompiler SCP4 in its processing dealing with programs as input data uses this
encoding function and utilizes its properties.
%
%
The image of $\mathbb{D}$ under the encoding is a proper subset of $\mathbb{D}$, i.\,e., $\underline{\mathbb{D}} \neq \mathbb{D}$.
For example, $\expr{\brackets{\expr{\var{Var}}~\var{\texttt{'}s\texttt{'}}~\expr{\var{name}}}} \notin \underline{\mathbb{D}}$.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
{\small
\begin{figure}[htb]
%\fbox{\parbox{12cm}{
%\fbox{\parbox{330pt}{
\begin{center}
{\hrule height 0.8pt \medskip}
%
% *$ENTRY
% Int { (Call s.f e.d) e.P = <Eval <EvalCall s.f (e.d) e.P> e.P>; }
%
\fsent{Int}{\patts{\brackets{\patt{\patt{\var{Call}}{\var{s.f}}}{\var{e.d}}}}{\var{e.P}}}{\fapp{Eval}{\args{\fapp{EvalCall}{\args{\args{\var{s.f}}{\var{e.d}}}{\var{e.P}}}}{\var{e.P}}}}
%
{\fnew}
%
%
%
% (e.env) ((Call s.f e.ex) e.exp) e.P
% = <Eval <EvalCall s.f (<Eval (e.env) (e.ex) e.P>) e.P> e.P>
% <Eval (e.env) (e.exp) e.P>;
%
\lfsent{Eval}{\patts{\brackets{\var{e.env}}{:\brackets{\patt{\patt{\var{Call}}{\var{s.f}}}{\var{e.q}}}{:\var{e.exp}}}}{e.P}}{\fapp{Eval}{\args{\fapp{EvalCall}{\threeargs{\var{s.f}}{\fapp{Eval}{\args{\brackets{\var{e.env}}{:\var{e.q}}}{\var{e.P}}}}{\var{e.P}}}}{\var{e.P}}}{\,\texttt{++}\,\fapp{Eval}{\args{\brackets{\var{e.env}}{:\var{e.exp}}}{\var{e.P}}}}}
%
%
% (e.env) ((Var e.var) e.exp) e.P
% = <Subst (e.env) (Var e.var)> <Eval (e.env) (e.exp) e.P>;
%
\fsent{Eval}{\patts{\brackets{\var{e.env}}{:\brackets{\patt{\var{Var}}{\var{e.var}}}{:\var{e.exp}}}}{e.P}}
{\fapp{Subst}{\args{\var{e.env}}{\brackets{\app{\var{Var}}{\var{e.var}}}{}}}{}{\,\texttt{++}\,\fapp{Eval}{\args{\brackets{\var{e.env}}{:\var{e.exp}}}{\var{e.P}}}{}}}
%
%
% (e.env) (('*' e.ex) e.exp) e.P
% = ('*' <Eval (e.env) (e.ex) e.P>) <Eval (e.env) (e.exp) e.P>;
%
\fsent{Eval}{\patts{\brackets{\var{e.env}}{:\brackets{\patt{\var{\texttt{'*'}}}{\var{e.q}}}{:\var{e.exp}}}}{e.P}}{\brackets{\app{\var{\texttt{'*'}}}{\fapp{Eval}{\args{\brackets{\var{e.env}}{:\var{e.q}}}{\var{e.P}}}}}{\;{:}\;\fapp{Eval}{\args{\brackets{\var{e.env}}{:\var{e.exp}}}{\var{e.P}}}{}}}
%
%
% (e.env) (s.x e.exp) e.P = s.x <Eval (e.env) (e.exp) e.P>;
%
\fsent{Eval}{\patts{\brackets{\var{e.env}}{:\var{s.x}}{:\var{e.exp}}}{e.P}}
{\expr{\var{s.x}}{\;{:}\;\fapp{Eval}{\args{\brackets{\var{e.env}}{:\var{e.exp}}}{\var{e.P}}}{}}}
%
%
% (e.env) () e.P = ;
%
\fsent{Eval}{\patts{\brackets{\var{e.env}}{:\Nil}}{e.P}}{\Nil}
%
%
%{\fnew}
%
% s.f (e.d) (Prog s.n) = <Matching False (((False)'='(False)) <LookFor s.f <Prog s.n>>) (e.d)>;
%
%EvalCall {
% s.f (e.d) (Prog s.n) = <Matching False () (<LookFor s.f <Prog s.n>>) (e.d)>;
%}
%
\shiftfsent{EvalCall}{\threepatts{\var{s.f}}{\var{e.d}}{\brackets{\patt{\var{Prog}}{\var{s.n}}}{}}}{\fapp{Matching}{\args{\args{\var{\False}}{\var{\Nil}}}\args{\fapp{LookFor}{\args{\var{s.f}}{\fapp{Prog}{\var{s.n}}}}}{\var{e.d}}}}
%
{\fnew}
% False (t.sent ((e.p)'='(e.exp)) e.def) (e.d) =
% <Matching <Match (e.p) (e.d) ()> (((e.p)'='(e.exp)) e.def) (e.d)>;
%
% False (e.old) (((e.p)'='(e.expr)) e.def) (e.d) =
% <Matching <RigitMatch (e.p)(e.d) ()> (e.expr) (e.def) (e.d)>;
%
\lfsent{Matching}{
\patts{\patts{\var{\False}}{\var{e.old}}}
{\patts{\brackets{\brackets{\var{e.p}}{{\;:}\texttt{'='}{\;:\;}\brackets{\var{e.exp}}}}{{\;:\;}\var{e.def}}}{\var{e.d}}}
% \patts{\patts{\var{\False}}{\brackets{\var{e.old}}}}
%
%{\patts{\brackets{\brackets{\var{e.p}}{{\;:}\texttt{'='}{\;:\;}\brackets{\var{e.exp}}}}{{\;:\;}\var{e.def}}}{\var{e.d}}}
}
{\fapp{Matching}{\args{\args{\fapp{Match}{\threeargs{\var{e.p}}{\var{e.d}}{\brackets{\texttt{[]}}}}}{\var{e.exp}}}{\args{\var{e.def}}{\var{e.d}}}}}
%
% (e.env) (((e.p)'='(e.exp)) e.def) (e.d) = (e.env) (e.exp);
%
% (e.env) (e.expr) (e.def) (e.d) = (e.env) (e.expr);
%
\fsent{Matching}{\patts{
\patts{\brackets{\var{e.env}}}{\var{e.exp}}}
% \patts{\brackets{\var{e.env}}}{\brackets{\var{e.exp}}}}
{\patts{\var{e.def}}{\var{e.d}}}
}
{\brackets{\var{e.env}}{:\var{e.exp}}}
%
%
%{\fnew}
% ((Var 'e' s.n)) (e.d) (e.env)
%% = <Match () () <PutVar ((Var 'e' s.n) e.d) (e.env)>>;
% = <PutVar ((Var 'e' s.n) e.d) (e.env)>;
%
\shiftfsent{Match}{
\threepatts{\brackets{\var{Var}~\texttt{'e'}~\var{s.n}}}{\var{e.d}}{\brackets{\var{e.env}}{}}
}
{{\fapp{PutVar}{\args{\brackets{\patt{\var{Var}}{\patt{\texttt{'e'}}{\var{s.n}}}}{\,:\;}\var{e.d}}{\brackets{\var{e.env}}{}}}{}}}
%
% ((Var 's' s.n) e.p) (s.x e.d) (e.env)
% = <Match (e.p)(e.d) <PutVar ((Var 's' s.n) s.x) (e.env)>>;
\shiftlfsent{Match}{
\threepatts{\brackets{\var{Var}~\texttt{'s'}~\var{s.n}}{{\;:\;}\var{e.p}}}{\var{s.x}{\,:\,}\var{e.d}}{\brackets{\var{e.env}}{}}
}
{\fapp{Match}{\threeargs{\expr{\var{e.p}}}{\expr{\var{e.d}}}{\fapp{PutVar}{\args{\brackets{\patt{\var{Var}}{\patt{\texttt{'s'}}{\var{s.n}}}}{\,:\;}\var{s.x}}{\brackets{\var{e.env}}{}}}{}} }}
%
% ((Var 't' s.n) e.p) (t.x e.d) (e.env)
% = <Match (e.p)(e.d) <PutVar ((Var 't' s.n) t.x) (e.env)>>;
%
% (('*' e.q) e.p) (('*' e.x) e.d) (e.env)
% = <Match (e.p)(e.d) <Match (e.q)(e.x) (e.env)>>;
\shiftlfsent{Match}{
\threepatts{\brackets{\texttt{'*'}~\var{e.q}}{{\;:\;}\var{e.p}}}{\brackets{\texttt{'*'}~\var{e.x}}{{\;:\;}\var{e.d}}}{\brackets{\var{e.env}}{}}
}
{\fapp{Match}{\threeargs{{\expr\var{e.p}}}{\expr{\var{e.d}}}{\fapp{Match}{\threeargs{\expr{\var{e.q}}}{\expr{\var{e.x}}}{\brackets{\var{e.env}}{}}}{}}}}
%
% (s.x e.p) (s.x e.d) (e.env) = <Match (e.p)(e.d) (e.env)>;
%
\shiftfsent{Match}{
\threepatts{\expr{\var{s.x}{{\;:\;}\var{e.p}}}}{\expr{\var{s.x}{{\;:\;}\var{e.d}}}}{\brackets{\expr{\var{e.env}}}{}}
}
{\fapp{Match}{\threeargs{\expr{\var{e.p}}}{\expr{\var{e.d}}}{\brackets{\expr{\var{e.env}}}{}}}{}}
%
%() () (e.env) = (e.env);
\shiftfsent{Match}{
\threepatts{\texttt{[]}}{\texttt{[]}}{\brackets{\var{e.env}}{}}
}
{\brackets{\var{e.env}}}
%
% (e.p)'='(e.d) e.fail = False;
% (e.p) (e.d) e.fail = False;
\shiftfsent{Match}{
\threepatts{\var{e.p}}{\var{e.d}}{\var{e.fail}}}
%\patts{\brackets{\var{e.p}}{{\;:}\texttt{'='}{\;:\;}\brackets{\var{e.d}}}}{\var{e.fail}}}
{\var{\False}}
%
%
{\fnew}
%PutVar { t.assign (e.env) = <CheckRepVar <PutV t.assign (e.env)>>; }
% PutVar { t.assign (e.env) = <CheckRepVar <PutV t.assign (e.env) ()>>; }
\fsent{PutVar}{
\patts{\var{e.assign}}{\brackets{\var{e.env}}{}}
}
{\fapp{CheckRepVar}{\fapp{PutV}{\threeargs{\brackets{\var{e.assign}}}{\var{e.env}}{\texttt{[]}}}{}}}
%
% ((Var s.t s.n) e.value) (((Var s.t s.n) e.old-value) e.env)
% = ((Var s.t s.n) e.old-value) e.env <Eq (e.value) (e.value1)>;
%
%* Flat:
% ((Var s.t s.n) e.value) (((Var s.t s.n) e.pval) e.env) (e.penv)
%* = <Eq (e.value) (e.pval)> ++ e.penv ++ (((Var s.t s.n) e.pval) : e.env);
% = <Eq (e.value) (e.pval)> e.penv ((Var s.t s.n) e.pval) e.env;
%
% Flat
\shiftlfsent{PutV}{
\threepatts{\brackets{\brackets{\var{Var}~\var{s.t}~\var{s.n}}{{\;:\;}\expr{\var{e.val}}}}}
{\brackets{\brackets{\var{Var}~\var{s.t}~\var{s.n}}{{\;:\;}\var{e.pval}}}{{\;:\;}\expr{\var{e.env}}}{}}{\var{e.penv}{}}
}
{{{\expr{\brackets{\fapp{Eq}{\args{\var{e.val}}{\var{e.pval}}}}}}{\;:\brackets{\brackets{\var{Var}~\var{s.t}~\var{s.n}}{{\;:\;}\var{e.pval}}}{{\;:\;}{\expr{\var{e.env}}}}} }}
%
%
%
%
% t.assign (t.olda e.env) = t.olda <PutV t.assign (e.env)>;
%
% Flat:
% t.assign (t.passign e.env) (e.penv) = <PutV t.assign (e.env) (t.passign e.penv)>;
%
%
% Flat:
%
\shiftlfsent{PutV}{
\threepatts{\brackets{\var{e.assign}}}{\brackets{\var{e.passign}}{{\;:\;}\var{e.env}}{}}
{\var{e.penv}{}}
}
{\fapp{PutV}{\threeargs{\brackets{\var{e.assign}}}{\var{e.env}}{\expr{\brackets{\expr{\var{e.passign}}}{\;:\;}\expr{\var{e.penv}}}}{}}}
%
% t.assign () = t.assign True;
%
% Flat:
% t.assign () (e.penv) = True t.assign e.penv;
%
% Flat:
\shiftfsent{PutV}{
\threepatts{\brackets{\var{e.assign}}}{\texttt{[]}}{\var{e.penv}{}}
}
{{{\expr{\brackets{\var{\True}}}}{\;:\expr{\brackets{\var{e.assign}}{\;:\;}\expr{\var{e.penv}}}}}}
%
%
% (s.x) (s.x) = True;
%
%
{\fnew}
%
% e.env True = (e.env);
%
% Flat:
% True e.env = (e.env);
%
\shiftfsent{CheckRepVar}{
% Flat:
\expr{\brackets{\var{\True}}{:}\var{e.env}}
}
{\brackets{\var{e.env}}{}}
%
% e.trash False = False;
%
% Flat:
% False e.trash = False;
%
\shiftfsent{CheckRepVar}{
% Flat:
\expr{\brackets{\var{\False}}{:}\var{e.env}}
}
{\var{\False}}
%
%
{\fnew}
%
% (s.1 e.xpr1) (s.1 e.xpr2) = <Eq (e.xpr1) (e.xpr2)>;
\fsent{Eq}{
\patts{\var{s.x}{\;:\;}\var{e.xs}}{\var{s.x}{\;:\;}\var{e.ys}}
}
{{\fapp{Eq}{\args{\var{e.xs}}{\var{e.ys}}}{}}}
%
%
% (('*' e.x) e.ex) (('*' e.y) e.ey) = <ContEq <Eq (e.x) (e.y)> (e.ex) (e.ey)>;
%
\fsent{Eq}{
\patts{\brackets{\texttt{'*'}~\var{e.x}}{{\;:\;}\var{e.xs}}}{\brackets{\texttt{'*'}~\var{e.y}}{{\;:\;}\var{e.ys}}}
}
{{\fapp{ContEq}{\threeargs{\fapp{Eq}{\args{\expr{\var{e.x}}}{\expr{\var{e.y}}}}{}}{\expr{\var{e.xs}}}{\expr{\var{e.ys}}}}{}}}
%
% () () = True;
%
\fsent{Eq}{
\patts{\texttt{[]}}{\texttt{[]}}
}
{\var{\True}}
%
% (e.xpr1) (e.xpr2) = False;
%
\fsent{Eq}{
\patts{\var{e.xs}}{\var{e.ys}}
}
{\var{\False}}
%
%ContEq {
% False (e.ex) (e.ey) = False;
% True (e.ex) (e.ey) = <Eq (e.ex) (e.ey)>;
%}
%
% False (e.ex) (e.ey) = False;
\shiftfsent{ContEq}{
\threepatts{\var{\False}}{\var{e.xs}}{\var{e.ys}}}
{\var{\False}}
%
% True (e.ex) (e.ey) = <Eq (e.ex) (e.ey)>;
\shiftfsent{ContEq}{
\threepatts{\var{\True}}{\var{e.xs}}{\var{e.ys}}}
{{\fapp{Eq}{\args{\var{e.xs}}{\var{e.ys}}}{}}}
%
%
{\fnew}
%
% s.f ((s.f e.def) e.P) = e.def;
%
\fsent{LookFor}{
\patts{\var{s.f}}{\brackets{\var{s.f}{\;:\;}\var{e.def}}{{\;:\;}\var{e.P}}}
}
{\var{e.def}}
%
% s.f ((s.g e.def) e.P) = /*<Prout LookFor>*/ <LookFor s.f (e.P)>;
%
\fsent{LookFor}{
\patts{\var{s.f}}{\brackets{\var{s.g}{\;:\;}\var{e.def}}{{\;:\;}\var{e.P}}}
}
{{\fapp{LookFor}{\args{\var{s.f}}{\var{e.P}}}{}}}
%
%
{\fnew}
%
% (((Var s.t s.n) e.value) e.env) (Var s.t s.n) = e.value;
%
\fsent{Subst}{
\patts{\brackets{\brackets{\var{Var}~\var{s.t}~\var{s.n}}{{\;:\;}\expr{\var{e.val}}}}{{\;:\;}\expr{\var{e.env}}}}{\brackets{\var{Var}~\var{s.t}~\var{s.n}}{}}
}
{\var{e.val}}
%
% (t.assign e.env) t.var = <Subst (e.env) t.var>;
%
\fsent{Subst}{
\patts{\var{\brackets{e.assign}}{{\;:\;}\expr{\var{e.env}}}}{\expr{\var{e.var}}}
%\patts{\var{t.assign}{{\;:\;}\expr{\var{e.env}}}}{\expr{\var{t.var}}}
}
{{\fapp{Subst}{\args{\var{e.env}}{\var{e.var}}}{}}}
\medskip
{\hrule height 0.8pt}
\end{center}
%} }
\caption{Self-Interpreter}\label{fig:Self-Interpreter}
\label{program}
\end{figure}
}
\clearpage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{The Interpreter}\label{subsec:Interpreter}
The self-interpreter used in the experiments is given in Figure \ref{fig:Self-Interpreter}.
The entry point is of the following form
{${\fapp{Int}{\args{\expr{\brackets{\expr{\var{Call}}~\expr{\var{s.f}}~\expr{\var{e.d}}}}}{\expr{\var{e.P}}}}{}}$}.
Here the first argument is the application constructor of the main function to be executed. The second argument provides the name of a program to be interpreted. The encoded source of the program will be returned by a function call of {$\expr{\var{Prog}}$} whenever it is asked by {$\expr{\var{EvalCall}}$}. For example, interpretation of program model Synapse N+1 given in Section \ref{subsec:Program-Model} starts with the following application
{${\fapp{Int}{\args{\expr{\brackets{\expr{\var{Call}}~\expr{\var{Main}}~\underline{\expr{\var{d}_0}}}}}{\expr{\brackets{\expr{\var{Prog}}~\expr{\var{Synapse}}}}}}{}}$},
where {$\expr{\var{d}_0}$} is an input data given to program Synapse.
Due to the large size of the encoded programs we omit the definition of function {$Prog$}.
%
{${\fapp{EvalCall}{\args{\expr{\brackets{\expr{\var{Call}}~\expr{\var{s.f}}~\expr{\var{e.d}}}}}{\expr{\var{e.P}}}}{}}$}
%
asks for the definition of function {$\expr{\var{s.f}}$}, calling {$ \expr{\var{LookFor}} $}, and initiates matching the data given by {$\expr{\var{e.d}}$} against the patterns of the definition rules. In order to start this pattern matching, it imitates a fail happening in matching the data against a previous nonexistent pattern.
Function {$\expr{\var{Matching}}$} runs over the definition rules, testing the result of matching the input data ({$\expr{\var{e.d}}$}) against the current pattern considered. In the case if the result is {$\expr{\var{\False}}$} the function calls function {$\expr{\var{Match}}$}, asking for matching the input data against the next rule pattern. The environment {$\expr{\var{e.env}}$} is initialized by {$\expr{\var{\texttt{[]}}}$} (see the third argument of the {$\expr{\var{Match}}$} call).
If the pattern matching succeeds then function {$\expr{\var{Matching}}$} returns {$\expr{\brackets{\var{e.env}}{:}\var{e.exp}}$}, where expression {$\expr{\var{e.exp}}$} is the right-hand side of the current rule and the environment includes the variable assignments computed by the pattern matching.
Function {$\expr{\var{Match}}$} is trying to match the input data given in its second argument, step by step, against the pattern given in its first argument. It computes the environment containing the variable substitution defined by the matching (see the first and second function rules).
If a variable is encountered then function {$\expr{\var{PutVar}}$} calls {$\expr{\var{PutV}}$} looking for an assignment to the same variable and, if such an assignment exists, the function tests a possible coincidence of the new and old values assigned to the variable.
The third rule of function {$\expr{\var{Match}}$} deals with the tree structure, calling this function twice.
Function {$\expr{\var{Eval}}$} passes through an expression given in its second argument. The second {$\expr{\var{Eval}}$} rule deals with a variable and calls function {$\expr{\var{Subst}}$} looking the environment for the variable value and replacing the variable with its value.
We intend to specialize interpreter {$\expr{\var{Int}}$} with respect to its second argument.
%
The corresponding \emph{Refal} source code of the self-interpreter may be found in \\ \url{http://refal.botik.ru/protocols/Self-Int-Refal.zip}.
\section{Specifying Cache Coherence Protocols}\label{sec:Specifying-Cache}
We show our method \cite{Lis_Nem:Programming, Lis_Nem:IJFCS08} for specifying
non-deterministic systems by an example used through this paper.
%
The Synapse N+1 protocol definition given below is borrowed from \cite{Delzanno:Automatic}.
The parameterized version of the protocol is considered and \emph{counting abstraction} is used in the specification.
The protocol has to react to five external non-deterministic events by updating its states being three integer counters. The initial value of counter {$\expr{\var{invalid}}$} is parameterized
(so it could be any positive integer), while the other two counters are initialized by zero.
The primed state names stand for the updated state values. The empty updates mean that nothing happened.
%\begin{center}
\begin{tabular}{ll}
(rh) & \psent{dirty + valid \ge 1}{} \\
(rm) & \psent{invalid \ge 1}{dirty^\prime = 0, valid^\prime = valid + 1, invalid^\prime = invalid + dirty - 1} \\
(wh1) & \psent{dirty \ge 1}{} \\
(wh2) & \psent{valid \ge 1}{valid^\prime = 0, dirty^\prime = 1, invalid^\prime = invalid + dirty + valid - 1} \\
(wm) & \psent{invalid \ge 1}{valid^\prime = 0, dirty^\prime = 1, invalid^\prime = invalid + dirty + valid - 1}
\end{tabular}
%\end{center}
\paragraph{Specification of Safety Properties}\label{subsubsec:Spec-Safety-Prop}
%
Any state reached by the protocol should not satisfy any of the two following properties:
%
%\begin{tabular}{cl}
% (1) & \pprop{invalid \ge 0, dirty \ge 1, valid \ge 1} \\
% (2) & \pprop{invalid \ge 0, dirty \ge 2, valid \ge 0}
%\end{tabular}
%
(1)~~ \pprop{invalid \ge 0, dirty \ge 1, valid \ge 1};
(2)~~ \pprop{invalid \ge 0, dirty \ge 2, valid \ge 0}.
\begin{figure}[htb]
\begin{center}
{\hrule height 0.8pt \medskip}
% $ENTRY Go { (e.time) (e.is) = <Loop (e.time) (Invalid I e.is)(Dirty )(Valid ) >; }
\fsent{Main}{\expr{\brackets{\var{e.time}}}{\,:\,}\brackets{\expr{\var{e.is}}}}
{\fapp{Loop}{\brackets{\var{e.time}}{\,:\,}\expr{\brackets{\var{Invalid}~\var{I}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~}}{\,:\,}\expr{\brackets{\var{Valid}~}}}}
%
%Loop {
% () (Invalid e.x1)(Dirty e.y2)(Valid e.z3) =
% <Test (Invalid e.x1)(Dirty e.y2)(Valid e.z3)>;
% (s.t e.time) (Invalid e.x1)(Dirty e.y2)(Valid e.z3) =
% <Loop (e.time)
% <Event s.t (Invalid e.x1)(Dirty e.y2)(Valid e.z3)>>;
%}
{\fnew}
%
\lfsent{Loop}{\brackets{\texttt{[]}}{\,:\,}{\expr{\brackets{\var{Invalid}~\var{e.is}}}}{\,:\,}{\expr{\brackets{\var{Dirty}~\var{e.ds}}}}{\,:\,}{\expr{\brackets{\var{Valid}~\var{e.vs}}}}}
{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{\,:\,}\brackets{\var{Dirty}~\var{e.ds}}{\,:\,}\brackets{\var{Valid}~\var{e.vs}}}}
%
%
\lfsent{Loop}{\brackets{\var{s.t}{\,:\,}\var{e.time}}{\,:\,}\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}
{\fapp{Loop}{\brackets{\var{e.time}}{\,:\,}\fapp{Event}{\var{s.t}{\,:\,}\brackets{\var{Invalid}~\var{e.is}}{\,:\,}\brackets{\var{Dirty}~\var{e.ds}}{\,:\,}\brackets{\var{Valid}~\var{e.vs}}}}}
%
%
%Event {
%* rh Trivial
%* rm
% rm (Invalid I e.x1) (Dirty e.y2) (Valid e.z3) = (Invalid e.y2 e.x1) (Dirty ) (Valid I e.z3);
%* wh1 Trivial
%* wh2
% wh2 (Invalid e.x1) (Dirty e.y2) (Valid I e.z3) = (Invalid e.z3 e.y2 e.x1) (Dirty I) (Valid );
%* wm
% wm (Invalid I e.x1) (Dirty e.y2) (Valid e.z3) = (Invalid e.z3 e.y2 e.x1) (Dirty I) (Valid );
%}
{\fnew}
%
\lfsent{Event}{\var{rm}{\,:\,}\expr{\brackets{\var{Invalid}~\var{I}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}
{\brackets{\var{Invalid}~\fapp{Append}{\brackets{\var{e.ds}}{\,:\,}\brackets{\var{e.is}}}}{\,:\,}\brackets{\var{Dirty}~}{\,:\,}\brackets{\var{Valid}~\var{I}~\var{e.vs}}}
%
\lfsent{Event}{\var{wh2}{\,:\,}\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{I}~\var{e.vs}}}}
{\brackets{\var{Invalid}~\fapp{Append}{\brackets{\var{e.vs}}{\,:\,}\brackets{\fapp{Append}{\brackets{\var{e.ds}}{\,:\,}\brackets{\var{e.is}}}}}}{\,:\,}\brackets{\var{Dirty~\var{I}}}{\,:\,}\brackets{\var{Valid~}}}
%
\lfsent{Event}{\var{wm}{\,:\,}\expr{\brackets{\var{Invalid}~\var{I}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}
{\brackets{\var{Invalid}~\fapp{Append}{\brackets{\var{e.vs}}{\,:\,}\brackets{\fapp{Append}{\brackets{\var{e.ds}}{\,:\,}\brackets{\var{e.is}}}}}}{\,:\,}\brackets{\var{Dirty~\var{I}}}{\,:\,}\brackets{\var{Valid}{~}}}
%
%Append {
% () (e.ys) = e.ys;
% (s.x e.xs) (e.ys) = s.x <Append (e.xs) (e.ys)>;
%}
%
\shiftfsent{Append}{\expr{\brackets{\texttt{[]}}}{\,:\,}\expr{\brackets{\var{e.ys}}}}
{\var{e.ys}}
%{\brackets{\var{e.ys}}}
%
\shiftfsent{Append}{\expr{\brackets{\var{s.x}{\,:\,}\var{e.xs}}}{\,:\,}\expr{\brackets{\var{e.ys}}}}
{\var{s.x}{\,:\,}\fapp{Append}{\brackets{\var{e.xs}}{\,:\,}\brackets{\var{e.ys}}}}
%
%Test {
%* dirty >= 1, valid >= 1
%(Invalid e.1) (Dirty I e.2) (Valid I e.3) = False;
%* dirty >= 2
%(Invalid e.1) (Dirty I I e.2) (Valid e.3) = False;
%
%(Invalid e.1) (Dirty e.2) (Valid e.3) = True;
%}
{\fnew}
%
\fsent{Test}{\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{I}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{I}~\var{e.vs}}}}
{\var{False}}
%
\fsent{Test}{\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{I}~\var{I}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}
{\var{False}}
%
\fsent{Test}{\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}
{\var{True}}
\medskip
{\hrule height 0.8pt}
\vspace{-5pt}
\end{center}
\caption{Model of the Synapse N+1 cache coherence protocol}\label{fig:Synapse}
\end{figure}
\vspace{-5pt}
\subsection{Program Model of the Synapse N+1 Cache Coherence Protocol}\label{subsec:Program-Model}
Let us then specify a program model of our sample protocol.
The Synapse N+1 program
%
is given in Figure \ref{fig:Synapse}.
The idea behind the program specifications modeling the reactive systems is given in Introduction \ref{sec:Introduction} above. The \emph{finite} stream of events is modeled by a $\expr{\var{time}}$ value. The time ticks
are labeled by the events. The counters' values are specified in the unary notation. The unary addition is directly defined by function $\expr{\var{Append}}$, i.e., without referencing to the corresponding macros.
%
Function $\expr{\var{Loop}}$ exhausts
the event stream, step by step, and calls for $\expr{\var{Test}}$ verifying the safety property required from the protocol. Thus function $\expr{\var{Main}}$ is a predicate.
Note that given input values the partial predicate terminates since the event stream is finite. The termination is normal, if the final protocol state asked by the input stream is reachable one, otherwise it is abnormal.
\section{On Supercompilation}\label{sec:Supercompilation}
In this paper we are interested in one particular approach in program transformation and specialization, known as supercompilation\footnote{From \emph{super}vised \emph{compilation}.}.
Supercompilation is a powerful semantics-based program transformation
technique~\cite{SGJ:96,Tur:86} having a long history well back to the 1960-70s, when it was proposed by V.~Turchin. The main idea behind a supercompiler is to observe the behavior of a functional program $p$ running on a \emph{partially} defined input with the aim to define a program, which would be equivalent to the original one (on the domain of the latter), but having improved properties.
%%%
Given a program and its parameterized entry point, supercompilation is performed by an \emph{unfold-fold cycle} unfolding this entry point.
It reduces the redundancy that could be present in the original program.
It folds the tree into a finite graph of states and transitions between possible parameterized
configurations of the computing system.
And, finally, it analyses global properties of the graph and specializes this graph with respect to these properties (without additional unfolding steps).\footnote{See also Section \ref{sec:App-Structure-SCP4} in Appendix.} The resulting program definition is constructed solely based on the meta-interpretation of the source program rather than by a (step-by-step) transformation of the program.
%
The result of supercompilation may be a specialized version of the original program, taking into account the properties of partially known arguments, or just a re-formulated, and sometimes more efficient, equivalent program (on the domain of the original).
Turchin's ideas have been studied by a number of authors for a long time and have, to some extent, been brought to the algorithmic and implementation stage \cite{NT:00}. From the very beginning the development of supercompilation has been conducted mainly in the context of the programming language Refal \cite{N:03, Nemytykh:SCP4book, Nem_Pin_Tur, Turchin:Refal5}.
A number of model supercompilers for subsets of functional languages based on Lisp data were implemented with the aim of formalizing some aspects of the supercompilation algorithms
\cite{Jonsson_Nordlander, Klyuchnikov:HOSC, SGJ:96}.
The most advanced supercompiler for Refal is SCP4 \cite{N:03, Nemytykh:SCP4book, NT:00}.
The verification system VeriMAP \cite{VeriMAP:2014} by De\,E.~Angelis et al. \cite{FioPettProSen:Ver-IterSpec14, FioPettProSen:Ver-Linear-Fib15} uses nontrivial properties of integers recognized by both CLP built-in predicates and external SMT solvers. We,
like the VeriMAP authors,
use a nontrivial property of the configurations. The property is the associativity of the built-in append function \texttt{++} supported by the supercompiler SCP4 itself\footnote{As well as by the real programming language in terms of which the experiments described in this paper were done.}, rather than by an external solver.
\subsection{The Well-Quasi-Ordering on {${\mathbb{E}}$}}\label{subsec:Higman-Kruskal}
%
The following relation is a variant of the Higman-Kruskal relation and is a well-quasi-ordering \cite{Higman, Kruskal} (see also \cite{Leuschel:98}).
\numberwithin{equation}{section}
\begin{definition}
The homeomorphic embedding relation $\proptoeq$ is the smallest transitive relation on $\mathbb{E}$ satisfying the following properties,
where $f \in \Fn{n},\; \alpha, \beta, \tau, s, t, t_{1}, \ldots, t_{n} \in {\mathbb E}$
and {$\alpha, \beta, \tau \in {\cal T}$}.
%
\vspace{-5pt}
\begin{align}
%1.
& {\forall x,y \in {\cal V}_e.\; x \proptoeq y, \forall u,v \in {\cal V}_s.\; u \proptoeq v;}
&\text{Variables}\label{def:emb:vars} \\
%
%2.
&{\Nil \proptoeq t,\; t \proptoeq t,\; t \proptoeq f(\;{t_{1}},\; {\ldots},\; t,\ldots, {t_{n}}\;),\;
t \proptoeq (t),\;
t \proptoeq \alpha{\,{:}\,}t;}
%\tau \proptoeq \tau{\,{:}\,}t;}
&\text{Monotonicity}\label{def:emb:mon} \\
%
%3.
&\text{if~\;} {s \proptoeq {\zb}t \text{~and~} \alpha \proptoeq {\zb}\beta, \text{~then~}
{(}s{)} \proptoeq {(}t{)},
\alpha{\texttt{:}\,}s \proptoeq \,\beta{\,{:}\;}t};
& \notag \\
%
%4.
&\text{if~\;} {s \proptoeq {\zb}t}, \text{~then~}
{f(\;t_{1},\; \ldots,\; s,\ldots, t_{n}\;) \proptoeq {\zb}f(\;t_{1},\; {\ldots},\; t,\ldots, t_{n}\;)}.
& \notag %\\
\end{align}
\end{definition}\label{def:emb}
Note that the definition takes into account function {$\expr{\var{append}}$}, since its infix notation {$\expr{\var{exp_1}}\; \append\; \expr{\var{exp_2}}$} stands for {$\texttt{ append}(~\expr{\var{exp_1}},\; \expr{\var{exp_2}}~)$}.
We use relation $\proptoeq$ modulo associativity of \texttt{\;++\;} and the following equalities %\\
{${\expr{\var{term}}{\;:\;}\expr{\var{exp_1}}} = {\expr{\var{term}}~\append~\expr{\var{exp_1}}}
$}, {${\expr{\var{exp}} ~\append~ \Nil} = \expr{\var{exp}}$} and {${\Nil ~\append~ \expr{\var{exp}}} = \expr{\var{exp}}$}.
\begin{corollary}
If $t_1, \ldots, t_{n-1} \in {\cal T}$ and $t_{n} \in \mathbb{E}$,
and given {$i_1, \ldots, i_j$} such that {$1 \leq i_1 < i_2 < \ldots < i_j \leq n$},
then {$t_{i_1}{\;{:}\;} \ldots{\;{:}\;} t_{i_j}\, \proptoeq\; t_1{\;{:}\;} \ldots{\;{:}\;} t_n$}.
\end{corollary}\label{cor:rem}
\begin{corollary}
{For any~}
$f \in \Fn{n},\; \alpha, \beta, \gamma, t_1,\ldots, t_n \in \mathbb{E}$~~ (~ monotonicity of relation $\notproptoeq$ ~)
\vspace{-5pt}
\begin{align}
%1
&\text{if~} \alpha \,\notproptoeq\; \beta, \text{~then~}
f(\;t_{1},\; \ldots,\; t_{i-1},\; \alpha,\; t_{i+1},\; \ldots,\; t_{n}\;) \notproptoeq
{\zb}f(\;t_{1},\; \ldots,\; t_{i-1},\; \beta,\; t_{i+1},\; \ldots,\; t_{n}\;).
& \label{Monotonicity} %\\
% &\text{Monotonicity}\label{Monotonicity} %\\
%3
\end{align}
\vspace{-10pt}
%78
\end{corollary}\label{cor:trans-mon}
Given an infinite sequence of expressions $t_1, \ldots, t_n, \ldots$, relation $\proptoeq$ is relevant to approximation of loops increasing the syntactical structures
in the sequence; or in other words to looking for the regular similar cases of mathematical induction on the structure of the expressions. That is to say the cases, which allow us to refer one to another by a step of the induction.
An additional restriction separates the basic cases of the induction from the regular ones. The restriction is:
% $$
{$
\forall \sigma\; . \texttt{(\Nil)} \notpropto \texttt{(}\sigma\texttt{)} \;\&\;
% \land
\forall v \in {\cal V}_s. \texttt{(\Nil)} \notpropto \texttt{(}v\texttt{)}
$}.
% $$
We impose this restriction on the relation $\proptoeq$ modulo the equalities above and denote
the obtained relation as $\precceq$. It is
easy to see that such a restriction does not violate the quasi-ordering
property. Note that the restriction may be varied in the obvious way, but for our experiments its simplest case given above is used to control generalization and has turned out to be sufficient.
In the sequel, $t_1 \prec t_2$ stands for the following relation $t_1 \precceq t_2$ and $t_1 \neq t_2$, which is transitive.
\begin{definition}\label{def:configuration}
A parameterized
configuration is a finite sequence of the form\\
\emph{$\texttt{let}~ \expr{\var{e.h} ~\texttt{=}~
\fapp{f_1}{\threeargs{\expr{\var{exp_{11}}}}{~\ldots~}{\expr{\var{exp_{1m}}}}}{}
~~\texttt{in}}~~
\ldots\;~~
\texttt{let}~ \expr{\var{e.h} ~\texttt{=}~
\fapp{f_k}{\threeargs{\expr{\var{exp_{k1}}}}{~\ldots~}{\expr{\var{exp_{kj}}}}}{} ~~\texttt{in}~~
\expr{\var{exp_{n+1}}}}
$},
where $\expr{\var{exp_{n+1}}}$ is passive, for all $i>1$ $\expr{\var{\mu_{\expr{\var{e.h}}}(\fapp{f_i}{\ldots})}} = \expr{\var{\mu_{\expr{\var{e.h}}}(exp_{n+1})}} = 1$, and $\expr{\var{\mu_{\expr{\var{e.h}}}(\fapp{f_1}{\ldots})}} = 0$;
for all $i$ and all $j$ variable {$\expr{\var{e.h}}$} does not occur in any function application being a sub-expression of $\expr{\var{exp_{ij}}}$.
In the sequel, we refer to such a function application $\fapp{f_i}{\ldots}$ given explicitly in the configuration as an upper function application.
%
\end{definition}\label{def:config}
The configurations present the function application stacks, in which all constructors' applications not occurring in arguments of the upper function applications are moved to the rightmost expressions. Here the \emph{append} {$\append$} is treated as a complex constructor\footnote{I.e., we use nontrivial properties of configurations containing the $\expr{\var{append}}$ \texttt{++}. See the remark made in the footnote on p.\,\pageref{foot:append}.}
, rather than a function. The rightmost expression is the bottom of the stack. Since the value of {$\expr{\var{e.h}}$} is reassigned in each \texttt{let} in the stack, for brevity sake, we use the following presentation of the configurations: \\
{$\fapp{f_1}{\threeargs{\expr{\var{exp_{11}}}}{~\ldots~}{\expr{\var{exp_{1m}}}}},\;~
\ldots\;,~
\fapp{f_k}{\threeargs{\expr{\var{exp_{k1}}}}{~\ldots~}{\expr{\var{exp_{kj}}}}},\;~ \expr{\var{exp_{n+1}}}
$},
%
where variable $\expr{\var{e.h}}$ is replaced with bullet {$\bullet$}. I.e., the bullet is just a placeholder. The last expression may be omitted if it equals {$\bullet$}.
%
An example follows
{$
%$$
\expr{\fapp{f}{\var{a}{\;:\,}\var{e.xs}\append \var{e.ys}},}~~
%\expr{\fapp{g}{\fapp{g}{\bullet} \append \var{e.ys}},}~~
\expr{\fapp{g}{\threeargs{\bullet \append \var{e.ys}}{(\var{Var}~ b~c)}{\Nil}},}~~
\expr{\fapp{f}{\var{s.x}{\;:\,}\bullet},}~
\expr{\var{s.x}{\;:\,} \bullet\append \fapp{t}{\var{s.x}{\;:\,}\var{e.zs}},}~~\bullet.
%$$
$}
%
\subsection{The Well-Disordering on Timed Configurations}\label{subsec:Turchin}
Let a program to be specialized and a path starting at the root of the tree unfolded by the unfold-fold loop widely used in program specialization be given. The vertices in the path are labeled by the program parameterized configurations. These configurations form a sequence. Given a configuration from such a sequence and a function application from the configuration, we label the application by the time when it is generated by the unfold-fold loop. Such a labeled function application is said to be a timed application. A configuration is said to be timed if all upper function applications in the configuration are timed. Note that, given a timed configuration, all its timed applications have differing time-labels.
Given two different configurations $C_1, C_2$, if the unfold-fold loop copies an upper function application from $C_1$ and uses this copy in $C_2$, then $C_1, C_2$ share this timed application.
In the sequel, a sequence of the timed configurations generated by the unfold-fold loop is also called just a path.
In this section we define a binary relation $\tur$ on the timed configurations in the path. The relation is originated from V.\,F.~Turchin \cite{Turchin:Generalization88} (see also \cite{Nemytykh:SCP4book, AntoninaNepeivoda:Sbornik2014, AntoninaNepeivoda:VPT2016}). It is \emph{not} transitive\footnote{See Section \ref{subsec:Non-Transitivity} in Appendix for an example of the non-transitivity.}, but like the well-quasi-ordering it satisfies the following crucial property used by supercompilation to stop the loop unfolding the tree.
For any infinite path $C_1, C_2,\; \ldots,\; C_n,\; \ldots$ there exist two timed configurations $C_i, C_j$ such that $i < j$ and $C_i \tur C_j$ (see \cite{Turchin:Generalization88, AntoninaNepeivoda:VPT2016}). For this reason we call relation $\tur$ a well-disordering relation. In the sequel, the time-labels are denoted with subscripts.
\begin{definition}\label{def:Turchin}
Given a
sequence of timed configurations $C_1,\; \ldots\; C_n,\; \ldots$; $C_i$ and $C_j$ are elements of the sequence such that $i < j$ and
$ C_i \; ::=\; f_{t_1}^1(\;\ldots\;),\, \ldots,\, f_{t_k}^k(\;\ldots\;), \expr{\var{exp_1}}$,
$ C_j\; ::=\; g_{\tau_1}^1(\;\ldots\;),\, \ldots,\, g_{\tau_m}^m(\;\ldots\;), \expr{\var{exp_2}}$,
where $f_{t_s}^s$ and $g_{\tau_q}^q$, $1 \le s \le k$ and $1 \le q \le m$, stand for function names $f^s$, $g^q$ labeled with times ${t_s}$ and ${\tau_q}$, respectively, and $\expr{\var{exp_1}}, \expr{\var{exp_2}}$ are passive expressions.
If $k \le m$, $\delta = m-k$ and $\exists l\,.\, (1 < l \le k)$ such that $\forall s\,.\, (0 \le s \le k-l)$
$f_{t_{l+s}}^{l+s} = g_{\tau_{\delta+l+s}}^{\delta+l+s}$ (i.e., $f^{l+s} = g^{\delta+l+s}$ and $ {t_{l+s}} = {\tau_{\delta+l+s}}$ hold), $f_{t_{l-1}}^{l-1} \neq g_{\tau_{\delta+l-1}}^{\delta+l-1}$, and
$\forall s\,.\, (0 < s < l)$ $f_{t_{s}}^s \simeq g_{\tau_{s}}^s$ (i.e., $f^s = g^s$),
then $C_i \tur C_j$.
We say that configurations $C_i$, $C_j$ are in Turchin's relation $C_i \tur C_j$.
%
This longest coincided rest of the configurations are said to be a context, while the parts equal one to another modulo their time-labels are called prefixes of the corresponding configurations.
\end{definition}
The idea behind this definition is as follows. The function applications in the context never took a part in computing the configuration $C_j$, in this segment of the path, while any function applications in the prefix of $C_i$ took a part in computing the configuration $C_j$. Since the prefixes of $C_i, C_j$ coincide modulo their time-labels, these prefixes approximate a loop in the program being specialized. The prefix of $C_i$ is the entry point in this loop, while the prefix of $C_j$ initiates the loop iterations.
The common context approximates computations after this loop.
%
Note that Turchin's relation does not impose any restriction on the arguments of the function applications in $C_i, C_j$.
For example, consider the following two configurations
$C_1 ~::= ~ f_4(\ldots),\, f_3(\ldots),\, g_2(\ldots),\, t_1(\ldots),\, \bullet$ ~and~
$C_2 ~::= ~ f_{10}(\ldots),\, f_7(\ldots),\, g_5(\ldots),\, ~\ldots,~ t_1(\ldots),\, \bullet$ , then $C_1 \tur C_2$ holds. Here the context is $t_1(\ldots)$,
the prefix of $C_1$ is $f_4(\ldots),\, f_3(\ldots),\, g_2(\ldots)$, and
the prefix of $C_2$ is $f_{10}(\ldots),\, f_7(\ldots),\, g_5(\ldots)$,
where the subscripts of the application names stand for the time-labels.
See also Section \ref{subsec:Non-Transitivity} for a detailed example regarding Turchin's relation.
\subsection{The Strategy Controlling the Unfolding Loop}\label{subsec:Strategy}
Now we describe the main relation controlling the unfold-fold loop. That is to say, given a path starting at the root of the unfolded tree, and two timed configurations $C_1, C_2$ in the path such that $C_1$ was generated before $C_2$, this relation stops the loop unfolding the tree and calls the tools responsible for folding this path. These tools, firstly, attempt to fold $C_2$ by a previous configuration and, if that is impossible, then attempt to generalize this configuration pair.
%
The relation is a composition of relations $\tur$ and $\precceq$. It is denoted with $\turprec$ and is a well-disordering (see \cite{Turchin:Generalization88, AntoninaNepeivoda:VPT2016}).
Thus we are given two timed configurations $C_1, C_2$ from a path, such that $C_1$ is generated before $C_2$, and $C_2$ is the last configuration in the path. If relation $C_1 \tur C_2$ does not hold, then the unfold-fold loop unfolds the current configuration $C_2$ and goes on. In the case relation $C_1 \tur C_2$ holds, these configurations are of the forms (see Section \ref{subsec:Turchin} for the
notation used below): \\
%
$C_1 \; =\; f_{t_1}^1(\;\ldots\;),\, \ldots,\, f_{t_{l-1}}^{l-1}(\;\ldots\;),
f_{t_l}^l(\;\ldots\;), \ldots,\, f_{t_k}^k(\;\ldots\;), \expr{\var{exp_1}}$, \\
$C_2\; =\; f_{\tau_1}^1(\;\ldots\;),\, \ldots,\, f_{\tau_{l-1}}^{l-1}(\;\ldots\;),
g_{\tau_l}^l(\;\ldots\;),\, \ldots,\, g_{\tau_{m}}^{m}(\;\ldots\;),\ f_{t_l}^l(\;\ldots\;), \ldots,\, f_{t_k}^k(\;\ldots\;), \expr{\var{exp_2}}$,
%
where the context starts at $f_{t_l}^l(\;\ldots\;)$.
%
Let $C_i^{p}$ stand for the prefix of $C_i$, and $C_i^{c}$ stand for the context of $C_i$ followed by $\expr{\var{exp_i}}$.
Now we compare the prefixes as follows.
If there exists $i$
$(1 \le i < l)$ such that $f_{t_i}^i(\;\ldots\;) \precceq f_{\tau_i}^i(\;\ldots\;)$ does not hold, then $C_2$ is unfolded and the unfold-fold loop goes on.
Else, the sub-tree rooted in $C_1$ is removed and the specialization task defined by the $C_1$ is decomposed into the two specialization tasks corresponding to $C_1^{p}$ and $C_1^{c}$.
%
Further the usual attempts to fold $C_2^{p}$ by $C_1^{p}$ and $C_2^{c}$ by $C_1^{c}$, respectively, do work. If some of these attempts fail, then the corresponding configurations are generalized. Note that the context may be generalized despite the fact that it does not take a part in computing the current configuration $C_2$, since a narrowing of the context parameters may have happened.
A parameterized program configuration is said to be a transitive configuration if one-step unfolding of the configuration results in a tree containing only the vertices with at most one outgoing edge. That is to say, any of the tree vertices is not a branching vertex.
For example, any function application of the form $f(d_1, \ldots, d_n)$, where any $d_i \in \mathbb{D}$, is transitive.
For the sake of simplicity, in the experiments described in this paper, the following strategy is used. The unfold-fold loop skips all transitive configurations encountered and removes them from the tree being unfolded.
%
In the sequel, we refer to the strategy described in this section, including relation $\turprec$, as the $\turprec$-strategy.
%\section{The Verification Method in Action}\label{sec:Verif-Method-in-Action}
\section{Indirect Verifying the Synapse N+1 Program Model}\label{sec:Verif-Method-in-Action}
In this section we present an application of our program verification method based on supercompilation of intermediate interpretations. In general the method may perform a number of program specializations\footnote{I.\,e., the iterated ordinary supercompilation, which does not use any intermediate interpretation, of the residual program produced by one indirect verification.}, but all the cache coherence protocol program models that we have tried to verify by supercompiler SCP4 require at most two specializations.
Given a program partial predicate modeling both a cache coherence protocol and a safety property required from the protocol, we use supercompilation aiming at moving the property hidden in the program semantics to a simple syntactic property of the residual program generated by supercompilation, i.e., this syntactic property should be easily recognized. In the experiments discussed in this paper we hope the corresponding residual programs will include no operator {$\expr{\var{return}~\var{False}};$}.
Since the original direct program model terminates on any input data (see Section \ref{subsec:Program-Model}), this property means that the residual predicate never returns {$\expr{\var{False}}$} and always {$\expr{\var{True}}$}.
Thus we conclude the original program model satisfies the given safety property. In the terms of functional language {${\cal L}$} presented in Section \ref{subsec:Self-Int-Language} the corresponding syntactic property is \emph{``No rule's right-hand side contains identifier {$\expr{\var{False}}$}''}.\footnote{Actually {$\expr{\var{False}}$} is never encountered at all in any residual program generated by repeated launching the supercompiler SCP4 verifying the cache coherence protocol models considered in this paper. I.e., the property is simpler than the formulated one.}
We can now turn to the program modeling the Synapse N+1 protocol given in Section \ref{subsec:Program-Model}.
%
In order to show that the Synapse program model is safe, below we specialize the self-interpreter {$\expr{\var{Int}}$} (see Section \ref{subsec:Interpreter}) with respect to the Synapse program model rather than the program model itself.
Since program Synapse terminates, the self-interpreter terminates when it interprets any call of the {$\expr{\var{Main}}$} entry function of Synapse.
Since Synapse is a partial predicate, the calls of the forms %\\
{\small $\fapp{Int}{\hspace{-2pt}\args{\expr{\brackets{\expr{\var{Call}}~\expr{\var{Main}}~\expr{\var{e.d}}}}}{\expr{\brackets{\expr{\var{Prog}}~\expr{\var{Synapse}}}}}\hspace{-2pt}}{}$},
where {$e.d$} takes any data, define the same partial predicate. Hence, the self-interpreter restricted to such calls is just another program model of protocol Synapse N+1. This indirect program model is much more complicated as compared with the direct model.
We intend now to show that supercompiler SCP4 \cite{N:03, Nemytykh:SCP4book, NT:00} is able to verify this model.
%
Thus our experiments show potential capabilities of the method for verifying the safety properties of the functional programs modeling some complex non-deterministic parameterized systems. In particular, the experiments can also be considered as a partial verification of the intermediate interpreter used. In other words, verifying the interpreter with respect to a set of the interpreted programs that specify the cache coherence protocols.
%
This specialization by supercompilation is performed by following the usual \emph{unfold-fold cycle} controlled by the $\turprec$-strategy described in Section \ref{subsec:Strategy}.
Note that this program specification includes both the function call and constructor application stacks, where the size of the first one is uniformly bounded on the input parameter while the second one is not.
We start off by unfolding the initial configuration
%$$
{$
{\fapp{Int}{\args{\expr{\brackets{\expr{\var{Call}}~\expr{\var{Main}}~\expr{\var{e.d}}}}}{\expr{\brackets{\expr{\var{Prog}}~\expr{\var{Synapse}}}}}}{}}
$},
%$$
where the value of {$\expr{\var{e.d}}$} is unknown.
%
The safety property will be proved if supercompilation is able to recognize all rules of the interpreted program model, containing the {$\expr{\var{False}}$} identifier, as being unreachable from this
initial configuration.
In our early work \cite{Lis_Nem:IJFCS08} we have given a formal model of the verification procedure above by supercompilation. Let a program model and its safety property be given as described above, i.e., a partial program predicate. Given an initial parameterized configuration of the partial predicate, it has been shown that the unfold-fold cycle may be seen as a series of proof attempts by structure induction over the program configurations encountered during supercompilation aiming at verification of the safety property. Here the initial configuration specifies the statement that we have to prove.
%
There are too many program configurations generated by the unfold-fold cycle starting with the initial configuration given above and the self-interpreter configurations are very large. As a consequence it is not possible to consider all the configurations in details. We study the configurations' properties being relevant to the proof attempts and the method for reasoning on such properties.
%
\subsection{On Meta-Reasoning}\label{sub:Meta-Reasoning}
Let a program $P_0$ written in ${\cal L}$ and a function application $f(d_0)$, where $d_0 \in \mathbb{D}$ is its input data, be given. Let $\expr{\var{\Prog}}$ stand for expression $(\expr{\var{Prog}~\; \var{N_{P_0}}})$, where $\expr{\var{N_{P_0}}}$ is the program name.
The unfolding loop standing alone produces a computation path $C_0, C_1, \ldots, C_n, \ldots$ starting off $f(d_0)$. If $f(d_0)$ terminates then the path is finite $C_0, C_1, \ldots, C_k$. In such a case, for any $0 \le i < k$ $C_i$ is a configuration not containing parameters, while $C_k$ is either a passive expression, if partial function $f$ defined on the given input data, or the abnormal termination sign $\bot$ otherwise. If the application does not terminate then all $C_i$ are non-parameterized configurations. The unfolding iterates function $\expr{\var{step}}(\cdot)$ such that $\expr{\var{step}}(C_i) = C_{i+1}$.
Now let us consider the following non-parameterized configuration %\\
$K_0 = \expr{\var{Eval}}( (\Nil){\;:\;}\underline{f(\; d_0 \;)}, \expr{\var{\Prog}} )$ %\\
%
of the self-interpreter. If $f(d_0)$ terminates then the loop unfolding the configuration $K_0$ results in the encoded passive configuration produced by the loop unfolding $f(d_0)$.
% $K_1 = step(K_0) = $ %\\
$$ K_1 = step(K_0) =
\fapp{Eval}{\args{\fapp{EvalCall}{\threeargs{\var{\underline{f}}}{\fapp{Eval}{\args{\brackets{\var{\Nil}}{:\var{\underline{d_0}}}}{\var{\Prog}}}}{\var{\Prog}}}}{\var{\Prog}}}{\,\append\,\fapp{Eval}{\args{\brackets{\var{\Nil}}{:\var{\Nil}}}{\var{\Prog}}}}
$$
Expression $K_1$ is not a configuration. According to the strategy described in Section \ref{subsec:Interpreter} the unfolding has to decompose expression $K_1$ in a sequence of configurations connected by the let-variables. This decomposition results in \\
$
\left\{~ \fapp{Eval}{\args{\brackets{\var{\Nil}}{:\var{\underline{d_0}}}}{\var{\Prog}}},~
\fapp{EvalCall}{\threeargs{\var{\underline{f}}}{\bullet}{\expr{\var{\Prog}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Prog}}}},~ \bullet~ \right\},~
$ \\
$
\texttt{\hspace{80pt} let}~ \var{e.x} ~\texttt{=}~ \bullet~ ~\texttt{in}~
\left\{~ {
\fapp{Eval}{\args{\brackets{\var{\Nil}}{:\var{\Nil}}}{\expr{\var{\Prog}}}}{},~
\var{e.x}\,\append\, \bullet~
} \right\}
$, where $\expr{\var{e.x}}$ is a fresh parameter.
Hence, considering modulo the arguments, the following holds.
Given a function-call stack element $\expr{\var{f}}$, this $\expr{\var{step}}$ maps the interpreted stack element to this segment of the interpreting function-call stack represented by the first configuration above, when this stack segment will be computed then its result is declared as a value of parameter $\expr{\var{e.x}}$ and the last configuration will be unfolded.
Note that
(1) these two configurations split by the \texttt{let}-construct will be unfolded completely separately one from the other, i.e., the first configuration becomes the input of the unfolding loop, while the second configuration is postponed for a future unfolding call;
(2) built-in function append $\append$ is not inserted in the stack at all, since it is treated by the supercompiler as a kind of
a special constructor, which properties are known by the supercompiler handling this special constructor on the fly.
The steps' sequence $\expr{\var{step}}(K_i),\; \ldots,\; \expr{\var{step}}(K_{j-1})$ between two consecutive applications $\expr{\var{step}}(K_i),\; \expr{\var{step}}(K_j)$ of the first $\expr{\var{Eval}}$ rewriting rule unfolds the big-step of the interpreter, interpreting the regular step corresponding to the application of a rewriting rule of the $f$ definition interpreted.
Given an expression $\expr{\var{exp}}$ to be interpreted by the interpreter, $\expr{\var{exp}}$ defines the current state of the $\expr{\var{P_0}}$ function-call stack. Let $C$ be the configuration representing this stack state (see Section \ref{subsec:Interpreter}). Let $f(exp_1)$ be the function application on the top of the stack. Then the current step $\expr{\var{step}}(K_i)$ corresponding to the application of the first $\expr{\var{Eval}}$ rewriting rule maps $\expr{\var{f}}$ to the stack segment $\expr{\var{Eval_1}}$, $\expr{\var{EvalCall_2}}$, $\expr{\var{Eval_3}}$ of the interpreter, considering modulo their arguments, and this stack segment becomes the leading segment of the interpreting function-call stack. The remainder of the interpreted stack is encoded in the arguments of $\expr{\var{Eval_3}}$, $\expr{\var{Eval_4}}$.
This remark allows us to follow the development of these two stacks in parallel.
Given the following two parameterized configurations $f(exp_1)$ and $Eval((exp_{env}){\;:\;}\underline{f(}\; exp_1 \;\underline{)}, \var{\Prog} )$ we are going to unfold these configurations in parallel, step by step. The simpler logic of unfolding
$f(exp_1)$ will provide hints on the logic unfolding
$Eval((exp_{env}){\;:\;}\underline{f(}\; exp_1 \;\underline{)}, \var{\Prog} )$.
Now we consider the set of the configuration pairs that may be generated by the unfold-fold loop and are in the relation {$\turprec$}.
\subsection{Internal Properties of the Interpreter Big-Step}\label{subsub:Internal-Properties}
In this section we consider several properties of the configurations generated by the unfold-fold loop inside one big-step of the self-interpreter.
Thus in order to prove indirectly that the program model is safe, we start off by unfolding the following initial configuration
%$$
{$
{\fapp{Int}{\args{\expr{\brackets{\expr{\var{Call}}~\expr{\var{Main}}~{\expr{\var{e.d}}}}}}{\expr{\brackets{\expr{\var{Prog}}~\expr{\var{Synapse}}}}}}{}}
$},
%$$
where the value of {$\expr{\var{e.d}}$} is unknown. Let $\expr{\var{\Syn}}$ stand for $\expr{\brackets{\expr{\var{Prog}}~\expr{\var{Synapse}}}}$.
%
Consider any parameterized configuration $C_b$ generated by the unfold-fold loop and initializing a big-step of the interpreter.
Firstly, we assume that $C_b$ is not generalized and no configuration was generalized by this loop before $C_b$. In such a case, $C_b$ is of the following form %\\
$$
\fapp{Eval}{\args{\brackets{\expr{\var{env}}}{:\expr{\var{\underline{arg}}}}}{\expr{\var{\Syn}}}},~
\fapp{EvalCall}{\threeargs{\var{\underline{f}}}{\bullet}{\expr{\var{\Syn}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
%\bullet~
$$ %\\
where ${\expr{\var{arg}}}$ stands
for the formal \emph{syntactic} argument taken from the right-hand side of a rewriting rule where $\underline{\fapp{f}{\var{arg}}{}}$\,
originates from,
$\expr{\var{env}}~{::=}~(~\expr{\var{var}}{\;:\;}\expr{\var{val}}~){\;:\;}\expr{\var{env}} ~|~ \Nil$, $\expr{\var{var}}~{::=}~\underline{\expr{\var{s.n}}} ~|~ \underline{\expr{\var{e.n}}}$, and $\expr{\var{val}}$ stands for a partial known value of variable $\expr{\var{var}}$.
Since application $\underline{\fapp{f}{\var{arg}}{}}$\, is on the top of the stack, argument ${\expr{\var{arg}}}$ includes no function application.
As a consequence, the leading $\expr{\var{Eval}}$ application has only to look for variables and to call substitution $\expr{\var{Subst}}$ if a variable is encountered.
Thus, excluding all the transitive configurations encountered before the substitution, we consider the following configuration \\
$
\left\{~
\fapp{Subst}{\args{\var{env}}{\brackets{\app{\var{Var}}{\var{\underline{var_{t.n}}}}}{}}}{},~ \bullet~
\right\},~
$ %\\
$
\texttt{ let}~
\var{e.x_1} ~\texttt{=}~ \bullet~ ~\texttt{in}~
\left\{~
\left\{~ {
\fapp{Eval}{\args{\brackets{\var{env}}{:\expr{\var{\underline{arg_1}}}}}{\expr{\var{\Syn}}}}{},~
\bullet~
} \right\},~ \right.
$ \\
$
\texttt{\hspace{125pt} let}~ \var{e.x_2} ~\texttt{=}~ \bullet~ ~\texttt{in}~
$ %, \\
$
\left. \left\{~
\fapp{EvalCall}{\threeargs{\var{\underline{f}}}{\var{e.x_1}\,\append\, \var{e.x_2}}{\expr{\var{\Syn}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
\right\}~ \right\} %\bigr\}~
$ \\
where $\expr{\var{e.x_1}},\, \expr{\var{e.x_2}}$ are fresh parameters,
${\expr{\var{arg_1}}}$ stands for a part of ${\expr{\var{arg}}}$ above to be
processed,
and $\underline{\expr{\var{var_{t.n}}}}$ denotes the type and the name of the variable encountered.
We turn now to the first configuration to be unfolded. All configurations
unfolded, step by step, from the first configuration are transitive since $\expr{\var{Subst}}$ tests only types and names of the environment variables. Function $\expr{\var{Subst}}$ is tail-recursive and returns value $\expr{\var{val}}$ asked for.
We skip transforming these transitive configurations and continue with the next one. \\
$
\left\{~ {
\fapp{Eval}{\args{\brackets{\var{env}}{:\expr{\var{\underline{arg_1}}}}}{\expr{\var{\Syn}}}}{},~
\bullet~
} \right\},~
$ %\\
$
\texttt{\hspace{0pt}let}~ \var{e.x_2} ~\texttt{=}~ \bullet~ ~\texttt{in}~
$ %, \\
$
\left\{~
\fapp{EvalCall}{\threeargs{\var{\underline{f}}}{\var{val}\,\append\, \var{e.x_2}}{\expr{\var{\Syn}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
\right\}
$ \\
By our assumption above, the loop unfolding this first configuration never generates a function application. So the leading configuration proceeds to look for the variables in the same way shown above.
When $\expr{\var{arg}}$ is entirely processed and all variables occurring in $\expr{\var{arg}}$ are replaced with their partially known values from the environment, then the current configuration looks as follows.
\vspace{-10pt}
$$
%\left\{~
\fapp{EvalCall}{\threeargs{\var{\underline{f}}}{\var{arg_2}}{\expr{\var{\Syn}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
%\right\}
$$ %\\
Here expression $\expr{\var{arg_2}}$ is $\expr{\var{\underline{arg}}}\theta$, were $\theta$ is the substitution defined by environment $\expr{\var{env}}$.
%
I.\,e., $\expr{\var{arg_2}}$ may include parameters standing for unknown data, while $\expr{\var{\underline{arg}}}$ does not.
Function $\expr\var{EvalCall}$ is defined by the only rewriting rule. So, any application of this function is one-step transitive. Recalling $\expr\var{\Syn}$, we turn to the next configuration.
\vspace{-10pt}
$$
%\left\{~
\fapp{Prog}{\expr{\var{Synapse}}}{},~
\fapp{LookFor}{\args{\expr{\var{\underline{f}}}}{\bullet}},~
\fapp{Matching}{\args{\threeargs{\var{\False}}{\var{\Nil}}{\bullet}}{\expr{\var{arg_2}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
%\right\}
$$ %\\
$\fapp{Prog}{\expr{\var{Synapse}}}{}$ returns the source code of the interpreted program $\expr{\var{Synapse}}$, while the $\expr{\var{LookFor}}$ application returns the definition of the function called by the interpreter, using the known name $\expr{\var{\underline{f}}}$. Skipping the corresponding transitive configurations, we have:
\vspace{-10pt}
$$
%\left\{~
\fapp{Matching}{\args{\threeargs{\var{\False}}{\var{\Nil}}{\brackets{\brackets{\var{\,\underline{p_1}\,}}{{\;:}\texttt{'='}{\;:\;}\brackets{\,\var{\underline{exp_1}}\,}}}{{\;:\;}\var{\underline{def_{r_1}}}\,}}}{\expr{\var{arg_2}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
%\right\}
$$ %\\
Here the third $\expr{\var{Matching}}$ argument is the $\expr{\var{f}}$ definition, where $\expr{\var{p_1}}$, $\expr{\var{exp_1}}$, $\expr{\var{def_{r_1}}}$ stand for the pattern, the right-hand side of the first rewriting rule of the definition, and the rest of this definition, respectively.
This $\expr{\var{Matching}}$ application transitively initiates matching the parameterized data $\expr{\var{arg_2}}$ against pattern $\expr{\var{\underline{p_1}}}$ and calls another $\expr{\var{Matching}}$ application in the context of this pattern matching. This second $\expr{\var{Matching}}$ application is provided with the $\expr{\var{f}}$ definition rest and $\expr{\var{arg_2}}$ for the case this pattern matching will fail. The next configuration is as follows.
\vspace{-15pt}
\begin{gather}\label{conf:Match}
\fapp{Match}{\threeargs{\var{\underline{p_1}\,}}{\var{arg_2}}{\brackets{\var{\Nil}}}},~
\fapp{Matching}{\args{\threeargs{\var{\bullet}}{\var{\underline{exp_1}}}{\var{\underline{def_{r_1}}}\,}}{\expr{\var{arg_2}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
\tag{\checkmark}%\label{conf:Match}
\end{gather}
\begin{remark}\label{rem:1st-on-transitive}
By now all the configurations generated by the unfolding loop were transitive. The steps
processing syntactic structure of the function application considered might meet constructor applications. These constructor applications are accumulated in the second $\expr\var{EvalCall}$ argument.
The analysis above did not use any particular property of the interpreted program despite the fact that the source code of the interpreted program has been received and
processed.
\end{remark}
Now we start to deal with function $\expr{\var{Match}}$ playing the main role in our analysis.
%
In order to unfold this configuration, we have now to use some particular properties of the interpreted program.
Since for any pattern $\expr{\var{p_1}}$ in program Synapse and any $\expr{\var{v}} \in {\cal V}$
$\expr{\var{\mu_v(p_1)}} < 2$ holds, Proposition \ref{prop:Match} below implies that the unfold-fold loop never stops unfolding the configuration \ref{conf:Match} until the $\expr{\var{Match}}$ application on the top of the stack will be completely unfolded to several passive expressions, step by step.
These expressions will appear on different possible computation paths starting at the configuration above. Skipping the steps unfolding the tree rooted in this stack-top configuration, we turn to the configurations that appear on the leaves of this tree. Each path starting at the top configuration leads to a configuration of one of the following two forms. These configurations are transitive.
\vspace{-15pt}
\begin{gather*}
%$$
%\left\{~
\fapp{Matching}{\args{\threeargs{\brackets{\var{env_1}}}{\var{\underline{exp_1}}}{\var{\underline{def_{r_1}}}\,}}{\expr{\var{arg_3}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots \\
%\right\}
%$$ %\\
%
%$$
%\left\{~
\fapp{Matching}{\args{\threeargs{\var{\False}}{\var{\underline{exp_1}}}{\var{\underline{def_{r_1}}}\,}}{\expr{\var{arg_3}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
%\right\}
%$$ %\\
\end{gather*}
In the first case, the pattern matching did succeed and function $\expr{\var{Matching}}$ replaces the current function application with the right-hand side of the chosen rewriting rule, provided with the constructed environment. The big-step being considered has been finished.
In order to launch the next big-step, interpreter $\expr{\var{Int}}$ has now to update the top of the interpreting function application stack.
In the second case, the pattern matching fails and function $\expr{\var{Matching}}$ once again calls $\expr{\var{Match}}$, aiming to match the parameterized data against the pattern of the next rewriting rule of function $\expr{\var{f}}$.
The next configuration is of the form \ref{conf:Match} above, in which the third $\expr{\var{Matching}}$ argument value is decremented with the rewriting rule has been considered.
If this value is empty and cannot be decremented, then, according to the language ${\cal L}$ semantics \ref{subsec:Self-Int-Language}, we have the abnormal deadlock state and the interpreter work is interrupted.
Starting off from this configuration, the unfold-fold loop proceeds in the way shown above.
\begin{proposition}\label{prop:Match}
For any pattern $\expr{\var{p_0}}$ such that for any $\expr{\var{v}} \in {\cal V}$
$\expr{\var{\mu_v}(\var{p_0})} < 2$ and any parameterized passive expression $\expr{\var{d}}$, the unfold-fold loop, starting off from configuration
$\fapp{Match}{\threeargs{\var{\underline{p_0}\,}}{\var{d}}{\brackets{\var{\Nil}}}}$
and controlled by the $\turprec$-strategy, results in a tree program\footnote{I.e., without any function application, excepting an entry point of this residual program.} such that any non-transitive vertex in the tree is labeled by a configuration of the form
$\fapp{Match}{\threeargs{\var{\underline{p_i}\,}}{\var{d_i}}{\brackets{\var{env_i}}}},~ \ldots~ $.
Given a path in the tree and any two configurations of the forms
$\fapp{Match}{\threeargs{\var{\underline{p_i}\,}}{\var{d_i}}{\brackets{\var{env_i}}}},~ \ldots~ $ and
$\fapp{Match}{\threeargs{\var{\underline{p_j}\,}}{\var{d_j}}{\brackets{\var{env_j}}}},~ \ldots~ $ belonging to the path, such that the second configuration is a descendant of the first one, then
$\expr{\var{\underline{p_j}}} \prec \expr{\var{\underline{p_i}}}$ holds.
\end{proposition}
\vspace{-15pt}
\paragraph{Proof}
If all descendants of configuration $\fapp{Match}{\threeargs{\var{\underline{p_0}\,}}{\var{d}}{\brackets{\var{\Nil}}}}$
are transitive then the unfold-fold loop results in a tree being a root and this tree satisfies the property required.
%
Now consider non-transitive descendants of $\fapp{Match}{\threeargs{\var{\underline{p_0}\,}}{\var{d}}{\brackets{\var{\Nil}}}}$ that may be generated by the unfold-fold loop before the first generalization or folding action
happened. The patterns of the $\expr{\var{PutV}}$ rewriting rules never test unknown data, hence any application of $\expr{\var{PutV}}$ is transitive. Since for any $\expr{\var{v}} \in {\cal V}$ relation $\expr{\var{\mu_v}(\var{p_0})} < 2$ holds, then function $\expr{\var{Eq}}$ will be never applied and the application of $\expr{\var{CheckRepVar}}$ is transitive.
As a consequence, all the non-transitive descendants are of the forms $\fapp{Match}{\threeargs{\var{\underline{p_i}\,}}{\var{d_i}}{\brackets{\var{env_i}}}}, \ldots~ $.
Note that only the paths originated by applications of the 2-nd, 3-rd, 4-th $\expr{\var{Match}}$ rewriting rules may contain configurations of such forms.
Consider a configuration $\fapp{Match}{\threeargs{\var{\underline{p_i}\,}}{\var{d_i}}{\brackets{\var{env_i}}}}, \ldots~ $.
Below $M_i$ denotes such a configuration.
Since $\expr{\var{p_i}}$ is a constant, hence one-step unfolding this configuration by the 2-nd rewriting rule leads to configuration
$\fapp{PutVar}{\args{\expr{\var{\underline{s.n}}}{\,:\;}\expr{\var{d_s}}}{\brackets{\var{env_i}}{}}},~
\fapp{Match}{\threeargs{\var{\underline{p_{i+1}}\,}}{\var{d_{i+1}}}{\bullet}}, \ldots~ $ such that
$\expr{\var{\underline{p_{i+1}}}}$ is a proper piece of $\expr{\var{\underline{p_i}}}$, in which at least one constructor is removed. Hence, $\expr{\var{\underline{p_{i+1}}}} \prec \expr{\var{\underline{p_i}}}$ holds.
Since the $\expr{\var{PutVar}}$ application is transitive, a number of unfolding steps lead transitively to
$\fapp{Match}{\threeargs{\var{\underline{p_{i+1}}\,}}{\var{d_{i+1}}}{\brackets{\var{env_{i+1}}}{}}}, \ldots~ $ such that $\expr{\var{\underline{p_{i+1}}}} \prec \expr{\var{\underline{p_i}}}$.
One-step unfolding the configuration $\fapp{Match}{\threeargs{\var{\underline{p_i}\,}}{\var{d_i}}{\brackets{\var{env_i}}}}, \ldots~ $ by the 3-rd rewriting rule leads to configuration
$\fapp{Match}{\threeargs{\var{\underline{p_{i+1}}\,}}{\var{d_{i+1}}}{\brackets{\var{env_i}}}},~
\fapp{Match}{\threeargs{\var{\underline{p_{i+2}}\,}}{\var{d_{i+2}}}{\bullet}}, \ldots~ $ such that
$\expr{\var{\underline{p_{i+1}}}}$ and $\expr{\var{\underline{p_{i+2}}}}$ are proper pieces of constant $\expr{\var{\underline{p_i}}}$. Hence, $\expr{\var{\underline{p_{i+1}}}} \prec \expr{\var{\underline{p_i}}}$ and $\expr{\var{\underline{p_{i+2}}}} \prec \expr{\var{\underline{p_i}}}$ hold.
One-step unfolding the configuration $\fapp{Match}{\threeargs{\var{\underline{p_i}\,}}{\var{d_i}}{\brackets{\var{env_i}}}}, \ldots~ $ by the 4-th rewriting rule leads to configuration
$\fapp{Match}{\threeargs{\var{\underline{p_{i+1}}\,}}{\var{d_{i+1}}}{\brackets{\var{env_i}}}},~ \ldots~ $ such that
$\expr{\var{\underline{p_{i+1}}}}$ is a proper piece of $\expr{\var{\underline{p_i}}}$, in which at least one constructor is removed. Hence, $\expr{\var{\underline{p_{i+1}}}} \prec \expr{\var{\underline{p_i}}}$ holds.
Now consider any two configurations of the forms
$\fapp{Match}{\threeargs{\var{\underline{p_i}\,}}{\var{d_i}}{\brackets{\var{env_i}}}}, \ldots~ $
and \\
$\fapp{Match}{\threeargs{\var{\underline{p_j}\,}}{\var{d_j}}{\brackets{\var{env_j}}}}, \ldots~ $
such that the second configuration belongs to a path originating from the first one and is encountered before any generalization. Hence, $\expr{\var{\underline{p_i}}}$ and $\expr{\var{\underline{p_j}}}$ are constants.
Given a configuration $C$, the length of $C$, denoted by $ln_c(C)$, is the number of the \emph{upper} function applications in $C$. (See Definition \ref{def:configuration} above.)
If $ln_c(M_j) < ln_c(M_i)$ then $M_i \nottur M_j$ and the Turchin relation prevents $M_j,\, M_i$ from generalization and $M_j$ from any folding action. (See Section \ref{subsec:Strategy}.)
If $ln_c(M_j) \ge ln_c(M_i)$ then we consider the first shortest configuration $M_k$ in the path segment being considered.
%
By definition of the stack,
$\fapp{Match}{\threeargs{\var{\underline{p_k}\,}}{\var{d_k}}{\bullet}}$
is from $M_i$ and $\fapp{Match}{\threeargs{\var{\underline{p_j}\,}}{\var{d_j}}{\brackets{\var{env_j}}}}$ is a descendent of $\fapp{Match}{\threeargs{\var{\underline{p_k}\,}}{\var{d_k}}{\brackets{\var{env_k}}}}$.
Since $\fapp{Match}{\threeargs{\var{\underline{p_k}\,}}{\var{d_k}}{\bullet}}$ took a part in computing $M_j$, it is the last function application of the stack prefix defined by the following Turchin relation $M_i \tur M_j$, which holds.
%
On the other hand, by the reasoning given above, for any $p_{j_l}$ from the prefix of $M_j$, defined by \emph{this} Turchin relation, $\underline{p_{j_l}} \prec \underline{p_k}$ holds, and, as a consequence,
%
the following relation $\fapp{Match}{\threeargs{\var{\underline{p_{j_l}}\,}}{\var{d_{j_l}}}{\brackets{\var{env_{j_l}}}}} \prec \fapp{Match}{\threeargs{\var{\underline{p_k}\,}}{\var{d_k}}{\bullet}}$ holds.
According to Turchin's relation, this relation prevents $M_j,\, M_i$ from generalization and $M_j$ from any folding action. (See Section \ref{subsec:Strategy}.)
The proposition has been proven.
%\\
$\Box$
\subsection{Dealing with the Interpreter Function-Application Stack}\label{subsub:Int-Stack}
Firstly, assuming again that no generalization happened in the unfold-fold loop up to now,
given a right-hand side $\expr{\var{exp_0}}$ of a rewriting rule returned by function $\expr{\var{Matching}}$ as described in Section \ref{subsub:Internal-Properties}, the following configuration has to map, step by step, the segment of the interpreted function-application stack, that is defined by known $\expr{\var{\underline{exp_0}}}$, on the top of the interpreting stack.
\vspace{-5pt}
$$
%\left\{~
\fapp{Eval}{\args{\brackets{\var{env}}{{\;:\;}\var{\underline{exp_0}}\,}}{\expr{\var{\Syn}}}},~ \ldots
%\right\}
$$ %\\
According to the call-by-value semantics, function $\expr{\var{Eval}}$ looks for the function application, whose right bracket is the leftmost closing bracket, in completely known $\expr{\var{\underline{exp_0}}}$. It moves from left to right along $\expr{\var{\underline{exp_0}}}$, substitutes transitively the variables encountered, as shown in Section \ref{subsub:Internal-Properties}, pushes the interpreted function application in the interpreting stack, mapping it into an $\expr{\var{EvalCall}}$ application, whenever the interpreted application should be pushed in the interpreted stack. See Section \ref{sub:Meta-Reasoning} for the details. Finally the depth first $\expr{\var{EvalCall}}$ application starts the next big-step.
Since for any pattern $\expr{\var{p}}$ of program Synapse and any $\expr{\var{v}} \in {\cal V}$
$\expr{\var{\mu_v(p)}} < 2$ holds,
hence, all applications
of $\expr{\var{Eq}}$, $\expr{\var{ContEq}}$ and $\expr{\var{PutV}}$
are transitive. This note together with Proposition \ref{prop:Match} implies
Proposition \ref{prop:FirstGener} below.
Let $\expr{\var{p_i}}$ stand for sub-patterns of a pattern of program Synapse,
$\expr{\var{arg_i}}$ and $\expr{\var{def}}$ stand for partially known parameterized expressions and several, maybe zero, rewriting rules being a rest of a function definition of Synapse, respectively.
Let $\expr{\var{exp}}$ stand for the right-hand side of a rewriting rule from this definition. %\\
$\expr{\var{env}}~{::=}~(~\expr{\var{var}}{\;:\;}\expr{\var{val}}~){\;:\;}\expr{\var{env}} ~|~ \Nil$, $\expr{\var{var}}~{::=}~\underline{\expr{\var{s.n}}} ~|~ \underline{\expr{\var{e.n}}}$\,, and $\expr{\var{val}}$ stands for a partially known value of variable $\expr{\var{var}}$.
Let $\expr{\var{Int_0}}$ denote
%$$
{$
{\fapp{Int}{\args{\expr{\brackets{\expr{\var{Call}}~\expr{\var{Main}}~\expr{\var{e.d}}}}}{\expr{\var{\Syn}}}}{}}
$},
%$$
where the value of {$\expr{\var{e.d}}$} is unknown.
\begin{proposition}\label{prop:FirstGener}
Let the unfold-fold loop be controlled by the $\turprec$-strategy. Let it start off from the initial configuration $\expr{\var{Int_0}}$.
Then the first generalized configuration generated by this loop, if any, will generalize two configurations of the following forms and any configuration folded, before this generalization, by a previous configuration is of the following form, where $n > 0$,
%\\
\vspace{-10pt}
\begin{gather}\label{conf:GenMatching}
\fapp{Match}{\threeargs{\var{\underline{p_1}\,}}{\var{arg_1}}{\brackets{\var{env}}}},~
\ldots,~
\fapp{Match}{\threeargs{\var{\underline{p_n}\,}}{\var{arg_n}}{\var{\bullet}}},~
\fapp{Matching}{\args{\threeargs{\var{\bullet}}{\var{\underline{exp}}}{\var{\underline{def}}\,}}{\expr{\var{arg_0}}}},~ \tag{\P} \\
\hspace{345pt} \fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
\notag
\end{gather}
\end{proposition}
Now consider any application of the form $\fapp{Match}{\threeargs{\var{\underline{p_1}\,}}{\var{arg_1}}{\brackets{\var{env}}}}$ staying on the stack top. Let $\expr{\var{Match_1}}$ denote this application.
Only the third rewriting rule of $\expr{\var{Match}}$ increases the stack. In this case the next state after the stack \ref{conf:GenMatching} is of the form $\expr{\var{Match_3}},~ \expr{\var{Match_2}}\; \ldots$.
Then, by Proposition \ref{prop:Match}, along any path originating from $\expr{\var{Match_2}}$ the application $\expr{\var{Match_2}}$ is not replaced until application $\expr{\var{Match_3}}$ will be completely unfolded.
Hence, for any stack state of the form $f_i,~ \ldots, ~ \expr{\var{Match_2}},~ \ldots$ on such a path, where $f_i$ denotes any function application, the following relation
$\expr{\var{Match_2}},~ \ldots \nottur f_i,~ \ldots, ~ \expr{\var{Match_2}},~ \ldots$ holds. That proves the following corollary using the denotations given above.
\begin{corollary}\label{prop:FirstGener2}
Given a timed application $\fapp{Matching_{t_0}}{\args{\threeargs{\var{\bullet}}{\var{\underline{exp}}}{\var{\underline{def}}\,}}{\expr{\var{arg_0}}}}$,
any two timed configurations of the form
{$
\ldots,~
\fapp{Matching_{t_0}}{\args{\threeargs{\var{\bullet}}{\var{\underline{exp}}}{\var{\underline{def}}\,}}{\expr{\var{arg_0}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
$}
can neither be generalized nor folded one by the other.
\end{corollary}
Since any application {$\fapp{Matching}{\args{\threeargs{\var{\dots}}{\var{\underline{exp}}}{\var{\underline{def}}}}}$} decreases, step by step, the list {$\var{\underline{def}}$} of the rewriting rules, the following corollary holds.
\begin{corollary}\label{prop:FirstGener3}
Given a big-step of {$\var{Int}$}, a timed pair {$\expr{\var{\underline{exp_{t_1}}}},\,\expr{\var{\underline{def_{t_1}}}}$}\footnote{Here we use the denotation given above and the timed expressions, which are defined in the same way as the timed applications \ref{subsec:Turchin}.}, and a timed application \\ $\fapp{Matching_{\tau_0}}{\args{\threeargs{\var{\bullet}}{\var{\underline{exp_{t_1}}}}{\var{\underline{def_{t_1}}}\,}}{\expr{\var{arg_0}}}}$ inside this big-step, then any two timed configurations of the form \\
{$
\ldots,~
\fapp{Matching_{\tau_i}}{\args{\threeargs{\var{\bullet}}{\var{\underline{exp_{t_i}}}}{\var{\underline{def_{t_i}}}\,}}{\expr{\var{arg_0}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots
$}
can neither be generalized nor folded one by the other.
\end{corollary}
Given a function definition $F$ and a rewriting rule $r$ of the definition, let $\expr{\var{exp_{F,r}}}$ stand for the right-hand side of $r$, while $\expr{\var{def_{F,r}}}$ stand for the rest of this definition rules following the rule $r$.
%
The following is a simple syntactic property of the Synapse program model given in Section \ref{sec:Specifying-Cache}.
\vspace{-10pt}
\begin{gather}\label{prop:SyntacticProperty}
\text{For any~} F_1, F_2 \in \{ \var{Main}, \var{Loop}, \var{Event}, \var{Append}, \var{Test} \} \text{~and for any two \emph{distinct} rewriting rules~} r_1, r_2\\
\text{~of~} F_1, F_2\text{, respectively,} %\\
(\expr{\var{exp_{F_1,r_1}}}, \expr{\var{def_{F_1,r_1}}}) \neq (\expr{\var{exp_{F_2,r_2}}}, \expr{\var{def_{F_2,r_2}}})
\text{~holds.} \notag
\end{gather}
That together with Corollaries \ref{prop:FirstGener2}, \ref{prop:FirstGener3} imply:
\begin{proposition}\label{prop:NoLocalFirstGener}
%
Given two configurations $C_1$ and $C_2$ of the form \ref{conf:GenMatching} to be generalized or folded one by the other. Then (1) $C_1$ and $C_2$ cannot belong to the same big-step of $\var{Int}$; (2) there are two functions $F_1$, $F_2$ of a cache coherence protocol model from the series mentioned in Section \ref{sec:Conclusion} (and specified in the way shown in Section \ref{sec:Specifying-Cache})
and rewriting rules $r_1, r_2$ of $F_1, F_2$, respectively, such that
$(\expr{\var{exp_{F_1,r_1}}}, \expr{\var{def_{F_1,r_1}}}) = (\expr{\var{exp_{F_2,r_2}}}, \expr{\var{def_{F_2,r_2}}})$, where functions $F_1$, $F_2$ and rules $r_1, r_2$ may coincide, respectively.
%
\end{proposition}
\begin{remark}\label{rem:2st-on-Synapse-properties}
Proposition \ref{prop:NoLocalFirstGener} depends on Property \ref{prop:SyntacticProperty}. Nevertheless, the restriction imposed by \ref{prop:SyntacticProperty} is very weak and the most of programs written in ${\cal L}$ satisfy \ref{prop:SyntacticProperty}.
It can easily be overcome by providing the interpreting function $\var{Matching}$ with an additional argument that is the interpreted function name.
The second statement of this proposition is well and crucial for the expectation of removing the interpretation overheads.
Despite the fact that the reasoning above follows the Synapse program model, it can be applied to any protocol model used in our experiments described in this paper.
\end{remark}
\emph{We conclude that any configuration encountered by the loop unfolding the given big-step is neither generalized with another configuration generated in unfolding \emph{this} big-step nor folded by such a configuration.}
\subsection{On Generalizing the Interpreter Configurations}\label{subsub:Rem-Interpreter}
The unfold-fold loop processes the paths originating from the initial configuration $\expr{\var{Int_0}}$, following the corresponding interpreted paths. The latter ones are processed according to the order of the rewriting rules in the Synapse function definitions.
The initial configuration $\var{Int_0}$ is unfolded according to function definition of $\var{Main}$ of the interpreted program. Application of this function leads transitively to the following function application
\vspace{-5pt}
%
{$$\fapp{Loop}{\expr{\brackets{\var{time}}}{\,:\,}\expr{\brackets{\var{Invalid}~\var{I}~\var{is}}}{\,:\,}\expr{\brackets{\var{Dirty}~}}{\,:\,}\expr{\brackets{\var{Valid}~}}{}}$$}
%
The interpreter has to match this call against the left-hand side of the first rewriting rule of the $\var{Loop}$ definition. The first corresponding pattern is:
{$\brackets{\texttt{[]}}{\,:\,}{\expr{\brackets{\var{Invalid}~\var{e.is}}}}{\,:\,}{\expr{\brackets{\var{Dirty}~\var{e.ds}}}}{\,:\,}{\expr{\brackets{\var{Valid}~\var{e.vs}}}}$}.
The pattern matching processes the pattern and argument from the left to the right, by means of function $\var{Match}$. The known part of the tree structure is mapped into the interpreting stack by the third rule of $\var{Match}$. The number of $\var{Match}$ applications in the stack is increased by this rewriting rule.
In the given context of specialization the values of $\var{time}$ and $\var{is}$ are unknown. Hence, the prefix of this stack that is responsible for matching the argument constant structure on the left-hand side of $\var{time}$ will transitively disappear and the unfolding loop will stop at the configuration of the following form \\
%
$\fapp{Match}{\threeargs{\var{\Nil}}{\var{time}}{\brackets{\var{\Nil}}}},~
\fapp{Match}{\threeargs{\var{\underline{p_2}\,}}{\var{arg_2}}{\var{\bullet}}},~
\fapp{Matching}{\args{\threeargs{\var{\bullet}}{\var{\underline{exp}}}{\var{\underline{def}}\,}}{\expr{\var{arg_0}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \bullet$. \\
%
Here the leading $\var{Match}$ application meets the unknown data $\var{time}$ and has to match it against $\var{\Nil}$ given in the first argument. The environment in the third argument is empty since no variable was still assigned up to now.
The second $\var{Match}$ application is responsible for matching the suspended part of the input data $\var{arg_2}$ against the rest $\var{\underline{p_2}}$ of the pattern. I.\,e., $\var{arg_2}$ equals
%
{$\expr{\brackets{\var{Invalid}~\var{I}~\var{is}}}{\,:\,}\expr{\brackets{\var{Dirty}~}}{\,:\,}\expr{\brackets{\var{Valid}~}}$}
and $\var{p_2}$ equals
{${\expr{\brackets{\var{Invalid}~\var{e.is}}}}{\,:\,}{\expr{\brackets{\var{Dirty}~\var{e.ds}}}}{\,:\,}{\expr{\brackets{\var{Valid}~\var{e.vs}}}}$}.
Now we note that the arguments of all applications of the recursive $\var{Loop}$ and $\var{Append}$ functions have exactly the same constant prefix as considered above. That leads to the following proposition.
\begin{proposition}\label{prop:FirstGener4}
Let the unfold-fold loop be controlled by the $\turprec$-strategy. Let it start off from the initial configuration $\expr{\var{Int_0}}$.
Then the first generalized configuration generated by this loop, if any, will generalize two configurations of the following forms and any configuration folded, before this generalization, by a previous configuration is of the following form \\
%
$\fapp{Match}{\threeargs{\var{\Nil}}{\var{arg_1}}{\brackets{\var{\Nil}}}},~
\fapp{Match}{\threeargs{\var{\underline{p_2}\,}}{\var{arg_2}}{\var{\bullet}}},~
\fapp{Matching}{\args{\threeargs{\var{\bullet}}{\var{\underline{exp}}}{\var{\underline{def}}\,}}{\expr{\var{arg_0}}}},~
\fapp{Eval}{\args{\bullet}{\expr{\var{\Syn}}}},~ \ldots $
\end{proposition}
In the given context of specialization the Turchin relation plays a crucial role in preventing the encountered configurations from generalization (see Proposition \ref{prop:Match}). It never forces decomposing the generalized configurations as might do, in general (see Section \ref{subsec:Turchin}).
\paragraph{The first generalization} has happened on the path unfolding the interpreted $\var{Loop}$ along the recursive branch following the iteration of the protocol event $\var{rm}$. No configuration was folded before this generalization. Only the number of $\var{Valid}$ items taking a part in the Synapse protocol was generalized. It serves as an accumulator and occurs twice in the generalized configuration $C_{g_1}$. So this generalization does not violate the safety property. Actually, this parameter might be introduced still in the initial configuration $\expr{\var{Int_0}}$ and the corresponding initial configuration \emph{generalized in advance} may be seen as a more meaningful formulation of the verification task.
No other generalization of the configurations generated by the recursion defined in function $\var{Loop}$ has happened.
\vspace{-10pt}
\paragraph{The first folding}
action was done in the same context as the first generalization done. The only distinction consists in another action: a generated configuration was folded by $C_{g_1}$.
Thus there is the only variable to be nontrivially substituted by this folding. The variable is the accumulating parameter introduced by this generalization.
\vspace{-10pt}
\paragraph{The second folding}
action was performed by the generalized configuration $C_{g_1}$ itself. The folded configuration ends a branch following the iteration of the protocol event $\var{rm}$.
There are two variables to be nontrivially substituted by this folding. One of the variables is the accumulating parameter mentioned above, while the other one is substituted with constant $\var{\Nil}$.
\vspace{-10pt}
\paragraph{The third folding}
action was done by a regular configuration $C_1$. Configuration $C_1$ is a descendant of $C_{g_1}$.
The folded configuration ends a branch following the iteration of the protocol event $\var{wm}$. The corresponding substitution is completely trivial, i.\,e., the folded and folding configurations coincide modulo variables names.
The sub-tree rooted in $C_1$ is completely folded. Configuration $C_1$ is declared as an entry point of a residual function definition. The fist rewriting rule of this definition is an exit from a recursion returning the value $\var{True}$, while the second and third branches refer to $C_{g_1}$ and $C_1$, respectively.
\vspace{-10pt}
\paragraph{The second generalization}
is forced by the interpreted $\var{Append}$ that is directly defined. It has happened along the recursive branch following the iteration of the protocol event $\var{wh2}$. The generalized configurations include several suspended substitutions to be performed in completely known expressions. Thus these substitutions may be done before this generalization if one might reveal formal reasons for such treatment of the suspended substitutions. These suspended substitutions form a stack of the $\var{Eval}$ applications aiming at executing them. This stack is still presented with delayed syntax composition, i.\,e., the $\var{Eval}$ applications are not still pushed in the explicit function application stack of the corresponding configuration. The $\var{Eval}$ application stack was generalized. A part of its calls were completely generalized by a parameter generalizing a rest of this stack, while the other calls were partially generalized. This second part of the generalization is very bad. The corresponding generalizing substitution contains pieces of the interpreted program model. The pieces are names and types of several variables. Fortunately, this generalization does not violate the safety property to be verified.
Neither $\var{Dirty}$ nor $\var{Valid}$ counters were generalized by this generalization.
Below $C_{g_2}$ stands for the configuration constructed by the second generalization.
\vspace{-10pt}
\paragraph{The fourth folded configuration}
is a descendent of configuration $C_{g_2}$.
It was folded by the regular configuration $C_1$ used in the third folding. The corresponding substitution is quite trivial. There are two parameters in both the folded and folding configurations. The folding substitution renames the parameter corresponding to the initial unknown data $\var{e.time}$ and replaces the parameter, standing for the unknown value of the $\var{Invalid}$ counter, with concatenation of completely unknown data early split into three parts.
\vspace{-10pt}
\paragraph{The fifth folded configuration}
is a descendent of configuration $C_{g_2}$ and it is folded by $C_{g_2}$ as well. There are thirteen parameters occurring in $C_{g_2}$. Fife parameters are substituted with expressions containing names and/or types of some variables from the Synapse program model. One parameter is replaced with an expression including an application $\var{Eval}$ that presents a generalized environment of this program model.
The sub-tree rooted in $C_{g_2}$ is completely folded. Configuration $C_{g_2}$ is declared as an entry point of a residual function definition. The fist rewriting rule of this definition refers to $C_1$, while the seconds one refers to $C_{g_2}$, i.\,e., to itself.
\vspace{-10pt}
\paragraph{The sixth folding}
action was done by the regular configuration $C_1$ used above.
The folding substitution increases counter $\var{Invalid}$ and renames the variable corresponding to stream $\var{e.time}$.
\vspace{-10pt}
\paragraph{The third generalization}
is forced by the interpreted $\var{Append}$ that is directly defined.
It has happened along the recursive branch following the iteration of the protocol event $\var{wm}$. The corresponding generalized configuration $C_{g_3}$ has 14 parameters and the badness similar to $C_{g_2}$.
\vspace{-10pt}
\paragraph{The seventh folding}
action was done in a similar context as the fourth one done. The only distinction consists in increasing the $\var{Invalid}$ counter by a constant.
\vspace{-10pt}
\paragraph{The eighth folded configuration}
is a descendent of configuration $C_{g_3}$ and it is folded by $C_{g_3}$ as well. The corresponding folding substitution has the badness similar to the fifth folding substitution.
The sub-tree rooted in $C_{g_3}$ is completely folded. Configuration $C_{g_3}$ is declared as an entry point of a residual function definition. The fist rewriting rule of this definition refers to $C_1$, while the seconds one refers to $C_{g_3}$, i.\,e., to itself.
That in its turn allows us to fold the sub-tree rooted in the first generalized configuration $C_{g_1}$. Configuration $C_{g_1}$ is declared as an entry point of a residual function definition. The fist rewriting rule of this definition is an exit from a recursion returning the value $\var{True}$. The second rewriting rule calls this entry point $C_{g_1}$, while the third and fourth branches refer to $C_{g_2}$ and $C_{g_3}$, respectively.
\vspace{-10pt}
\paragraph{The last folded configuration}
belongs to the last branch originating from the initial configuration. It is folded by the regular configuration $C_1$, which belongs to a parallel path and was used in the third folding.
The entire specialized tree has been completely folded and the safety property has been proven. Note that no generalized configuration was refused by the generalized configurations that were generated later than the former one.
The crucial configurations of the unfolding history leading to verification of this program model are given in Appendix \ref{sec:App-History} and are self-sufficient.
%
The residual program, generated by supercompilation of the residual program resulted in specializing the self-interpreter with respect to the Synapse N+1 program model, is given in Section \ref{sec:App-Residual}.
\section{Conclusion}\label{sec:Conclusion}
We have shown that a combination of the verification via supercompilation method and the second Futamura projection allows us to perform verification of the program being interpreted. We discussed the crucial steps of the supercompliation process involved in a verification of a parameterized cache coherence protocol used as a case study.
In the same way we were able to verify all cache coherence protocols from \cite{Delzanno-Param:00, Delzanno-Futurebus:00}, including
MSI, MOSI, MESI, MOESI, Illinois University, Berkley RISC, DEC Firefly, IEEE Futurebus+, Xerox PARC Dragon,
specified in the interpreted language ${\cal L}$.
Furthermore, we were able to verify the same protocols specified in the language WHILE \cite{Jones:Complex}. The complexity of involved processes is huge and further research is required for their better understanding.
Our experimental results show that Turchin's supercompilation is able to verify rather complicated program models of non-deterministic parameterized computing systems. The corresponding models used in our experiments are constructed on the base of the well known series of the cache coherence protocols mentioned above. So \emph{they might be new challenges to be verified by program transformation rather than an approach for verifying the protocols themselves}.
This protocol series was early verified by Delzanno \cite{Delzanno-Param:00} and Esparza et al. \cite{Esparza:1999} in abstract terms of equality and inequality constraints. Using unfold-fold program transformation tools this protocol series was early verified by the supercompiler SCP4 \cite{Lis_Nem:CSR07, Lis_Nem:Programming, Lis_Nem:IJFCS08, Lis_Nem:Protocols07} in terms of a functional programming language, several of these protocols were verified in terms of logical programming \cite{Roychoudhury:2004, FioPettProSen:GenVer13}. One may consider the indirect protocol models presented in this paper as a new collection of tests developing the state-of-the-art unfold-fold program transformation.
The intermediate interpreter considered in this paper specifies the operational semantics of a \emph{Turing-complete} language ${\cal L}$. We have proved several statements
%
on properties of the configurations generated by the unfold-fold cycle in the process specializing {$\var{Int}$} with respect to the cache coherence protocols specified as shown in Section \ref{sec:Specifying-Cache}.
The main of them is Proposition \ref{prop:Match}.
Some of these properties \emph{do not depend on specific protocols} from the considered series, i.\,e., they hold for any protocol specified in the way shown in Section \ref{sec:Specifying-Cache}.
That allows us to reason, \emph{in a uniform way}, on huge amount of complicated configurations.
Note that the programs specifying the protocols include both the function call and constructor application stacks, where the size of the first one is uniformly bounded on the input parameter while the second one is not.
Unlike system VeriMAP \cite{VeriMAP:2014} our indirect verification method involves no post-specialization unfold-fold.
As a future work, we would like to address the issue of the description of suitable properties of interpreters to which our uniform reasonings demonstrated in this paper might be applied.
\paragraph{Acknowledgements:} We would like to thank Antonina Nepeivoda and several reviewers for helping to improve this work.
\label{sect:bib}
\bibliographystyle{plain}
\bibliography{lisitsa_nemytykh}
%
\newpage
\section{Appendix}\label{Appendix}
\subsection{General Structure of the Supercompiler SCP4}\label{sec:App-Structure-SCP4}
\begin{figure}[htb]
\begin{center}
{%\small
\begin{flushleft}
%
{\hrule height 0.8pt \medskip}
\textit{Input:} (i) A list $\expr{\var{Tasks}}$ of parameterized entry configurations, (ii) a source program, and (iii) strategies for performing the transformation.\\
\textit{Output:} A set of $\expr{\var{residual}}$ function definitions.\\
{\medskip \hrule width 3cm \medskip}
%
$\expr{\var{residual}{~:=~}\texttt{\Nil}}$ \texttt{;}\hspace{200pt} \texttt{/*~} Initialization. \hspace{47pt}\texttt{~*/}\\
%
%
$\expr{\var{do}{}}$
%
\texttt{\{~}\\
\hspace{20pt}$\expr{\var{current}\text{-}\var{task}{~:=~}\fapp{head}{\var{Tasks}}}$ \texttt{;}\\
\hspace{20pt}$\expr{\var{unfolding}}$ \texttt{;} \hspace{205pt} \texttt{/*~} This actions may add \hspace{12pt}\texttt{~*/}\\
% Named in supercompilation as $\expr{\var{driving}}
\hspace{20pt}$\expr{\var{folding}~\&~\var{generalization}}$ \texttt{;}\hspace{142pt} \texttt{/*~} configurations to $\expr{\var{Tasks}}$. \texttt{~*/}\\
%
\hspace{20pt}$\expr{\var{if}~\brackets{~ \text{the} ~\var{current}\text{-}\var{task}~ \text{has been completely folded}~}}$ \\
\hspace{25pt}\texttt{\{~} $\expr{\var{global}\text{-}\var{analysis}}$ \texttt{;}\\
\hspace{35pt} $\expr{\var{specialization}~ \text{with respect to the global properties}}$ \texttt{;}\\
\hspace{35pt} $\expr{\var{propagation}~ \text{of the global information over}~ \var{Tasks}}$ \texttt{;}\\
%
\hspace{37pt}$\expr{\var{if}~\brackets{~ \text{the} ~\var{current}\text{-}\var{task}~ \text{is not empty}~}}$ \\
\hspace{42pt}\texttt{\{~}$\expr{\var{residual}{~:=~}\var{residual} ~\cup~ \{ \var{current}\text{-}\var{task} \}}$\texttt{;~\}~}\\
\hspace{37pt}$\expr{\var{Tasks}{~:=~}\fapp{tail}{\var{Tasks}}}$ \texttt{;}\\
%
\hspace{25pt}\texttt{\}~;}\\
%
\texttt{\}~}$\expr{\var{while}{}~\brackets{~\text{there is a configuration in} ~{\var{Tasks}{}}~}}$\\
$\expr{\var{dead}\text{-}\var{code}\text{-}\var{analysis}}$ \texttt{;}\\
{\medskip \hrule height 0.8pt \medskip}
\end{flushleft}
}
\end{center}
\caption{General Structure of the Supercompiler SCP4}\label{fig:SCP4}
\end{figure}
\subsection{Residual Program}\label{sec:App-Residual}
The residual program, generated by supercompilation of the residual program resulted in specializing the self-interpreter \ref{fig:Self-Interpreter} with respect to the Synapse N+1 program model \ref{fig:Synapse}, is given in Figure \ref{fig:ResidualSynapse}, where, for sake of readability, the variables' names and the entry function name were renamed.
The following three residual functions $\expr{\var{F12}}$, $\expr{\var{F31}}$, $\expr{\var{F46}}$ are specialized versions of the recursion defined in function $\expr{\var{Loop}}$, while the two residual functions $\expr{\var{F64}}$ and $\expr{\var{F100}}$ are reflection of the recursion defined by function $\expr{\var{Append}}$ directly specified in the Synapse N+1 program.
Any right-hand side of the rewriting rules generated by the first supercompilation, which are not shown here, includes no identifier $\expr{\var{False}}$. Hence, the Synapse N+1 program model already was successfully verified by the first application of the supercompiler SCP4, but the corresponding residual models includes syntactic pieces of the second rewiring rule of function $\expr{\var{Append}}$. The second application of this supercompiler removes these syntactic pieces.
See Section \ref{sec:App-History} for some details of the first supercompilation application.
\begin{figure}[htb]
\begin{center}
% $ENTRY Go { (e.time) (e.is) = <Loop (e.time) (Invalid I e.is)(Dirty )(Valid ) >; }
%
%IntRes( ('*' ):('*' e.is) ) = True ;
%IntRes( ('*' rm : e.time):('*' e.is) ) = F12( (e.time) : e.is);
%IntRes( ('*' wm):('*' e.is) ) = True ;
%IntRes( ('*' wm : rm : e.time):('*' I : e.is) ) = F12( (e.time) : I : e.is);
%IntRes( ('*' wm : wm : e.time):('*' I : e.is) ) = F46( (e.time) : e.is);
%IntRes( ('*' ):('*' e.is) ) = True ;
\fsent{IntRes}{\expr{\brackets{\texttt{'*'}}}{\,:\,}\brackets{\texttt{'*'}{\;:\;}\expr{\var{e.is}}}}{\expr{\var{True}}}
%
%IntRes( ('*' rm : e.time):('*' e.is) ) = F12( (e.time) : e.is);
\fsent{IntRes}{\expr{\brackets{\texttt{'*'}{\;:\;}\var{rm}{\,:\,}\var{e.time}}}{\,:\,}\brackets{\texttt{'*'}{\;:\;}\expr{\var{e.is}}}}
{\fapp{F12}{\brackets{\var{e.time}}{\,:\,}\expr{\var{e.is}}}}
%
%IntRes( ('*' wm):('*' e.is) ) = True ;
\fsent{IntRes}{\expr{\brackets{\texttt{'*'}{\;:\;}\var{wm}}}{\,:\,}\brackets{\texttt{'*'}{~:\,}\expr{\var{e.is}}}}{\expr{\var{True}}}
%
%IntRes( ('*' wm : rm : e.time):('*' I : e.is) ) = F12( (e.time) : I : e.is);
\fsent{IntRes}{\expr{\brackets{\texttt{'*'}{\;:\;}\var{wm}{\,:\,}\var{rm}{\,:\,}\var{e.time}}}{\,:\,}\brackets{\texttt{'*'}{\;:\;}\var{I}{\,:\,}\expr{\var{e.is}}}}
{\fapp{F12}{\brackets{\var{e.time}}{\,:\,}\expr{\var{I}{\,:\,}\var{e.is}}}}
%
%IntRes( ('*' wm : wm : e.time):('*' I : e.is) ) = F46( (e.time) : e.is);
\fsent{IntRes}{\expr{\brackets{\texttt{'*'}{\;:\;}\var{wm}{\,:\,}\var{wm}{\,:\,}\var{e.time}}}{\,:\,}\brackets{\texttt{'*'}{\;:\;}\var{I}{\,:\,}\expr{\var{e.is}}}}
{\fapp{F46}{\brackets{\var{e.time}}{\,:\,}\expr{\var{e.is}}}}
%
%
%F12( () : e.is2 ) = True;
%F12( (rm : e.time) : I : e.is2 ) = F31( ():(e.time) : e.is2 );
%F12( (wh2) e.is2 ) = True;
%F12( (wh2 : rm : e.time) : I : e.is2 ) = F12( (e.time) : I : e.is2 );
%F12( (wh2 : wm : e.time) : I : e.is2 ) = F46( (e.time) e.is2 );
%F12( (wm : e.time) : I : e.is2 ) = F46( (e.time) : e.is2 );
{\fnew}
%
%F12( () : e.is2 ) = True;
\fsent{F12}{\expr{\brackets{\var{\Nil}}}{\,:\,}\expr{\var{e.is2}}}{\expr{\var{True}}}
%
%F12( (rm : e.time) : I : e.is2 ) = F31( ():(e.time) : e.is2 );
\fsent{F12}{\expr{\brackets{\var{rm}{\,:\,}\var{e.time}}}{\;:\;}\var{I}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F31}{\brackets{\var{\Nil}}{\,:\,}\brackets{\var{e.time}}{\,:\,}\expr{\var{e.is2}}}}
%
%F12( (wh2) e.is2 ) = True;
\fsent{F12}{\expr{\brackets{\var{wh2}}}{\;:\;}\expr{\var{e.is2}}}{\expr{\var{True}}}
%
%F12( (wh2 : rm : e.time) : I : e.is2 ) = F12( (e.time) : I : e.is2 );
\fsent{F12}{\expr{\brackets{\var{wh2}{\,:\,}\var{rm}{\,:\,}\var{e.time}}}{\;:\;}\var{I}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F12}{\brackets{\var{e.time}}{\;:\;}\var{I}{\,:\,}\expr{\var{e.is2}}}}
%
%F12( (wh2 : wm : e.time) : I : e.is2 ) = F46( (e.time) e.is2 );
\fsent{F12}{\expr{\brackets{\var{wh2}{\,:\,}\var{wm}{\,:\,}\var{e.time}}}{\;:\;}\var{I}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F46}{\brackets{\var{e.time}}{\,:\,}\expr{\var{e.is2}}}}
%
%F12( (wm : e.time) : I : e.is2 ) = F46( (e.time) : e.is2 );
\fsent{F12}{\expr{\brackets{\var{wm}{\,:\,}\var{e.time}}}{\;:\;}\var{I}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F46}{\brackets{\var{e.time}}{\,:\,}\expr{\var{e.is2}}}}
%
%F31( (e.is3):() : e.is2 ) = True;
%F31( (e.is3):(rm : e.time) : I : e.is2 ) = F31( (I : e.is3) : (e.time) : e.is2 );
%F31( (e.is3):(wh2 : e.time) : e.is2 ) = F64( (e.is3) : (e.is2) : (e.time) );
%F31( (e.is3):(wm : e.time) : I : e.is2 ) = F100( (e.is3) : (e.is2) : (e.time) );
{\fnew}
%
%F31( (e.is3):() : e.is2 ) = True;
\fsent{F31}{\expr{\brackets{\var{e.is3}}{\,:\,}\expr{\brackets{\var{\Nil}}}}{\,:\,}\expr{\var{e.is2}}}{\expr{\var{True}}}
%
%F31( (e.is3):(rm : e.time) : I : e.is2 ) = F31( (I : e.is3) : (e.time) : e.is2 );
\fsent{F31}{\expr{\brackets{\var{e.is3}}{\,:\,}\brackets{\var{rm}{\,:\,}\var{e.time}}}{\;:\;}\var{I}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F31}{\brackets{\var{I}{\;:\;}\var{e.is3}}{\,:\,}\brackets{\var{e.time}}{\,:\,}\expr{\var{e.is2}}}}
%
%F31( (e.is3):(wh2 : e.time) : e.is2 ) = F64( (e.is3) : (e.is2) : (e.time) );
\fsent{F31}{\expr{\brackets{\var{e.is3}}{\,:\,}\brackets{\var{wh2}{\,:\,}\var{e.time}}}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F64}{\brackets{\var{e.is3}}{\,:\,}\brackets{\expr{\var{e.is2}}}{\,:\,}\brackets{\var{e.time}}}}
%
%F31( (e.is3):(wm : e.time) : I : e.is2 ) = F100( (e.is3) : (e.is2) : (e.time) );
\fsent{F31}{\expr{\brackets{\var{e.is3}}{\,:\,}\brackets{\var{wm}{\,:\,}\var{e.time}}}{\;:\;}\expr{\var{I}}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F100}{\brackets{\var{e.is3}}{\,:\,}\brackets{\expr{\var{e.is2}}}{\,:\,}\brackets{\var{e.time}}}}
%
%
%F46( () : e.is2 = True ;
%F46( (rm : e.time) : e.is2 ) = F12( (e.time) : I : e.is2);
%F46( (wm : e.time) : e.is2 ) = F46( (e.time) : e.is2);
%
{\fnew}
%
%F46( () : e.is2 = True ;
\fsent{F46}{\expr{\brackets{\var{\Nil}}}{\,:\,}\expr{\var{e.is2}}}{\expr{\var{True}}}
%
%F46( (rm : e.time) : e.is2 ) = F12( (e.time) : I : e.is2);
\fsent{F46}{\expr{\brackets{\var{rm}{\,:\,}\var{e.time}}}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F12}{\brackets{\var{e.time}}{\;:\;}\var{I}{\,:\,}\expr{\var{e.is2}}}}
%
%F46( (wm : e.time) : e.is2 ) = F46( (e.time) : e.is2);
\fsent{F46}{\expr{\brackets{\var{wm}{\,:\,}\var{e.time}}}{\;:\;}\expr{\var{e.is2}}}
{\fapp{F46}{\brackets{\var{e.time}}{\,:\,}\expr{\var{e.is2}}}}
%
%
%F64( ():(e.ys2) : (e.time) : e.ys3 ) = F46( (e.time) : e.ys3 ++ e.ys2 );
%F64( (s.x1 : e.xs2) : (e.ys2) : (e.time) : e.ys3 )
% = F64( (e.xs2) : (e.ys2) : (e.time) : e.ys3 ++ s.x1 );
{\fnew}
%
%F64( ():(e.ys2) : (e.time) : e.ys3 ) = F46( (e.time) : e.ys3 ++ e.ys2 );
\fsent{F64}{\expr{\brackets{\var{\Nil}}{\,:\,}\brackets{\var{e.ys2}}{\,:\,}\brackets{\var{e.time}}}{\;:\;}\expr{\var{e.ys3}}}
{\fapp{F46}{\brackets{\var{e.time}}{\,:\,}\expr{\var{e.ys3}~\append~\var{e.ys2}}}}
%
%F64( (s.x1 : e.xs2) : (e.ys2) : (e.time) : e.ys3 )
% = F64( (e.xs2) : (e.ys2) : (e.time) : e.ys3 ++ s.x1 );
\fsent{F64}{\expr{\brackets{\var{s.x1}{\;:\;}\var{e.xs2}}{\,:\,}\brackets{\var{e.ys2}}{\,:\,}\brackets{\var{e.time}}}{\;:\;}\expr{\var{e.ys3}}}
{\fapp{F64}{\expr{\brackets{\var{e.xs2}}{\,:\,}\brackets{\var{e.ys2}}{\,:\,}\brackets{\var{e.time}}}{\;:\;}\expr{\var{e.ys3}~\append~\var{s.x1}}}}
%
%
%
%F100( () : (e.ys2) : (e.time) : e.ys3 ) = F46( (e.time) : I : e.ys3 ++ e.ys2 );
%F100( (s.x1 : e.xs2) : (e.ys2) : (e.time) : e.ys3 )
% = F100( (e.xs2) : (e.ys2) : (e.time) : e.ys3 ++ s.x1 );
{\fnew}
%
%F100( () : (e.ys2) : (e.time) : e.ys3 ) = F46( (e.time) : I : e.ys3 ++ e.ys2 );
\fsent{F100}{\expr{\brackets{\var{\Nil}}{\,:\,}\brackets{\var{e.ys2}}{\,:\,}\brackets{\var{e.time}}}{\;:\;}\expr{\var{e.ys3}}}
{\fapp{F46}{\brackets{\var{e.time}}{\;:\;}\var{I}{\;:\;}\expr{\var{e.ys3}~\append~\var{e.ys2}}}}
%
%F100( (s.x1 : e.xs2) : (e.ys2) : (e.time) : e.ys3 )
% = F100( (e.xs2) : (e.ys2) : (e.time) : e.ys3 ++ s.x1 );
\fsent{F100}{\expr{\brackets{\var{s.x1}{\;:\;}\var{e.xs2}}{\,:\,}\brackets{\var{e.ys2}}{\,:\,}\brackets{\var{e.time}}}{\;:\;}\expr{\var{e.ys3}}}
{\fapp{F100}{\expr{\brackets{\var{e.xs2}}{\,:\,}\brackets{\var{e.ys2}}{\,:\,}\brackets{\var{e.time}}}{\;:\;}\expr{\var{e.ys3}~\append~\var{s.x1}}}}
\end{center}
\caption{Residual Model of the Synapse N+1 Cache Coherence Protocol}\label{fig:ResidualSynapse}
\end{figure}
\clearpage
\subsection{Non-Transitivity of Turchin's Relation}\label{subsec:Non-Transitivity}
The following example shows that Turchin's relation \ref{subsec:Turchin} is not transitive.
The idea of the example is borrowed from \cite{AntoninaNepeivoda:Sbornik2014}.
\medskip
\noindent
\begin{tabular}{ll|ll}
%Main( e.xs ) = C( Fb( Fab( e.xs ) ) );
$[R_0]$ & \fsent{Main}{\expr{\var{e.xs}}}
{\fapp{C}{\fapp{Fb}{\fapp{Fab}{\var{e.xs}}}}} &
%F( ) = ;
$[R_7]$ & \fsent{F}{\expr{\var{\Nil}}}{\expr{\var{\Nil}}}
\\
$ $ & & %\medskip
%F( e.xs ) = Fc( Fab( e.xs) );
$[R_8]$ & \fsent{F}{\expr{\var{e.xs}}}
{\fapp{Fc}{\fapp{Fab}{\expr{\var{e.xs}}}}}
\\
%Fab( ) = 'c';
$[R_1]$ & \fsent{Fab}{\expr{\var{\Nil}}}{\expr{\texttt{'c'}}} &
$ $ & %\medskip
\\
%
%Fab( 'a' : e.xs ) = 'b' : Fab( e.xs);
$[R_2]$ & \fsent{Fab}{\expr{\texttt{'a'}{\,:\,}\expr{\var{e.xs}}}}
{\expr{\texttt{'b'}{\,:\,}}{\expr{\fapp{Fab}{\expr{\var{e.xs}}}}}} &
%Fb( ) = ;
$[R_9]$ & \fsent{Fb}{\expr{\var{\Nil}}}{\expr{\var{\Nil}}}
\\
%
%Fab( e.xs ) = Fc( Fab( e.xs) );
$[R_3]$ & \fsent{Fab}{\expr{\var{e.xs}}}
{\fapp{Fc}{\fapp{Fab}{\expr{\var{e.xs}}}}} &
%Fb( 'b' : e.xs ) = 'b' : e.xs;
$[R_{10}]$ & \fsent{Fb}{\expr{\texttt{'b'}{\,:\;}\expr{\var{e.xs}}}}
{\expr{\texttt{'b'}{\,:\;}\expr{\expr{\var{e.xs}}}}}
\\
$ $ & & %\medskip
%Fb( s.y : e.xs ) = E( s.y : Fb( F( e.xs) ) );
$[R_{11}]$ & \fsent{Fb}{\expr{\var{s.y}{\,:\,}\var{e.xs}}}
{\fapp{E}{\expr{\var{s.y}{\,:\,}\fapp{Fb}{\fapp{F}{\var{e.xs}}}}}}
\\
%
%Fc( ) = ;
$[R_4]$ & \fsent{Fc}{\expr{\var{\Nil}}}{\expr{\var{\Nil}}} &
$ $ & %\medskip
\\
%
%Fc( c : e.xs ) = 'd' : 'd';
$[R_5]$ & \fsent{Fc}{\expr{\texttt{'c'}{\,:\,}\expr{\var{e.xs}}}}
{\texttt{'d'}{\,:\,}\texttt{'d'}} &
$~\ldots $ & \fsent{E}{\expr{\ldots}}{\expr{\ldots}}
\\
%
%Fc( s.y : e.xs ) = s.y : Fc( e.xs);
$[R_6]$ & \fsent{Fc}{\expr{\var{s.y}{\,:\,}\expr{\var{e.xs}}}}
{\expr{\var{s.y}{\,:\,}{\expr{\fapp{Fc}{\expr{\var{e.xs}}}}}}} &
$~\ldots $ & \expr{~\ldots\ldots\ldots\ldots\ldots\ldots}
\\
$ $ & %\medskip
\\
%
$~\ldots $ & \fsent{C}{\expr{\ldots}}{\expr{\ldots}}
\\
$~\ldots $ & \expr{~\ldots\ldots\ldots\ldots\ldots\ldots}
\\
\end{tabular}
\medskip
Consider the path starting at initial configuration $\expr{\var{Main}}$ and following the sequence of the rewriting rules $[R_0], [R_3], [R_1], [R_5], [R_{11}], [R_8]$:\\
$\text{[1]:\;}\fapp{Main_0}{\expr{\var{e.xs}}} \stackrel{R_0}{\longrightarrow}
\text{[2]:\;}\fapp{Fab_3}{\var{e.xs}}, \fapp{Fb_2}{\var{\bullet}}, \fapp{C_1}{\var{\bullet}}
\stackrel{R_3}{\longrightarrow}
\text{[3]:\;}\fapp{Fab_5}{\var{e.xs}}, \fapp{Fc_4}{\var{\bullet}}, \fapp{Fb_2}{\var{\bullet}}, \fapp{C_1}{\var{\bullet}}$ \\
$\stackrel{R_1}{\longrightarrow}
\text{[4]:\;}\fapp{Fc_4}{\texttt{'c'}}, \fapp{Fb_2}{\var{\bullet}}, \fapp{C_1}{\var{\bullet}}
\stackrel{R_5}{\longrightarrow}
\text{[5]:\;}\fapp{Fb_2}{\texttt{'d'}{\,:\,}\texttt{'d'}}, \fapp{C_1}{\var{\bullet}}$ \\
$\stackrel{R_{11}}{\longrightarrow}
\text{[6]:\;}\fapp{F_8}{\texttt{'d'}}, \fapp{Fb_7}{\var{\bullet}}, \fapp{E_6}{\expr{\texttt{'d'}{\,:\;}\var{\bullet}}}, \fapp{C_1}{\var{\bullet}}$ \\
$\stackrel{R_8}{\longrightarrow}
\text{[7]:\;}\fapp{Fab_{10}}{\texttt{'d'}}, \fapp{Fc_9}{\var{\bullet}}, \fapp{Fb_7}{\var{\bullet}}, \fapp{E_6}{\expr{\texttt{'d'}{\,:\;}\var{\bullet}}}, \fapp{C_1}{\var{\bullet}}
$
Here the pairs [2], [3] and [3], [7] of the timed configurations are in Turchin's relation:
\begin{itemize}
\item[-] [2] $\tur$ [3] holds, where the common context is $\fapp{Fb_2}{\var{\bullet}}, \fapp{C_1}{\var{\bullet}}$ and the prefixes are $\fapp{Fab_3}{\var{e.xs}}$ and $\fapp{Fab_5}{\var{e.xs}}$, respectively;
%
\item[-] [3] $\tur$ [7] hold, where the common context is $\fapp{C_1}{\var{\bullet}}$ and the prefixes are \\
$\fapp{Fab_5}{\var{e.xs}}, \fapp{Fc_4}{\var{\bullet}}, \fapp{Fb_2}{\var{\bullet}}$ and $\fapp{Fab_{10}}{\texttt{'d'}}, \fapp{Fc_9}{\var{\bullet}}, \fapp{Fb_7}{\var{\bullet}}$, respectively.
\end{itemize}
While [2] $\tur$ [7] does not hold.
\subsection{Generalized and Folded Configurations}\label{sec:App-History}
\subsubsection{Generalization}\label{sec:App-Gener}
\begin{enumerate}
\item \emph{Gener-1}: {$\expr{\var{Loop}}$}. The first generalization has happened on the path unfolding the interpreted $\var{Loop}$ along the recursive branch following the iteration of the protocol event $\var{rm}$. No configuration was folded before this generalization. The boxed pieces of the configurations below stand for the generalized parts. Only the number of $\var{Valid}$ items taking a part in the Synapse protocol was generalized. It serves as an accumulator and occurs twice in the generalized configuration. So this generalization does not violate the safety property. %\\
\noindent
The previous configuration:\\
{\small{
$\fapp{Match}{\threeargs{\Nil}{\expr{\var{e.101}}}{\expr{\brackets{\Nil}}}}$,
\\
$\fapp{Match}{\threeargs{\underline{( \var{Invalid}~\var{e.is}){:}(\var{Dirty}~\var{e.ds} ){:}(\var{Valid}~ \var{e.vs} )}}
{\underline{\expr{{(} \var{Invalid}}}~ \var{e.102} \underline{){:}(\var{Dirty}~ ){:}(\var{Valid}~ \var{I}~\boxed{\Nil} )}}{\bullet}}$,
\\
%
$\expr{\var{Matching}}(~\bullet,~\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}\;,$\\
}} %\small
%
%
%
{\small{ ${{~~~~}(\;}\encodlfsent{Loop}{\expr{\brackets{\var{s.t}{\,:\,}\var{e.time}}}{\,:\,}\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}
{\fapp{Loop}{\expr{\brackets{\var{e.time}}}{\,:\,}\fapp{Event}{\var{s.t}{\,:\,}\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}}}
\\\;{~~~~}),~
\underline{\expr{(}}\expr{\var{e.101}~} \underline{{):(}\expr{\var{Invalid}~}} \expr{~\var{e.102}~} \underline{{):(}\expr{\var{Dirty}~}{):(}\expr{\var{Valid}~} \expr{~\var{I}}~\boxed{\Nil})}$
%
\\ ${)}$, %Matching
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
}} %\small
\\
\\
The current configuration:\\
{\small{
$\fapp{Match}{\threeargs{\Nil}{\expr{\var{e.101}}}{\expr{\brackets{\Nil}}}}$,
\\
$\fapp{Match}{\threeargs{\underline{( \var{Invalid}~\var{e.is}){:}(\var{Dirty}~\var{e.ds} ){:}(\var{Valid}~ \var{e.vs} )}}
{\underline{\expr{{(} \var{Invalid}}}~ \var{e.102} \underline{){:}(\var{Dirty}~ ){:}(\var{Valid}~ \var{I}~ \boxed{\var{I}} )}}{\bullet}}$,
\\
%
$\expr{\var{Matching}}(~\bullet,~\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}\;,$\\
}} %\small
%
%
%
{\small{ ${{~~~~}(\;}\encodlfsent{Loop}{\expr{\brackets{\var{s.t}{\,:\,}\var{e.time}}}{\,:\,}\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}
{\fapp{Loop}{\expr{\brackets{\var{e.time}}}{\,:\,}\fapp{Event}{\var{s.t}{\,:\,}\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}}}
\\\;{~~~~}),~
\underline{\expr{(}}\expr{\var{e.101}~} \underline{{):(}\expr{\var{Invalid}~}} \expr{~\var{e.102}~} \underline{{):(}\expr{\var{Dirty}~}{):(}\expr{\var{Valid}~} \expr{~\var{I}~ \boxed{\var{I}}})}$
%
\\ ${)}$, %Matching
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
}} %\small
\\
\\
The generalized configuration:\\
%{ e.101 <-e.136 ; e.102 <-e.137 ; [] <-e.138.inf ; }
{\small{
$\fapp{Match}{\threeargs{\Nil}{\expr{\var{e.101}}}{\expr{\brackets{\Nil}}}}$,
\\
$\fapp{Match}{\threeargs{\underline{( \var{Invalid}~\var{e.is}){:}(\var{Dirty}~\var{e.ds} ){:}(\var{Valid}~ \var{e.vs} )}}
{\underline{\expr{{(} \var{Invalid}}}~ \var{e.102} \underline{){:}(\expr{\var{Dirty}}~ ){:}(\expr{\var{Valid}}~ \expr{\var{I}}}~\boxed{\expr{\var{e.138}}}~ \underline{)}}{\bullet}}$,
\\
%
$\expr{\var{Matching}}(~\bullet,~\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}\;,$\\
}} %\small
%
%
%
{\small{ ${{~~~~}(\;}\encodlfsent{Loop}{\expr{\brackets{\var{s.t}{\,:\,}\var{e.time}}}{\,:\,}\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}
{\fapp{Loop}{\expr{\brackets{\var{e.time}}}{\,:\,}\fapp{Event}{\var{s.t}{\,:\,}\expr{\brackets{\var{Invalid}~\var{e.is}}}{\,:\,}\expr{\brackets{\var{Dirty}~\var{e.ds}}}{\,:\,}\expr{\brackets{\var{Valid}~\var{e.vs}}}}}}
\\\;{~~~~}),~
\underline{\expr{(}}\expr{\var{e.101}~} \underline{{):(}\expr{\var{Invalid}~}} \expr{~\var{e.102}~} \underline{{):(}\expr{\var{Dirty}~}{):(}\expr{\var{Valid}~} \expr{~\var{I}}}~~\boxed{\var{e.138}}~\underline{)}$
%
\\ ${)}$, %Matching
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
}} %\small
\\
\item \emph{Gener-2}: {$\expr{\var{Append}}$} %\\
The second generalization is forced by the interpreted $\var{Append}$ that is directly defined. It has happened along the recursive branch following the iteration of the protocol event $\var{wh2}$. The generalized configurations include several suspended substitutions to be performed in completely known expressions. Thus these substitutions may be done before this generalization if one might reveal formal reasons for such treatment of the suspended substitutions. These suspended substitutions form a stack of the $\var{Eval}$ applications aiming at executing them. This stack is still presented with delayed syntax composition, i.\,e., the $\var{Eval}$ applications are not still pushed in the explicit function application stack of the corresponding configuration. The $\var{Eval}$ application stack was generalized. A part of its calls were completely generalized by a parameter generalizing a rest of this stack, while the other calls were partially generalized. This second part of the generalization is very bad. The corresponding generalizing substitution contains pieces of the interpreted program model. The pieces are names and types of several variables. Fortunately, this generalization does not violate the safety property to be verified.
Neither $\var{Dirty}$ nor $\var{Valid}$ counters were generalized by this generalization.
Below $C_{g_2}$ stands for the configuration constructed by the second generalization.
The cause leading to the bad generalization is a wrong choice of the sequence of the steps generalizing the two configurations. Since constructor $\append$ is associative some sub-expressions of these configurations may be processed from both the left and right sides of the sub-expressions. The supercompiler SCP4 makes a bad choice in the situation described above. There are simple syntactic tricks allowing us overcome this problems. Nevertheless, the indirect specification of the Synapse N+1 protocol can be verified without using the tricks.
\noindent
The previous configuration:\\
%<RigitMatch_1gg (()(e.138.inf )())> <-h.0 ;
{\small{
$\fapp{Match}{\threeargs{\Nil}{\boxed{\expr{\var{e.138}}}}{\expr{\brackets{\Nil}}}}$,
\\
%<RigitMatch_1gg ((* (Var e e2 )))((* e.137 ))h.0 > <-h.0 ;
$\fapp{Match}{\threeargs{\underline{( \var{e.ys} )}}
{\underline{\expr{{(} }}~ \var{e.137} \underline{)}}{\bullet}}$,
\\
%<Matching_c0 h.0 ((Var e e2 ))((((* (Var s sx )(Var e e1 ))(* (Var e e2 ))) '='
% ((Var s sx )(Call Append (* (Var e e1 ))(* (Var e e2 ))))))
% ((* e.138.inf )(* e.137 ))> <-h.0 ;
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~~\boxed{\expr{\var{e.138}}}~~ \underline{{):(}}~\expr{\var{e.137}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$,
\\
%<EvalCall_c8 Loop ((* e.136 )
% (* Invalid h.0
% <Eval_o (((Var e vs ) e.138.inf )((Var e is )e.137 )
% ((Var e ds )))((* Dirty I )(* Valid ))(Prog Synapse )
% >
% )
% <Eval_o (((Var e vs )e.138.inf )((Var e is )e.137 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.138.inf )((Var e is )e.137 )((Var s t )wh2 )
% ((Var e time )e.136 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.136} \underline{):(} ~\var{Invalid}~~~ ~\boxedNilL~
~{\bullet}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~}%{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.\boxed{vs}}}}
{\;:\;}~{\expr{\var{e.138}}}~}{\;:\;}}
{\expr{\brackets{~\underline{\expr{\var{\boxed{e}.\boxed{is}}}}
{\;:\;}~\boxed{\expr{\var{e.137}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e.\boxed{ds}}}}{\;:\;}~\boxed{\expr{\Nil}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
} \\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
~\boxedNilR
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
{~~~~~~~~~~~~~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}~\boxed{\expr{\var{e.138}}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
% (* Dirty I )(* Valid )
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
{~~~~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}~\boxed{\expr{\var{e.138}}}}~{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wh2}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.136}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Gener-2
%
%
\\
The current configuration:\\
%<RigitMatch_1gg (()(e.138.inf )())> <-h.0 ;
{\small{
$\fapp{Match}{\threeargs{\Nil}{\boxed{\expr{\var{e.138}}}}{\expr{\brackets{\Nil}}}}$,
\\
%<RigitMatch_1gg ((* (Var e e2 )))((* e.137 ))h.0 > <-h.0 ;
$\fapp{Match}{\threeargs{\underline{( \var{e.ys} )}}
{\underline{\expr{{(} }}~ \var{e.137} \underline{)}}{\bullet}}$,
\\
%<Matching_c0 h.0 ((Var e e2 ))((((* (Var s sx )(Var e e1 ))(* (Var e e2 ))) '='
% ((Var s sx )(Call Append (* (Var e e1 ))(* (Var e e2 ))))))
% ((* e.138.inf )(* e.137 ))> <-h.0 ;
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~~\boxed{\expr{\var{e.138}}}~~ \underline{{):(}} \expr{\var{e.137}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$,
\\
%<EvalCall_c8 Loop ((* e.136 )
% (* Invalid s.195.inf h.0
% <Eval_o (((Var e ys )e.137 )((Var s x )s.195.inf )((Var e xs )e.138.inf ))()
% (Prog Synapse )
% >
% <Eval_o (((Var e vs )s.195.inf e.138.inf )((Var e is )e.137 )
% ((Var e ds )))((* Dirty I )(* Valid ))(Prog Synapse )
% >
% )
% <Eval_o (((Var e vs )s.195.inf e.138.inf )((Var e is )e.137 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I s.195.inf e.138.inf )((Var e is )e.137 )
% ((Var s t )wh2 )((Var e time )e.136 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.136} \underline{):(} ~\var{Invalid}~~~ \boxed{\expr{\var{s.195}}}~
~{\bullet}~~\texttt{++}~~\\
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
{~~~~~~~~~~~~~~~~~~~~}{~~~}%{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.\boxed{ys}}}}{\;:\;}
\expr{\var{e.137}}}{\;:\;}}
{\expr{\brackets{~\underline{\expr{\var{\boxed{s}.\boxed{x}}}}
{\;:\;}~\boxed{\expr{\var{s.195}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e.\boxed{xs}}}}
{\;:\;}~\boxed{\expr{\var{e.138}}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
{~~~~~~~~~~~~~~~~~~~~}{~~~}%{~~~~~~~}
\boxed{
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}{\expr{\var{s.195}}}{\;:\;}\expr{\var{e.138}}}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}
}
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
{~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}~\boxed{\expr{\var{s.195}}{\;:\;}\expr{\var{e.138}}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
% (* Dirty I )(* Valid )
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
{~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}~\boxed{\expr{\var{s.195}}{\;:\;}\expr{\var{e.138}}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wh2}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.136}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Gener-2 -- Append
\\
%Generalization without splitting of the stacks.
%Generalized restrictions: s.208.inf != s.210.inf; s.208.inf != s.211.inf; s.208.inf != s.213.inf;
% s.210.inf != s.211.inf; s.210.inf != s.213.inf; s.211.inf != s.213.inf;
%The reductions are:
%To previous: { e.138.inf <-e.202.inf ; e.137 <-e.203 ; e.136 <-e.206 ; [] <-e.207.inf ;
% vs <-s.208.inf ; e.138.inf <-e.209 ; e <-s.210.inf ; is <-s.211.inf ; e.137 <-e.212 ;
% ds <-s.213.inf ; [] <-e.214.inf ; [] <-e.215 ; e.138.inf <-e.216.inf ;
% }
%To current: { e.138.inf <-e.202.inf ; e.137 <-e.203 ; e.136 <-e.206 ; s.195.inf <-e.207.inf ;
% ys <-s.208.inf ; e.137 <-e.209 ; s <-s.210.inf ; sx <-s.211.inf ; s.195.inf <-e.212 ;
% xs <-s.213.inf ; e.138.inf <-e.214.inf ;
% <Eval_o (((Var e vs )s.195.inf e.138.inf )((Var e is )e.137 )((Var e ds )))()
% (Prog Synapse )> <-e.215 ;
% s.195.inf e.138.inf <-e.216.inf ;
% }
%\newpage
The generalized configuration:\\ % Gener-2 Append
%<RigitMatch_1gg (()(e.138.inf )())> <-h.0 ;
{\small{
$\fapp{Match}{\threeargs{\Nil}{\boxed{\expr{\var{e.202}}}}{\expr{\brackets{\Nil}}}}$,
\\
%<RigitMatch_1gg ((* (Var e e2 )))((* e.137 ))h.0 > <-h.0 ;
$\fapp{Match}{\threeargs{\underline{( \var{e.ys} )}}
{\underline{\expr{{(} }}~ \var{e.137} \underline{)}}{\bullet}}$,
\\
%<Matching_c0 h.0 ((Var e e2 ))((((* (Var s sx )(Var e e1 ))(* (Var e e2 ))) '='
% ((Var s sx )(Call Append (* (Var e e1 ))(* (Var e e2 ))))))
% ((* e.138.inf )(* e.137 ))> <-h.0 ;
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~~\boxed{\expr{\var{e.202}}}~~ \underline{{):(}} \expr{\var{e.137}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$,
\\
%<EvalCall_c8 Loop ((* e.136 )
% (* Invalid h.0
% <Eval_o (((Var e vs ) e.138.inf )((Var e is )e.137 )
% ((Var e ds )))((* Dirty I )(* Valid ))(Prog Synapse )
% >
% )
% <Eval_o (((Var e vs )e.138.inf )((Var e is )e.137 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.138.inf )((Var e is )e.137 )((Var s t )wh2 )
% ((Var e time )e.136 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.136} \underline{):(} ~\var{Invalid}~~~ \boxed{\expr{\var{e.207}}}~
~\texttt{++}~
~{\bullet}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~}%{~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.}}}\boxed{\expr{\var{s.208}}}
{\;:\;}~{\expr{\var{e.209}}}~}{\;:\;}}
{\expr{\brackets{\expr{\var{~\boxed{\expr{\var{s.210}}}\underline{.}\boxed{\expr{\var{s.211}}}}}
{\;:\;}~\boxed{\expr{\var{e.212}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e.}}}\boxed{\expr{\var{s.213}}}
{\;:\;}~\boxed{\expr{\var{e.214}}}~}}}
{\;:\;}{\Nil}} ,}\\ %-,}
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
%+}
{~)} %~)
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\texttt{++}~~ \boxed{\expr{\var{e.215}}}
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
{~~~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}~\boxed{\expr{\var{e.216}}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
% (* Dirty I )(* Valid )
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
{~~~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}~\boxed{\expr{\var{e.216}}}~}~{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wh2}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.136}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the generalized configuration Gener-2
%\newpage
\item \emph{Gener-3}: {$\expr{\var{Append}}$} %\\
{The third generalization}
is forced by the interpreted $\var{Append}$ that is directly defined.
It has happened along the recursive branch following the iteration of the protocol event $\var{wm}$. The corresponding generalized configuration $C_{g_3}$ has 14 parameters and the badness similar to $C_{g_2}$.
\noindent
The previous configuration:\\
%<RigitMatch_1gg (()(e.138.inf )())> <-h.0 ;
{\small{
$\fapp{Match}{\threeargs{\Nil}{\boxed{\expr{\var{e.138}}}}{\expr{\brackets{\Nil}}}}$,
\\
%<RigitMatch_1gg ((* (Var e e2 )))((* e.137 ))h.0 > <-h.0 ;
$\fapp{Match}{\threeargs{\underline{( \var{e.ys} )}}
{\underline{\expr{{(} }}~ \var{e.137} \underline{)}}{\bullet}}$,
\\
%<Matching_c0 h.0 ((Var e e2 ))((((* (Var s sx )(Var e e1 ))(* (Var e e2 ))) '='
% ((Var s sx )(Call Append (* (Var e e1 ))(* (Var e e2 ))))))
% ((* e.138.inf )(* e.137 ))> <-h.0 ;
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~~\boxed{\expr{\var{e.138}}}~~ \underline{{):(}} \expr{\var{e.137}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
%<EvalCall_c8 Loop ((* e.136 )
% (* Invalid h.0
% <Eval_o (((Var e vs ) e.138.inf )((Var e is )e.137 )
% ((Var e ds )))((* Dirty I )(* Valid ))(Prog Synapse )
% >
% )
% <Eval_o (((Var e vs )e.138.inf )((Var e is )e.137 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.138.inf )((Var e is )e.137 )((Var s t )wh2 )
% ((Var e time )e.136 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.136} \underline{):(} ~\var{Invalid}~~ ~\var{I}~~~ ~\boxedNilL~~
~{\bullet}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.ys}}}{\;:\;}
\expr{\var{e.137}}}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{s.x}}}
{\;:\;}~\boxed{\expr{\var{I}}}~}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.xs}}}
{\;:\;}~\boxed{\expr{\var{e.138}}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.\boxed{vs}}}}
{\;:\;}~\boxed{\var{I}{\;:\;}{\expr{\var{e.138}}}}~}{\;:\;}}
{\expr{\brackets{\;\underline{\expr{\var{\boxed{e}.\boxed{is}}}}
{\;:\;}~\boxed{\expr{\var{e.137}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e.\boxed{ds}}}}{\;:\;}~\boxed{\expr{\Nil}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
} \\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\boxedNilR
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
{~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}} {\;:\;}~\var{I}
{\;:\;}~\boxed{\expr{\var{e.138}}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
% (* Dirty I )(* Valid )
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
{~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}~\boxed{\expr{\var{e.138}}}~}~{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}
{\;:\;}\expr{\var{I}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wm}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.136}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Gener-3
%
%
\\
The current configuration:\\
%<RigitMatch_1gg (()(e.138.inf )())> <-h.0 ;
{\small{
$\fapp{Match}{\threeargs{\Nil}{\boxed{\expr{\var{e.138}}}}{\expr{\brackets{\Nil}}}}$,
\\
%<RigitMatch_1gg ((* (Var e e2 )))((* e.137 ))h.0 > <-h.0 ;
$\fapp{Match}{\threeargs{\underline{( \var{e.ys} )}}
{\underline{\expr{{(} }}~ \var{e.137} \underline{)}}{\bullet}}$,
\\
%<Matching_c0 h.0 ((Var e e2 ))((((* (Var s sx )(Var e e1 ))(* (Var e e2 ))) '='
% ((Var s sx )(Call Append (* (Var e e1 ))(* (Var e e2 ))))))
% ((* e.138.inf )(* e.137 ))> <-h.0 ;
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~~\boxed{\expr{\var{e.138}}}~~ \underline{{):(}} \expr{\var{e.137}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
%<EvalCall_c8 Loop ((* e.136 )
% (* Invalid s.195.inf h.0
% <Eval_o (((Var e ys )e.137 )((Var s x )s.195.inf )((Var e xs )e.138.inf ))()
% (Prog Synapse )
% >
% <Eval_o (((Var e vs )s.195.inf e.138.inf )((Var e is )e.137 )
% ((Var e ds )))((* Dirty I )(* Valid ))(Prog Synapse )
% >
% )
% <Eval_o (((Var e vs )s.195.inf e.138.inf )((Var e is )e.137 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I s.195.inf e.138.inf )((Var e is )e.137 )
% ((Var s t )wh2 )((Var e time )e.136 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.136} \underline{):(} ~\var{Invalid}~~ \var{I}
~~~\boxed{\expr{\var{s.240}}}~
~{\bullet}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.ys}}}{\;:\;}
\expr{\var{e.137}}}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{s.x}}}
{\;:\;}~\boxed{\expr{\var{s.240}}}~}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.xs}}}
{\;:\;}~\boxed{\expr{\var{e.138}}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
{~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.\boxed{ys}}}}{\;:\;}
~\boxed{\expr{\var{e.137}}}~}{\;:\;}}
{\expr{\brackets{\;\underline{\expr{\var{\boxed{s}.\boxed{x}}}}
{\;:\;}~\boxed{\expr{\var{I}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e.\boxed{xs}}}}
{\;:\;}~\boxed{\expr{\var{s.240}{\;:\;}\var{e.138}}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\boxed{
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}{\expr{\var{I}}}
{\;:\;}{\expr{\var{s.240}}}{\;:\;}\expr{\var{e.138}}}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}
}
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
{~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}{\expr{\var{I}}}
{\;:\;}~\boxed{\expr{\var{s.240}}{\;:\;}\expr{\var{e.138}}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
% (* Dirty I )(* Valid )
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
{~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}~\boxed{\expr{\var{s.240}}{\;:\;}\expr{\var{e.138}}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}} {\;:\;}\expr{\var{I}}
{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wm}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.136}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Gener-3 -- Append
\\
\newpage
The generalized configuration:\\ % Gener-3 Append
%Generalization without splitting of the stacks.
%Generalized restrictions: s.259.inf != s.261.inf; s.259.inf != s.262.inf; s.259.inf != s.264.inf;
% s.261.inf != s.262.inf; s.261.inf != s.264.inf; s.262.inf != s.264.inf;
%The reductions are:
%To previous: {
% e.138.inf <-e.250.inf ; e.137 <-e.251 ; e.136 <-e.254 ;
% [] <-e.255.inf ;
% I <-s.257.inf ;
% vs <-s.259.inf ; I e.138.inf <-e.260 ; e <-s.261.inf ;
% is <-s.262.inf ; e.137 <-e.263 ; ds <-s.264.inf ; [] <-e.265.inf ;
% [] <-e.266 ; e.138.inf <-e.267.inf ;
% }
%
%<RigitMatch_1gg (()(e.138.inf )())> <-h.0 ;
{\small{
$\fapp{Match}{\threeargs{\Nil}{\boxed{\expr{\var{e.250}}}}{\expr{\brackets{\Nil}}}}$,
\\
%<RigitMatch_1gg ((* (Var e e2 )))((* e.137 ))h.0 > <-h.0 ;
$\fapp{Match}{\threeargs{\underline{( \var{e.ys} )}}
{\underline{\expr{{(} }}~ \var{e.137} \underline{)}}{\bullet}}$,
\\
%<Matching_c0 h.0 ((Var e e2 ))((((* (Var s sx )(Var e e1 ))(* (Var e e2 ))) '='
% ((Var s sx )(Call Append (* (Var e e1 ))(* (Var e e2 ))))))
% ((* e.138.inf )(* e.137 ))> <-h.0 ;
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~~\boxed{\expr{\var{e.138}}}~~ \underline{{):(}} \expr{\var{e.137}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$,
\\
%<EvalCall_c8 Loop ((* e.136 )
% (* Invalid h.0
% <Eval_o (((Var e vs ) e.138.inf )((Var e is )e.137 )
% ((Var e ds )))((* Dirty I )(* Valid ))(Prog Synapse )
% >
% )
% <Eval_o (((Var e vs )e.138.inf )((Var e is )e.137 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.138.inf )((Var e is )e.137 )((Var s t )wh2 )
% ((Var e time )e.136 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.136} \underline{):(} ~\var{Invalid}~~ ~\var{I}~
~~ \boxed{\expr\var{e.255}}~~ \texttt{++}~~
~{\bullet}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.ys}}}{\;:\;}
\expr{\var{e.137}}}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{s.x}}}
{\;:\;}~\boxed{\expr{\var{s.257}}}~}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.xs}}}
{\;:\;}~\boxed{\expr{\var{e.250}}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.}}}\boxed{s.259}
{\;:\;}~\boxed{\expr{\var{e.260}}}~}{\;:\;}}
{\expr{\brackets{~\expr{\var{\boxed{s.261}\underline{.}\boxed{s.262}}}
{\;:\;}~\boxed{\expr{\var{e.137}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e.}}}\boxed{s.264}
{\;:\;}~\boxed{\expr{e.265}}~}}}
{\;:\;}{\Nil}} ,}\\ %-,}
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
%+}
{~)} %~)
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\texttt{++}~~\boxed{\expr{\var{e.266}}}
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
{~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}} {\;:\;}~\var{I}
{\;:\;}~\boxed{\expr{\var{e.267}}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
% (* Dirty I )(* Valid )
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
{~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}~\boxed{\expr{\var{e.267}}}~}~{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}
{\;:\;}\expr{\var{I}}{\;:\;}\expr{\var{e.137}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wm}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.136}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
%\\
}} % The end of the generalized configuration Gener-3
%
%
%\\
\end{enumerate}
%\newpage
\subsubsection{Folding}\label{sec:App-Folding}
In this subsection the boxed pieces of the current configurations stand for the parts to be substituted in the corresponding previous configurations, while the double boxed variables of the previous configurations are variables of the substitutions folding the current configurations. The trivial part of these substitutions may be omitted.
\begin{enumerate}
\item \emph{Folding}-1: % {$\expr{\var{Loop-1}}$} (Gener-1-{$\expr{\var{Loop}}$}): \\
The first folding action was done in the same context as the first generalization done. The only distinction consists in another action: a generated configuration was folded by the generalized configuration constructed by the first generalization.
Thus there is the only variable to be nontrivially substituted by this folding. The variable is the accumulating parameter introduced by this generalization.
%\\
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
% <RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.137 )(* Dirty )(* Valid I I e.138.inf ))h.0 > <-h.0 ;
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~ \var{e.137} \underline{){:}(\var{Dirty}~ ){:}(\expr{\var{Valid}}}~ \var{I}~ ~\boxed{\var{I}~ \var{e.138}}\;\underline{)}}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid e.137 )(* Dirty )(* Valid I I e.138.inf ))> <-h.0 ;
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~ \var{e.137}
\underline{):(\var{Dirty}~ ){:}(\expr{\var{Valid}}}~~
\var{I}~ ~\boxed{\var{I}~ \var{e.138}}\;\underline{)}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-1
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
% <RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.137 )(* Dirty )(* Valid I e.138.inf ))h.0 > <-h.0 ;
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~ \var{e.137} \underline{){:}(\var{Dirty}~ ){:}(\expr{\var{Valid}}}~ \var{I}~ ~\boxed{\boxed{\var{e.138}}}\;\underline{)}}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid e.137 )(* Dirty )(* Valid I e.138.inf ))> <-h.0 ;
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~ \var{e.137}
\underline{):(\var{Dirty}~ ){:}(\expr{\var{Valid}}}~~
\var{I}~ ~\boxed{\boxed{\var{e.138}}}\;\underline{)}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-1
\\
The substitution:\\
$\expr{\var{e.136}~:=~\var{e.136};}~~$
$\expr{\var{e.137}~:=~\var{e.137};}~~$
$\expr{\var{e.138}~:=~\var{I}~\var{:\;} \var{e.138};}~~$
%
% Reference:
%{ e.136 <-e.136 ; e.137 <-e.137 ; I e.138.inf <-e.138.inf ; } <F637 e.136 , e.137 , e.138.inf >
\\
\item \emph{Folding}-2: % {$\expr{\var{Loop-2}}$} (Gener-1-{$\expr{\var{Loop}}$},
% Folding-1-{$\expr{\var{Loop}}$}): \\
The second folding action was performed by the first generalized configuration itself. The folded configuration ends a branch following the iteration of the protocol event $\var{rm}$.
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid I e.137 )(* Dirty )(* Valid I ))h.0 > <-h.0 ;
%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\var{I}~ \var{e.137}}\; \underline{){:}(\var{Dirty}~ ){:}(\expr{\var{Valid}}}~~ \var{I}~~ \boxed{\var{\Nil}}\;\underline{)}}{\bullet}}$,
\\
%
% <Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid I e.137 )(* Dirty )(* Valid I ))> <-h.0 ;
%
%%%%%%%%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~
\boxed{\var{I}~ \var{e.137}}\;
\underline{):(\var{Dirty}~ ){:}(\expr{\var{Valid}}}~~
\var{I}~ ~\boxed{\var{\Nil}}\;\underline{)}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-2
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
% <RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.137 )(* Dirty )(* Valid I e.138.inf ))h.0 > <-h.0 ;
%%%%%%%%%%%%%%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\boxed{\var{e.137}}}\; \underline{){:}(\var{Dirty}~ ){:}(\expr{\var{Valid}}}~~ \var{I}~ ~\boxed{\boxed{\var{e.138}}}\;\underline{)}}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid e.137 )(* Dirty )(* Valid I e.138.inf ))> <-h.0 ;
%%%%%%%%%%%%%%%%%%%%%%%%%
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~ ~\boxed{\boxed{\var{e.137}}}\;
\underline{):(\var{Dirty}~ ){:}(\expr{\var{Valid}}}~~
\var{I}~ ~\boxed{\boxed{\var{e.138}}}\;\underline{)}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-2
\\
The substitution:\\
$\expr{\var{e.136}~:=~\var{e.136};}~~$
$\expr{\var{e.137}~:=~\var{I}~\var{:\;} \var{e.137};}~~$
$\expr{\var{e.138}~:=~\var{\Nil};}~~$
%
% Reference:
% { e.136 <-e.136 ; I e.137 <-e.137 ; [] <-e.138.inf ; } <F637 e.136 , e.137 , e.138.inf >
\\
\item \emph{Folding}-3: % {$\expr{\var{Loop-3}}$} (Gener-1-{$\expr{\var{Loop}}$},
% Folding-1-{$\expr{\var{Loop}}$}, Folding-2-{$\expr{\var{Loop}}$} ): \\
The third folding action was done by a regular configuration $C_1$ below.
Configuration $C_1$ is a descendant of the generalized configuration $C_{g_1}$ constructed by the first generalization.
The folded configuration ends a branch following the iteration of the protocol event $\var{wm}$. The corresponding substitution is completely trivial, i.\,e., the folded and folding configurations coincide modulo variables names.
The sub-tree rooted in $C_1$ is completely folded. Configuration $C_1$ is declared as an entry point of a residual function definition. The fist rewriting rule of this definition is an exit from a recursion returning the value $\var{True}$, while the second and third branches refer to $C_{g_1}$ and $C_1$, respectively.
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid I e.137 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\var{I}~ \var{e.137}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~~
\underline{){:}(\expr{\var{Valid}}~ )}~
}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid I e.137 )(* Dirty I )(* Valid ))> <-h.0 ;
%%%%%%%%
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~
\boxed{\var{I}~ \var{e.137}}\;
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}} ~)}~
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-3
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.137 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%%%%%%%%%%%%%%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\boxed{\var{e.137}}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~
\underline{){:}(\expr{\var{Valid}} ~)} }{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid e.137 )(* Dirty I )(* Valid ))> <-h.0 ;
%%%%%%%%%%%%%%%%%%%%%%%%%
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~
~\boxed{\boxed{\var{e.137}}}\;
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}}~ )}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-3
\\
The substitution:\\
$\expr{\var{e.136}~:=~\var{e.136};}~~$
$\expr{\var{e.137}~:=~\var{I}~\var{:\;}\var{e.137};}~~$
\\
Function $\expr{\var{F1047}( \var{e.136}, \var{e.137} )}$ has been created.
%
% Reference:
% { e.136 <-e.136 ; I e.137 <-e.137 ; } <F1047 e.136 , e.137 >
\\
%
\item \emph{Folding}-4: % {$\expr{\var{Loop-4}}$}
% (Gener-1-{$\expr{\var{Loop}}$},\\
% Folding-1-{$\expr{\var{Loop}}$}, Folding-2-{$\expr{\var{Loop}}$}, Folding-3-{$\expr{\var{Loop}}$}\\
% Gener-2
% ): \\
{The fourth folded configuration}
is a descendent of configuration $C_{g_2}$.
It was folded by the regular configuration $C_1$ used in the third folding. The corresponding substitution is quite trivial. There are two parameters in both the folded and folding configurations. The folding substitution renames the parameter corresponding to the initial unknown data $\var{e.time}$ and replaces the parameter standing for the unknown value of the $\var{Invalid}$ counter with concatenation of completely unknown data early split into three parts.
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.206 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.206}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.207.inf e.203 e.215 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%
%$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}
%\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
$\expr{\var{Match}}{(~}{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}
\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}{~,}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~}{~~~~~~~~~~~~~~}
\args{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\var{e.207}\append \var{e.203}\append \var{e.215}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~~
\underline{){:}(\expr{\var{Valid}}~ )}~
}{\bullet}{~)}$,
\\
%
% <Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.206 )(* Invalid e.207.inf e.203 e.215 )(* Dirty I )(* Valid ))> <-h.0 ;
%
%%%%%%%%
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.206}}\underline{\expr{ {):(} \var{Invalid}}}~~
\boxed{\var{e.207}\append \var{e.203}\append \var{e.215}}~
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}} ~)}~
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-4
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.137 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\boxed{\var{e.137}}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~
\underline{){:}(\expr{\var{Valid}} ~)} }{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid e.137 )(* Dirty I )(* Valid ))> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%%%%%
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~ ~\boxed{\boxed{\var{e.137}}}~
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}}~ )}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-4
\\
The substitution:\\
$\expr{\var{e.136}~:=~\var{e.136};}~~$
$\expr{\var{e.137}~:=~\var{e.207}\append\var{e.203}\append\var{e.215};}~~$
\\
%
% Reference:
% { e.206 <-e.136 ; e.207.inf e.203 e.215 <-e.137 ; } <F1047 e.136 , e.137 >
\\
%777
\item \emph{Folding}-5: % {$\expr{\var{Append}}$}-1 \\
% (Gener-1-{$\expr{\var{Loop}}$}, %\\
% Folding-1-{$\expr{\var{Loop}}$}, Folding-2-{$\expr{\var{Loop}}$}, Folding-3-{$\expr{\var{Loop}}$}\\
% Gener-2,\\
% Folding-4-{$\expr{\var{Loop}}$}
% ): \\
The fifth folded configuration
is a descendent of configuration $C_{g_2}$ and it is folded by $C_{g_2}$ as well. There are thirteen parameters occurring in $C_{g_2}$. Fife parameters are substituted with expressions containing names and/or types of some variables from the Synapse program model. One parameter is replaced with an expression including an application $\var{Eval}$ that presents a generalized environment of this program model.
The sub-tree rooted in $C_{g_2}$ is completely folded. Configuration $C_{g_2}$ is declared as an entry point of a residual function definition. The fist rewriting rule of this definition refers to $C_1$, while the seconds one refers to $C_{g_2}$, i.\,e., to itself.
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.202 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.202}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* (Var e ys )))((* e.203 ))h.0 > <-h.0 ;
%
%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\expr{\var{e.ys}}}}}}
{\underline{\expr{{(}}}~~ \var{e.203}\;
\underline{)}~}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Var e ys ))((((* (Var s sx )(Var e xs ))(* (Var e ys ))) '='
% ((Var s sx )(Call Append (* (Var e xs ))(* (Var e ys ))))))
% ((* e.202.inf )(* e.203 ))> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%
%
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~\expr{\var{e.202}}~~ \underline{{):(}} \expr{\var{e.203}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$,
\\
%
%<EvalCall_c8 Loop ((* e.206 )
% (* Invalid e.207.inf s.223.inf h.0
% <Eval_o (((Var e ys )e.203 )((Var s x )s.223.inf )
% ((Var e xs )e.202.inf ))()(Prog Synapse )
% >
% <Eval_o (((Var e s.208.inf )e.209 )((Var s.210.inf s.211.inf )e.212 )
% ((Var e s.213.inf )e.214.inf ))()(Prog Synapse )
% >
% e.215
% )
% <Eval_o (((Var e vs )e.216.inf )((Var e is )e.203 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.216.inf )((Var e is )e.203 )((Var s t )wh2 )
% ((Var e time )e.206 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%
%
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.206} \underline{):(} ~\var{Invalid}~
~~\boxed{\var{e.207}~\texttt{++}~\expr{\var{s.223}}}~\texttt{++}~
~{\bullet}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%1
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.}}\boxed{\expr{\var{ys}}}}\;}~{\;:\;}
~\boxed{\expr{\var{e.203}}}~{\;:\;}}
{\expr{\brackets{~\underline{\boxed{\expr{\var{s}}}.\boxed{\expr{\var{x}}}}
{\;:\;}~\boxed{\expr{\var{s.223}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e}}.\boxed{\expr{\var{xs}}}}
{\;:\;}~\boxed{\expr{\var{e.202}}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~~}{~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%2
%\fapp{Eval}{\args{\brackets{
\hspace{-60pt}\boxed{
%\expr{\var{Eval}(~}{{\brackets{
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.}}}\expr{\var{s.208}}{\;:\;}
~\expr{\var{e.209}}~}{\;:\;}}
{\expr{\brackets{\expr{\var{s.210}\underline{.}\expr{\var{s.211}}}
{\;:\;}\expr{\var{e.212}}~}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.}}}\expr{\var{s.213}}
{\;:\;}\expr{\var{e.214}}~}}}
{\;:\;}{\Nil}} %,}\\ %-,}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}
% {~)} %~)
% \\
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
~~\texttt{++}~~\expr{\var{e.215}}
}
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
%3
{~~~~~~~~~~~~~~~~~~~~}{~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}\expr{\var{e.216}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.203}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
% (* Dirty I )(* Valid )
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
%4 7777
{~~~~~~~~~~~~~~~~~~~~}{~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}\expr{\var{e.216}}}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}
{\;:\;}\expr{\var{e.203}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wh2}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.206}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-5
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.202 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.202}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* (Var e ys )))((* e.203 ))h.0 > <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\expr{\var{e.ys}}}}}}
{\underline{\expr{{(}}}~~ \var{e.203}\;
\underline{)}~}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Var e ys ))((((* (Var s sx )(Var e xs ))(* (Var e ys ))) '='
% ((Var s sx )(Call Append (* (Var e xs ))(* (Var e ys ))))))
% ((* e.202.inf )(* e.203 ))> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%
%
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~\expr{\var{e.202}}~ \underline{{):(}} \expr{\var{e.203}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$,
\\
%
%<EvalCall_c8 Loop ((* e.206 )
% (* Invalid e.207.inf h.0
% <Eval_o (((Var e s.208.inf )e.209 )((Var s.210.inf s.211.inf )e.212 )
% ((Var e s.213.inf )e.214.inf ))()(Prog Synapse )
% >
% e.215
% )
% <Eval_o (((Var e vs )e.216.inf )((Var e is )e.203 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.216.inf )((Var e is )e.203 )((Var s t )wh2 )
% ((Var e time )e.206 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%
%
%<EvalCall_c8 Loop ((* e.136 )
% (* Invalid h.0
% <Eval_o (((Var e vs ) e.138.inf )((Var e is )e.137 )
% ((Var e ds )))((* Dirty I )(* Valid ))(Prog Synapse )
% >
% )
% <Eval_o (((Var e vs )e.138.inf )((Var e is )e.137 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.138.inf )((Var e is )e.137 )((Var s t )wh2 )
% ((Var e time )e.136 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
%
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.206} \underline{):(} ~\var{Invalid}~~ ~\boxed{\boxed{\var{e.207}}}~
~\texttt{++}~~{\bullet}~~\texttt{++}~~\\
%1
{~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.}}}\boxed{\boxed{\expr{\var{s.208}}}}~{\;:\;}
\boxed{\boxed{\expr{\var{e.209}}}}~}{\;:\;}}
{\expr{\brackets{
~\boxed{\boxed{\expr{\var{s.210}}}}\underline{.}\boxed{\boxed{\expr{\var{s.211}}}}
{\;:\;}~\boxed{\boxed{\expr{\var{e.212}}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e.}}}\boxed{\boxed{\expr{\var{s.213}}}}
{\;:\;}~\boxed{\boxed{\expr{\var{e.214}}}}~}}}
{\;:\;}{\Nil}} ,}\\ %-,}
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
%+}
{~)} %~)
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\texttt{++}~~\boxed{\boxed{\expr{\var{e.215}}}}
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
{~~~~~~~~~~~~~~~~~~~~}{~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%2
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}~\expr{\var{e.216}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.203}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
{~~~~~~~~~~~~~~~~~~~~}{~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%3
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}~\expr{\var{e.216}}}~{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}
{\;:\;}\expr{\var{e.203}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wh2}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.206}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-5
\\
The substitution:\\
$\expr{\var{e.202}~:=~\var{e.202};}~~$ $\expr{\var{e.207}~:=~\var{e.207}~\var{s.223};}~~$
$\expr{\var{s.208}~:=~\var{ys};}~~$ $\expr{\var{e.209}~:=~\var{e.203};}~~$ \\
$\expr{\var{s.210}~:=~\var{\texttt{'}s\texttt{'}};}~~$ $\expr{\var{s.211}~:=~\var{x};}~~$
$\expr{\var{e.212}~:=~\var{s.223};}~~$ $\expr{\var{s.213}~:=~\var{xs};}~~$
$\expr{\var{e.214}~:=~\var{e.202};}~~$ \\
$\expr{\var{e.215}~:=
% <Eval_o (((Var e s.208.inf )e.209 )((Var s.210.inf s.211.inf )e.212 )
% ((Var e s.213.inf )e.214.inf ))()(Prog Synapse )> e.215 <-e.215 ;
%%%%%%%%%%
%
\expr{\var{Eval}(~}{{\brackets{
%\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.}}}\var{s.208}{\;:\;}
\expr{\var{e.209}}}{\;:\;}}
{\expr{\brackets{\expr{\var{s.210}}\underline{.}\expr{\var{s.211}}
{\;:\;}\expr{\var{e.212}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.}}}\expr{\var{s.213}}
{\;:\;}\expr{\var{e.214}}}}}
{\;:\;}{\Nil}} ,}\\ %-,}
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
%+}
{~)} %~)
}
~~\texttt{++}~~\expr{\var{e.215}};
$
\\
$\expr{\var{e.216}~:=~\var{e.216};}~~$ $\expr{\var{e.203}~:=~\var{e.203};}~~$
$\expr{\var{e.206}~:=~\var{e.206};}~~$
\\
Function \\
$\expr{\var{F1646}( \var{e.202}, \var{e.203}, \var{e.206}, \var{e.207}, \var{s.208},
\var{e.209}, \var{s.210}, \var{s.211}, \var{e.212}, \var{s.213}, \var{e.214}, \var{e.215},
\var{e.216} )}$ \\
has been created.
%
%The reduct is:
%To previous:
%{ e.202.inf <-e.202.inf ; e.207.inf s.223.inf <-e.207.inf ;
% ys <-s.208.inf ; e.203 <-e.209 ; s <-s.210.inf ; x <-s.211.inf ;
% s.223.inf <-e.212 ; xs <-s.213.inf ; e.202.inf <-e.214.inf ;
% <Eval_o (((Var e s.208.inf )e.209 )((Var s.210.inf s.211.inf )e.212 )
% ((Var e s.213.inf )e.214.inf ))()(Prog Synapse )> e.215 <-e.215 ;
% e.216.inf <-e.216.inf ; e.203 <-e.203 ; e.206 <-e.206 ;
%}
%%%%%%%%%%%%%%% ?????
% $\expr{\var{s.208}~:=~\var{s.208};}~~$ $\expr{\var{e.209}~:=~\var{e.209};}~~$
% $\expr{\var{s.210}~:=~\var{s.210};}~~$ $\expr{\var{s.211}~:=~\var{s.211};}~~$
% $\expr{\var{e.212}~:=~\var{e.212};}~~$ $\expr{\var{s.213}~:=~\var{s.213};}~~$
% $\expr{\var{e.214}~:=~\var{e.214};}~~$
%\\
% Reference:
%{ s.208.inf <-s.208.inf ; e.209 <-e.209 ;
% s.210.inf <-s.210.inf ; s.211.inf <-s.211.inf ;
% e.212 <-e.212 ; s.213.inf <-s.213.inf ; e.214.inf <-e.214.inf ;
%}
%{Begin
%<Eval_o (((Var e s.208.inf )e.209 )((Var s.210.inf s.211.inf )e.212 )((Var e s.213.inf )e.214.inf ))()(Prog Synapse )> <-h.0 ; h.0 <-e.230 ; end};
%{ e.202.inf <-e.202.inf ; e.207.inf s.223.inf <-e.207.inf ;
% ys <-s.208.inf ; e.203 <-e.209 ; s <-s.210.inf ; sx <-s.211.inf ;
% s.223.inf <-e.212 ; xs <-s.213.inf ; e.202.inf <-e.214.inf ;
% e.230 e.215 <-e.215 ; e.216.inf <-e.216.inf ; e.203 <-e.203 ; e.206 <-e.206 ;
%} <F1646 e.202.inf , e.207.inf , s.208.inf , e.209 , s.210.inf , s.211.inf , e.212 , s.213.inf , %e.214.inf , e.215 , e.216.inf , e.203 , e.206 > <-e.148 ;
\\
%
\item \emph{Folding}-6: %{$\expr{\var{Loop}}$}-5 \\
% (Gener-1-{$\expr{\var{Loop}}$}, %\\
% Folding-1-{$\expr{\var{Loop}}$}, Folding-2-{$\expr{\var{Loop}}$}, Folding-3-{$\expr{\var{Loop}}$}\\
% Gener-2,\\
% Folding-4-{$\expr{\var{Loop}}$}, Folding-5-{$\expr{\var{Append}}$}
% ): \\
{The sixth folding}
action was done by the regular configuration $C_1$ used above.
The folding substitution increases counter $\var{Invalid}$ and renames the variable corresponding to stream $\var{e.time}$.
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid I e.137 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%
%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\var{I}~ \var{e.137}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~~
\underline{){:}(\expr{\var{Valid}}~ )}~
}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid I e.137 )(* Dirty I )(* Valid ))> <-h.0 ;
%
%%%%%%%%
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~
\boxed{\var{I}~ \var{e.137}}~
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}} ~)}~
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-6
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.136}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.137 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\boxed{\var{e.137}}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~
\underline{){:}(\expr{\var{Valid}} ~)} }{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid e.137 )(* Dirty I )(* Valid ))> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%%%%%
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~ ~\boxed{\boxed{\var{e.137}}}~
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}}~ )}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-6
\\
The substitution:\\
$\expr{\var{e.136}~:=~\var{e.136};}~~$
$\expr{\var{e.137}~:=~\var{I}~\var{:}\; \var{e.137};}~~$
\\
%
% Reference:
% { e.136 <-e.136 ; I e.137 <-e.137 ; } <F1047 e.136 , e.137 >
\\
\item \emph{Folding}-7: %{$\expr{\var{Loop}}$}-6 \\
% (Gener-1-{$\expr{\var{Loop}}$}, %\\
% Folding-1-{$\expr{\var{Loop}}$}, Folding-2-{$\expr{\var{Loop}}$}, Folding-3-{$\expr{\var{Loop}}$}\\
% Gener-2,\\
% Folding-4-{$\expr{\var{Loop}}$}, Folding-5-{$\expr{\var{Append}}$},
% Folding-6-{$\expr{\var{Loop}}$},\\
% Gener-3,\\
% ): \\
{The seventh folding}
action was done in a similar context as the fourth one done. The only distinction consists in increasing the $\var{Invalid}$ counter by a constant.
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.254 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{~\boxed{\expr{\var{e.254}}}~}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid I e.255.inf e.251 e.266 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%
%
$\expr{\var{Match}}{(~}{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}
\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}{~,}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~}{~~~~~~~~~~~}
\args{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\var{I}~
\var{e.255}\append\var{e.251}\append\var{e.266}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~~
\underline{){:}(\expr{\var{Valid}}~ )}~
}{\bullet}{~)}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.254 )(* Invalid I e.255.inf e.251 e.266 )(* Dirty I )(* Valid ))> <-h.0 ;
%
%%%%%%%%
%
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~
\boxed{\var{I}~ \var{e.255}\append\var{e.251}\append\var{e.266}}~
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}} ~)}~
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-7
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\boxed{\boxed{\expr{\var{e.136}}}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.137 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\boxed{\var{e.137}}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~
\underline{){:}(\expr{\var{Valid}} ~)} }{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid e.137 )(* Dirty I )(* Valid ))> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%%%%%
%
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~ ~\boxed{\boxed{\var{e.137}}}~
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}}~ )}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-7
\\
The substitution:\\
$\expr{\var{e.254}~:=~\var{e.136};}~~$
$\expr{\var{e.137}~:=~\var{I}~\var{:}\; \var{e.255}\append\var{e.251}\append\var{e.266};}~~$
\\
%
% Reference:
% { e.254 <-e.136 ; I e.255.inf e.251 e.266 <-e.137 ; } <F1047 e.136 , e.137 >
\\
\item \emph{Folding}-8: %{$\expr{\var{Append}}$}-2 \\
% (Gener-1-{$\expr{\var{Loop}}$}, %\\
% Folding-1-{$\expr{\var{Loop}}$}, Folding-2-{$\expr{\var{Loop}}$}, Folding-3-{$\expr{\var{Loop}}$}, %\\
% Gener-2,%\\
% Folding-4-{$\expr{\var{Loop}}$}, Folding-5-{$\expr{\var{Append}}$},
% Folding-6-{$\expr{\var{Loop}}$},%\\
% Gener-3, %\\
% Folding-7-{$\expr{\var{Loop}}$},
% ): \\
{The eighth folded configuration}
is a descendent of configuration $C_{g_3}$ and it is folded by $C_{g_3}$ as well. The corresponding folding substitution has the badness similar to the fifth folding substitution.
The sub-tree rooted in $C_{g_3}$ is completely folded. Configuration $C_{g_3}$ is declared as an entry point of a residual function definition. The fist rewriting rule of this definition refers to $C_1$, while the seconds one refers to $C_{g_3}$, i.\,e., to itself.
That in its turn allows us to fold the sub-tree rooted in the first generalized configuration $C_{g_1}$. Configuration $C_{g_1}$ is declared as an entry point of a residual function definition. The fist rewriting rule of this definition is an exit from a recursion returning the value $\var{True}$. The second rewriting rule calls this entry point $C_{g_1}$, while the third and fourth branches refer to $C_{g_2}$ and $C_{g_3}$, respectively.
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.250 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.250}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* (Var e ys )))((* e.251 ))h.0 > <-h.0 ;
%
%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\expr{\var{e.ys}}}}}}
{\underline{\expr{{(}}}~~ \var{e.251}\;
\underline{)}~}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Var e ys ))((((* (Var s sx )(Var e xs ))(* (Var e ys ))) '='
% ((Var s sx )(Call Append (* (Var e xs ))(* (Var e ys ))))))
% ((* e.250.inf )(* e.251 ))> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%
%
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~\expr{\var{e.250}}~~ \underline{{):(}} \expr{\var{e.251}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$,
\\
%
%<EvalCall_c8 Loop ((* e.254 )
% (* Invalid I e.255.inf s.274.inf h.0
% <Eval_o (((Var e ys )e.251 )((Var s x )s.274.inf )
% ((Var e xs )e.250.inf ))()(Prog Synapse )
% >
% <Eval_o (((Var e ys )e.251 )((Var s sx )s.257.inf )
% ((Var e xs )s.274.inf e.250.inf ))()(Prog Synapse )>
% <Eval_o (((Var e s.259.inf )e.260 )((Var s.261.inf s.262.inf )e.263 )
% ((Var e s.264.inf )e.265.inf ))()(Prog Synapse )>
% e.266
% )
% <Eval_o (((Var e vs )I e.267.inf )((Var e is )e.251 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.267.inf )((Var e is )I e.251 )((Var s t )wm )
% ((Var e time )e.254 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%
%
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.254} \underline{):(} ~\var{Invalid}~~ \expr{\var{I}}~{:}
~~\boxed{\var{e.255}\append\expr{\var{s.274}}}\append
~{\bullet}~~\texttt{++}~~\\
{~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%1
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.ys}}}~{\;:\;}
~\boxed{\expr{\var{e.251}}}~{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{s.x}}}
{\;:\;}~\boxed{\expr{\var{s.274}}}~}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.xs}}}}
{\;:\;}\expr{\var{e.250}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
{~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%2
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.}}\boxed{\expr{\var{ys}}}}\;}~{\;:\;}
~\boxed{\expr{\var{e.251}}}~{\;:\;}}
{\expr{\brackets{~\underline{\boxed{\expr{\var{s}}}.\boxed{\expr{\var{x}}}}
{\;:\;}~\boxed{\expr{\var{s.257}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e}}.\boxed{\expr{\var{xs}}}}
{\;:\;}~\boxed{\expr{\var{s.274}}~\expr{\var{e.250}}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%3
%\fapp{Eval}{\args{\brackets{
\hspace{-60pt}\boxed{
%\expr{\var{Eval}(~}{{\brackets{
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.}}}\expr{\var{s.259}}{\;:\;}
~\expr{\var{e.260}}~}{\;:\;}}
{\expr{\brackets{\expr{\var{s.261}\underline{.}\expr{\var{s.262}}}
{\;:\;}\expr{\var{e.263}}~}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.}}}\expr{\var{s.264}}
{\;:\;}\expr{\var{e.265}}~}}}
{\;:\;}{\Nil}} %,}\\ %-,}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}
% {~)} %~)
% \\
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
~~\texttt{++}~~\expr{\var{266}}
}
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
%4
{~~~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}\expr{\var{I}}{\;:\;}\expr{\var{e.267}}}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}
{\;:\;}\expr{\var{e.251}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
% (* Dirty I )(* Valid )
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
%5
{~~~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}\expr{\var{I}}{\;:\;}\expr{\var{e.267}}}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}
{\;:\;}\expr{\var{I}}{\;:\;}\expr{\var{e.251}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wm}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.254}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-8
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.250 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\expr{\var{e.250}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* (Var e ys )))((* e.251 ))h.0 > <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\expr{\var{e.ys}}}}}}
{\underline{\expr{{(}}}~~ \var{e.251}\;
\underline{)}~}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Var e ys ))((((* (Var s sx )(Var e xs ))(* (Var e ys ))) '='
% ((Var s sx )(Call Append (* (Var e xs ))(* (Var e ys ))))))
% ((* e.250.inf )(* e.251 ))> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%
%
$\expr{\var{Matching}}(~\bullet,~\underline{\expr{\var{e.ys}}},
~\underline{\ldots~\text{The 2-nd}~\var{Append}~\text{rule}~\ldots}\;,~
\underline{\expr{(}} ~\expr{\var{e.250}}~ \underline{{):(}} \expr{\var{e.251}~} \underline{{)}}
~)$,
\\
%<Eval_o h.0 (Prog Synapse )> <-h.0 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$,
\\
%
%<EvalCall_c8 Loop ((* e.254 )
% (* Invalid I e.255.inf h.0
% <Eval_o (((Var e ys )e.251 )((Var s sx )s.257.inf )
% ((Var e xs )e.250.inf ))()(Prog Synapse )
% >
% <Eval_o (((Var e s.259.inf )e.260 )((Var s.261.inf s.262.inf )e.263 )
% ((Var e s.264.inf )e.265.inf ))()(Prog Synapse )
% >
% e.266
% )
% <Eval_o (((Var e vs )I e.267.inf )((Var e is )e.251 )((Var e ds )))
% ((* Dirty I )(* Valid ))(Prog Synapse )>
% <Eval_o (((Var e vs )I e.267.inf )((Var e is )I e.251 )((Var s t )wm )
% ((Var e time )e.254 )((Var e ds )))()(Prog Synapse )>
% )(Prog Synapse )> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%
%
$\fapp{EvalCall}{\threeargs{\var{Loop}}
{\underline{\expr{{(} }}~ \var{e.254} \underline{):(} ~\var{Invalid}~~ \expr{\var{I}}~{:\;}
~\boxed{\boxed{\var{e.255}}}\append
~{\bullet}~\append~\\
{~~~~~~~~}{~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%1
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.ys}}}}~{\;:\;}
~\boxed{\expr{\var{e.251}}}~{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{s.x}}}
{\;:\;}~\boxed{\boxed{\expr{\var{s.257}}}}~}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.xs}}}
{\;:\;}\expr{\var{e.250}}~}}}
{\;:\;}{\Nil}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~\\
%2
{~~~~~~~~}{~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\;\underline{\expr{\var{e.}}}\boxed{\boxed{\expr{\var{s.259}}}}~{\;:\;}
\boxed{\boxed{\expr{\var{e.260}}}}\;}{\;:\;}}
{\expr{\brackets{~
\boxed{\boxed{\expr{\var{s.261}}}}\underline{.}\boxed{\boxed{\expr{\var{s.262}}}}
{\;:\;}~\boxed{\boxed{\expr{\var{e.263}}}}~}}}{\;:\;}
\expr{\brackets{\;\underline{\expr{\var{e.}}}\boxed{\boxed{\expr{\var{s.264}}}}
{\;:\;}~\boxed{\boxed{\expr{\var{e.265}}}}~}}}
{\;:\;}{\Nil}} ,}\\ %-,}
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
%+}
{~)} %~)
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
\texttt{++}~~\boxed{\boxed{\expr{\var{e.266}}}}
\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
\underline{)} {\;:\;} \\
{~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%3
\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}
{\;:\;}\expr{\var{I}}~{\;:\;}~\expr{\var{e.267}}~}{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{e.251}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}\underline{\expr{\brackets{\expr{\var{Dirty}~\var{I}}}}{\;:\;}
\expr{\brackets{\expr{\var{Valid}~}}}
}}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
}~~\texttt{++}~~
\\
{~~~~~~~~~~~~~~~~}
%{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~}
%4
%\fapp{Eval}{\args{\brackets{
\expr{\var{Eval}(~}{{\brackets{
\expr{\brackets{\underline{\expr{\var{e.vs}}}{\;:\;}\expr{\var{I}}
{\;:\;}~\expr{\var{e.267}}}~{\;:\;}}
{\expr{\brackets{\underline{\expr{\var{e.is}}}{\;:\;}\expr{\var{I}}
{\;:\;}\expr{\var{e.251}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{s.t}}}{\;:\;}\expr{\var{wm}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.time}}}{\;:\;}\expr{\var{e.254}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.ds}}}{\;:\;}\expr{\Nil}}}
}
{\;:\;}{\Nil},}
}\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~~~~}{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}{~)}}
%\\
} % , -- comma
{~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
\\
{}}$,
%
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-8
\\
The substitution:\\
$\expr{\var{e.255}~:=~\var{e.255}\append\var{s.274};}~~$ $\expr{\var{s.257}~:=~\var{s.274};}~~$
$\expr{\var{e.250}~:=~\var{e.250};}~~$ $\expr{\var{s.259}~:=~\var{ys};}~~$ \\
$\expr{\var{e.260}~:=~\var{e.251};}~~$ $\expr{\var{s.261}~:=~\var{\texttt{'}s\texttt{'}};}~~$
$\expr{\var{s.262}~:=~\var{x};}~~$ $\expr{\var{e.263}~:=~\var{s.257};}~~$ \\
$\expr{\var{s.264}~:=~\var{xs};}~~$
$\expr{\var{e.265}~:=~\var{s.274}~\var{e.250};}~~$
\\
$\expr{\var{e.266}~:=
\expr{\var{Eval}(~}{{\brackets{
%\fapp{Eval}{\args{\brackets{
\expr{\brackets{\underline{\expr{\var{e.}}}\var{s.259}{\;:\;}
\expr{\var{e.260}}}{\;:\;}}
{\expr{\brackets{\expr{\var{s.261}}\underline{.}\expr{\var{s.262}}
{\;:\;}\expr{\var{e.263}}}}}{\;:\;}
\expr{\brackets{\underline{\expr{\var{e.}}}\expr{\var{s.264}}
{\;:\;}\expr{\var{e.265}}}}}
{\;:\;}{\Nil}} ,}\\ %-,}
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~}
{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}
%+}
{~)} %~)
}
~~\texttt{++}~~\expr{\var{e.266}};
$
\\
$\expr{\var{e.267}~:=~\var{e.267};}~~$ $\expr{\var{e.251}~:=~\var{e.251};}~~$
$\expr{\var{e.254}~:=~\var{e.254};}~~$
\\
\\
Function \\
$\expr{\var{F1959}(
\var{e.249}, \var{e.250}, \var{e.253}, \var{e.254}, \var{s.256}, \var{s.258},
\var{e.259}, \var{s.260}, \var{s.261}, \var{e.262},\\
{~~~~~~~~~~~~~~~~~~~~}{~~~~~~}{~~~~~~}{~~~~~~}{~~~~~~}{~~~~~~}{~~~~~~}{~~~~~~}{~~~~~~}{~~~~~~}{~}
\var{s.263}, \var{e.264}, \var{e.265}, \var{e.266}
)}$ has been created.
\\
Function $\expr{\var{F637}(
\var{e.136}, \var{e.137}, \var{e.138}
)}$ has been created.
%
%The reduct is:
%To previous:
%{ e.255.inf s.274.inf <-e.255.inf ; s.274.inf <-s.257.inf ; e.250.inf <-e.250.inf ;
% ys <-s.259.inf ; e.251 <-e.260 ; s <-s.261.inf ; x <-s.262.inf ; s.257.inf <-e.263 ;
% xs <-s.264.inf ; s.274.inf e.250.inf <-e.265.inf ;
% <Eval_o (((Var e s.259.inf )e.260 )((Var s.261.inf s.262.inf )e.263 )
% ((Var e s.264.inf )e.265.inf ))()(Prog Synapse )> e.266 <-e.266 ;
% e.267.inf <-e.267.inf ; e.251 <-e.251 ; e.254 <-e.254 ;
%}
%%%%%%%%%%%%%%%
%\\
% Reference:
%{ s.259.inf <-s.259.inf ; e.260 <-e.260 ; s.261.inf <-s.261.inf ;
% s.262.inf <-s.262.inf ; e.263 <-e.263 ; s.264.inf <-s.264.inf ;
% e.265.inf <-e.265.inf ;
%}
%{Begin
% <Eval_o (((Var e s.259.inf )e.260 )((Var s.261.inf s.262.inf )e.263 )
% ((Var e s.264.inf )e.265.inf ))()(Prog Synapse )> <-h.0 ;
% h.0 <-e.284 ;
%end};
%{ e.255.inf s.274.inf <-e.255.inf ; s.274.inf <-s.257.inf ; e.250.inf <-e.250.inf ;
% ys <-s.259.inf ; e.251 <-e.260 ; s <-s.261.inf ; x <-s.262.inf ; s.257.inf <-e.263 ;
% xs <-s.264.inf ; s.274.inf e.250.inf <-e.265.inf ; e.284 e.266 <-e.266 ;
% e.267.inf <-e.267.inf ; e.251 <-e.251 ; e.254 <-e.254 ; }
% <F1959 e.255.inf , s.257.inf , e.250.inf , s.259.inf , e.260 ,
% s.261.inf , s.262.inf , e.263 , s.264.inf , e.265.inf ,
% e.266 , e.267.inf , e.251 , e.254
% > <-e.148 ;
\\
\item \emph{Folding}-9: %{$\expr{\var{Loop}}$}-7 \\
% (Gener-1-{$\expr{\var{Loop}}$}, %\\
% Folding-1-{$\expr{\var{Loop}}$}, Folding-2-{$\expr{\var{Loop}}$}, Folding-3-{$\expr{\var{Loop}}$}, %\\
% Gener-2, %\\
% Folding-4-{$\expr{\var{Loop}}$}, Folding-5-{$\expr{\var{Append}}$},
% Folding-6-{$\expr{\var{Loop}}$}, %\\
% Gener-3, %\\
% Folding-7-{$\expr{\var{Loop}}$}, Folding-8-{$\expr{\var{Append}}$}
% ): \\
The last folded configuration belongs to the last branch originating from the initial configuration. It is folded by the regular configuration $C_1$, which belongs to a parallel path and was used in the third folding.
\noindent
The current configuration:\\
{\small{
% <RigitMatch_1gg (()(e.101 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{~\boxed{\expr{\var{e.101}}}~}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.102 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%
%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\var{e.102}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~~
\underline{){:}(\expr{\var{Valid}}~ )}~
}{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.101 )(* Invalid e.102 )(* Dirty I )(* Valid ))> <-h.0 ;
%
%%%%%%%%
%
%$\fapp{Matching}{\args{\threeargs{\bullet}
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.101}}\underline{\expr{ {):(} \var{Invalid}}}~~
\boxed{\var{e.102}}~
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}} ~)}~
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the current configuration Folding-9
\\
To the previous configuration:\\
{\small{
% <RigitMatch_1gg (()(e.136 )())> <-h.0 ;
$\fapp{Match}{\threeargs{\var{\Nil}}{\boxed{\boxed{\expr{\var{e.136}}}}}{\expr{\brackets{\var{\Nil}}}}}$,
\\
%
%<RigitMatch_1gg ((* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))
% ((* Invalid e.137 )(* Dirty I )(* Valid ))h.0 > <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%
$\fapp{Match}{\threeargs{\underline{\expr{\brackets{\var{Invalid}~\expr{\var{e.is}}}}{\;:\;}\expr{\brackets{\var{Dirty}~\expr{\var{e.ds}}}}{\;:\;}\expr{\brackets{\expr{\var{Valid}}~ \expr{\var{e.vs}}}}}}
{\underline{\expr{{(} \var{Invalid}}}~~ \boxed{\boxed{\var{e.137}}}\;
\underline{){:}(\expr{\var{Dirty}}}~ ~\var{I}~
\underline{){:}(\expr{\var{Valid}} ~)} }{\bullet}}$,
\\
%
%<Matching_c0 h.0 ((Call Test (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs ))))
% ((((* (Var s t )(Var e time ))(* Invalid (Var e is ))
% (* Dirty (Var e ds ))(* Valid (Var e vs )))
% '=' ((Call Loop (* (Var e time ))(Call Event (Var s t )
% (* Invalid (Var e is ))(* Dirty (Var e ds ))(* Valid (Var e vs )))))))
% ((* e.136 )(* Invalid e.137 )(* Dirty I )(* Valid ))> <-h.0 ;
%
%%%%%%%%%%%%%%%%%%%%%%%%%
%
$\expr{\var{Matching}}{(~}{\args{\threeargs{\bullet}
{\underline{\fapp{Test}{\brackets{\var{Invalid}~\var{e.is}}{:}\brackets{\var{Dirty}~\var{e.ds}}{:}\brackets{\var{Valid}~\var{e.vs}}}{}}}
{~\underline{\ldots~\text{The 2-nd}~\var{Loop}~\text{rule}~\ldots}\;}}{}}$
\\
$
{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}{~~~~~~~~~~~~~~~~~}
\underline{(\;}\expr{\var{e.136}}\underline{\expr{ {):(} \var{Invalid}}}~~ ~\boxed{\boxed{\var{e.137}}}~
\underline{):(\expr{\var{Dirty}}}~~ \var{I}~
\underline{){:}(\expr{\var{Valid}}~ )}
{~~)}$, %Matching(...)
\\
%
%
%<Eval_o h.0 (Prog Synapse )> <-h.0 ; h.0 <-e.148 ;
$\fapp{Eval}{\args{\bullet}{\expr{\brackets{\var{Prog}~ \var{Synapse}}}}}$
\\
}} % The end of the previous configuration Folding-8
\\
The substitution:\\
$\expr{\var{e.136}~:=~\var{e.101};}~~$
$\expr{\var{e.137}~:=~\var{e.102};}~~$
\\
%
% Reference:
% { e.101 <-e.136 ; e.102 <-e.137 ; } <F1047 e.136 , e.137 >
%\\
% \item
\end{enumerate}
\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{10}
\bibitem{AhmedLisitsaNemytykh:NSPK}
A.~Ahmed, A.P. Lisitsa, and A.P. Nemytykh.
\newblock Cryptographic protocol verification via supercompilation ({A} case
study).
\newblock In {\em VPT 2013}, volume~16 of {\em EPiC Series}, pages 16--29.
EasyChair, 2013.
\bibitem{FioPettProSen:Ver-IterSpec14}
De~E. Angelis, F.~Fioravanti, A.~Pettorossi, and M.~Proietti.
\newblock Program verification via iterated specialization.
\newblock {\em Science of Computer Programming}, 95 / {Selected} and extended
papers from Partial Evaluation and Program Manipulation 2013(Part
2):149--175, 2014.
\newblock
doi:{\href{http://dx.doi.org/10.1016/j.scico.2014.05.017}{10.1016/j.scico.2014.05.017}}.
\bibitem{VeriMAP:2014}
De~E. Angelis, F.~Fioravanti, A.~Pettorossi, and M.~Proietti.
\newblock Verimap: A tool for verifying programs through transformations.
\newblock In {\em Proc. of ({TACAS} 2014)}, volume 8413 of {\em LNCS}, pages
568--574. Springer, 2014.
\newblock
doi:{\href{http://dx.doi.org/10.1007/978-3-642-54862-8_47}{10.1007/978-3-642-54862-8\_47}}.
\bibitem{FioPettProSen:Ver-Linear-Fib15}
De~E. Angelis, F.~Fioravanti, A.~Pettorossi, and M.~Proietti.
\newblock Proving correctness of imperative programs by linearizing constrained
{Horn} clauses.
\newblock {\em Theory and Practice of Logic Programming}, 15 / 31st
{International} Conference on Logic Programming(4--5):635--650, July 2015.
\newblock
doi:{\href{http://dx.doi.org/10.1017/S1471068415000289}{10.1017/S1471068415000289}}.
\bibitem{Delzanno:Automatic}
G.~Delzanno.
\newblock Automatic verification of cache coherence protocols via
infinite-state constraint-based model checking.
\newblock [online].
\newblock \url{http://www.disi.unige.it/person/DelzannoG/protocol.html}.
\bibitem{Delzanno-Param:00}
G.~Delzanno.
\newblock Automatic verification of parameterized cache coherence protocols.
\newblock In {\em The {Proc.} of the 12th {Int.} {Conference} on {Computer}
Aided Verification}, volume 1855 of {\em LNCS}, pages 53--68, 2000.
\bibitem{Delzanno-Futurebus:00}
G.~Delzanno.
\newblock Verification of consistency protocols via infinite-state symbolic
model checking, {A} case study: the {IEEE} {Futurebus+} protocol.
\newblock In {\em The {Proc.} of {FORTE/PSTV}}, pages 171--186. Springer US,
2000.
\bibitem{Esparza:1999}
J.~Esparza, A.~Finkel, and R.~Mayr.
\newblock On the verification of broadcast protocols.
\newblock In {\em Logic in {Computer} {Science}, 1999. {Proceedings}. 14th
{Symposium} on}, pages 352--359. IEEE, 1999.
\bibitem{FioPettPro:01}
F.~Fioravanti, A.~Pettorossi, and M.~Proietti.
\newblock Verifying {CTL} properties of infinite state systems by specializing
constraint logic programs.
\newblock In {\em the Proc. of {VCL}01}, volume DSSE-TR-2001-3 of {\em Tech.
Rep.}, pages 85--96, UK, 2001. University of Southampton.
\bibitem{FioPettProSen:GenVer13}
F.~Fioravanti, A.~Pettorossi, M.~Proietti, and V.~Senni.
\newblock Generalization strategies for the verification of infinite state
systems.
\newblock In W.~Faber and N.~Leone, editors, {\em Theory and Practice of Logic
Programming}, volume 13 / {Special} Issue 02 (25th {GULP} annual conference),
pages 175--199. Cambridge University Press, March 2013.
\bibitem{Futamura:1971}
Y.~Futamura.
\newblock Partial evaluation of computing process an approach to a
compiler-compiler.
\newblock {\em Systems, Computers, Controls}, 2(5):45--50, 1971.
\bibitem{GH:1998}
J.~P. Gallagher, J.~C. Peralta, and H.~Saglam.
\newblock Analysis of imperative programs through analysis of constraint logic
programs.
\newblock In B.~Demoen and V.~Lifschitz, editors, {\em SAS 1998}, volume 1503
of {\em LNCS}, pages 246--261. Springer, 1998.
\newblock
doi:{\href{http://dx.doi.org/10.1007/978-3-540-27775-0_3}{10.1007/978-3-540-27775-0\_3}}.
\bibitem{Hamilton:VPT2015}
G.~W. Hamilton.
\newblock Verifying temporal properties of reactive systems by transformation.
\newblock {\em Electronic Proceedings in Theoretical Computer Science},
199:33--49, 2015.
\newblock
doi:{\href{http://dx.doi.org/10.4204/EPTCS.199.3}{10.4204/EPTCS.199.3}}.
\bibitem{Hamilton:VPT2016}
G.~W. Hamilton.
\newblock Generating counterexamples for model checking by transformation.
\newblock {\em Electronic Proceedings in Theoretical Computer Science},
216:65--82, 2016.
\newblock doi:{\href{
http://dx.doi.org/10.4204/EPTCS.216.4}{10.4204/EPTCS.216.4}}.
\bibitem{Higman}
G.~Higman.
\newblock Ordering by divisibility in abstract algebras.
\newblock {\em Proc. London Math. Soc.}, 2(7):326--336, 1952.
\bibitem{Jones:Complex}
N.~D. Jones.
\newblock {\em Computability and Complexity from a Programming Perspective}.
\newblock The MIT Press, 2000.
\bibitem{Jones:IntSpecialisation}
N.~D. Jones.
\newblock Transformation by interpreter specialisation.
\newblock {\em Science of Computer Programming}, 52:307--339, 2004.
\newblock
doi:{\href{http://dx.doi.org/10.1016/j.scico.2004.03.010}{10.1016/j.scico.2004.03.010}}.
\bibitem{Jonsson_Nordlander}
P.~A. Jonsson and J.~Nordlander.
\newblock Positive supercompilation for a higher order call-by-value language.
\newblock {\em ACM {SIGPLAN} {Notices}}, 44(1):277--288, 2009.
\newblock
doi:{\href{http://doi.acm.org/10.1145/1480881.1480916}{10.1145/1480881.1480916}}.
\bibitem{Klimov:PetriNets12}
A.~V. Klimov.
\newblock Solving coverability problem for monotonic counter systems by
supercompilation.
\newblock In {\em the Proc. of PSI'11}, volume 7162 of {\em LNCS}, pages
193--209, 2012.
\newblock
doi:{\href{http://dx.doi.org/10.1007/978-3-642-29709-0_18}{10.1007/978-3-642-29709-0\_18}}.
\bibitem{Klyuchnikov:HOSC}
I.~Klyuchnikov.
\newblock Supercompiler {HOSC} 1.5: homeomorphic embedding and generalization
in a higher-order setting.
\newblock Technical Report~62, Keldysh Institute of Applied Mathematics,
Moscow, 2010.
\bibitem{Kruskal}
J.~B. Kruskal.
\newblock Well-quasi-ordering, the tree theorem, and {Vazsonyi's} conjecture.
\newblock {\em Trans. Amer. Math. Society}, 95:210--225, March 1960.
\newblock
doi:{\href{http://dx.doi.org/10.1090/S0002-9947-1960-0111704-1}{10.1090/S0002-9947-1960-0111704-1}}.
\bibitem{Leuschel:04}
H.~Lehmann and M.~Leuschel.
\newblock Inductive theorem proving by program specialisation: Generating
proofs for {Isabelle} using {Ecce}.
\newblock In {\em Proceedings of {LOPSTR03}}, volume 3018 of {\em LNCS}, pages
1--19, 2004.
\newblock
doi:{\href{http://dx.doi.org/10.1007/978-3-540-25938-1_1}{10.1007/978-3-540-25938-1\_1}}.
\bibitem{Leuschel:98}
M.~Leuschel.
\newblock On the power of homeomorphic embedding for online termination.
\newblock In {\em Proc. of the {SAS'98}}, volume 1503 of {\em LNCS}, pages
230--245, 1998.
\bibitem{Lis_Nem:CSR07}
A.~P. Lisitsa and A.~P. Nemytykh.
\newblock A note on specialization of interpreters.
\newblock In {\em The 2-nd International Symposium on Computer Science in
Russia (CSR-2007)}, volume 4649 of {\em LNCS}, pages 237--248, 2007.
\bibitem{Lis_Nem:Programming}
A.~P. Lisitsa and A.~P. Nemytykh.
\newblock Verification as parameterized testing ({Experiments} with the {SCP4}
supercompiler).
\newblock {\em Programmirovanie, (In {Russian})}, 1:22--34, 2007.
\newblock English translation in \emph{J. Programming and Computer Software},
Vol. {\bfseries 33}, No.1, pp: 14--23, 2007.
\bibitem{Lis_Nem:Protocols07}
A.~P. Lisitsa and A.~P. Nemytykh.
\newblock Experiments on verification via supercompilation.
\newblock [online], 2007--2009.
\newblock \url{http://refal.botik.ru/protocols/}.
\bibitem{Lis_Nem:IJFCS08}
A.~P. Lisitsa and A.~P. Nemytykh.
\newblock Reachability analysis in verification via supercompilation.
\newblock {\em International Journal of Foundations of Computer Science},
19(4):953--970, August 2008.
\bibitem{N:03}
A.~P. Nemytykh.
\newblock The supercompiler {SCP4}: General structure. (extended abstract).
\newblock In {\em the Proc. of PSI'03}, volume 2890 of {\em LNCS}, pages
162--170, 2003.
\newblock
doi:{\href{http://dx.doi.org/10.1007/978-3-540-39866-0_18}{10.1007/978-3-540-39866-0\_18}}.
\bibitem{Nemytykh:SCP4book}
A.~P. Nemytykh.
\newblock {\em The Supercompiler {SCP4}: General Structure}.
\newblock URSS, Moscow, 2007.
\newblock (Book in {Russian}).
\bibitem{Nem_Pin_Tur}
A.~P. Nemytykh, V.~A. Pinchuk, and V.~F. Turchin.
\newblock A self-applicable supercompiler.
\newblock In {\em PEPM'96}, volume 1110 of {\em LNCS}, pages 322--337.
Springer-Verlag, 1996.
\bibitem{NT:00}
A.~P. Nemytykh and V.~F. Turchin.
\newblock The supercompiler {SCP4}: Sources, on-line demonstration.
\newblock [online], 2000.
\newblock \url{http://www.botik.ru/pub/local/scp/refal5/}.
\bibitem{ANepeivoda:PingPong}
Antonina Nepeivoda.
\newblock Ping-pong protocols as prefix grammars and {Turchin} relation.
\newblock In {\em VPT 2013}, volume~16 of {\em EPiC Series}, pages 74--87.
EasyChair, 2013.
\bibitem{AntoninaNepeivoda:Sbornik2014}
Antonina Nepeivoda.
\newblock Turchin's relation and loop approximation in program analysis.
\newblock {\em Proceedings on the Functional Language Refal (in Russian)},
1:170--192, 2014.
\newblock ISBN:978-5-9905410-1-6, available at
{\href{http://refal.botik.ru/library/refal2014_issue-I.pdf}{http://refal.botik.ru/library/refal2014\_issue-I.pdf}}.
\bibitem{AntoninaNepeivoda:VPT2016}
Antonina Nepeivoda.
\newblock Turchin's relation for call-by-name computations: {A} formal
approach.
\newblock {\em Electronic Proceedings in Theoretical Computer Science},
216:137--159, 2016.
\newblock
doi:{\href{http://dx.doi.org/10.4204/EPTCS.216.8}{10.4204/EPTCS.216.8}}.
\bibitem{Roychoudhury:2004}
A.~Roychoudhury and I.~V. Ramakrishnan.
\newblock Inductively verifying invariant properties of parameterized systems.
\newblock {\em Automated Software Engineering}, 11(2):101--139, 2004.
\bibitem{SGJ:96}
M.~H. S{\o}rensen, R.~Gl\"{u}ck, and N.~D. Jones.
\newblock A positive supercompiler.
\newblock {\em Journal of Functional Programming}, 6(6):811--838, 1996.
\bibitem{Turchin:Report20}
V.~F. Turchin.
\newblock The language {Refal} \--- the theory of compilation and metasystem
analysis.
\newblock Technical Report~20, Courant Institute of Mathematical Sciences, New
York University, February 1980.
\bibitem{Tur:86}
V.~F. Turchin.
\newblock The concept of a supercompiler.
\newblock {\em ACM Transactions on Programming Languages and Systems},
8(3):292--325, 1986.
\newblock doi:\href{http://doi.acm.org/10.1145/5956.5957}{10.1145/5956.5957}.
\bibitem{Turchin:Generalization88}
V.~F. Turchin.
\newblock The algorithm of generalization in the supercompiler.
\newblock In {\em Proc. of the IFIP TC2 Workshop, Partial Evaluation and Mixed
Computation}, pages 531--549. North-Holland Publishing Co., 1988.
\bibitem{Turchin:Refal5}
V.~F. Turchin.
\newblock {\em Refal-5, Programming Guide and Reference Manual}.
\newblock New England Publishing Co., Holyoke, Massachusetts, 1989.
\newblock Electronic version: \url{http://www.botik.ru/pub/local/scp/refal5/},
2000.
\bibitem{Refal5:PZ}
V.~F. Turchin, D.~V. Turchin, A.~P. Konyshev, and A.~P. Nemytykh.
\newblock Refal-5: Sources, executable modules.
\newblock [online], 2000.
\newblock \url{http://www.botik.ru/pub/local/scp/refal5/}.
\bibitem{Begin:BABYLON}
L.~van Begin.
\newblock The {BABYLON} project: A tool for specification and verification of
parameterized systems to benchmark infinite-state model checkers.
\newblock [online].
\newblock \url{http://www.ulb.ac.be/di/ssd/lvbegin/CST/}.
\end{thebibliography}