## Formal Inference Rules: WRITE-G and W-G-SHARED-BORROW ### Overview The image displays two formal inference rules, presented side-by-side, which appear to define operational semantics for a programming language or type system. The rules use mathematical notation common in programming language theory, involving state transformations, pointers, and what seems to be a borrowing or loan mechanism. The left rule is labeled "WRITE-G" and the right rule is labeled "W-G-SHARED-BORROW". ### Components/Axes The image is a diagram, not a chart. Its components are the two inference rules themselves. **Common Notation Elements:** * **Horizontal Line:** Separates the premises (above) from the conclusion (below) in each rule. * **Greek Letters:** `Ω` (Omega) represents a state or environment. `p` likely represents a pointer or location. * **Mapsto Arrow (`↦`):** Denotes an update or mapping, e.g., `p ↦ v` means "update location `p` with value `v`". * **Turnstile (`⊢`):** Often denotes a typing or validity judgment, e.g., `Ω ⊢ p(v_p)` means "in state `Ω`, `p(v_p)` is valid/well-formed". * **Rightwards Arrow (`→`):** Represents a transition or evaluation step, e.g., `v → v'` means "value `v` transitions to `v'`". * **Superscript `g`:** Appears above the transition arrow (`→^g`), possibly indicating a specific kind of transition (e.g., "good" or "global"). * **Prime Symbol (`'`):** Used to denote a new or updated version of a variable/state, e.g., `Ω'` is a new state derived from `Ω`. ### Detailed Analysis #### Rule 1: WRITE-G (Left Side) * **Label:** `WRITE-G` (Top-left of the rule block). * **Premises (Above the line):** 1. `p = P[x]`: A pointer `p` is defined as the projection `P[x]`. 2. `x ↦ v_x ∈ Ω`: The state `Ω` contains a mapping from `x` to a value `v_x`. 3. `Ω ⊢ p(v_p) →^g v'_x ⊣ Ω'`: In state `Ω`, the operation `p(v_p)` (likely a write through pointer `p` with value `v_p`) transitions via `g` to a new value `v'_x`, producing a new state `Ω'`. 4. `Ω'' = Ω'[x ↦ v'_x]`: A second new state `Ω''` is defined as `Ω'` with the mapping for `x` updated to `v'_x`. * **Conclusion (Below the line):** * `Ω[p ↦ v] = Ω''`: The overall state transition. Starting from state `Ω`, performing the update `p ↦ v` results in the final state `Ω''`. **Spatial Grounding:** The label `WRITE-G` is positioned at the top-left of the left-hand rule block. The horizontal line spans the width of the rule's notation. #### Rule 2: W-G-SHARED-BORROW (Right Side) * **Label:** `W-G-SHARED-BORROW` (Top-left of the rule block). * **Premises (Above the line):** 1. `loan^s {ℓ ∪ _} v_p ∈ Ω`: The state `Ω` contains a "shared loan" (`loan^s`) for a location set `{ℓ ∪ _}` (where `_` is a wildcard) associated with value `v_p`. 2. `Ω ⊢ p(v_p) →^g v'_p ⊣ Ω'`: Similar to the first rule, in state `Ω`, the operation `p(v_p)` transitions via `g` to a new value `v'_p`, producing a new state `Ω'`. * **Intermediate Definition (Between premises and conclusion):** * `Ω'' = [loan^s {ℓ ∪ _} v'_p / loan^s {ℓ ∪ _} v_p] Ω'`: State `Ω''` is defined as `Ω'` where the old loan `loan^s {ℓ ∪ _} v_p` is replaced by the new loan `loan^s {ℓ ∪ _} v'_p`. The square brackets `[_ / _]` denote substitution. * **Conclusion (Below the line):** * `Ω ⊢ (*^s p)(borrow^s ℓ) →^g borrow^s ℓ + Ω''`: The overall transition. Starting from state `Ω`, the operation `(*^s p)(borrow^s ℓ)` (likely dereferencing a shared pointer `p` to perform a shared borrow of location `ℓ`) transitions via `g` to a result consisting of a new shared borrow `borrow^s ℓ` and the updated state `Ω''`. **Spatial Grounding:** The label `W-G-SHARED-BORROW` is positioned at the top-left of the right-hand rule block. The intermediate definition for `Ω''` is placed directly below the premises and above the main horizontal line. ### Key Observations 1. **Structural Parallelism:** Both rules share a core structure: a premise involving a state transition `Ω ⊢ p(v_p) →^g v' ⊣ Ω'`, followed by a definition of a final state `Ω''` that incorporates the result of that transition. 2. **State Propagation:** The final state `Ω''` in both rules is built upon the intermediate state `Ω'` produced by the core transition. 3. **Borrowing Semantics:** The right rule explicitly introduces concepts of "loans" (`loan^s`) and "borrows" (`borrow^s`), with a superscript `s` likely denoting "shared". This suggests a memory model with controlled access, similar to Rust's borrowing system. 4. **Substitution Notation:** The use of `[... / ...]` for substitution in the right rule is a standard notation in operational semantics for updating a structure (here, the state `Ω'`). ### Interpretation These inference rules formally specify how certain operations modify a program's state (`Ω`). * **WRITE-G** defines the semantics of a **write operation** through a pointer `p`. It ensures that if `p` is derived from a variable `x`, writing through `p` not only updates the state via `p` but also correctly propagates that change back to the original variable `x` in the final state `Ω''`. This rule enforces consistency between a pointer and its origin. * **W-G-SHARED-BORROW** defines the semantics of a **shared borrow operation** (`borrow^s ℓ`) performed via a shared pointer `p`. It handles a more complex scenario where the state contains an existing "loan" (a record of borrowed access). The operation updates the value associated with that loan (`v_p` to `v'_p`) and returns both the new borrow token and the updated state. This rule is crucial for managing aliasing and ensuring memory safety in a system with shared references. **Underlying Principle:** Together, these rules likely form part of a formal model for a language with explicit memory management, pointers, and a borrowing system to prevent data races or violations of ownership invariants. The `g` superscript on the transition arrow might indicate that these are "good" or "valid" transitions that preserve core system properties. The rules meticulously track how state changes propagate through different levels of indirection (pointers, loans) to maintain a consistent global state.