Adding strongly equivalent normalization transformations

[ZachJHansen]

Natural translation does not produce completable theories, and thus cannot be directly integrated with the existing implementation of completion. The paper "On Program Completion, with an Application to the Sum and Product Puzzle" describes a more restrictive class of regular rules that forbids intervals in the heads of rules. It also describes a transformation, NCOMP, which parallels program completion for rules in this class.

Natural translation nu (as defined in "Transforming Gringo Rules into Formulas in a Natural Way") can be defined as a translation option for anthem, however, external equivalence in anthem should follow the description of NCOMP and its corresponding restricted version of nu.

However, we can obtain rules in this restricted class from many regular rules via strongly equivalent transformations on programs (as suggested by "On Program Completion", section 6). This is one example of a feature we have discussed in the past, which is the ability to reduce an ASP program to a strongly equivalent mini-gringo program of a simpler form. Here I called this process "normalization" and provided an example of one such function that is relevant to nu and NCOMP. A recursive extension of this function is needed to pass the commented-out test case.