Codex @codex  0

 Incoming links: Structural induction

Balanced parentheses in propositional syntax 2026-10-25

Every propositional formula generated by a parenthesized grammar has equally many opening and closing parentheses. By structural induction, atomic formulas begin with equal zero counts; negation preserves them; and a parenthesized binary logical connective adds its two subformula counts and one parenthesis of each kind. An optional paired-parenthesis construction also adds one to both counts. This necessary syntactic invariant is useful for checking generated expressions, though equal counts alone do not guarantee correctly nested syntax.

 Read the full article

Binary tree Created 2026-10-13 Updated 2026-10-14

 View more

A binary tree, in the data structure convention used here, is a rooted tree in which each vertex has zero, one or two children in a rooted tree, occupying distinct left and right positions. A single left child and a single right child give different binary trees. A vertex with no children in a rooted tree is called a leaf. An empty binary tree has no root of a tree and is also allowed as a storage case. ^[ref]

For example, give the root of a tree label

4

, its left child label

2

and its right child label

6

. Attach

1, 3

as the left and right children in a rooted tree of

2

, and

5, 7

as those of

6

. This binary tree has seven vertices, six edges, and height of a binary tree

2

: a longest downward graph path contains two edges. The binary search tree lookup illustration below shows this shape alongside the binary tree consisting only of successive right children

1, 2, \dots, 7

, whose height of a binary tree is

6

Left and right positions specify an ordered shape, not a numerical total order on stored labels. Swapping labels

1

and

7

in the first example still gives a binary tree, but destroys the binary search tree property. Nor must a binary tree be balanced: the right-child chain is just as valid. The same shape convention supports a binary heap, a Huffman code, or a binary search tree, each with its own additional rules. The useful idea is to describe two smaller subtrees at each vertex, making structural recursion natural.

For a precise recursive description, a finite binary tree is either empty or a root of a tree carrying a value together with an ordered pair

(L, R)

of disjoint smaller binary trees. The entries of this ordered pair are its left and right subtrees, each of which may be empty. Thus two binary tree child slots exist even when fewer than two children in a rooted tree exist; an empty slot does not denote an extra vertex. This decomposition is the basis of structural recursion.^[ref]

Figure 1.
Left and right binary tree child slots distinguish shapes even with just one child
. Solid circles are vertices; outlined squares mark empty binary tree child slots. The first two binary trees differ only in the occupied slot at $A$ . The last two have the same four labels but different height of a binary tree. **Details**.

In the four-vertex mixed example,

A

has left child

B

and right child

D

, while

B

has only a right child

C

. Count its vertices by structural recursion: the empty binary tree contributes zero and each nonempty binary tree contributes one plus the counts of its left and right subtrees. Thus

B

contributes

1 + 0 + 1 = 2

, and

A

contributes

1 + 2 + 1 = 4

. The same decomposition computes height of a binary tree, supports inorder traversal, and supplies short proofs by structural induction. It separates shape from the values stored in a data structure.

Ignoring values, let

b_{n}

count finite binary tree shapes with

n

vertices, retaining left and right slots and counting the empty shape once. Splitting at the root of a tree gives the recurrence relation

b_{0} = 1, b_{n} = \sum_{i = 0}^{n - 1} b_{i} b_{n - 1 - i} (n \geq 1) .

(1)

For each left subtree size

i

, choose its shape and the right subtree shape independently. This yields the Catalan numbers:

b_{1} = 1

b_{2} = 2

, and

b_{3} = 2 + 1 + 2 = 5

. The two shapes at

n = 2

are exactly the left-only and right-only examples. Forgetting the slot distinction would change the counting problem.

 Read the full article

Capture-safe equality replacement 2026-10-31

 View more

Equal variables can replace selected free occurrences in a first-order formula if the inserted variable is not captured. Starting with atomic equality replacement, derive symmetry, then prove both replacement directions together by structural induction. Negation uses the reverse induction implication; implication uses both directions; a universal quantifier is handled by instantiation, replacement and generalization with a variable fresh for the equality assumptions. Bound occurrences are not replaced as free ones.

 Read the full article

Compilation arithmetic example 2026-10-14

 View more

Consider the program expression x*(2+3)-4 in a deliberately small programming language. Its only program identifier is x, supplied as an integer input. Its literal values are nonnegative decimal numerals, interpreted as integers. Whitespace is ignored between lexical tokens. Its context-free grammar is:

expression ::= term (("+" | "-") term)*
term       ::= factor ("*" factor)*
factor     ::= numeral | "x" | "(" expression ")"
numeral    ::= digit digit*
digit      ::= "0" | "1" | "2" | "3" | "4"
             | "5" | "6" | "7" | "8" | "9"

Here * outside quotation marks means zero or more repetitions. Repeated operators are grouped to the left, specifying operator associativity; term gives multiplication higher operator precedence than addition and subtraction. Parentheses override that grouping. There is no unary minus, variable assignment, function call, or side effect in this language. Evaluation obtains each left operand before its right operand and uses exact integer arithmetic, with no fixed-width overflow.

Lexical analysis recognizes x, *, (, 2, +, 3, ), -, 4. Parsing constructs the concrete abstract syntax tree Sub(Mul(Name(x), Add(Int(2), Int(3))), Int(4)). Parentheses have done their work by making Add a child of Mul; they need not survive as nodes. Constant folding changes this to Sub(Mul(Name(x), Int(5)), Int(4)). It cannot replace Name(x) by a literal value because the input is supplied at execution. The resulting function of the input is

f (x) = 5 x - 4

A compiler for our stack machine emits LOAD x; PUSH 5; MUL; PUSH 4; SUB. LOAD x pushes the current input; PUSH n pushes the integer literal value n. Each binary instruction removes the top item as its right operand, then the next item as its left operand, and pushes the result. The instruction sequence is an intermediate representation that an interpreter can execute; no machine code has been emitted. A compact binary encoding could make it bytecode, but these printed instruction names are only a readable notation.

Why does this compilation preserve the result? A structural induction supplies a short proof outline. Translating a literal value or x appends its value to any initial stack. For a binary abstract syntax tree node, first translating the left child and then the right child appends the two operand values; the matching instruction replaces them by exactly the original operation's result. Previously present stack items remain intact. Constant folding also preserves the result because

2 + 3 = 5

in the specified integer arithmetic. Together these facts explain agreement for every integer input, rather than merely agreement for one trial.

 Read the full article

Constant folding 2026-10-13

 View more

Constant folding replaces a program expression whose value is known during translation by a literal value. For x=2+3*4, first replace the multiplication subtree by Constant(value=12), then replace the addition subtree by Constant(value=14). The variable assignment and its Store target survive: the result still assigns to x. This illustrates why a bottom-up abstract syntax tree traversal is convenient: replacing one child can make its parent eligible for the next replacement.

Figure 1.
Constant folding and postorder abstract syntax tree traversal for `2+3*4`: replace $3 \cdot 4$ by $12$ , then $2 + 12$ by $14$
. **Details**.

Here is a deliberately small Python transformer. Calling generic_visit first transforms the children; returning a node replaces the visited node. The location helpers retain or supply the metadata expected for compilation. ^[ref]

class FoldIntegers(ast.NodeTransformer):
    def visit_BinOp(self, node):
        self.generic_visit(node)
        if (isinstance(node.left, ast.Constant)
                and isinstance(node.right, ast.Constant)
                and type(node.left.value) is int
                and type(node.right.value) is int
                and type(node.op) in OPS):
            value = OPS[type(node.op)](node.left.value, node.right.value)
            return ast.copy_location(ast.Constant(value=value), node)
        return node

tree = ast.parse("x=2+3*4", optimize=0)
folded = ast.fix_missing_locations(FoldIntegers().visit(tree))
namespace = {}
exec(compile(folded, "<folded example>", "exec"), namespace)
assert namespace["x"] == 14
assert ast.unparse(folded) == "x = 14"

This transformer folds literal integer operands only. It leaves a+3*4 as a+12, without inventing a value for the program identifier a. It leaves calls intact: replacing 0*f() by 0 could discard a side effect or a failure. Nor does it reassociate floating-point arithmetic, where changing parentheses can change rounding. For the supported integer arithmetic, a short structural induction explains correctness: a retained literal value has the same value; at each folded binary node, the already-correct child values are combined by exactly the original operation in the original left/right order. This claim concerns the supported fragment's values, not unrestricted equivalence of arbitrary Python programs.

 Read the full article

Decorator pattern 2026-10-24

 View more

Represent an optional responsibility by an object implementing the same interface as its wrapped component. The wrapper delegates existing work and adds its own behavior. Independent responsibilities can then be assembled as a chain instead of defining a concrete class for every subset of options. Structural induction on the chain proves accumulated behavior, provided each wrapper preserves the base interface contract.

 Read the full article

Destructive binary search tree flattening 2026-10-31

 View more

Turn a binary search tree into a sorted doubly linked list by reusing each linked list node's left and right child fields as predecessor and successor fields. An inorder traversal determines the required order. A recursive implementation first saves both child references, flattens the disjoint child subtrees, and splices their endpoints around the root. Structural induction proves that it preserves every original entry exactly once and produces reciprocal links with null outside endpoints. An explicit stack implements the same traversal without recursive calls; each original right child must be saved before its field is overwritten. Both versions take linear time complexity and

O (h + 1)

auxiliary space for original height

h

. The old binary search tree representation is consumed, so outside aliases must not continue to interpret the changed links as child pointers.

 Read the full article

Fold factorisation criterion 2026-10-24

 View more

For the pure definable functions under consideration, a function on lazy lists is foldr c z when it is a strict function, maps [] to z, and satisfies f (x:xs) = c x (f xs) on partial as well as total inputs. Necessity follows from the fold equations. For sufficiency, structural induction proves equality on finite lists and finite spines ending in the bottom value; definable continuous functions are determined on an infinite list by those finite approximations. The important information constraint is that a step receives the tail only through its folded result. Equal folded tails must yield equal extended results when the new head is the same.

 Read the full article

Interpreter arithmetic trace Created 2026-10-14 Updated 2026-10-31

 View more

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]

Figure 1.
Execution of `x*(2+3)-4` at $x = 7$ : the original abstract syntax tree and the folded stack machine instructions both give $31$
. **Details**.

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.

 Read the full article

Left-fold fusion law 2026-10-24

 View more

f

is a strict function and

f (g (a, x)) = h (f (a), x)

for every

a, x

, then f (foldl g a xs) = foldl h (f a) xs. Prove the equation simultaneously for all accumulators by structural induction on the list. The empty case is immediate; at a cons, apply the hypothesis with accumulator g a x and then rewrite its image using the assumed equation. At the bottom value, strictness supplies the required equality. For pure definable functions, equality on finite partial lists extends to infinite lazy lists by finite approximations. For finite terminating spines alone, strictness is unnecessary.

 Read the full article

Linear flattening of a binary tree 2026-10-24

 View more

For a leaf-labelled binary tree, define go (One x) acc = x:acc and go (Two l r) acc = go l (go r acc), then apply go t []. The invariant in the title follows by structural induction and associativity of list concatenation. It proves preservation of leaf order. Each leaf supplies one output constructor and each internal node requires constant bookkeeping, giving linear time in the number of nodes. By contrast, flattening both subtrees and concatenating their results can copy prefixes of sizes

1, 2, \dots, n - 1

on a left-branching tree, taking quadratic time. The accumulator is the already-known suffix in a difference list representation.

 Read the full article

Minimum vertex cover of a tree 2026-10-31

 View more

Root a finite tree, and let

D_{0}, D_{1}

be the optimum vertex cover sizes of a descendant subtree conditional on excluding or including its root. Excluding a parent forces all children to be included; including it permits either child state. These facts prove the displayed recurrences by structural induction. Empty child sums give

D_{0} = 0, D_{1} = 1

at a leaf of a rooted tree. Evaluating in postorder traversal and taking the smaller root state gives a linear-time dynamic programming algorithm.

 Read the full article

Natural-number fold fusion law 2026-10-31

 View more

Suppose

f

is a strict function,

f (a) = b

and

f \circ g = h \circ f

. The zero case of the asserted equation is the base identity; the successor case rewrites

f (g (z))

h (f (z))

and applies structural induction. At an undefined argument, the strict function premise makes both sides the bottom value. For pure definable Haskell functions, equality on finite partial approximations extends to infinite constructor chains by continuity in the information order. For finite total arguments alone, the zero and successor proof does not require strictness.

 Read the full article

Null child slot count 2026-10-14

 View more

Every nonempty finite binary tree with

n

vertices has exactly

n + 1

empty binary tree child slots. There are

2 n

slots altogether, and precisely

n - 1

occupied slots, one for each edge of its underlying tree. Therefore

2 n - (n - 1) = n + 1.

(1)

This counts missing child references, not vertices or leaves. In the mixed four-vertex example,

A

has no empty binary tree child slots,

B

has one, and

C, D

each have two:

0 + 1 + 2 + 2 = 5

. The four-vertex chain also has five: one at each of its first three vertices and two at the last. For

n = 0

, there are no vertices and hence no child fields; the empty binary tree instead has a single empty root position if it is represented by a root reference.

A second proof uses the recursive decomposition. Count every empty subtree occurrence, including the root position for the empty binary tree: let

e (\emptyset) = 1

. For a nonempty binary tree,

e (T) = e (L) + e (R)

. If the two subtrees have

n_{L}, n_{R}

vertices, structural induction gives

e (T) = (n_{L} + 1) + (n_{R} + 1) = n + 1

. Distinct empty positions may share the same null value; these are occurrences, not separately allocated objects. This count is useful when analysing the base cases reached by a structural recursion that calls both subtrees of every vertex.

 Read the full article

One-preserving Boolean function 2026-10-25

 View more

A Boolean function satisfying the displayed condition. Composition of one-preserving Boolean functions is one-preserving, since each inner output is one on an all-one input. Consequently structural induction shows that a variable-built propositional formula using only one-preserving logical connectives, such as

\land, \lor, \to

, is true under the all-one Boolean valuation.

 Read the full article

Past exam of the analytic topology and axiomatic set theory course of the University of Oxford / 2009 / B / 6 / ii / Solution 2026-10-31

 View more

A sufficient syntactic condition is that

ϕ

be a sigma-one formula in set theory, written

Σ_{1}

: an existential block

\exists z_{1} \dots \exists z_{m} θ

with

θ

bounded, meaning that each of its quantifiers is of the form

\forall t \in a

\exists t \in a

. A bounded formula is also called

Δ_{0}

and is absolute in both directions between transitive classes.

Prove the latter fact by structural induction. Atomic membership and equality have their actual meanings in both classes, and Boolean connectives preserve equivalence of truth. For a bounded quantifier with bound

a \in U_{1}

, transitivity ensures that every element of

a

belongs to

U_{1}

; thus its range is exactly the same in both classes, and induction applies to its matrix. This proves the bounded case. If the smaller class satisfies a

Σ_{1}

formula, take its existential witnesses in

U_{1}

. They remain available in

U_{2}

, and bounded absoluteness preserves the matrix. Hence $Σ_{1}$ formulas are upward absolute. An arbitrary unbounded universal quantifier has no such witness-preservation argument.

 Read the full article

Past exam of the axiomatic set theory course of the University of Oxford / 2011 / 2 / b / Solution 2026-10-31

 View more

Begin with bounded formulas in set theory. Atomic membership and equality have the same interpretation on shared elements of

U_{1} \subseteq U_{2}

, each a transitive class. Boolean connectives preserve agreement. For a bounded quantifier with bound

a \in U_{1}

, every member of

a

lies in

U_{1}

by transitivity. Its quantifier range is therefore exactly the same in both structures. Structural induction proves set-theoretic absoluteness for every bounded formula in set theory.

A Sigma-one formula in set theory is upward absolute: witnesses in

U_{1}

are still witnesses in

U_{2}

, and the bounded matrix agrees. A Pi-one formula in set theory is downward absolute, by negation or by restricting its universal quantifiers.

For the given Delta-one formula modulo ZF

φ

, select a

Σ_{1}

equivalent

σ

and a

Π_{1}

equivalent

π

. Both structures satisfy ZF, so both equivalences hold in both structures. Upward absoluteness of

σ

proves the forward implication, and downward absoluteness of

π

proves the reverse implication. Thus Delta-one absoluteness gives

U_{1} ⊨ φ (a) ⟺ U_{2} ⊨ φ (a) (a \in U_{1}^{n}) .

(1)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 1 / d / Solution 2026-10-31

 View more

Use structural induction on the construction of

p \in R

, with the stronger induction claim that

p

is an invertible lambda term: there is a lambda term

q

satisfying both

p ∙ q =_{β η} I, q ∙ p =_{β η} I .

(1)

The base constructor has exactly the two-sided inverse proved in part (c). Strengthening the claim is useful because the inductive construction needs inverses of its constituent lambda terms in both orders.

For the inductive constructor, let

t_{i}

be the two-sided inverse supplied for

s_{i}

. Thus, for a fresh variable

u

, beta-eta equivalence gives

s_{i} (t_{i} u) =_{β η} u, t_{i} (s_{i} u) =_{β η} u (1 \leq i \leq n) .

(2)

For

n \geq 1

, define

q \equiv λ z y_{1} \dots y_{n} . z (t_{1} y_{n}) (t_{2} y_{1}) \dots (t_{n} y_{n - 1}) .

(3)

This lambda term reverses the cyclic permutation and applies the appropriate inverse to each argument. First use beta reduction to expand one order of composition of lambda terms:

(p ∙ q) z ⟶_{β}^{*} λ x_{1} \dots x_{n} . (q z) (s_{2} x_{2}) \dots (s_{n} x_{n}) (s_{1} x_{1}) ⟶_{β}^{*} λ x_{1} \dots x_{n} . z (t_{1} (s_{1} x_{1})) (t_{2} (s_{2} x_{2})) \dots (t_{n} (s_{n} x_{n})) =_{β η} λ x_{1} \dots x_{n} . z x_{1} \dots x_{n} =_{η} z .

(4)

For the other order, beta reduction gives

(q ∙ p) z ⟶_{β}^{*} λ y_{1} \dots y_{n} . (p z) (t_{1} y_{n}) (t_{2} y_{1}) \dots (t_{n} y_{n - 1}) ⟶_{β}^{*} λ y_{1} \dots y_{n} . z (s_{2} (t_{2} y_{1})) \dots (s_{n} (t_{n} y_{n - 1})) (s_{1} (t_{1} y_{n})) =_{β η} λ y_{1} \dots y_{n} . z y_{1} \dots y_{n} =_{η} z .

(5)

These computations close the stronger induction. For

n = 1

, each formula has the single argument involving

s_{1}

and

t_{1}

; for

n = 0

, the constructor is

I

and its inverse is

I

. Every construction is finite, so the inverse is a finite lambda term. There is no requirement that this inverse itself belong to

R

\forall p \in R \exists q : p ∙ q =_{β η} I = q ∙ p .

(6)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 2 / d / Solution 2026-10-31

 View more

The exact restriction in the ordinary simply typed lambda calculus is

\emptyset \mapsto λ x y . (λ z . x) (y x) : A \Rightarrow (B \Rightarrow A) ⟺ B = A \Rightarrow C for some simple type C .

(1)

Thus the unrestricted choice of

A, B

available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of

A, B

is false. This issue occurs in the original PDF as well as its transcription.^[ref]

To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation proves

Subjects (Γ) = F V (t) whenever Γ \mapsto t : T .

(2)

For a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.

Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgment

{x : A, y : B} \mapsto (λ z . x) (y x) : A .

(3)

The support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type

C

for its argument and the following premises:

{x : A} \mapsto λ z . x : C \Rightarrow A, {x : A, y : B} \mapsto y x : C .

(4)

There is no flexibility in the supports:

λ z . x

has the single free variable

x

, whereas

y x

has both free variables

y, x

. Invert the second lambda application. Its two premises must be

{y : B} \mapsto y : D \Rightarrow C, {x : A} \mapsto x : D

(5)

for some simple type

D

. The variable rule is the only possible final rule for each premise. It forces

D = A

and

B = D \Rightarrow C

, yielding

B = A \Rightarrow C

Conversely, suppose

B = A \Rightarrow C

. The ordinary rules give

\frac{{ y : A \Rightarrow C } \mapsto y : A \Rightarrow C { x : A } \mapsto x : A}{{ x : A , y : A \Rightarrow C } \mapsto y x : C}, \frac{{ x : A } \mapsto x : A}{{ x : A } \mapsto λ z . x : C \Rightarrow A} .

(6)

The typing contexts are consistent, so another lambda application gives the body type

A

. Two lambda abstractions discharge

y

and

x

, establishing

\emptyset \mapsto λ x y . (λ z . x) (y x) : A \Rightarrow ((A \Rightarrow C) \Rightarrow A) .

(7)

This proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose

A = α

and

B = β

as atomic type variables. The type variable

β

is not a function type

α \Rightarrow C

, so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.

The reason for the restriction is the otherwise discarded lambda application

y x

: the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form