## Type Inference Rules: Operational Semantics ### Overview The image presents a set of type inference rules, likely representing the operational semantics of a programming language with borrowing and memory management features. Each rule describes how a program state transitions to a new state based on certain conditions. ### Components/Axes Each rule generally follows the format: * **Rule Name:** (e.g., E-MUT-BORROW, E-SHARED-OR-RESERVED-BORROW) * **Premises:** Conditions that must be true for the rule to apply. These are written above the horizontal line. * **Conclusion:** The resulting state transition if the premises are met. This is written below the horizontal line. * **Context:** Ω represents the typing context or environment. * **Variables:** Various symbols like `p`, `v`, `l`, `r`, `s`, etc., represent program variables, values, locations, or other semantic entities. ### Detailed Analysis or ### Content Details Here's a breakdown of each rule: **1. E-MUT-BORROW** * Premises: * `Ω(p) => v`: The value of `p` in context `Ω` is `v`. * `{⊥, loan, borrow'} ∉ v`: `v` does not contain `⊥`, `loan`, or `borrow'`. * `*s ∉ p`: `p` is not marked with `*s`. * `l fresh`: `l` is a fresh location. * `Ω(p) -loan^l=> Ω'`: The context `Ω` is updated such that `p` now loans `l`, resulting in context `Ω'`. * Conclusion: * `Ω ⊢ &mut p ⇝ borrow^l v + Ω'`: The mutable borrow of `p` results in `borrow^l v` and the updated context `Ω'`. **2. E-SHARED-OR-RESERVED-BORROW** * Premises: * `Ω(p) => v`: The value of `p` in context `Ω` is `v`. * `{⊥, loan^m, borrow^r} ∉ v`: `v` does not contain `⊥`, `loan^m`, or `borrow^r`. * `l fresh`: `l` is a fresh location. * `Ω' = Ω[p ↦ v']`: The context `Ω'` is `Ω` updated with `p` mapping to `v'`. * `v' = loans^s {l ∪ l'} v'' if v = loans^s {l'} v''`: `v'` is `loans^s {l ∪ l'} v''` if `v` is `loans^s {l'} v''`. * `v' = loans^s {l} v otherwise`: Otherwise, `v'` is `loans^s {l} v`. * Conclusion: * `Ω ⊢ &p ⇝ borrow^s,l v' + Ω'`: The shared or reserved borrow of `p` results in `borrow^s,l v'` and the updated context `Ω'`. **3. E-MOVE** * Premises: * `Ω(p) => v`: The value of `p` in context `Ω` is `v`. * `{⊥, loan, borrow'} ∉ v`: `v` does not contain `⊥`, `loan`, or `borrow'`. * `{*m, *s} ∉ p`: `p` is not marked with `*m` or `*s`. * `Ω(p) ⟵ ⊥ => Ω'`: The context `Ω` is updated such that `p` is now `⊥`, resulting in context `Ω'`. * Conclusion: * `Ω ⊢ move p ⇝ v + Ω'`: Moving `p` results in `v` and the updated context `Ω'`. **4. E-COPY** * Premises: * `Ω(p) => v`: The value of `p` in context `Ω` is `v`. * `{⊥, loan^m, borrow^m,r} ∉ v`: `v` does not contain `⊥`, `loan^m`, or `borrow^m,r`. * Conclusion: * `Ω ⊢ copy v ⇝ v' + Ω'`: Copying `v` results in `v'` and the updated context `Ω'`. * Conclusion: * `Ω ⊢ copy p ⇝ v' + Ω'`: Copying `p` results in `v'` and the updated context `Ω'`. **5. E-CONSTRUCTOR** * Premises: * `Ω_i ⊢ op_i ⇝ v_i + Ω_{i+1}`: The operation `op_i` in context `Ω_i` results in `v_i` and the updated context `Ω_{i+1}`. * `Ω_0 ⊢ C[f = op] ⇝ C[f = v] + Ω_n`: The constructor `C[f = op]` in context `Ω_0` results in `C[f = v]` and the updated context `Ω_n`. **6. E-RETURN** * Premises: * `Ω_i ⊢ x_{local,i} := ⊥ ⇝ () + Ω_{i+1}`: Setting the local variable `x_{local,i}` to `⊥` results in `()` and the updated context `Ω_{i+1}`. * `Ω_n(x_{ret}) => v`: The value of `x_{ret}` in context `Ω_n` is `v`. * `{⊥, loan, borrow'} ∉ v`: `v` does not contain `⊥`, `loan`, or `borrow'`. * Conclusion: * `Ω_0 ⊢ return ⇝ return v + Ω_n`: Returning results in `return v` and the updated context `Ω_n`. **7. E-IFTHENELSE-T** * Premises: * `Ω ⊢ op ⇝ true + Ω'`: The operation `op` in context `Ω` results in `true` and the updated context `Ω'`. * `Ω' ⊢ s_1 ⇝ r + Ω''`: The statement `s_1` in context `Ω'` results in `r` and the updated context `Ω''`. * Conclusion: * `Ω ⊢ if op then s_1 else s_2 ⇝ r + Ω''`: The if-then-else statement results in `r` and the updated context `Ω''`. **8. E-ASSIGN** * Premises: * `Ω ⊢ rv ⇝ v + Ω'`: Evaluating `rv` in context `Ω` results in `v` and the updated context `Ω'`. * `Ω'(p) => v_p`: The value of `p` in context `Ω'` is `v_p`. * `v_p has no outer loans`: `v_p` has no outer loans. * `x_{old} fresh`: `x_{old}` is a fresh variable. * `Ω'(p) ⟵ v => Ω''`: The context `Ω'` is updated such that `p` is now `v`, resulting in context `Ω''`. * `Ω''' = Ω''[x_{old} ↦ v_p]`: The context `Ω'''` is `Ω''` updated with `x_{old}` mapping to `v_p`. * Conclusion: * `Ω ⊢ p := rv ⇝ () + Ω'''`: The assignment results in `()` and the updated context `Ω'''`. **9. E-FREE** * Premises: * `Ω(p) => Box v`: The value of `p` in context `Ω` is `Box v`. * `Ω ⊢ p := ⊥ ⇝ () + Ω'`: The context `Ω` is updated such that `p` is now `⊥`, resulting in context `Ω'`. * Conclusion: * `Ω ⊢ free p ⇝ () + Ω'`: Freeing `p` results in `()` and the updated context `Ω'`. **10. E-MATCH** * Premises: * `Ω ⊢ p ⇝^s C[f = v]`: Matching `p` results in `C[f = v]`. * `Ω ⊢ s ⇝ r + Ω'`: The statement `s` results in `r` and the updated context `Ω'`. * Conclusion: * `Ω ⊢ match p with ... | C -> s | ... ⇝ r + Ω'`: The match statement results in `r` and the updated context `Ω'`. ### Key Observations * The rules define how different operations (borrowing, moving, copying, assignment, etc.) affect the program state, represented by the context `Ω`. * The rules often involve checks to ensure that certain conditions are met before an operation can proceed (e.g., checking for existing loans or borrows). * The rules update the context `Ω` to reflect the changes caused by the operation. ### Interpretation These rules describe the operational semantics of a language with memory safety features, likely related to borrowing and ownership. The rules ensure that memory is accessed and modified in a safe and controlled manner, preventing issues like dangling pointers and data races. The presence of "loan" and "borrow" concepts suggests a system similar to Rust's borrow checker. The rules enforce constraints on how memory can be accessed and modified, ensuring that multiple mutable references to the same memory location are not allowed simultaneously, and that references do not outlive the data they point to. The rules are crucial for understanding the behavior of programs written in this language and for verifying their correctness.

\n ## Mathematical Formulas: Operational Semantics ### Overview The image presents a collection of mathematical formulas, likely representing operational semantics for a programming language or a formal system. Each formula defines a transition rule, showing how a system state changes based on a specific operation. The formulas use a notation involving state variables (Ω), preconditions, operations, and resulting states (Ω'). The notation includes symbols for borrowing, loans, and various logical operations. ### Components/Axes There are no axes or traditional chart components. The image consists entirely of mathematical expressions. Each expression is labeled with a name indicating the operation it defines (e.g., "E-MUT-Borrow", "E-SHARED-OR-RESERVED-Borrow"). The formulas are arranged in a grid-like structure, with each formula occupying a distinct rectangular region. ### Detailed Analysis or Content Details Here's a transcription of each formula, attempting to capture the mathematical notation as accurately as possible: **1. E-MUT-Borrow** Ω(p) ⇒ v {L, loan, borrow"} ∉ v x⁵ ∉ p ⇔ p ⊣ fresh Ω & mut p ↦ borrow" l v Ω' **2. E-SHARED-OR-RESERVED-Borrow** Ω(p) ⇒ v {L, loanᵐ, borrow"} ∉ v v' = {loans' {l | u} if u' = loans' {l"} v' = loans' {l} v otherwise Ω & p ↦ borrow"s l v Ω' **3. E-Move** Ω(p) ⇒ v {L, loan, borrow"} ∉ v {xᵐ, x⁵} ∉ p Ω(p) ↦ ⊥ ⊣ Ω' Ω & move p ↦ v Ω' **4. E-Copy** Ω(p) ⇒ v {L, loanᵐ, borrowᵐr} ∉ v Ω & copy p ↦ v' Ω' **5. E-CONSTRUCTOR** Ωᵢ + opᵢ ⇒ vᵢ Ωᵢ + 1 Ω₀ + [lf = op] ↦ C[lf = v] ↦ Ωₙ **6. E-RETURN** Ωᵢ + localᵢ i := 1 ↦ Ωᵢ + 1 Ωₙ(xᵣet) ⇒ v {L, loan, borrow"} ∉ v Ω₀ + return ↦ return v ↦ Ωₙ **7. E-IF-THEN-ELSE-T** Ω + op true ⇒ Ω' Ω + S₁ ↦ r ↦ Ω" r: if op then s₁ else s₂ ↦ r ↦ Ω" **8. E-FREE** Ω(p) ⇒ Box v Ω & free p ↦ () ↦ Ω' **9. E-ASSIGN** Ω & r v ↦ v' ↦ Ω' Ω'(p) ⇒ vₚ up has no outer loans Ω'(p) ↦ v ↦ Ω" Ω" = [xold ↦ vₚ] **10. E-MATCH** Ω & p ↦ C[f = v] Ω & s ↦ r ↦ Ω' Ω & match p with ... | C → s | ... ↦ r ↦ Ω' ### Key Observations * The formulas consistently use the notation Ω to represent a state, and Ω' to represent the resulting state after an operation. * The curly braces { } are used to denote sets of conditions or properties that must hold for the transition to be valid. * The symbol "↦" appears to represent a state transition or assignment. * The notation "∉" indicates set membership exclusion. * The formulas involve concepts like borrowing, loans, and mutation, suggesting a system dealing with resource management or memory allocation. * The formulas are highly symbolic and require a deep understanding of the underlying formal system to interpret fully. ### Interpretation The image presents a formal specification of the operational semantics of a programming language or a computational model. Each formula defines a rule for how the system's state changes when a particular operation is performed. These rules are crucial for defining the meaning of the language and for reasoning about its behavior. The presence of concepts like "borrowing" and "loans" suggests that the system may be concerned with managing resources, such as memory or access rights. The formulas involving "move" and "copy" indicate operations related to data manipulation. The "match" formula suggests pattern matching capabilities. The formulas are written in a highly abstract and mathematical style, typical of formal semantics. They are intended to be precise and unambiguous, allowing for rigorous analysis and verification of the system's behavior. The notation is dense and requires specialized knowledge to interpret correctly. The overall structure suggests a well-defined and formally specified system.

## Formal Inference Rules: Operational Semantics ### Overview The image displays a set of ten formal inference rules, likely defining the operational semantics for a programming language or type system with explicit memory management, borrowing, and ownership concepts. The rules are presented in a standard "premise over conclusion" format separated by a horizontal line. The notation uses a state or environment variable `Ω` (Omega) that is transformed by each operation. ### Components/Axes The image is a single panel containing ten distinct, labeled inference rules arranged in two columns. Each rule has: 1. **Rule Name:** A label at the top (e.g., `E-MUT-BORROW`). 2. **Premises:** One or more logical statements above the horizontal line, defining the conditions under which the rule applies. 3. **Conclusion:** A statement below the horizontal line, defining the result of applying the rule. 4. **Notation:** Uses symbols including `Ω`, `⇒`, `⊢`, `↦`, `ℓ`, `v`, `p`, `⊥`, `*`, `&`, `{}`, `⊥`, `⊤`, `()`, and various superscripts/subscripts (`m`, `r`, `s`, `loc`, `ret`). ### Detailed Analysis: Rule-by-Rule Transcription **Left Column (Top to Bottom):** 1. **Rule: E-MUT-BORROW** * **Premises:** * `Ω(p) ⇒ v` * `{⊥, loan^m, borrow^r} ∉ v` * `*^s ∉ p` * `ℓ fresh` * `Ω(p) ← loan^m ℓ ⇒ Ω'` * **Conclusion:** `Ω ⊢ &mut p ⇝ borrow^m ℓ v ⊣ Ω'` 2. **Rule: E-MOVE** * **Premises:** * `Ω(p) ⇒ v` * `{⊥, loan^m, borrow^r} ∉ v` * `{*^m, *^s} ∉ p` * `Ω(p) ⊥ ⇒ Ω'` * **Conclusion:** `Ω ⊢ move p ⇝ v ⊣ Ω'` 3. **Rule: E-CONSTRUCTOR** * **Premises:** * `Ω_i ⊢ op_i ⇝ v_i ⊣ Ω_{i+1}` (for a sequence of operations `op_i`) * **Conclusion:** `Ω_0 ⊢ C[f⃗ = op⃗] ⇝ C[f⃗ = v⃗] ⊣ Ω_n` 4. **Rule: E-IFTHENELSE-T** * **Premises:** * `Ω ⊢ op ⇝ true ⊣ Ω'` * `Ω' ⊢ s_1 ⇝ r ⊣ Ω''` * **Conclusion:** `Ω ⊢ if op then s_1 else s_2 ⇝ r ⊣ Ω''` 5. **Rule: E-FREE** * **Premises:** * `Ω(p) ⇒ Box v` * `Ω ⊢ p := ⊥ ⇝ () ⊣ Ω'` * **Conclusion:** `Ω ⊢ free p ⇝ () ⊣ Ω'` **Right Column (Top to Bottom):** 6. **Rule: E-SHARED-OR-RESERVED-BORROW** * **Premises:** * `Ω(p) ⇒ v` * `{⊥, loan^m, borrow^r} ∉ v` * `ℓ fresh` * `Ω' = Ω[p ↦ v']` * **Definition of v':** * `v' = { loan^s {ℓ ∪ ℓ} v'' if v = loan^s {ℓ} v''` * `loan^s {ℓ} v otherwise` * **Conclusion:** `Ω ⊢ & p ⇝ borrow^{r,s} ℓ ⊣ Ω'` 7. **Rule: E-COPY** * **Premises:** * `Ω(p) ⇒ v` * `{⊥, loan^m, borrow^{m,r}} ∉ v` * **Conclusion:** `Ω ⊢ copy p ⇝ v' ⊣ Ω'` (Note: The relationship between `v` and `v'` is not explicitly defined in this rule's premise line). 8. **Rule: E-RETURN** * **Premises:** * `Ω_i ⊢ x_{local,i} := ⊥ ⇝ () ⊣ Ω_{i+1}` (for a sequence of local variables) * `Ω_n(x_{ret}) ⇒ v` * `{⊥, loan^m, borrow^r} ∉ v` * **Conclusion:** `Ω_0 ⊢ return ⇝ return v ⊣ Ω_n` 9. **Rule: E-ASSIGN** * **Premises:** * `Ω ⊢ rv ⇝ v ⊣ Ω'` * `Ω'(p) ⇒ v_p` * `v_p has no outer loans` * `x_{old} fresh` * `Ω'(p) ← v ⇒ Ω''` * `Ω''' = Ω''[x_{old} ↦ v_p]` * **Conclusion:** `Ω ⊢ p := rv ⇝ () ⊣ Ω'''` 10. **Rule: E-MATCH** * **Premises:** * `Ω ⊢ p ⇝^s C[f⃗ = v⃗]` * `Ω ⊢ s ⇝ r ⊣ Ω'` (where `s` is likely the match arm body corresponding to the pattern `C`) * **Conclusion:** `Ω ⊢ match p with ... | C -> s | ... ⇝ r ⊣ Ω'` ### Key Observations * **State Threading:** Every rule transforms the environment `Ω` to a new version (`Ω'`, `Ω''`, etc.), indicating a stateful operational semantics. * **Borrowing & Loans:** The rules explicitly model borrowing (`borrow^m`, `borrow^r`, `borrow^s`) and loaning (`loan^m`, `loan^s`) of resources, with checks to prevent invalid states (e.g., `{⊥, loan^m, borrow^r} ∉ v`). * **Freshness:** The concept of "fresh" (`ℓ fresh`, `x_{old} fresh`) is used to introduce new, unique identifiers or variables. * **Ownership & Move Semantics:** Rules like `E-MOVE` and `E-FREE` suggest affine or linear type system characteristics, where resources have single ownership and can be moved or explicitly freed. * **Pattern Matching:** The `E-MATCH` rule indicates the language has algebraic data types and pattern matching. ### Interpretation This set of inference rules formally defines the step-by-step execution (operational semantics) for a low-level programming language with a sophisticated memory management model. The system appears designed to ensure memory safety at the language level, likely preventing issues like use-after-free, double-free, and data races. The rules for borrowing (`&mut`, `&`) and moving (`move`) are central, suggesting a model similar to Rust's ownership system. The `Ω` environment tracks the state of memory locations (`p`), recording whether they are valid (`v`), moved from (`⊥`), or currently loaned/borrowed. The checks in the premises (e.g., `no outer loans` in `E-ASSIGN`) are static conditions enforced during execution to maintain invariants. Collectively, these rules provide a precise, mathematical specification for compiler writers or language designers. They describe how expressions and statements manipulate owned resources and shared borrows, ensuring that operations are only performed when the resource is in a valid state, thereby guaranteeing safety properties by construction. The presence of rules for constructors, conditionals, returns, and pattern matching shows this is a specification for a complete, albeit core, programming language fragment.

## Technical Ruleset: Memory and Type System Operations ### Overview The image presents a formal set of rules governing memory operations, type systems, and ownership semantics in a programming language. Each rule is labeled (e.g., `E-Mut-Borrow`, `E-Move`) and defines logical relationships between program states, ownership, and borrowing constraints. ### Components/Axes - **Labels**: - `E-Mut-Borrow`, `E-Move`, `E-Shared-Or-Reserved-Borrow`, `E-Copy`, `E-Constructor`, `E-Return`, `E-Assign`, `E-IfThenElse-T`, `E-Free`, `E-Match`. - **Logical Formulas**: - Premises (e.g., `Ω(p) ⇒ v`, `Ω(p) ⊢ loan^m, borrow^r ∉ v`). - Conclusions (e.g., `Ω ⊢ borrow^m ℓ v ⊢ Ω'`). - **Operators/Symbols**: - `⇒` (implies), `⊢` (proves), `∉` (not in), `∪` (union), `↔` (if and only if), `→` (arrow), `:=` (assignment). ### Detailed Analysis 1. **E-Mut-Borrow**: - Premise: `Ω(p) ⇒ v` and `Ω(p) ⊢ loan^m, borrow^r ∉ v`. - Conclusion: `Ω ⊢ &mut p ⇔ borrow^m ℓ v ⊢ Ω'`. - *Interpretation*: Allows mutable borrowing of a value `v` under ownership constraints. 2. **E-Move**: - Premise: `Ω(p) ⇒ v`, `Ω(p) ⊢ loan^m, borrow^r ∉ v`, and `(*^m, *^s) ∉ p`. - Conclusion: `Ω ⊢ move p ⇔ v ⊢ Ω'`. - *Interpretation*: Moves ownership of `v` from `p` to a new state `Ω'`. 3. **E-Shared-Or-Reserved-Borrow**: - Premise: `Ω(p) ⇒ v`, `Ω(p) ⊢ loan^m, borrow^r ∉ v`, and `ℓ fresh`. - Conclusion: `Ω' = Ω[p ↦ v']`, where `v'` depends on `v` and `ℓ`. - *Interpretation*: Handles shared or reserved borrowing with freshness conditions. 4. **E-Copy**: - Premise: `Ω(p) ⇒ v`, `Ω(p) ⊢ loan^m, borrow^m,r ∉ v`. - Conclusion: `Ω ⊢ copy v ⇒ v' ⊢ Ω'`. - *Interpretation*: Copies `v` into `v'` under ownership constraints. 5. **E-Constructor**: - Premise: `Ω_i ⊢ op_i ⇔ v_i ⊢ Ω_{i+1}`. - Conclusion: `Ω_0 ⊢ C[f = op] ⇔ C[f = v] ⊢ Ω_n`. - *Interpretation*: Constructs values using operations `op_i` and tracks ownership across steps. 6. **E-Return**: - Premise: `Ω_i ⊢ x_local,i := ⊥ ⇔ () ⊢ Ω_{i+1}`. - Conclusion: `Ω_n(x_ret) ⇒ v`, `Ω_0 ⊢ return ⇔ return v ⊢ Ω_n`. - *Interpretation*: Returns a value `v` after local variable initialization. 7. **E-Assign**: - Premise: `Ω ⊢ rv ⇔ v ⊢ Ω'`, `x_old fresh`, `v_p has no outer loans`. - Conclusion: `Ω' ⊢ p := rv ⇔ () ⊢ Ω''`. - *Interpretation*: Assigns `rv` to `p` with freshness and ownership checks. 8. **E-IfThenElse-T**: - Premise: `Ω ⊢ op ⇔ true ⊢ Ω'`, `Ω' ⊢ s_1 ⇔ r ⊢ Ω''`, `Ω ⊢ if op then s_1 else s_2 ⇔ r ⊢ Ω''`. - *Interpretation*: Conditional execution with ownership tracking for branches. 9. **E-Free**: - Premise: `Ω(p) ⇒ Box v`, `Ω ⊢ p := ⊥ ⇔ () ⊢ Ω'`. - Conclusion: `Ω ⊢ free p ⇔ () ⊢ Ω'`. - *Interpretation*: Frees a boxed value `v` and updates ownership. 10. **E-Match**: - Premise: `Ω ⊢ p ⇒ C[f = v]`, `Ω ⊢ s ⇔ r ⊢ Ω'`. - Conclusion: `Ω ⊢ match p with ... ⇒ s ⇔ r ⊢ Ω'`. - *Interpretation*: Matches patterns `p` against constructors `C` and updates ownership. ### Key Observations - **Ownership Constraints**: Rules like `loan^m, borrow^r ∉ v` enforce that values cannot be simultaneously loaned or borrowed. - **Freshness**: Variables like `ℓ` and `x_old` are marked `fresh` to avoid capture in closures. - **Ownership Transfers**: Operations like `move` and `return` explicitly transfer ownership between states. ### Interpretation This ruleset formalizes a type system with ownership and borrowing semantics, likely inspired by Rust or similar languages. Key features include: - **Memory Safety**: Rules prevent dangling pointers by tracking loans and borrows. - **Type Inference**: The `E-Constructor` and `E-Match` rules suggest a type inference mechanism for algebraic data types. - **Concurrency Safety**: The absence of simultaneous loans/borrows ensures thread-safe access. The absence of numerical data or visual trends indicates this is a formal specification rather than empirical data. The rules collectively define a sound and complete system for managing resources in a concurrent, memory-safe language.