Inductive inference of term rewriting systems from positive data

In this paper, we study inferability of term rewriting systems from positive examples alone. We define a class of simple flat term rewriting systems that are inferable from positive examples. In flat term rewriting systems, nesting of defined symbols is forbidden in both left- and right-hand sides. A flat TRS is simple if the size of redexes in the right-hand sides is bounded by the size of the corresponding left-hand sides. The class of simple flat TRSs is rich enough to include many divide-and-conquer programs like addition, doubling, tree-count, list-count, split, append, etc. The relation between our results and the known results on Prolog programs is also discussed. In particular, flat TRSs can define functions (like doubling), whose output is bigger in size than the input, which is not possible with linearly-moded Prolog programs.