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