Subsumption-oriented Push-Down Automata

This paper presents Subsumption—oriented Push—Down Auto-mata (SPDA), a very general stack formalism used to describe forest (“AND- OR” tree) traversals. These automata may be used for parsing or the interpretation of logic programs. SPDA allow a Dynamic Programming execution which breaks computations into combinable, sharable and storable sub-computations. They provide computation sharing and operational completeness and solves some of the problems posed by the usual depth-first, left-to-right traversals (as implemented in PROLOG). We give an axiomatization of SPDA and two examples of their use: the evaluation of logic programs and parsing with Tree Adjoining Grammars. SPDA may also serve in other areas such as Constraint Logic Programming, Abstract Interpretations, or Contextual parsing.