In the context of the study of rule-based programming, we focus in this paper on the property of C-reducibility, expressing that every term reduces to a constructor term on at least one of its rewriting derivations. This property implies completeness of function definitions, and enables to stop evaluations of a program on a constructor form, even if the program is not terminating. We propose an inductive procedure proving C-reducibility of rewriting. The rewriting relation on ground terms is simulated through an abstraction mechanism and narrowing. The induction hypothesis allows assuming that terms smaller than the starting terms rewrite into a constructor term. The existence of the induction ordering is checked during the proof process, by ensuring satisfiability of ordering constraints. The proof is constructive, in the sense that the branch leading to a constructor term can be computed from the proof trees establishing C-reducibility for every term
展开▼
机译：在基于规则的程序设计研究的背景下，我们将重点放在 C 可归约性的属性上，表示每个项至少在其一个重写派生项中都简化为构造器项。此属性表示函数定义的完整性，并且即使在程序未终止的情况下，也可以停止以构造函数形式对程序进行求值。我们提出了一种归纳程序，证明了 C 的可重写性。通过抽象机制和缩小来模拟基本术语的重写关系。归纳假设允许假设小于开始项的项会重写为构造器项。通过确保排序约束的可满足性，在证明过程中检查归纳排序的存在。证明是建设性的，从某种意义上说，可以从证明树为每个项建立 C 可归约性的证明树中计算出构造函数项的分支
展开▼
