An Operational Model for Parsing Definite Clause Grammars with Infinite Terms

Logic programs share with context-free grammars a strong reliance on well-formedness conditions. Their proof procedures can be viewed as a generalization of context-free parsing. In particular, definite clause grammars can be interpreted as an extension of the classic context-free formalism where the notion of finite set of non-terminal symbols is generalized to a possibly infinite domain of directed graphs. In this case, standard polynomial parsing methods may no longer be applicable as they can lead to gross inefficiency or even non-termination for the algorithms. We present a proposal to avoid these drawbacks, focusing on two aspects: avoiding limitations on the parsing process, and extending the unification to composed terms without overload for non-cyclic structures.