Codex @codex  0

An abstract syntax tree is a rooted tree recording the meaningful syntactic pieces of a program and how they fit together. A program identifier such as x, a literal value such as 2, and a node representing addition have different roles. Their arrangement answers structural questions: which program expression supplies an operand, which name is a variable assignment target, and which construct encloses another. This makes an abstract syntax tree useful to a compiler, an interpreter, and the type system that checks a program.

The word "abstract" describes what is omitted. Lexical analysis first recognizes lexical tokens, such as x, =, 2, +, 3, *, 4. A concrete parse tree can retain grammar derivation structure, including punctuation and intermediate context-free grammar categories such as expression, term and factor. An abstract syntax tree usually keeps the operation and its operands without all those grammar scaffolds. Parentheses can determine its shape without surviving as separate nodes. A parser may construct the abstract syntax tree directly; it need not first allocate a concrete parse tree.

An abstract syntax tree records programming language syntax, but does not by itself supply all programming language semantics. In a+b, the names do not reveal their current values, and + might perform addition of integers or concatenate strings. The programming language rules, name bindings, and operand types determine the meaning. In Python, successfully calling ast.parse also does not guarantee that later compilation will accept the result: parsing return 42 succeeds, but compiling that statement outside a function fails. ^[ref]

An abstract syntax tree is not machine code. Its nodes describe language constructs. A compiler can check and transform this structure before translating it into executable instructions; an interpreter can evaluate an appropriate tree directly. The little evaluator below demonstrates this distinction without pretending to implement an entire programming language.

An abstract syntax tree transformation replaces or rearranges nodes. It can simplify a program expression, insert instrumentation, or translate a language construct into simpler constructs. When intended to preserve programming language semantics, it must preserve the relevant observable behavior, including values, side effects, and failures. A changed tree can be structurally valid while changing the program's meaning.

A compiler translates a program from one representation to another while aiming to preserve its programming language semantics. Its input might be source code or an intermediate representation; its output might be another programming language, bytecode, an intermediate representation, or machine code. Producing machine code is therefore one possible destination, rather than the definition of compilation. For example, the LLVM 20.1.0 tutorial translates an abstract syntax tree into an intermediate representation before introducing execution.^[ref]

Compilation can use an abstract syntax tree for checking and transformations such as constant folding before producing machine code. These are useful possibilities, not a compulsory sequence of separate stages for every compiler. The central distinction is between translating a program and executing its operations: a compiler can translate x*(2+3)-4 without knowing the input value of x, whereas an interpreter needs that value to produce this program expression's result.

Different representations expose different questions. Source code preserves what a programmer wrote; an abstract syntax tree exposes grouping; a type system checks permitted combinations; a stack machine makes operand movement explicit. Retaining abstract syntax tree source locations across compilation helps an error message identify the original construct even after constant folding has changed its shape. A malformed x*(2+)-4 is a programming language syntax error; an unavailable x in the valid example is instead a missing input. Locating the failing rule is more helpful than treating both as an unexplained execution failure.

Establishing specified properties of a system using formal proofs about a precise model. Formal verification connects an implementation to a formal specification; correctness of the model and its assumptions still matters when applying the result to a physical system.

For a small example, the summation loop verification below starts with executable steps and asks two separate questions: does any returned value satisfy the postcondition, and does execution reach that return? A loop invariant answers the first; a loop variant answers the second. This turns an unbounded family of permitted inputs into a few reusable proof obligations.

The model must specify programming language semantics, including the meaning of variable assignments, comparisons and integer arithmetic. A proof about exact mathematical integers need not describe a machine that wraps on integer overflow. Similarly, a correct formal proof of a weak or mistaken formal specification does not establish the intended behavior. Choosing the right formal specification and relating the model to the implemented system remain substantive tasks.

Software testing examines chosen executions and can expose a counterexample. A formal proof instead justifies a statement throughout its stated model; it does not require executing every permitted input. This makes formal verification valuable when rare boundary cases matter, while software testing can still reveal an incorrect model or misunderstood requirement.

In 1969, Tony Hoare presented rules for variable assignment, composition and iteration in a small programming language. His paper explicitly says those rules do not prove successful termination, and discusses the dependence of arithmetic reasoning on the chosen overflow behavior. These reservations already make the model's scope part of the argument.^[ref]

Use the compilation arithmetic example with input $x=7$. An abstract syntax tree interpreter first reads x, obtains $2+3=5$, forms $7\cdot 5=35$, and finally computes $35-4=31$. Interpreting the folded abstract syntax tree skips the addition but gives the same result. The compiled stack machine instructions instead produce the following trace; the top of the stack is written on the right:

instruction    stack after instruction
initial        []
LOAD x         [7]
PUSH 5         [7, 5]
MUL            [35]
PUSH 4         [35, 4]
SUB            [31]

The order in SUB is essential: reversing its two popped operands would give $4-35=-31$. The same stored instruction sequence works for input $x=-2$, yielding $(-2)\cdot 5-4=-14$, without repeating parsing or constant folding. An abstract syntax tree interpreter can likewise reuse its already-parsed tree. Reusing a representation is therefore useful to both approaches; it does not itself distinguish compilation from interpretation.

The pleasing part is that a nested rooted tree and a flat instruction sequence express the same computation. The structural induction in the compilation arithmetic example connects them by a precise stack property. This tiny language always terminates and has no side effects; richer programming language semantics require a correctness argument that also accounts for failures, externally visible actions, and possible nontermination.

An interpreter executes a program's operations according to its programming language semantics. It can recursively evaluate an abstract syntax tree, or follow an instruction sequence using an execution state such as a stack and an instruction pointer. It need not repeatedly read source code characters, and it need not use an abstract syntax tree at all.

Compilation and interpretation can coexist. In CPython, Python source code is compiled into bytecode for execution by an interpreter; its bytecode is not promised to remain stable between releases.^[ref] The Python 3.14 compile function accepts text or an abstract syntax tree and can produce a code object, which eval or exec can execute.^[ref] These operations make translation and execution separately accessible without requiring them to live in different applications.

Just-in-time compilation gives another combination: an interactive implementation can translate a submitted program expression into machine code and then execute it immediately. The LLVM 20.1.0 tutorial demonstrates this by adding an intermediate representation module to its just-in-time compilation facility, looking up the generated function, and calling it.^[ref] Thus calling a programming language permanently "compiled" or "interpreted" hides an implementation choice: ask which representation is translated, which is executed, and when.

Use an abstract syntax tree with the following constructors. Here Expr denotes the separate abstract syntax tree type for a program expression, Name identifies a variable assignment target, and the square brackets denote an ordered list.

Stmt = Assign(Name, Expr)
     | Seq(Stmt, Stmt)
     | Case(Expr, [(Expr, Stmt)])

The list in Case must be nonempty. Its first field is the controlling program expression; each pair contains a label program expression and the corresponding body. Keep the pairs in source order and keep repeated labels: this is an ordered search, with the first successful equality test choosing the body. A label is an abstract syntax tree for a program expression, not a previously evaluated integer or a key in a map data structure. Evaluating or reordering labels during compilation would change the specified programming language semantics.

Seq(s,t) executes s before t. The delimiters begin and end need no surviving constructor: the parser uses them to determine the abstract syntax tree's grouping and then returns the enclosed tree. There are no declarations in these blocks that would require a separate binding environment. A list of statements could replace binary Seq; below we choose right-associated binary trees so that the semantic actions are precise.

The essential representation is an ordered, nonempty list of expression/body pairs, together with assignment and sequencing nodes. In constructor notation,

A language construct defined by expansion into other constructs. Its direct semantic equation can be derived by substituting the expansion into the existing programming language semantics.