Skip to content
Weltenwanderer Weltenwanderer

ADR-014: AST-to-State-Machine Extraction via Free/Forgetful Adjunction

Context

The compiler must extract a finite state machine from the AST to run decidability checks — exhaustiveness, totality — without carrying the full syntactic weight of the AST into the checker. The AST is rich: expressions, guards, field assignments, source positions. The state machine is minimal: states, transitions, labels. The question is whether stripping the AST down to a state machine preserves the properties to be checked.

Without a formal justification, the extraction is an implementation choice that may lose guarantees, and the checker’s correctness argument becomes informal.

The Free/Forgetful Adjunction section (Th-4) in specs/theory.allium formalises the relationship.

Decision

Model the extraction as a free/forgetful adjunction between the category of state machines and the category of ASTs:

  • Forgetful functor (Forget): AST → StateMachine — strips syntax, retains the transition system (states, event labels, command labels).
  • Free functor (Free): StateMachine → AST — embeds a minimal machine into the full syntactic category.

Free ⊣ Forget guarantees that properties proven on the image of Forget (the extracted machine) hold for the original AST object. Exhaustiveness and totality checks run on the extracted machine; their results apply to the AST by the adjunction’s universal property.

Consequences

Positive

  • Justifies running exhaustiveness and totality checks on the extracted state machine rather than the full AST.
  • Decidability results from automata theory apply directly to the extracted machine.
  • Clean separation: syntactic richness stays in the AST layer; semantic checking operates on the minimal machine.

Negative

  • The adjunction is a theoretical justification, not a runtime mechanism; it does not produce code.
  • Properties that depend on expression content — guard satisfiability, field type compatibility — cannot be checked on the stripped machine alone; they require the full AST (see ADR-015 for the satisfiability approach).