Introduction

In the current context of a rapidly evolving research effort towards LLM-based formal reasoning and theorem proving, our aim is to contribute a novel approach that complements existing methods with a focus on formal guarantees of correctness.

In this blog post Proposition 7: Truth by Construction, we introduced the core idea of our approach: guide LLMs to produce only tokens that are guaranteed to be part of a correct expression in a language. Such approaches already exist in various forms, but our contribution lies in the generalization of this idea to a larger and extensible class of formal languages, along with a concrete algorithm to achieve this goal.

This document serves as a formal specification of the theoretical foundations, as documentation of the algorithm, and as a reference for future work building upon this approach.

The Aufbau Engine

Aufbau is the grammar-driven completion engine powering the Proposition 7 project. Given a grammar and a partial expression it computes the set of next tokens that can extend the expression toward a complete, well-typed program. The central guarantee is that every suggested token keeps the expression on a valid trajectory that can then be completed until it reaches a complete (a word in the language defined by the grammar)

The name comes from the German word for “construction” or “build-up” from Carnap’s Der logische Aufbau der Welt

Structure

The specification follows the layered structure of the implementation:

1. Basic Concepts : alphabets, Kleene closure, formal languages, and the completability set $\mathcal{C}_L(s)$ at the heart of the engine

2. Concepts: the more advanced theoretical framework

3. Parsing: the chart parser, the segment model, the span cache and its invalidation strategy, and the meta-parser that reads grammar specifications.

4. Typing: the type system, the inference rules encoded in grammar specs, context propagation, and the typed AST overlay that is built on top of the partial parse forest.

5. Completion: how the engine synthesizes and scores completion candidates, and how the beam synthesizer explores the space of completions.

Invariant

The key correctness property that runs through every layer of the specification:

DONE Basic Concepts and Notations

First, we are going to establish some simple concepts of programming language theory, so that we can refer to them later in the specification.

We are going to use shorthand notation for ranges of symbols in alphabets. For example a-z denotes all lowercase letters from a to z, and 0-9 denotes all digits from 0 to 9.

An alphabet can be subjected to various operations to create different kinds of sets. We usually call those sets languages. The Kleene star operation, denoted $X^*$, creates the set of all possible strings that can be formed by concatenating zero or more elements from $X$. It’s similar to the power set operation, but instead of creating subsets, it creates strings.

A language is defined as a set of strings over an alphabet. A string is a finite sequence of symbols from the alphabet. A string in a language is called a word.

The concatenation operation is written as $s \cdot t$ or the shorthand $st$ for strings $s, t \in \Sigma^\ast$. It is defined as the string obtained by appending $t$ to $s$.

Definitions and notations

Let $L$ be a formal language over an alphabet $\Sigma$.

An expression $s \in \Sigma^\ast$ is said to be completable in $L$ if there exists some $s’ \in \Sigma^\ast$ such that $ss’ \in L$

The completability set is central to our formalism. We can use it to state an important equivalence:

Completability of $s$ in $L$ thus reduces to checking whether its completability set is non-empty.

DONE Theoretical Foundation

This chapter defines the formal structures underlying the Aufbau system: grammars, parse forests, partial trees, typing judgments, and the completability guarantee.

Sources: src/logic/grammar/mod.rs, src/logic/partial/structure.rs, src/logic/typing/mod.rs

Grammar

Symbol

Production

DONE Partial Trees and Forests

Parse Forest

In the implementation, partial parse forests are stored as Shared Packed Parse Forrects (SPPF) to save up space.

Partial Parser

The parser is sound in the sense that every prefix of $s$ will be accepted by it and produce a forest.

Tree Paths

We use $x[i]$ for the child at index $i$, and extend this to relative paths $x[p]$.

Terminal Status and Extensibility

A terminal node matching input $s$ has a status:

• Complete: Matched a full token. It may carry an extension derivative $D_s(r)$ for further matching.
• Partial: Matched only a prefix. It carries a remainder derivative for what must follow.

A terminal can be both complete and extensible. For example, /[a-z]+/ matching foo is complete but extensible by bar. Conversely, a terminal is incomplete and not extensible only if its remainder regex is $\emptyset$ (a parse error). This distinction is critical for binding resolution where bindings to extensible terminals on the rightmost spine are treated as Partial.

Completeness and Frontiers

A node is complete by induction:

• A terminal is complete if it matched the full input.
• A non-terminal $v$ is complete $\iff$ all symbols in its production $\pi(v)$ are satisfied.

Note that this is not extacly the same as extensibility. A (complete) tree will have no frontier, but can have extensible nodes.

Monotonicity

For partial parses $\mathcal{F}(s)$ extending to $\mathcal{F}(s \cdot t)$, the frontier path length is monotonically non-decreasing.

This property is a primary invariant for parser correctness; a decreasing frontier indicates an engine failure.

T = Expression
     └─[0]→ Abstraction(abs)  [complete = false]
            ├─[0]→ "λ"
            ├─[1]→ Identifier("x")
            ├─[2]→ ":"
            ├─[3]→ Type
            │      └─[0]→ AtomicType
            │             └─[0]→ BaseType("Int")
            ├─[4]→ "."
            └─[5]→ Expression  [Missing / End of Input]

DONE Binding Resolution

Given grammar $G = (N, T, P, S, \Theta, A)$, we construct a binding map $\beta: \mathcal{B} \times P \to \mathcal{P}^*$ associating binding identifiers with grammar paths.

Grammar paths navigate grammar structure relative to a production. Alternative indices act as constraints: we only follow a path if the tree node’s chosen alternative matches the path. This allows grammar paths to convert to tree paths at runtime while ensuring the tree respects the specified structure.

Regular Grammar Paths

Example: binding τ through nested parentheses: $$ \beta(\tau, \text{Abstraction}) = 3@0 \cdot (0@1 \cdot 1@0)^* \cdot 0@0 \cdot 0 $$

Binding Map Construction

For each production $p \in P$ with rule $\Theta(p)$:

1. Extraction: Let $\mathcal{B}_\theta$ be bindings mentioned in $\Theta(p)$.
2. Traversal: For $b \in \mathcal{B}_\theta$, find $b$ in $p$ at position $k$. If $\alpha_k[b]$ is a non-terminal, recursively explore alternatives in $A(\alpha_k)$ via BFS.
3. Invariant Extraction: Compute acyclic grammar paths $\mathcal{P}_b^p$ from rule $\theta$ to binding $b$. Paths must include alternative annotations. Use regular grammar paths for cycles.
4. Store: $\beta(b, p) = \mathcal{P}_b^p$.

Grammar paths are static; they are fixed at load time and guide tree path generation during evaluation.

Binding Resolution

For tree $T$, binding $b$, and node $N$, we resolve nodes $V_b$ by matching tree paths against $R_b = \beta(b, N)$. A node $v$ matches if:

1. Edge Match: The edge index sequence matches $R_b$.
2. Alternative Verification: For every step $i@k$, the tree node has alternative $k$.

If edge match succeeds but alternative verification fails for all invariants, the parse is rejected.

Correctness and Constraints

DONE Type System

This chapter defines the type language, the typed tree and forest structures, the typing judgment, and the subtyping relation. Types in Aufbau are not information carriers in the classical sense: they are constraints on completability. A type describes what extensions of a partial expression may become.

The Typing Judgment

Tree Status

This lattice is monotone: status can only move from $\text{Partial}$ toward $\text{Valid}$ or $\text{Invalid}$, never in reverse.

The forest is $\text{Invalid}$ only when all of its trees have been rejected.

Monotonicity makes typed search efficient: once a state is $\text{Invalid}$, the entire subtree below it in the search space can be pruned without examination.

Typed Trees and Forests

The typing engine $\vdash_\Theta$ maps a tree to either a status or rejection. This lifts trees and forests into typed counterparts.

The typing engine thus acts as a constructor:

$$ \vdash_\Theta t = \begin{cases} \hat{t} & \text{if } \vdash_\Theta t : \text{Valid}(\tau) \text{ or } \text{Partial}(\tau) \text{ for some } \tau \\ \text{Invalid} & \text{if the typing constraint is violated} \end{cases} $$

Extending the engine to forests:

$$ \vdash_\Theta \mathcal{F} = \begin{cases} \hat{\mathcal{F}} & \text{if at least one tree in } \mathcal{F} \text{ produces a typed tree} \\ \text{Invalid} & \text{if every tree in } \mathcal{F} \text{ is } \text{Invalid} \end{cases} $$

A partial tree that is typedly invalid carries an inconsistency in its typing rules. It is syntactically valid but semantically invalid

Types as Constraints on Completability

Without typing, $\mathcal{C}_L(s)$ is the set of all syntactically valid extensions of a prefix $s$. The typed tree structure gives this a sharper interpretation: every type $\tau$ assigned to a node in $\hat{t}$ is a constraint asserting that any syntactic completion of that subtree must produce a value of type $\tau$, or the tree transitions to $\text{Invalid}$.

Types therefore define a refinement of the completability set:

$$ \mathcal{C}_{L,\Theta}(s) = \{\, a \in \mathcal{C}_L(s) \mid \Gamma \vdash_\Theta \mathcal{F}(sa) \neq \text{Invalid} \,\} $$

Typing can only narrow the completability set, never widen it. This refinement is computed incrementally:

1. The parser produces a partial forest $\mathcal{F}(s)$.
2. $\vdash_\Theta$ evaluates each tree, yielding $\hat{\mathcal{F}}$ or $\text{Invalid}$ per tree.
3. The synthesizer computes the grammar-level completion set $\mathcal{C}_L(s)$.
4. Each candidate token $a$ is tested by extension: parse $s \cdot a$, apply $\vdash_\Theta$, and retain only those where some root remains non-$\text{Invalid}$.

The type system acts as a filter, not a generator. It cannot propose completions the grammar does not support; it only rejects those that violate typing constraints.

Type Language

DONE Regex Engine

The regex engine underpins all terminal matching in the parser. It uses Brzozowski derivatives to match incrementally, a design that integrates naturally with partial parsing. The theoretical foundations (derivatives, two-level completability) are developed in Completability and Regular Expressions. This page covers only the implementation-specific choices.

Source: src/regex/

The Regex Type

Prefix Matching

The parser maps these outcomes to terminal node status: Extensible produces a Terminal::Complete with a non-null extension derivative; Prefix produces a Terminal::Partial with a remainder derivative.

Simplification (standard algebraic identities: $\emptyset \cdot r = \emptyset$, $\varepsilon \cdot r = r$, $r \mid r = r$, etc.) is applied after each derivative step to keep expression size bounded.

NFA Fallback

For full-string matching (matches) and maximum-length prefix matching (match_len), the engine compiles to an NFA via Thompson construction rather than using derivatives. This avoids the expression-growth problem derivatives can exhibit on long inputs.

DFA Intersection

has_intersection(r_1, r_2) checks $\mathcal{L}(r_1) \cap \mathcal{L}(r_2) \neq \emptyset$ by product-DFA construction. Used by the typing engine to detect overlapping terminal patterns.

String Generation

examples(n) generates up to $n$ concrete strings in $\mathcal{L}(r)$. The synthesizer uses this to find token candidates when extending a partial tree with a regex terminal.

DONE Grammar Specification

The grammar is composed of production rules with syntactic meaning and attached typing rules conveying semantic information about the language.

The core data structures are defined in src/logic/grammar/mod.rs.

Production Rules

Production rules define the syntactic structure of the language. Each rule maps a nonterminal to one or more alternative right-hand sides.

Nonterminal(rule_name) ::= symbol₁ symbol₂ ... | alternative₂ | ...

Bindings are resolved via grammar paths during type-checking. See src/logic/binding/grammar.rs for the path construction algorithm.

Epsilon Productions

An epsilon production represents an empty alternative, written as ε.

// Optional tail matching zero or more Terms
ProgramTail ::= Term ProgramTail | ε

Typing Rules

Typing rules attach semantic information to productions using an inference-rule format.

premise₁, premise₂, ...
------------------------ (rule_name)
conclusion

The rule name in parentheses must match a (rule_name) annotation on a production.

Premises

Premises express conditions for rule application.

Conclusions

Conclusions specify the rule’s result:

Checking mode (▷) is not implemented as a conclusion; use the check premise Γ ▷ e instead.

Meta-Variables

A meta-variable (written ?A, ?B, etc.) is a placeholder unified during type checking, allowing rules to express polymorphic constraints.

// ?A must unify with both the function's domain and the argument's type.
Γ ⊢ f : ?A → ?B, Γ ⊢ e : ?A
-------------------------------- (app)
?B

Context Operations

The typing context Γ maps variable names to types:

• Γ(x): Look up type of variable x.
• Γ[x:τ]: Extend context with binding x:τ.
• x ∈ Γ: Check if x is bound in context.

Type Syntax

Types in typing rules follow this syntax:

Example: Simply-Typed Lambda Calculus

A complete specification for STLC from examples/stlc.auf:

// Identifier (supports Unicode)
Identifier ::= /[A-Za-z_][A-Za-z0-9]*/

// Variables with var typing rule
Variable(var) ::= Identifier[x]

TypeName ::= /[A-Za-z0-9_τ₁₂₃₄₅₆₇₈₉₀]+/

// Base types (parentheses are literals, hence quoted)
BaseType ::= TypeName | '(' Type ')'

// Function types (right-associative)
AtomicType ::= BaseType | '(' Type ')'
FunctionType ::= AtomicType '->' Type
Type ::= AtomicType | FunctionType

// Lambda abstraction (dot is a literal)
Lambda(lambda) ::= 'λ' Identifier[a] ':' Type[τ] '.' Expression[e]

// Atomic expressions
AtomicExpression ::= Variable | '(' Expression ')' | Lambda

// Applications (left-associative)
Application(app) ::= Expression[l] AtomicExpression[r]

// Expressions (start symbol)
Expression ::= AtomicExpression |  Application

// Typing Rules
x ∈ Γ
----------- (var)
Γ(x)

Γ[a:τ] ⊢ e : ?B
--------------------------- (lambda)
τ → ?B

Γ ⊢ l : ?A → ?B, Γ ⊢ r : ?A
--------------------------------- (app)
?B

Source Files

DONE Partial Parsing

The partial parser implements the theoretical framework of partial forests as a memoized recursive-descent parser with regex-derivative terminal matching. Given an input $s \in \Sigma^*$, it produces a partial forest $\mathcal{F}$ containing all valid parse trees (complete and partial) consistent with the grammar $G$.

Source: src/logic/partial/parse.rs

Segmentation

The first stage of parsing tokenizes input into a sequence of segments.

Special tokens (multi-character operators like ->, <=) are matched longest-first. If a segment at the end of input is a strict prefix of a special token (e.g., - when -> exists in the grammar), it is marked as a partial special token. This flag disables caching for spans involving that segment, since the token’s identity is ambiguous until more input arrives.

Recursive Descent with Memoization

The parser is a recursive-descent parser over segments, augmented with:

1. A persistent span cache for cross-parse memoization
2. Cycle detection for left-recursive grammars
3. Depth-bounded recursion

Nonterminal Parsing

Alternative Ordering

This rotation distributes search effort across recursion depths, preventing systematic bias toward the first production. It is particularly important for left-recursive grammars where always trying the recursive alternative first would waste effort at shallow depths.

Symbol Sequence Parsing

A production’s right-hand side is a sequence of symbols parsed left-to-right. For each successful parse of the first symbol, the parser attempts to parse the remaining symbols with the unconsumed segments.

A critical invariant governs partial nodes: if a child node is partial (incomplete), it is accepted only if it consumed all remaining segments (i.e., it is at the frontier of the input). Partial nodes cannot appear in non-frontier positions.

Partial Terminals

Terminals are regex patterns matched via Brzozowski derivatives (see two-level language completability). Matching a segment against a terminal regex yields one of four outcomes:

At end-of-input (empty remaining segments), the parser produces a Terminal::Partial with the full regex as remainder. This enables downstream completion generation: the remainder derivative describes exactly which tokens could legally appear next.

The distinction between extension and remainder is central to the completability analysis:

• An extension derivative on a complete terminal means the terminal could accept more characters (e.g., identifier x could become xy).
• A remainder derivative on a partial terminal describes what characters are needed to complete the match.

Epsilon Productions

An epsilon production (empty right-hand side, $\varepsilon$) matches zero segments and produces a nonterminal with no children. Such a nonterminal is considered complete.

Recursion Limit

When the depth limit is hit, the parser returns a DepthLimit error. The MetaParser wrapper in src/logic/partial/meta.rs uses iterative deepening to find the minimum sufficient depth.

Incremental Parsing

The parser supports incremental parsing across successive calls. When input $s$ is extended to $s \cdot t$:

1. Normalize both segment sequences to position-independent keys.
2. If the new segments start with the previous segments (prefix match), reuse the span cache.
3. Otherwise, clear the cache entirely.

This prefix-stability property ensures that typing a single character does not require re-parsing the entire input from scratch.

DONE Tokenizer

The tokenizer converts a raw input string into a sequence of segments, the atomic units that the parser operates on. It is constructed once from a grammar’s special tokens and runs in a single linear pass over the input bytes.

Segment

The is_partial_special flag has a specific consequence for the parser: any span whose last segment is a partial special is excluded from the span cache. The token’s identity is not yet determined — it may grow into a complete special with more input, or may be classified as a word token.

Tokenizer Construction

Tokenizer::new(special_tokens, delimiters) sorts the special token list by length descending, then alphabetically as a tiebreak, then deduplicates. Longest-match priority is structural: the first special that matches at a given position wins, and since longer specials come first, a two-character -> takes priority over its one-character prefix -.

Delimiters (default: space, newline, tab) are consumed and discarded — they produce no segment.

Tokenization Algorithm

The tokenizer scans left to right, applying three cases at each position in order:

1. If any special token matches exactly at the current position, emit it as a segment and advance by its length. Because the list is sorted longest-first, this is always the longest possible special match.

2. If the entire remaining suffix is a strict prefix of some special token (but does not match any completely), emit it as a single segment with is_partial_special = true and stop. This case only fires when we are at the end of input, since otherwise there would be more characters to determine whether the match completes.

3. Consume characters one by one into a word token, stopping when:

   • a delimiter is reached
   • a complete special match starts at the current character
   • a partial-special prefix starts at the current character and there is a character-class transition from the previous character (word↔non-word boundary).

The character-class condition in case 3 is the critical subtlety.

DONE Type Inference

As we already explored, yhe type inference engine evaluates partial trees against the typing rules $\Theta$ attached to grammar productions.

The central judgment is $\Gamma \vdash_\Theta t : \mathcal{S}$, where $\mathcal{S}$ is a tree status in the lattice $$\{\text{Valid}(\tau), \text{Partial}(\tau), \text{TooDeep}, \text{Malformed}\}$$

Dispatch

Type checking is dispatched top-down from the root of the partial tree.

Completeness Promotion

This prevents permanently indeterminate states on finished subtrees. A complete, non-extensible subtree that cannot be assigned a definite type has definitively failed type checking.

Rule Application

When a non-terminal has an associated typing rule $\theta = (\text{premises}, \text{conclusion})$we can apply the following algorithm to resolve it.

1. Resolve bindings: compute $B = \text{resolve}(t, \theta)$ via runtime binding. Return $\text{Partial}$ if the target is at the frontier; return $\text{Malformed}$ if the structure is invalid.

2. Create unifier: initialize a unifier $U$ for meta-variable resolution.

3. Initialize context lanes: create named context maps. The primary lane is set by the conclusion’s context input, the first premise’s setting, or defaults to $\Gamma$.

4. Evaluate premises (in order): for each $p_i$, compute $\text{check_premise}(p_i)$:

   • Ok(G') updates the relevant context lane
   • Fail immediately returns Malformed
   • Partial sets a flag but evaluation continues since a later premise may still fail

5. If any premise was Partial: return $\text{Partial}(\top)$.

6. Evaluate conclusion: resolve the output type via the unifier and bindings, return $\text{Valid}(\tau)$.

7. Extract context transform: if the conclusion specifies $\Gamma \to \Gamma[x:\tau]$, build the extended context for sibling propagation.

The non-short-circuiting behavior on Partial premises (step 4) is deliberate: a Partial followed by a Fail should yield Malformed, not Partial.

Transparent Wrapper

Productions without typing rules are “transparent” to their child if they only have one, else they fail. This is done for convenience when writting grammars.

Type Cache

The cache is controlled by a thread-local flag (TYPE_CACHE_ENABLED, default true). Disabling it is useful for debugging but has significant performance cost on deep trees.

Meta-Variable Resolution

Meta-variables ($?A$, $?B$, etc.) are resolved via Hindley-Milner unification. The unifier maintains a substitution $\sigma: \text{MetaVar} \to \tau$ with the following invariants:

• Occurs check: $?X$ must not appear in $\tau$ before binding $?X := \tau$.
• Idempotent substitution: $\sigma(\sigma(\tau)) = \sigma(\tau)$.

$\top$ is treated as indeterminate in unification (not unified with concrete types), which is consistent with its role as “not yet determined” rather than “accepts everything.”

Resolution Pipeline

Type expressions undergo a two-stage resolution before use:

1. Meta resolution ($\text{solve_meta}$): substitute all bound meta-variables from the unifier’s substitution map.
2. Binding resolution ($\text{solve_binding}$): substitute all $\text{Atom}(x)$ variables with values read from the tree via the runtime binding system.

Subtyping

Equality is three-valued: $\text{equal}(\tau_1, \tau_2) \in \{\text{true}, \text{false}, \text{indeterminate}\}$. Indeterminate arises when either side contains $\top$, $\text{Path}(\cdots)$, or $\Gamma(x)$.

Depth Limit

The typing depth limit of 50 prevents infinite recursion on grammars with cyclic typing dependencies. It is bad design.

Context

WIP Premises

Premises are conditions above the line in a typing rule, evaluated left-to-right to thread the typing context.

Premise Result

Evaluating a premise yields a three-valued result:

• $\text{Ok}(\Gamma’)$: the premise holds. $\Gamma’$ is the modified context.
• $\text{Fail}$: the premise is definitively violated.
• $\text{Partial}$: the premise is undecided due to incomplete information.

This mirrors the tree status lattice. Typing constraints are deferred when information is missing.

Premise Types

Operation (Equality / Subtyping)

$\tau_1\ \text{op}\ \tau_2$ where $\text{op} \in \{=, \subseteq\}$.

• $\tau_1 = \tau_2$: unify the two types.
• $\tau_1 \subseteq \tau_2$: check the subtype relation.

Both use three-valued logic, returning $\text{Ok}$, $\text{Fail}$, or $\text{Partial}$.

Evaluation Order

Premises evaluate strictly left-to-right. The context from premise $i$ is input to $i+1$, unless in no-propagate mode. Premise ordering is semantically significant: reordering changes binding availability.

WIP Conclusion

The conclusion determines the rule’s result type and any modifications to the context $\Gamma$.

Source: src/logic/typing/eval.rs, src/logic/typing/rule.rs

Conclusion Kinds

Checking mode (void) is initiated by the Check premise $\Gamma \triangleright e$, not by a conclusion. All conclusions must return a type.

Type Conclusion

Context Lookup

Context Transform

DONE Completion

The completion pipeline takes a partial input string $s$ and produces a complete, well-typed expression in the language $L$ defined by grammar $G$. It is the core synthesis loop of Aufbau, the mechanism by which partial expressions are extended into valid programs.

The theoretical foundation for completability over two-level languages (where the grammar alphabet is itself a regular language over bytes) is developed in Completability and Regular Expressions.

This page is the roadmap for the completion subsection of the book. It is meant to be read linearly with the next three chapters in order: Synthesizer, Search, then Scoring. To avoid duplication, those chapters focus on one stage each instead of re-explaining the whole pipeline.

Pipeline Overview

The completion pipeline composes three components:

1. Synthesizer $\Sigma_s$: maintains incremental parsing state and exposes typed extension operations. Given input $s$ and a typing context $\Gamma$, it produces the set of type-valid next tokens.

2. Search: explores the space of token sequences that extend $s$ to a complete expression. The current implementation tries a greedy fast path first, then falls back to a priority-queue frontier.

3. Scoring: a heuristic function $|\sigma|: Q \to \mathbb{R}$ that ranks search states by estimated proximity to a valid completion. Guides the search toward promising branches.

The composition is:

$$\text{complete}(G, s, \Gamma) = \text{Search}(\Sigma_s(G, s), |\sigma|, \Gamma)$$

where $\Gamma$ is an optional external typing context.

Typed Completability

Recall from Basic Concepts that the completability set $\mathcal{C}_L(s) = \{a \in \Sigma : \exists s’ \in \Sigma^*, sas’ \in L\}$ is the set of valid next symbols. The completion pipeline computes a refined version:

$$\mathcal{C}_{L,\Theta}(s) = \{a \in \mathcal{C}_L(s) : \Gamma \vdash_\Theta \mathcal{F}(sa) \neq \text{Invalid}\}$$

This is the typed completability set, the set of next tokens that are both syntactically valid and consistent with all typing constraints. The type system explains why this refinement is always a subset of the syntactic completability set.

Data Flow

Input s ──→ Synthesizer ──→ completions_ctx ──→ Search loop
                │                                      │
                │            extend_with_regex ←───────┘
                │                   │
                └───────────────────┘
                        │
                  find_valid_completion ──→ Success / Exhausted

This diagram is intentionally high-level. The current implementation’s greedy fast path, beam-style child truncation, and local grounding preference are search-policy details described in Search.

Each iteration of the search loop:

1. Pops the highest-scored state from the priority queue
2. Checks whether the current typed forest already contains a complete root
3. If not, asks the synthesizer for completions_ctx at the current state
4. Extends the state with candidate tokens, scores and prunes the children, and pushes the survivors onto the queue

For the formal definition of completability over two-level languages (where terminals include regex patterns over $\Sigma_\text{vocab}$), including the Brzozowski derivative mechanism for partial token validation, see Completability and Regular Expressions.

Source Files

DONE Synthesizer

The synthesizer is the stateful interface between the parser and the search engine. It wraps incremental parsing with type-filtered extension operations, providing the search with a clean abstraction: given the current input, what are the valid next tokens?

Source: src/logic/partial/synth.rs

This chapter is meant to be read before Search. It only covers token generation and input extension; frontier management is described in Search, and numeric ranking is described in Scoring.

Definition

The synthesizer exposes the following operations:

Extension Semantics

Token Extension

The auto-separator is a syntactic heuristic, not a grammatical guarantee. It handles the common case where two adjacent identifiers or keywords require whitespace separation. The fallback to direct concatenation and explicit space ensures no valid extension is missed; at worst, the heuristic wastes one parse attempt.

Regex Extension

The candidate ordering is intentional: reusing grammar-derived literals and already-seen terminals tends to produce more coherent completions than inventing arbitrary new text. This is a heuristic for quality, not correctness; any valid candidate would produce a correct completion.

Step-by-step: building an expression token by token

This section traces exactly what the synthesizer does when the search engine calls extend repeatedly to build the expression let x = 1 from an empty input. The grammar assumed is a simple expression language where a let-binding has the form let <ident> = <expr>.

Initial state. The synthesizer starts with $s = \varepsilon$ (the empty string). partial() returns an empty forest; every nonterminal in $G$ is a candidate root. completions_ctx with any context will return the set of tokens that can begin a valid expression — including let.

Step 1: extend with let. The search engine calls extend(\texttt{"let"}, \Gamma). The auto-separator check sees $\text{last}(\varepsilon)$ is undefined so no separator is inserted. The MetaParser parses "let" and returns a partial forest with one active parse: a let-binding with three remaining holes (<ident>, =, <expr>). The synthesizer commits: $s \leftarrow \texttt{“let”}$.

After this step, completions_ctx returns only tokens that can extend "let" to a syntactically and type-valid string. In a well-designed grammar, that set consists entirely of identifiers matching [a-z][a-z0-9_]*.

Step 2: extend with x. The auto-separator check: $\text{last}(\texttt{“let”}) = \texttt{t} \in \mathcal{W}$ and $\text{first}(\texttt{“x”}) = \texttt{x} \in \mathcal{W}$, so a space is automatically inserted. The MetaParser parses "let x". The partial forest now has the <ident> hole filled; the remaining holes are = and <expr>. The synthesizer commits: $s \leftarrow \texttt{“let x”}$.

completions_ctx now returns only =, since that is the only token that can advance the let-binding parse.

Step 3: extend with =. $\text{last}(\texttt{“let x”}) = \texttt{x} \in \mathcal{W}$, $\text{first}(\texttt{“=”}) = \texttt{=} \notin \mathcal{W}$, so no auto-separator. The MetaParser parses "let x =". The partial forest has one hole remaining: <expr>. The synthesizer commits: $s \leftarrow \texttt{“let x =”}$.

completions_ctx with a typing context $\Gamma$ now filters: any token that begins a valid expression and whose eventual type is compatible with the binding context. Numeric literals (1, 2, …) and any bound variable in $\Gamma$ are valid.

Step 4: extend with 1. $\text{last}(\texttt{“let x =”}) = \texttt{=} \notin \mathcal{W}$, no auto-separator. The MetaParser parses "let x = 1". The partial forest now contains a complete parse rooted at the let-binding nonterminal. complete() returns Some(root). The search engine can now stop on this state.

The display in the widget mirrors what the synthesizer’s internal state looks like at each step: the accumulated string $s$, which holes in the parse tree have been filled, and what remains. Clicking any offered token fires a Web Audio blip and advances the state exactly as extend would.

Depth Retry

DONE Search

The search engine explores the space of token-level extensions to find a complete, well-typed expression. It uses a priority queue ordered by a heuristic scoring function.

Source: src/logic/search/mod.rs

This chapter is meant to be read after the completion overview and synthesizer chapters. It only describes search-side control flow: frontier management, pruning, and stopping conditions. Token generation lives in Synthesizer; the numeric heuristic itself lives in Scoring.

Operational Shape

Search Space

Algorithm

The module is documented as “Priority-guided DFS search.” This name is historical and relative: the predecessor algorithm was pure BFS, expanding every completion at every depth level before proceeding to the next. The current algorithm replaced that with a BinaryHeap (max-heap), making it structurally more depth-oriented in practice since high-scoring deep states are preferred over low-scoring shallow ones. This label applies to the heap-driven second phase; the greedy fast path runs before any frontier is built.

However, it is not true DFS. True DFS uses a stack (LIFO) and commits to fully exploring one branch before backtracking. This algorithm uses a priority queue: the next state popped is always the globally highest-scored state, regardless of which branch produced it. It freely interleaves exploration across branches whenever a state from a different branch scores higher than the current branch’s frontier. The depth bound $d_{\max}$ is a safety cutoff, not a stack discipline.

Concretely: if branch $A$ at depth 3 scores $2.1$ and branch $B$ at depth 1 scores $2.3$, the algorithm explores $B$ next. True DFS would continue with $A$. The algorithm makes no commitment to a single branch.

Formally, this is best-first search (BeFS) with scoring function $|\sigma|$. The “DFS” label reflects the intent (explore depth before breadth, relative to the predecessor) not the mechanism.

Configuration

Result

Search-Side Checks

The search code itself performs only lightweight checks. The meaning of the attached types comes from earlier chapters and from partial_typed_ctx; this chapter only documents what the search layer does with those typed forests.

State Deduplication

The search maintains a HashSet<String> keyed by the reconstructed surface input tree.text() of each state. Two states with identical reconstructed inputs are considered equivalent, even if they arrived via different token paths. This prevents re-exploration of states that parse the same surface string.

For how the surviving states are numerically ranked, continue to Scoring.

DONE Scoring

The scoring function $|\sigma|$ assigns a real-valued score to each search state, guiding the best-first search toward promising completions. This chapter documents only the numeric heuristic in calculate_score(). Deduplication, grounding preference, greedy completion, and beam truncation are search-policy details described in Search.

Source: src/logic/search/scoring.rs

This chapter is meant to be read after Search.

Score Tuple

Several components choose the best or shallowest root among alternatives rather than averaging over all roots. This is intentional: one promising parse alternative should be able to dominate the score early instead of being drowned out by worse siblings.

Sub-Score Definitions

Completeness

Expression nodes with children do not add direct bonus here; they only contribute through their descendants while still increasing the denominator. So the score prefers states with more concrete material and fewer empty placeholders.

Production Fullness

This rewards roots whose productions are already mostly filled, even if the tree is not yet complete.

Token Length Bonus

Open Slots Penalty

This is the dominant negative signal in practice: trees with fewer remaining holes tend to outrank structurally larger but more incomplete alternatives.

Simplicity

Recursion Penalty

Ordering

DONE Completability

This chapter formalizes the completability properties that Aufbau guarantees, connecting the theoretical definitions from Basic Concepts to the algorithmic implementation.

For the treatment of completability over two-level languages, where the grammar alphabet $\Sigma$ is itself a regular language over a byte alphabet $\Sigma_\text{vocab}$, see Completability and Regular Expressions.

Source: src/validation/completability.rs

Typed Completability

Recall from Basic Concepts that a string $s$ is completable in $L$ if $\mathcal{C}_L(s) \neq \emptyset$. The typing engine (see Type System) refines this:

Completion

Prefix Soundness

Condition 1 alone is insufficient. Consider an input like let x : int in. The body expression has not started, so the typed completion set may depend on the body’s grammar structure, which is complex to compute from scratch. But the partial tree itself is still consistent: the let-binding is well-formed so far, and the body is simply missing. Condition 2 catches these cases by checking the current tree status rather than demanding that forward extensions exist.

Two-Level Completability

The grammar alphabet $\Sigma$ contains elements that are themselves languages over a finer alphabet. String literals match single strings, but regex patterns like /[a-z][a-zA-Z0-9]*/ match sets of strings. This creates a two-level language structure:

$$L \subseteq \Sigma^* \quad \text{where} \quad \Sigma \subseteq \Sigma_\text{vocab}^*$$

The partial parser $\Phi_L$ operates at the $\Sigma$ level, but the actual input arrives at the $\Sigma_\text{vocab}$ level (bytes, characters, or model vocabulary tokens). A partial input may be in the middle of a token: the string bi is a prefix of the token /b(u|o|i)p/ but is not itself a token.

The Brzozowski derivative $D_s(r)$ resolves this: given a regex $r$ and a partial string $s$, the derivative $D_s(r)$ is a new regex matching exactly the valid suffixes of $s$ in $L(r)$. If $D_s(r) \neq \emptyset$, then $s$ is a valid prefix of some string in $L(r)$.

This is formalized in detail in Completability and Regular Expressions. The implementation lives in the custom regex engine at src/regex/.

DONE Validation

The validation system verifies that Aufbau’s engines produce correct results. It is the empirical counterpart to the formal properties defined in Completability: where the spec defines what must hold, the validation system checks that it holds on concrete grammars and inputs.

Source: src/validation/

Architecture

The validation system has three layers:

Layer 3: Test Suites (per-grammar: arithmetic, stlc, fun, imp, ...)
    │
    ▼
Layer 2: Test Harness (typed completion test runner, timeout, profiling)
    │
    ▼
Layer 1: Core Algorithms (completability.rs → search → scoring)

Layer 1 is the completion pipeline and the completability checker, i.e., the same algorithms used in production. The validation system does not use separate “test” algorithms; it validates the real pipeline.

Layer 2 is a test harness that wraps Layer 1 with:

• Per-test configuration (depth budget, initial context, expected pass/fail)
• Timeout enforcement (default: 300 seconds per test)
• Prefix soundness checking (verifying all prefixes, not just the final input)
• Profiling metadata (timing, states explored, visited states)

Layer 3 is a collection of test suites, each targeting a specific grammar from examples/*.auf.

What is Validated

Prefix Soundness

The primary property validated is prefix soundness: for a given input $s$ and grammar $G$, every prefix of $s$ must be typed-completable. This is checked by sound_complete, which:

1. Enumerates all non-whitespace prefixes of $s$
2. For each proper prefix: parses it, computes typed completions, and calls prefix_ok
3. For the full input: runs the complete search to find a valid completion
4. Reports the first failing prefix (if any)

A completion system that can find completions for let x : int in x but not for let x : int in is broken: the system would accept a token that leads to a dead end. Prefix soundness catches this class of bugs by testing every intermediate state.

Expected Failures

Tests can be marked xfail (expected to fail completion). This is used for inputs that are intentionally outside the grammar’s typed language. An xfail test passes if completion fails, and fails if completion unexpectedly succeeds.

Timeout Enforcement

Each test runs in a dedicated thread with a configurable timeout. This catches performance regressions and infinite loops in the search: if the search cannot find a completion within the time budget, the test fails with a timeout diagnostic.

Test Structure

Each grammar has a dedicated test module:

Parseability Checking

A separate, faster validation layer checks parseability: whether all prefixes of an input can be parsed at all (without completion search). This runs in $O(n^2)$ time (one parse per prefix) and catches parser bugs independently of the type system.

Complexity Analysis

The validation system includes an empirical complexity measurement module that determines the parse-time exponent $k$ in $O(n^k)$ via log-log linear regression over increasing input sizes. This is used to detect performance regressions and to empirically verify that the parser operates within expected complexity bounds.

WIP Implementation Map

This page maps the specification sections to source code modules.

Module Structure

Auxiliary Modules