本文作者为 Christophe Alias 与 Denis Barthou，均来自法国凡尔赛圣昆廷大学（U. of Versailles Saint-Quentin）的 PRISM 实验室。论文发表于 Electronic Notes in Theoretical Computer Science 第 82 卷第 2 期（2003 年），属于计算机科学中的程序分析与算法识别领域。该研究旨在解决算法模板（algorithm templates）识别中的一个核心问题：判断一个仿射递推方程组（System of Affine Recurrence Equations, SARE）是否为某个 SARE 模板的实例化（instantiation）。该问题在程序优化、程序理解、程序验证以及软硬件协同设计等方面具有重要应用价值。由于该问题已被证明是不可判定的（undecidable），作者提出了一个半判定过程（semi-decision procedure），其关键步骤是计算仿射关系的传递闭包（transitive closure of affine relations）。论文同时讨论了该算法的局限性，并指出了尚未解决的问题。

在学术背景方面，算法识别是计算机科学中的一个经典问题。其基本目标是将一段代码提交给分析器，使分析器能够自动判断出该代码所实现的算法，例如识别出某段程序是高斯消元（Gaussian elimination）的实现。这种能力可以支持多项重要技术：程序优化（用优化版本替换原始代码）、程序理解与逆向工程、程序验证（检查程序是否与规格说明一致）、以及软硬件协同设计（将软件代码替换为硬件加速调用）。已有的算法识别方法大多基于模式匹配（pattern matching），例如归约识别（reduction recognition）已被许多并行化编译器采用。然而，这些方法只识别与代码语义完全一致的算法，难以处理以通用术语描述的算法模板。算法模板抽象掉了实现细节，只保留算法的通用结构。例如，高斯消元、Warshall 传递闭包算法和 Floyd 最短路径算法都是代数路径问题（Algebraic Path Problem, APP）的不同实例，其区别仅在于底层的代数结构不同。为了识别这类通用算法，需要设计模板匹配方法，而不是为每个实例单独建立模式。该研究的目标就是在算法识别框架下提出一种能够识别 SARE 模板并进行实例化匹配的方法。

在方法层面，本研究基于 SARE 这一标准化形式。SARE 可以从静态控制程序（static control programs）自动转换得到，这一转换已被 Feautrier 等人的工作所支持。SARE 使用一组方程描述计算过程，每个方程形如“对于所有 i 属于定义域 d_k，x[i] = fk(… y[u{y,k}(i)] …)”，其中 x、y 为数组变量，fk 为函数符号，u{y,k} 为仿射依赖函数。SARE 模板与普通 SARE 的区别在于，模板方程中允许出现函数变量（function variables）和数组变量（array variables），分别用希腊字母表示。匹配问题定义为：给定两个已调度的 SARE，其中一个是模板，另一个是待识别程序，如果存在对模板变量的替换（substitution），使得在输入相等的前提下输出值相同，则称模板与该 SARE 匹配。

论文给出的匹配过程结合了 Huet 的句法术语合一算法与 Barthou 等人提出的 SARE 等价性检验算法。匹配过程从初始匹配子句开始，初始子句的形式为“id, (i ∈ d) : o[i] ?= o’[i]”，表示在不带替换且索引满足定义域约束的条件下，要求模板输出 o[i] 与待识别程序输出 o’[i] 相等。随后反复应用一组重写规则，直到得到求解形式（solved form）。求解形式分为失败子句 ⊥ 和成功子句 ✶c，其中 c 是一组包含替换 σ 及其上下文 r 的集合。规则包括 decompose、delete、conflict、generalize、compute、empty、substitute、project/imitate、project1、project2、input variable、input success 和 input failure。其中 decompose、delete 和 conflict 是经典合一规则，用于处理刚性-刚性对。generalize 规则将索引表达式改写为新的索引变量，compute 规则根据数组在 SARE 中的定义将其展开为若干子句。input variable 规则处理模板中的数组变量与待识别程序中具体项之间的匹配，input success 和 input failure 则比较两个输入数组在相同索引上的关系。substitute、project/imitate、project1 和 project2 规则沿用 Huet 算法，用于寻找函数变量的替换。该过程具有可靠性和完备性，但其执行可能需要进行参数数量级的展开步骤。

为了克服这一终止性问题，作者提出将匹配过程实现为一种记忆状态自动机（Memory State Automaton, MSA）。MSA 的状态由两部分组成：一个有限标签和一个整数向量。标签对应匹配子句，向量则是左右两侧索引变量的拼接。转移关系由触发关系（firing relation）定义，它表示转移前后的索引变量之间的仿射约束。自动机的初始状态为“id : o[i] ?= o’[i’]”，其可达集为所有满足 i = i’ 的向量。终止状态包括成功形式（包含替换 σ 和上下文 e）与失败形式 ⊥。MSA 的构造将每一条匹配规则映射为自动机中的转移。例如 decompose 产生一个与分支（and-branching），compute 产生一个选择分支（or-branching），而 Huet 规则产生项目与模仿之间的析取分支。论文证明了对应于 SARE 匹配问题的 MSA 具有有限数量的状态，因为待识别程序的子项数量有限，且函数变量的数量也有限。

MSA 构造完成后，通过算法 1 进行分析。该算法的步骤包括：首先计算每个节点的可达集，然后固定 input variable 和 input success 节点的上下文；对于 input variable 节点，如果存在相同的左侧索引对应多个不同的右侧索引，则将该节点替换为失败；删除不可达节点；将环折叠为单个节点；将得到的有向无环图转换为树；再通过递归应用 ∧、∨ 和 ✶ 的规则计算合一器集合；最后返回所有有效解。然而，该算法并不能完全解决匹配问题，因为传递闭包的计算本身不是有效过程。因此该算法只在传递闭包可计算的情况下有效。

论文通过一个归约模板的实例展示了 MSA 的构造与分析过程。该模板描述了一个归约操作：输出为 t[n]，t[0] = ψ[0]，且当 1 ≤ i ≤ n 时 t[i] = ϕ(t[i-1], ψ[i])。待识别程序是计算平方和的 SARE。MSA 分析得到了多个可能的解，其中只有替换 [ϕ → λxy.x + y, ψ_i → a[i] * ai] 在 n ≥ 1 的条件下对应真正的归约操作。其他解虽然满足匹配条件，但 ϕ 未被定义或不满足结合律。该实例展示了算法如何通过自动机构造和可达集计算得到所有潜在匹配解。

论文的主要结论指出，算法模板识别为代码理解、验证和优化提供了有前景的工具。与以往仅能识别已知算法的组合或完全相同语义代码的方法相比，该研究提出的基于 SARE 模板的方法能够识别由若干已知算法组合而成的未知算法。作者同时指出，未来工作将包括在基准应用上验证该方法的可行性、扩展已有 SARE 等价性检验原型、识别由构造类型参数化的模板，以及研究非仿射递推方程组情况下的适用性。该研究的主要亮点在于首次在算法识别框架下提出了 SARE 模板识别的半判定方法，并利用 MSA 将匹配过程转化为自动机分析，为处理参数化数量的重写步骤提供了可能的途径。虽然传递闭包的计算限制了该方法的完全可判定性，但该工作为后续算法模板识别研究奠定了基础。