We survey the definitions and main properties of first-order (FO) definable unary operations on relational structures, called FO-transductions, and of FO-definable binary operations based on disjoint union and Cartesian product. We focus our study on Backwards Translation Theorems and Splitting Theorems that permit to express FO properties of output structures in terms of finitely many FO properties of the corresponding input ones. In the particular cases where the operations are defined by quantifier-free (QF) formulas, the quantifier-heights of the obtained sentences are no larger than those of the input ones. It follows that the class of finite models of a FO sentence is recognizable with respect to the considered QF operations. Recognizability has interesting algorithmic properties based on finite automata on terms, for structures having bounded tree-width or clique-width. We extend our results to FO sentences constructed with modulo counting existential quantifiers.

翻译：我们综述了一阶可定义的一元运算（称为FO-变换）及基于不交并和笛卡尔积的FO-可定义二元运算的定义及其主要性质。研究重点在于逆向翻译定理和分裂定理，这些定理允许通过输入结构中有限个FO性质来表达输出结构的FO性质。在运算由无量词公式定义的特殊情形中，所得句子的量词深度不超过输入句子的量词深度。由此可知，对于所考虑的无量词运算，FO句子的有限模型类是可识别的。对于具有有界树宽或团宽的结构的项上有限自动机，可识别性具有重要的算法性质。我们将结果推广到包含模计数存在量词构造的FO句子。