## 2 A Motivating Example  
Before going to formal definitions, we start with a simple example to illustrate the main ideas behind ICOREs. We consider the classical string edit distance problem. We are given two sequences \(U\) and \(V\), to be compared under a simple edit model. There are three edit operations: Replacement of a character symbol, deletion of a character, and insertion of a character, which can be used to transform \(U\) into \(V\) or vice versa. Each position in \(U\) and \(V\) is edited exactly once. (Without this restriction, we would arrive at the more general notion of a transformation distance. Only when the basic edit model satisfies the triangle inequality, optimal edits and transformations coincide.) The space of candidate solutions is the set of all edit scripts for \(U\) and \(V\), defined as sequences of edit operations which transform \(U\) into \(V\). All edit operations are associated with an additive score, and eventually, the edit script with the minimal overall score defines the edit distance between \(U\) and \(V\). We propose to treat these edit scripts as formal objects, and more precisely to encode them as terms. To this end, we define three function symbols, one for each edit operation: rep, del, and ins. Each such operator takes as arguments the character symbol(s) involved in the operation. We also introduce a constant operator mty, which represents the empty edit script. For example, consider the two strings \(U=\)\"ACGTA\" and \(V=\)\"AATAG\" on the DNA alphabet \(\{\texttt{A},\texttt{C},\texttt{G},\texttt{T}\}\). One possible edit script is :  
\[ \begin{array}{l}\text{replacement of 'A' by 'A',}\\ \text{replacement of 'C' by 'A',}\\ \text{deletion of 'G',}\\ \text{replacement of 'T' by 'T',}\\ \text{replacement of 'A' by 'A',}\\ \text{insertion of 'G'}\end{array} \]  
This edit script is represented by the term  
\[c=\]  
rep (A,A,rep(C,A,del(G,rep(T,T,rep(A,A,ins(G,mty))))))))  
We call these terms _core terms_, as they represent the search space of candidate solutions. A visually better representation of this edit script would be an alignment of the two sequences, in this case  
A C G T A - A A - T A G  
A term representing an edit script contains in some sense the two input sequences: \(U\) is the concatenation of the first arguments of rep and of del. \(V\) is the concatenation of the second arguments of rep and the first arguments of ins. This projection is formally expressed with two term rewrite systems:  
\[ \begin{array}{rclrcl}\texttt{rep}(a,b,X)&\rightarrow&a{\sim}X&\texttt{ rep}(a,b,X)&\rightarrow&b{\sim}X\\ \texttt{del}(a,X)&\rightarrow&a{\sim}X&\texttt{del}(a,X)&\rightarrow&X\\ \texttt{ins}(a,X)&\rightarrow&X&\texttt{ins}(a,X)&\rightarrow&a{\sim}X\\ \texttt{mty}&\rightarrow&\varepsilon&\texttt{mty}&\rightarrow&\varepsilon \end{array} \]The alphabet character symbols \(a\) and \(b\) serve as nullary function symbols, extended by two operators \(\sim\) and \(\varepsilon\). \(\sim\) is a binary operator for the concatenation of two strings (or a character and a string), and \(\varepsilon\) is the empty string. So \(U\) is A\(\sim\)C\(\sim\)G\(\sim\)T\(\sim\)A and \(V\) is A\(\sim\)A\(\sim\)T\(\sim\)A\(\sim\)G.  
By construction, the two rewrite systems have the same left-hand sides. So we can conveniently merge their representation into a single tabular form. \[a{\sim}X \leftarrow \mathtt{rep}(a,b,X) \rightarrow b{\sim}X\] \[a{\sim}X \leftarrow \mathtt{del}(a,X) \rightarrow X\] \[X \leftarrow \mathtt{ins}(a,X) \rightarrow a{\sim}X\] \[\varepsilon \leftarrow \mathtt{mty} \rightarrow \varepsilon\]  
Since we search for the optimal edit script, we need to rank all candidate terms. The operators \(\{\mathtt{rep},\mathtt{del},\mathtt{ins},\mathtt{mty}\}\) constitute a signature (comparable to an interface in the programming language Java), where the operators are functions whose argument and result types are generic.