Phase 0, Section 4: Operational Semantics

Phase 0: Foundation — establishing the formal core calculus. Section 4 of 5: Operational Semantics.

1. What this section commits to

A model of what typed expressions mean and how they execute. Specifically:

• A denotational interpretation of types as sets of values.
• A small-step operational semantics relating expressions to their evaluations.
• A statement of type soundness (subject reduction + progress) — without the proof, which is deferred to the verification track in Phase 6.
• A principled separation between structural semantics (what the operations compute mathematically) and numerical semantics (what real floating-point implementations produce).

The typing rules from Sections 1, 2, and 3 are not modified here. Section 4 provides the model that those rules are sound against. If the model can't accommodate the rules, the rules are wrong — but I don't expect that to happen in this section.

2. The denotational model

2.1 Dtype interpretation

Each dtype denotes a set of values:

Two important points about FP dtypes:

• The value set is the standardized one. There is no ambiguity about which bit pattern represents which number.
• The operations on these values may not match real arithmetic. (a + b) + c ≠ a + (b + c) in IEEE 754. This is the numerical-semantics gap, addressed in §6.

2.2 Shape interpretation

A shape s = [d₁, ..., dₙ] denotes an index set under a substitution σ : ShapeVar → ℕ:

⟦[d₁, ..., dₙ]⟧_σ  =  Fin σ(d₁) × Fin σ(d₂) × ... × Fin σ(dₙ)

where Fin n = {0, 1, ..., n−1}. The substitution σ provides concrete integer values for any free shape variables in the shape expressions.

Empty shape [] denotes 1 (the singleton set), which is consistent with how scalars embed into the tensor algebra.

2.3 Tensor type interpretation

A tensor type denotes the set of functions from its index set to its value set, provided the refinements are satisfied by the substitution:

⟦Tensor[dt, s, R]⟧_σ  =
    { f : ⟦s⟧_σ → ⟦dt⟧  |  σ ⊨ R }

If σ does not satisfy R, the type denotes the empty set under that substitution. (This matches the typing-rule view that Sat(R) is checked at type formation.)

This is the "tensor-as-function-from-indices" model used in Dex, in array-language semantics, and informally in NumPy. It is mathematically clean and doesn't commit to any particular memory layout. The lowering (Phase 5) chooses the layout; the semantics doesn't constrain it.

2.4 Function type interpretation

⟦T₁ → T₂⟧_σ  =  ⟦T₁⟧_σ → ⟦T₂⟧_σ

Standard function space. The semantics is total — non-termination is not a concern in Phase 0 because there is no recursion or unbounded iteration. Later phases will need partiality (or a Diverge effect).

3. Values, expressions, and the runtime heap

3.1 Syntactic categories

Three distinct things, easy to conflate:

• Expressions e: terms that may contain operations to be evaluated (matmul (broadcast x s) y).
• Values v: irreducible terms — variables, literals, and tensor handles.
• Tensor data: the actual function-from-indices that a tensor handle refers to.

Values include scalar literals, but not tensor literals in syntax. A tensor of shape [1024, 1024] has a million entries; embedding that in syntax is impractical. Instead:

TensorValue ::= 〈τ : T〉

where τ is an opaque tensor handle and T is its type. Each handle τ refers to an entry in a runtime heap H : Handle ⇀ Function, where H(τ) is the function from indices to values that τ denotes.

3.2 The heap

The heap H is a partial function from handles to typed tensor data:

H(τ)  =  ( T_τ , f_τ )    where  f_τ : ⟦shape(T_τ)⟧_σ → ⟦dtype(T_τ)⟧

Operations that produce tensors allocate a fresh handle in the heap. The heap is not visible in the syntax of expressions; it is part of the configuration (H, e) over which reduction operates.

In Phase 0, the heap is grow-only: handles are never deallocated. Memory management is a later concern (Phase 5, hardware lowering, where it interacts with device memory). Adding deallocation in later phases is straightforward — linear types or a region calculus — and is anticipated by the "tensor types are linear by default" remark in memo 5 §3.1.

3.3 Well-typed heap (definition)

Theorems in §7 refer to “H is well-typed under Γ.” This section makes that predicate precise enough for mechanization (Lean) and implementation invariants.

Fix a shape substitution σ consistent with Γ (all shape variables in dom(σ) well-scoped under Γ). The heap H is well-typed under Γ with respect to σ when:

1. Coverage: Every handle in dom(H) is accounted for: the static context records the type of each live handle. Concretely, either Γ includes bindings τ : T for tensor values 〈τ : T〉, or (equivalently) the implementation maintains a map Γ_heap : Handle ⇀ Type disjoint from user variables; we write Γ, Γ_heap together as the “full” typing context for configurations.

2. Agreement: If H(τ) = (T_τ, f_τ) and the context assigns τ : T, then T ≡ T_τ up to α-renaming of refinements — the metadata T_τ stored beside f_τ matches the type the checker assigned to τ.

3. Inhabitation: Γ ⊢ T_τ type, and f_τ is a total function ⟦shape(T_τ)⟧_σ → ⟦dtype(T_τ)⟧ whose graph lies in the denotation ⟦T_τ⟧_σ: for every index i in ⟦shape(T_τ)⟧_σ, the value f_τ(i) is in ⟦dtype(T_τ)⟧, and σ satisfies the refinement predicates of T_τ (as in Section 1 §4).

Subject reduction (§7.1) assumes this invariant for H and concludes it for H'. An implementation proves (or tests) that each reduction rule preserves (1)–(3).

4. Reduction relation

The relation (H, e) → (H', e') says that in heap H, expression e reduces in one step to expression e', possibly producing an updated heap H'. Phase 0 commits to call-by-value, left-to-right evaluation.

4.1 Congruence (evaluation contexts)

The standard pattern: define an evaluation context E with a hole □ indicating where reduction can occur, then state that reduction inside the context propagates to reduction at the top.

E ::= □
    | op v₁ ... vᵢ₋₁ E eᵢ₊₁ ... eₙ
    | E e
    | v E

Reduction under context:

   (H, e) → (H', e')
─────────────────────────  (cong)
   (H, E[e]) → (H', E[e'])

This says: if a subterm reduces, the whole term takes that step. The shape of E enforces left-to-right argument evaluation: op v₁ ... vᵢ₋₁ E eᵢ₊₁ ... eₙ requires the first i−1 arguments to already be values before reducing the i-th.

4.2 Operation application

The single non-congruence rule:

   v₁, ..., vₙ are values    ⟦op⟧(v₁, ..., vₙ) = (H', τ)
─────────────────────────────────────────────────────────────  (op-apply)
                (H, op v₁ ... vₙ) → (H', 〈τ : T〉)

When all arguments are values, apply the operation's denotation ⟦op⟧. The denotation:

• Computes the resulting tensor function from the input tensor functions.
• Allocates a fresh handle τ in an updated heap H'.
• Returns the value 〈τ : T〉 where T is the operation's output type.

This single rule schema, parameterized by ⟦op⟧, covers every operation in the IR. The math for ⟦op⟧ is the per-operation specification.

5. Operation denotations

Each operation's ⟦op⟧ is the mathematical function it computes. For tensor f : Idx → ⟦dt⟧ and tensor g : Idx' → ⟦dt'⟧:

5.1 Elementwise unary

⟦unaryOp⟧(f) = λ i. unaryOp_scalar(f(i))

where unaryOp_scalar is the scalar version (e.g., relu_scalar(x) = max(0, x)).

5.2 Cast

⟦cast[dt₂]⟧(f) = λ i. convert_{dt₁ → dt₂}(f(i))

where convert_{dt₁ → dt₂} is the dtype conversion (FP rounding for narrowing FP, sign extension for integer widening, etc.). The bit-level details follow IEEE 754 for FP and standard two's-complement for integers.

5.3 Elementwise binary

⟦binOp⟧(f, g) = λ i. binOp_scalar(f(i), g(i))

The shapes of f and g are equal (enforced by typing); the indexing is pointwise.

5.4 Matmul

⟦matmul⟧(a, b) = λ (i, j, k). Σ_{l ∈ Fin K} a(i, j, l) · b(i, l, k)

The contraction is over the inner dimension K. The summation order is unspecified. This is a structural definition of matmul; the operational semantics does not constrain how the sum is reduced (e.g., naive sequential, tree reduction, blocked Kahan summation). See §6.

5.5 Reduce

⟦reduce[op, axis=i]⟧(f) = λ idx_minus_i. fold_op (λ d. f(d at axis i within idx))

where fold_op is the reduction operation (+ for sum, max for max, etc.). Again, the fold order is unspecified.

5.6 Transpose

⟦transpose[π]⟧(f) = λ (j₁, ..., jₙ). f(j_{π⁻¹(1)}, ..., j_{π⁻¹(n)})

Permute the indices according to π's inverse. Pure index manipulation; no data motion in the mathematical sense. Lowering may or may not produce a copy.

5.7 Reshape

⟦reshape[s']⟧(f) = λ idx'. f(unflatten(flatten(idx', s'), s))

where flatten converts a multi-dimensional index to a linear index in row-major order, and unflatten converts back. The operation is well-defined provided the volume of s equals the volume of s' — which is exactly the axiom asserted at type-checking time (Section 2 §10). Phase 0 trusts the assertion; the runtime check is a backstop.

5.8 Broadcast

⟦broadcast[s']⟧(f) = λ idx'. f(broadcast_index(idx', s, s'))

where broadcast_index reverses NumPy-style broadcasting: for each dimension of s', either reads the corresponding dim of idx' (if the source dim equals the target) or treats it as 0 (if the source dim is 1, broadcasting expands it).

5.9 Slice

⟦slice[axis=i, start=a, stop=b]⟧(f) = λ (j₁, ..., jₙ). f(j₁, ..., jᵢ + a, ..., jₙ)

Offset the index along the slice axis by the slice start. The output domain has size b − a along that axis.

5.10 Concat

⟦concat[axis=i]⟧(f, g) = λ idx.
    if idx[i] < size(f, i) then f(idx)
                          else g(idx with axis i shifted down by size(f, i))

The concatenated tensor reads from f for indices in the first range, from g for indices in the second.

6. The numerical-semantics gap

The most important §section in Phase 0 for understanding what the type system does not guarantee.

6.1 What the operational semantics says about FP arithmetic

The denotations in §5 define operations mathematically: matmul is a sum of products, reduce is a fold. The mathematical definition is associative and commutative (for +, *, min, max). The IEEE 754 implementation is not.

Two consequences:

1. The same expression can produce different bit patterns under different lowering choices (different reduction orders, different tile sizes, different accumulator precisions). All of these are "correct" with respect to the operational semantics.

2. The structural correctness of the compiler is independent of the numerical accuracy of its output. A verified compilation pass (Phase 6) proves that the right operations happen in the right order modulo associativity; it says nothing about how much error accumulates.

6.2 What this means for the typing rules

The typing rules do not produce numerical guarantees. A program of type Tensor[F32, [N], [N ≥ 1]] is guaranteed to produce a tensor of one or more F32 values; it is not guaranteed to produce values within any particular tolerance of the mathematical result.

Numerical bounds are a separate concern, addressed by:

• Refinement axes for numerical bounds (potential future work; not in Phase 0). A type like Tensor[F32, s, R, abs(x) ≤ 1] would carry an FP-value bound. The arithmetic of these bounds is a separate sub-language, probably interval arithmetic à la Gappa.
• Phase 6 verification of specific passes. Quantization passes prove specific error bounds. AD passes prove gradient correctness modulo FP error. These are pass-specific; the overall type system stays neutral.

6.3 The principled separation

This section commits to a two-layer correctness story:

The two layers compose. Verified structural correctness is sound regardless of numerical tolerance; verified numerical bounds are sound only when applied to a structurally-correct compilation. Neither layer subsumes the other.

This is the same separation memo 5 §7 argued for. Phase 0 ratifies it explicitly: the operational semantics is real-valued; the implementation is FP-valued; the gap is bridged by separate verification machinery applied to specific passes.

7. Type soundness theorem statement

The two standard theorems, stated only in Phase 0. The proof goes in Phase 6 (Lean 4 mechanization).

7.0 Scope: idealized reduction vs reshape

Subject reduction and progress below are stated for the idealized reduction relation in which every reshape satisfies the volume equality the type-checker assumed (Section 2 §10). They do not assert that every statically well-typed program runs to completion on a concrete machine: if that assumption was false at runtime, a conforming implementation may fault on reshape after the tensor is materialized—the runtime backstop for Section 2’s controlled unsoundness. Phase 6 proofs either model that check or restrict to configurations where reshape assumptions hold at runtime.

7.1 Subject reduction (preservation)

Theorem (Subject Reduction):
    If    Γ ⊢ e : T
    and   (H, e) → (H', e')
    and   H is well-typed under Γ
    then  Γ ⊢ e' : T
    and   H' is well-typed under Γ.

In words: if a well-typed expression takes a step, the result is still well-typed at the same type, and the heap remains consistent. This is the key property that makes the type system useful for guarantees about runtime behavior — types persist through evaluation.

“H is well-typed under Γ” is the predicate defined in §3.3 (with respect to the substitution σ induced by the evaluation configuration).

7.2 Progress

Theorem (Progress):
    If    ∅ ⊢ e : T
    and   H is well-typed under ∅
    then  either e is a value
          or there exists (H', e') such that (H, e) → (H', e').

In words: a closed, well-typed expression is either fully evaluated (a value) or can take another step. Under the idealized reduction of §7.0 there are no "stuck" terms; a concrete implementation may still fault when runtime checks contradict static assumptions (reshape and similar; §7.0).

7.3 Type soundness, as a corollary

Together, subject reduction and progress yield the soundness theorem:

Corollary (Type Soundness):
    If ∅ ⊢ e : T, then e evaluates to a value of type T,
    or evaluation continues forever.

In Phase 0, the second clause does not occur — there is no recursion or unbounded iteration, so every well-typed expression evaluates in finitely many steps. Later phases will need a more careful statement allowing for divergence (modeled as a Diverge effect or as partiality of evaluation).

7.4 What's deferred to verification

The Phase 0 statement of these theorems is a written-down deliverable. The proof requires:

• Mechanization of the syntax, types, and reduction rules in Lean 4.
• Proof of subject reduction by induction on the typing derivation, with case analysis on the reduction rule.
• Proof of progress by induction on the typing derivation, showing that each typing case produces either a value or a possible reduction.
• The proofs are non-trivial but standard. The closest reference template is the simply-typed lambda calculus soundness proof from Pierce's Types and Programming Languages, extended with the SMT-discharged refinement obligations.

The proof effort is estimated at 2–4 months of focused Lean 4 work for someone fluent in the tool. Most of the difficulty is in the SMT obligations: the proof has to either trust Z3 (axiomatic) or include a separate verified arithmetic decision procedure. The pragmatic answer is to trust Z3 in the proof and document the trust assumption.

This is why Phase 6 (verification) is a parallel track in the roadmap: the Lean 4 work informs the implementation, and the implementation reveals what's actually proof-relevant. Doing the proof at the end of the project means rewriting it; doing it alongside means the implementation stays proof-aware.

8. Resolved and new open issues

Resolved

• Section 1, deferred to Section 4: operational semantics for the typing rules. Done in §4–5.
• Section 2 §16, issue 4: numerical semantics of reduction. Closed by §6: the operational semantics is real-valued; FP semantics is a separate verification concern.

New (introduced or sharpened by this section)

1. Heap deallocation. Phase 0's heap is grow-only. Phase 5 (hardware lowering) needs explicit deallocation, which interacts with the type system: linear types? Region calculus? Reference counting? Decision deferred but flagged.

2. The "well-typed heap" relation (resolved in §3.3). The predicate “H is well-typed under Γ” is defined in §3.3 (coverage, agreement, inhabitation relative to σ). Implementations refine that definition in code; Lean mechanization should match §3.3.

3. Termination assumption. §7.3 is stated under the assumption that Phase 0 has no recursion. This is true now but easy to forget when later phases add control flow. Worth tracking explicitly so the soundness statement gets re-examined when divergence is added.

4. Bit-level reproducibility as a non-goal. This section makes it explicit: two correct compilations of the same expression may produce different bit patterns. Production users sometimes need bit-level reproducibility (regulated finance, certain scientific contexts). Achieving it requires constraining the lowering — picking a canonical reduction order and a canonical accumulator precision. Possible in principle, expensive in practice, out of scope for Phase 0. Listed as a Phase 6+ concern.

9. Decisions, summarized

10. Section 5 preview

Section 5 closes Phase 0 with implementation infrastructure:

• OCaml for the compiler frontend (parser, type-checker, IR, lowering driver).
• Rust for the runtime (heap, kernel dispatch, eventually NCCL/CUDA bindings).
• Lean 4 for the verification track (formal calculus, soundness proofs).
• MLIR as the IR substrate, accessed by emitting textual MLIR from OCaml and driving mlir-opt / mlir-translate / llc as subprocesses (no MLIR C++ API in Phase 0; see Section 5 §3).
• Z3 for SMT discharge, accessed via OCaml bindings (ocaml-z3).

The section will commit to repository structure, build orchestration, dependency management, milestone definition, and the FFI boundaries between the three languages. With Sections 1–4 setting the formal contract, Section 5 is the engineering plan to actually build it.

After Section 5, Phase 0 is complete and Phase 1 (the shape-typed core, end-to-end) begins.

End of Phase 0, Section 4.