## 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.
