Krishnan & Van Wyk (2012) -- Termination Analysis for Higher-Order Attribute Grammars

The paper

L. Krishnan and E. Van Wyk, “Termination analysis for higher-order attribute grammars,” Software Language Engineering (SLE 2012), LNCS 7745, pp. 44–63, 2013.

doi:10.1007/978-3-642-36089-3_4 · read the paper

A summary of the paper and how gen uses it.

SLE 2012, LNCS 7745, pp. 44-63. Springer, Heidelberg (2013). DOI 10.1007/978-3-642-36089-3_4. Lijesh Krishnan and Eric Van Wyk, Department of Computer Science and Engineering, University of Minnesota. Full proofs are in Krishnan’s PhD thesis (Composable Semantics Using Higher-Order Attribute Grammars, Minnesota 2012), cited by the paper as its reference [9]. Implemented in Silver and evaluated on ableJ, the Silver attribute grammar for Java 1.4.

Page citations below follow the authors’ preprint (pages 1-20) and the numbered results (Theorems 1-3, Lemmas 1-6, Figs. 1-8), which are the same in both versions.

Paper Summary

Higher-order attribute grammars (HOAGs, Vogt-Swierstra-Kuiper 1989) let an attribute’s value be a new syntax tree, which is then itself decorated and evaluated. That admits a failure mode no circularity analysis catches: evaluation that never repeats a dependency but generates an unbounded sequence of new trees, each built as a local attribute on its predecessor. Knuth’s circularity test and the HOAG extension of it both terminate cleanly on such a grammar and report nothing wrong. This paper supplies the missing analysis — to the authors’ knowledge the first of its kind — and it is conservative: it proves termination or it fails, and there exist terminating grammars on which it fails.

The analysis is stated over RHOAG (Fig. 4), a restricted class of HOAGs designed to be expressive enough for real grammars (ableJ converted into it “with a few modest modifications”) while isolating tree creation to local-attribute evaluation. The restrictions that matter: no inherited occurrences on the root; a production may not read its own synthesized or its children’s inherited occurrences; no nested attribute-on-attribute accesses; primitive functions neither take nor return trees. Silver’s forwarding is outside RHOAG but is shown translatable into it without loss of precision for this analysis (§6) — notably not for completeness or circularity, where translating forwarding away is known to lose precision.

The argument runs in two halves that meet in Theorem 3.

Half one — rewriting, for the non-inherited case (§4). Non-termination of attribute evaluation is first reduced to the existence of an infinite tree creation sequence (Theorem 1). Where no higher-order inherited attributes are involved, tree creation is modelled by generated term rewrite rules, so that an infinite creation sequence implies an infinite rewrite sequence (Lemma 2). Rule termination is discharged by the external prover AProVE. The generated rules are deliberately over-approximate — attribute instance names are dropped from sub-terms, so the rules derive sequences for every possible higher-order synthesized instance where only one occurs at run time.

Half two — an ordering, for the inherited case (§5). Higher-order inherited attributes break the rewriting model, because the rules lack the context in which inherited attributes are evaluated and represent such accesses with an INH placeholder. So the analysis additionally requires a well-founded, reflexive, transitive ordering ⪰ on non-terminals (conditions in Fig. 7), computed by Procedure A (Fig. 8):

1. build a directed graph G_NT on non-terminals, edge ⟨X, Y⟩ iff S(X, Y);
2. condense it to its strongly connected components as G_SCC, edge ⟨S_X, S_Y⟩ iff some X ∈ S_X, Y ∈ S_Y with I(X, Y), or with S(X, Y) and ¬S(Y, X);
3. if G_SCC has a cycle, return failure — the required ordering does not exist;
4. otherwise X ⪰ Y iff G_SCC has a (possibly trivial) path from X’s SCC to Y’s SCC, and X ≈ Y iff X and Y share an SCC.

Procedure A is condensation, then an acyclicity check, then reachability as the order. Lemma 3 says the ordering Procedure A produces satisfies Fig. 7.

Where they meet. Lemma 4: with ⪰ in hand, every created tree is no larger than the tree it was created on — t_i ⪰ t_(i+1), non-increasing, not strictly decreasing. Lemma 5: any infinite tree creation sequence therefore contains an infinite constant sub-sequence (t_0 ≈ t_1 ≈ t_2 ≈ ...), because only finitely many steps can strictly descend. Lemma 6: constant sub-sequences use no inherited accesses, so the rewrite rules do model them (via a pruned term where sub-trees below the constant level are replaced by INH). Theorem 3: if the grammar is complete and non-circular, the generated rewrite rules terminate, and the non-terminals can be ordered as required, then no improper evaluation sequence exists. The worked example: Stmt ≈ Expr, Stmt ≈ Type, Stmt ≻ Env; adding a C-style typedef type environment inherited on Env adds a level, Env ≻ TypeEnv, TypeEnv ≈ TypeRep.

§6 states the limits. The analysis cannot handle a definition whose generated tree carries the same production name as the defining production with children fetched through synthesized accesses (the generated rules are then always non-terminating). And “since the analysis assumes that the grammar is non-circular, it does not handle reference attribute grammars since the circularity problem is undecidable in that setting.” §8 lists relaxing that assumption, in order to handle RAGs, as future work, alongside a modular version whose composed-grammar ordering condition could be checked per extension.

How gen uses this

gen-scope: kinds minted in order

gen-scope’s demand cascade cites Fig. 7 and Theorem 3, which make termination follow from the existence of a well-founded ordering on the nonterminals. Söderberg and Hedin (2013, §7) restate the idea as ordering node types so that “each new NTA has a lower order than its host”.

gen-scope constructs a witness for that ordering instead of deciding whether one exists. mkKinds mints kinds from a list in order, and a kind’s below names resolve only against kinds minted earlier in the list. A kind that names itself, or a later kind, fails with an error naming the missing kind, so a cyclic below relation cannot be written. Each minted kind records depth = 1 + max { depth b : b ∈ below } (0 when below is empty), a natural number that strictly decreases along every edge. Every admissible order of one set of declarations mints the same depths. Where Procedure A can fail on a cycle in the condensation, the minting order makes that case inexpressible.

Scope limits of the result

The paper’s result is narrower than the one-sentence summary Söderberg and Hedin give, in four ways.

1. The ordering is non-increasing. Lemma 4 is t_i ⪰ t_(i+1). Equal-order steps are permitted, and they are what the paper calls a constant tree creation sequence. “Lower order than its host” describes the strict steps only.
2. The ordering is one of three conditions. Theorem 3 also needs completeness and non-circularity, and terminating rewrite rules. The ordering bounds the higher-order inherited steps, and the rewrite system discharges the constant runs it leaves (Lemma 6).
3. Reference attribute grammars are excluded. §6 rules RAGs out because circularity is undecidable for them, and §8 lists handling them as future work. gen-scope is a RAG evaluator, so the analysis does not give termination for its circular or reference constructs. Krishnan and Van Wyk cite Boyland 2005 for that undecidability.
4. Procedure A can fail. A cycle in the SCC condensation means no ordering exists, and the analysis reports failure.

The paper’s two-part argument maps onto gen-scope’s constructions. Its ordering handles the steps that cross levels, and something else must handle runs within one level. gen-scope’s minted depth covers the first. Within one level, gen-scope’s circular attributes iterate over a declared carrier, and the paper gives no termination argument for them.

Key Concepts

• Improper evaluation sequence / infinite tree creation sequence (§3, Theorem 1): the HOAG-specific non-termination that circularity analysis cannot see — evaluation generates unboundedly many new trees without ever repeating a dependency.

• RHOAG (Fig. 4): the restricted HOAG class the analysis is stated over. No inherited occurrences on the root, no nested attribute-on-attribute access, functions neither consume nor produce trees. Chosen so that tree creation is isolated to local-attribute evaluation.

• Rewrite-rule modelling of tree creation (§4, Lemma 2): generated term rewrite rules over-approximate the trees a grammar can build; if the rules terminate, no infinite creation sequence exists. Discharged by AProVE.

• The non-terminal ordering ⪰ / ≻ / ≈ (Fig. 7): well-founded, reflexive, transitive. X ≻ Y is forced by higher-order inherited use I(X, Y); X ⪰ Y by synthesized/local use S(X, Y).

• Procedure A (Fig. 8, Lemma 3): SCC graph -> condensation -> refuse on cycle -> order by reachability. X ≈ Y iff same SCC.

• Constant tree creation sequence (§5, Lemmas 4-6): a run of equal-order creation steps. The ordering permits them; the rewrite rules (over INH-pruned terms) close them.

• Theorem 3: complete + non-circular grammar, terminating generated rules, existing ordering ⇒ no improper evaluation sequence. All three conditions are required.

• Conservativeness (§6): AProVE is conservative, the ordering generator is conservative, and the generated rules over-derive. Terminating grammars can fail the analysis.

• RAG exclusion (§6, future work in §8): non-circularity is assumed, so reference attribute grammars are outside its scope.

• Forwarding as non-destructive rewriting (§6): a forwarding production designates a semantically equivalent tree and forwards unanswered attribute queries to it; translatable to higher-order attributes with generated copy rules, at no precision cost for this analysis.

Related papers

Cited works with summaries on this site: Vogt, Swierstra and Kuiper 1989 (Higher-Order Attribute Grammars), Hedin 2000 (Reference Attributed Grammars), Van Wyk et al. 2010 (Silver) and Sloane’s Kiama papers (2009, 2010). Söderberg and Hedin 2013 (Circular Higher-Order Reference Attribute Grammars) cites this paper. The paper also cites Knuth 1968 and its 1971 correction, Boyland 2005 (remote attributes and undecidable circularity), Ekman and Hedin 2007 (JastAdd), Van Wyk et al. 2002 (forwarding) and 2007 (ableJ), Dershowitz 1982 (orderings for term rewriting), Lee, Jones and Ben-Amram 2001 (size-change termination), Sereni and Jones 2005, Backhouse 2002, Johnsson 1987 and Giesl et al. 2003 (AProVE).