Söderberg & Hedin (2013) -- Circular Higher-Order Reference Attribute Grammars

The paper

E. Söderberg and G. Hedin, “Circular Higher-Order Reference Attribute Grammars,” Lecture notes in computer science, pp. 302–321, 2013.

doi:10.1007/978-3-319-02654-1_17

A summary of the paper and how gen uses it.

SLE 2013, LNCS 8225, pp. 302-321. Springer. DOI 10.1007/978-3-319-02654-1_17. Journal extension: Declarative rewriting through circular nonterminal attributes, COMLAN 44(A):3-24, 2015, DOI 10.1016/j.cl.2015.08.008.

Paper Summary

The paper unifies two previously-separate RAG extensions — circular attributes (fixed-point iteration, Farrow 1986 / Magnusson-Hedin 2007) and attribute-dependent rewrites (in-place AST transformation, Ekman-Hedin 2004) — into a single mechanism, the circular non-terminal attribute (circular NTA). Prior work evaluated circular attributes and rewrites in isolation, assuming no interdependence between them. Söderberg & Hedin show that when a rewrite’s when clause depends on a circular attribute AND the circular attribute depends (via the tree) on the rewritten node, evaluating the two in separate cycles produces WRONG results: the rewrite reads the circular attribute’s intermediate BOTTOM value, its guard is prematurely false, and the rewrite terminates too soon with a stale cached value (their Fig. 10-11: the child stabilizes at B when the correct final value is C).

The fix is to co-evaluate both in ONE fixed-point cycle so each sees the other’s changes. The unification: an NTA whose value is computed by fixed-point iteration over a bounded-height lattice, with a monotonic semantic function and a declared bottom value. A rewrite is then a special case of a circular NTA — §5 shows the general mapping. The deep reframing (§5.1) is to stop viewing the AG as an attribution of the PARSED (initial) AST, and instead view it as an attribution of a COMPUTED AST that is itself a function of the initial AST: “both the computed AST and the attributes of the computed AST is a function of the initial AST… the initial AST remains unchanged during the evaluation — it is only the attribution that changes, including the computed AST, until it has reached its final state, where all equations are satisfied.” Computed children are reference attributes; for nodes without rewrites they are copies of the initial children, and for nodes with rewrites they are defined by a circular NTA in the parent (Designs A/B/C, §5.2, progressively optimized to build NTAs only for node types that statically may-rewrite, and to skip value-comparison using a change-flag stack).

Well-definedness (§4.1) rests on the classical circular-AG conditions applied to AST values: values drawn from a lattice of bounded height, a monotonic semantic function, and a bottom value seeding the iteration (Def. 1 gives AST-value equality: same type, tokens, and recursively-equal children; the parent reference is a computed value, not part of the value). Nested/mutually-dependent circular NTAs converge to a common fixed point regardless of iteration order. Termination of the NTA-per-iteration-step view is handled by the Krishnan & Van Wyk (SLE 2012) conservative multi-level-NTA ordering — each generated NTA has a lower order than its host. §6 evaluates on Java name-reclassification rewrites (DemoJavaNames): the unified CIRCULAR-NTA algorithm matches or beats the specialized rewrite evaluators, with substantially better scaling on complex programs because more attributes can be cached during evaluation.

How gen uses this

gen-scope: circular attributes

The paper’s well-definedness contract is what a gen-scope circular attribute declares. circular { carrier; } f returns a declaration whose carrier states a bottom value, an order leq, a bounded height, and whether the order is over a quotient of the values (§2.4, §4.1: “a lattice of bounded height, that the semantic function is monotonic, and that a bottom value is provided as the starting point of the fixed-point iteration”). None of these can be recovered from f, so each is declared. As in the paper’s CIRCULAR-ATTR-EVAL (Fig. 5), the evaluator reads the declaration at demand time. A declaration with no carrier fails at its first demand with an error naming the missing terms. Mutually dependent circular instances iterate together in one shared round, the single co-evaluation cycle §3 shows is needed to avoid reading a stale intermediate value, and the iteration bound is derived from the declared heights.

gen-scope: bounded non-terminal attributes

gen-scope synthesizes child nodes from attributes (a node’s spawned and NTA children). Termination follows the technique §7 restates from Krishnan & Van Wyk 2012: order the node types so that “each new NTA has a lower order than its host”. A kind declares the kinds it may spawn in its below set, and each name in below resolves only against kinds registered strictly earlier, so a cyclic or self-referencing spawn cannot be written. A spawn of a kind outside below fails with an error naming it.

gen-memo: never cache a non-final value

gen-memo, gen’s incremental rebuilder, keeps §4.2’s obligation that a value computed during an unfinished fixed-point iteration is never served as final. A rebuild whose dependency cone reaches a cycle fails with a catchable error instead of caching anything, and cyclic components are solved separately to their fixed point by runScc.

gen-bind: values resolved at their producer

gen-bind thunks follow the §5.1 view of materialization as attribution over a static tree. A thunk created with mkThunkFrom records the scope that produced it. When the caller supplies that scope’s configuration, the thunk resolves against the producer’s configuration rather than the consumer’s.

Key Concepts

• Circular NTA (§4): a non-terminal (tree-valued) attribute computed by fixed-point iteration over a bounded-height lattice, monotonic semantic function, declared bottom value. Generalizes both circular attributes and rewrites.

• Rewrites as a special form of circular NTA (§5): an in-place AST rewrite = a circular NTA over the computed children, where the when clause is the change condition and consistency (no applicable when) is the fixed point. Enables freely mixing rewrites and circular attributes.

• Interdependence premature-termination bug (§3): separate evaluation cycles for a generative step and a circular attribute that depend on each other yield a stale intermediate (bottom) value read across the boundary; the generation terminates too soon. Fix = one shared cycle.

• Computed AST as attribution over the static initial AST (§5.1): reframe the AG as defining an attribution — including a computed AST — that is a pure function of the unchanged initial AST. Computed children are reference attributes; the initial AST is never mutated.

• Well-definedness conditions (§4.1): bounded-height value lattice + monotonic semantic function + bottom value. Nested circular NTAs reach a common fixed point independent of iteration order.

• Bounded-NTA termination (§7, via Krishnan & Van Wyk SLE 2012): conservative termination for multi-level NTAs by ordering node types so each generated NTA is lower-order than its host.

• Design B may-have-rewrite gating / Design C change-flag stack (§5.2): build NTAs only for statically rewrite-bearing node types (demand-driven), and skip value comparisons using a push/pop change-flag stack. A node with no rewrites returns its initial child unchanged.

• Forwarding contrast (§7, Van Wyk CC 2002): forwarding constructs the transformed tree as an NTA and auto-forwards attributes to it, KEEPING all intermediate steps; rewrites REPLACE nodes.

Related cited works

Vogt-Swierstra-Kuiper 1989 (HOAG/NTA), Hedin 2000 (RAGs), Magnusson-Hedin 2007 (circular RAGs), Ekman-Hedin 2004 (rewritable RAGs), Knuth 1968 (AGs), Boyland 2005 (remote attributes, undecidable static circularity), Krishnan-Van Wyk 2012 (HOAG termination), Van Wyk et al. 2002 (forwarding), Demers-Reps-Teitelbaum 1981 / Reps 1982 (incremental AG evaluation), Farrow 1986 (fixed-point circular AG evaluators).