## Type Theory Rules: Judgement Derivations ### Overview The image presents a collection of type theory inference rules, likely related to a formal system for programming languages or logic. Each rule defines how to derive a judgement (a statement about types and terms) from other judgements. The rules cover various constructs, including variables, functions, products, sums, recursive types, and control flow. ### Components/Axes The image consists of multiple inference rules. Each rule has the following structure: * **Premises:** Judgements above the horizontal line. These are the conditions that must be satisfied to apply the rule. * **Conclusion:** The judgement below the horizontal line. This is the judgement that can be derived if the premises are satisfied. * **Context (Γ):** A set of assumptions about the types of variables. * **Terms (M, N, V):** Expressions in the language. * **Types (A, B):** Classifications of terms. * **Judgements:** Statements of the form "Γ ⊢ M : A", meaning "in context Γ, term M has type A". * **Other Symbols:** Various symbols representing type constructors, term constructors, and operations (e.g., × for product types, + for sum types, μ for recursive types). ### Detailed Analysis or ### Content Details Here's a breakdown of each rule, transcribing the text and explaining its meaning: 1. **Variable Rule:** * `Γ, x: A, Γ' ⊢ x : A` * Meaning: If variable `x` has type `A` in the context, then `x` has type `A`. 2. **Unit Type Introduction:** * `Γ ⊢ • : B` * `Γ ⊢ • ⊏ • : B` * Meaning: The unit value `•` has type `B`. 3. **Union Type Introduction:** * `Γ ⊢ ∪ ⊏ ∪ : B` * Meaning: The union value `∪` has type `B`. 4. **Let Binding:** * `Γ ⊢ V ⊏ V' : A Γ, x: A ⊢ M ⊏ M' : B` * `Γ ⊢ let x = V; M ⊏ let x = V'; M': B` * Meaning: If `V` has type `A` and `M` has type `B` assuming `x` has type `A`, then `let x = V; M` has type `B`. 5. **Abort Rule:** * `Γ ⊢ V ⊏ V' : 0` * `Γ ⊢ abort V ⊏ abort V': B` * Meaning: If `V` has type `0` (empty type), then `abort V` has type `B`. 6. **Inl (Left Injection):** * `Γ ⊢ V ⊏ V' : A1` * `Γ ⊢ inl V ⊏ inl V': A1 + A2` * Meaning: If `V` has type `A1`, then `inl V` has type `A1 + A2` (sum type). 7. **Inr (Right Injection):** * `Γ ⊢ V ⊏ V' : A2` * `Γ ⊢ inr V ⊏ inr V': A1 + A2` * Meaning: If `V` has type `A2`, then `inr V` has type `A1 + A2` (sum type). 8. **Unit Value:** * `Γ ⊢ () ⊏ () : 1` * Meaning: The unit value `()` has type `1`. 9. **Case Analysis:** * `Γ ⊢ V ⊏ V' : A1 + A2 Γ, x1: A1 ⊢ M1 ⊏ M1' : B Γ, x2: A2 ⊢ M2 ⊏ M2' : B` * `Γ ⊢ case V {x1.M1 | x2.M2} ⊏ case V' {x1.M1' | x2.M2'}: B` * Meaning: If `V` has type `A1 + A2`, `M1` has type `B` assuming `x1` has type `A1`, and `M2` has type `B` assuming `x2` has type `A2`, then the case expression has type `B`. 10. **Pair Formation:** * `Γ ⊢ V1 ⊏ V1' : A1 Γ ⊢ V2 ⊏ V2' : A2` * `Γ ⊢ (V1, V2) ⊏ (V1', V2'): A1 × A2` * Meaning: If `V1` has type `A1` and `V2` has type `A2`, then the pair `(V1, V2)` has type `A1 × A2` (product type). 11. **Split (Pair Decomposition):** * `Γ ⊢ V ⊏ V' : A1 × A2 Γ, x: A1, y: A2 ⊢ M ⊏ M' : B` * `Γ ⊢ split V to (x, y).M ⊏ split V' to (x, y).M': B` * Meaning: If `V` has type `A1 × A2` and `M` has type `B` assuming `x` has type `A1` and `y` has type `A2`, then the split expression has type `B`. 12. **Roll (Recursive Type Introduction):** * `Γ ⊢ V ⊏ V' : A[μX.A/X]` * `Γ ⊢ rollμX.A V ⊏ rollμX.A V': μX.A` * Meaning: If `V` has type `A[μX.A/X]` (A with `μX.A` substituted for `X`), then `rollμX.A V` has type `μX.A` (recursive type). 13. **Unroll (Recursive Type Elimination):** * `Γ ⊢ V ⊏ V' : μX.A Γ, x: A[μX.A/X] ⊢ M ⊏ M' : B` * `Γ ⊢ unroll V to roll x.M ⊏ unroll V' to roll x.M': B` * Meaning: If `V` has type `μX.A` and `M` has type `B` assuming `x` has type `A[μX.A/X]`, then the unroll expression has type `B`. 14. **Thunk (Suspension):** * `Γ ⊢ M ⊏ M' : B` * `Γ ⊢ thunk M ⊏ thunk M': UB` * Meaning: If `M` has type `B`, then `thunk M` has type `UB` (suspended computation). 15. **Force (Evaluation of Suspension):** * `Γ ⊢ V ⊏ V' : UB` * `Γ ⊢ force V ⊏ force V': B` * Meaning: If `V` has type `UB`, then `force V` has type `B`. 16. **Return (Value):** * `Γ ⊢ M ⊏ M' : FA` * `Γ ⊢ ret V ⊏ ret V': A` * Meaning: If `M` has type `FA`, then `ret V` has type `A`. 17. **Bind (Monadic Binding):** * `Γ ⊢ M ⊏ M' : FA Γ, x: A ⊢ N ⊏ N' : B` * `Γ ⊢ bind x ← M; N ⊏ bind x ← M'; N': B` * Meaning: If `M` has type `FA` and `N` has type `B` assuming `x` has type `A`, then the bind expression has type `B`. 18. **Lambda Abstraction:** * `Γ, x: A ⊢ M ⊏ M' : B` * `Γ ⊢ λx: A.M ⊏ λx: A.M': A → B` * Meaning: If `M` has type `B` assuming `x` has type `A`, then `λx: A.M` has type `A → B` (function type). 19. **Application:** * `Γ ⊢ M ⊏ M' : A → B Γ ⊢ V ⊏ V' : A` * `Γ ⊢ MV ⊏ M'V': B` * Meaning: If `M` has type `A → B` and `V` has type `A`, then `MV` has type `B`. 20. **Record Update:** * `Γ ⊢ M1 ⊏ M1' : B1 Γ ⊢ M2 ⊏ M2' : B2` * `Γ ⊢ {π ← M1 | π' → M2} ⊏ {π ← M1' | π' → M2'}: B1 & B2` * Meaning: If `M1` has type `B1` and `M2` has type `B2`, then the record update expression has type `B1 & B2`. 21. **And Type Introduction (Left Projection):** * `Γ ⊢ M ⊏ M' : B1 & B2` * `Γ ⊢ πM ⊏ πM': B1` * Meaning: If `M` has type `B1 & B2` (product type), then `πM` (left projection) has type `B1`. 22. **And Type Introduction (Right Projection):** * `Γ ⊢ M ⊏ M' : B1 & B2` * `Γ ⊢ π'M ⊏ π'M': B2` * Meaning: If `M` has type `B1 & B2` (product type), then `π'M` (right projection) has type `B2`. 23. **Roll with Variable:** * `Γ ⊢ M ⊏ M' : B[vY.B/Y]` * `Γ ⊢ rollvY.B M ⊏ rollvY.B M': vY.B` * Meaning: If `M` has type `B[vY.B/Y]`, then `rollvY.B M` has type `vY.B`. 24. **Unroll with Variable:** * `Γ ⊢ M ⊏ M' : vY.B` * `Γ ⊢ unroll M ⊏ unroll M': B[vY.B/Y]` * Meaning: If `M` has type `vY.B`, then `unroll M` has type `B[vY.B/Y]`. ### Key Observations * The rules define a type system with features like sum types, product types, recursive types, and monadic effects. * The rules use a judgement form `Γ ⊢ M ⊏ M' : A`, which suggests a relation between two terms `M` and `M'` of type `A` in context `Γ`. This could represent a form of subtyping, refinement typing, or program equivalence. * The presence of `UB` and `FA` types, along with `thunk`, `force`, `ret`, and `bind` rules, indicates the presence of monadic effects, likely for handling side effects or control flow. * The rules for `roll` and `unroll` define recursive types, allowing for the definition of self-referential data structures. ### Interpretation The image presents a formal type system that likely underpins a programming language or logical framework. The rules define how to assign types to terms and how to derive new judgements from existing ones. The system includes features for handling data structures (products, sums, recursive types), control flow (monads), and potentially program equivalence or refinement. The specific meaning of the `⊏` relation would need further context to fully understand, but it likely plays a crucial role in the system's semantics. The rules are essential for ensuring type safety and reasoning about the behavior of programs within this system.

\n ## Mathematical Notation Grid ### Overview The image presents a grid of mathematical expressions, likely representing logical or type-theoretic statements. Each cell in the grid contains a single expression. The expressions are written using a combination of Greek letters, mathematical symbols, and subscripted variables. The overall layout is a rectangular arrangement of these expressions. ### Components/Axes There are no explicit axes or legends in the image. The grid itself forms the structure. The expressions are arranged in a roughly 6x7 grid. There is a small circular symbol in the top-center of the grid, which appears to be a bullet point or a small circle. ### Detailed Analysis or Content Details Here's a transcription of each expression in the grid, row by row. Due to the complexity of the notation, some interpretations may be approximate. **Row 1:** 1. Γ, x:A, Γ ⊢ x ∈ x:A 2. Γ ⊢ ∅:B • ∅:B 3. Γ ⊢ V ∈ V':0 4. Γ, x:A + M ∈ M':B 5. Γ ⊢ abort V ∈ abort V':B 6. Γ ⊢ V ∈ V':A₂ 7. Γ ⊢ find V ∈ find V':A₁ + A₂ **Row 2:** 8. Γ ⊢ V ∈ V':A₁ + A₂ 9. Γ, x₁, x₂:A + M₁ ∈ M₁':B 10. Γ ⊢ case V[x₁, x₂]M₁ ⊢ case V'[x₁, x₂]M₁':B 11. Γ ⊢ ∅():1 12. Γ ⊢ V₁(V₂):A₁ × A₂ 13. Γ, x:A, y:A + M ∈ M':B **Row 3:** 14. Γ ⊢ V ∈ V':A₁ × A₂ 15. Γ ⊢ V₂ ∈ V₂':A₂ 16. Γ ⊢ split V to (x, y)M ⊢ split V' to (x, y)M':B 17. Γ ⊢ V ∈ V':μ.A[X] 18. Γ, x:A, μ.A[X] + M ∈ M':B 19. Γ ⊢ rollμ.A V ⊢ rollμ.A V':μ.A **Row 4:** 20. Γ ⊢ unroll V to roll x.M ⊢ unroll V' to roll x.M':B 21. Γ ⊢ M ∈ M':B 22. Γ ⊢ V ∈ V':UB 23. Γ ⊢ force V ⊢ force V':B 24. Γ ⊢ ret V ⊢ ret V':FA **Row 5:** 25. Γ ⊢ M ∈ M':FA 26. Γ, x:A + N ∈ N':B 27. Γ, x:A + M ∈ M':B 28. Γ ⊢ λx:A M ⊢ λx:A M':A → B 29. Γ ⊢ M ∈ M':A → B 30. Γ ⊢ V ∈ V':A **Row 6:** 31. Γ ⊢ M ∈ M':B₁ & B₂ 32. Γ ⊢ M ∈ M':B₁ & B₂ 33. Γ ⊢ M ∈ M':B[V/Y] 34. Γ ⊢ π M ∈ π' M':B₁ 35. Γ ⊢ π' M₂ ∈ π' M₂':B₂ 36. Γ ⊢ roll y.V ⊢ roll y.V':B **Row 7:** 37. Γ ⊢ M ∈ M':Y/B 38. Γ ⊢ M ∈ M':Y/B 39. Γ ⊢ M ∈ M':B[V/Y] ### Key Observations The expressions appear to be related to a formal system, possibly a type theory or a logic for programming languages. The use of "Γ ⊢" suggests a proof or derivation context. The expressions involve concepts like types (A, B, etc.), variables (x, y, etc.), functions (λx:A M), and potentially some form of computation or evaluation (V, M). The presence of "roll" and "unroll" suggests operations on some data structure. The notation with "V/Y" indicates substitution. ### Interpretation The image likely represents a set of inference rules or type judgments within a formal system. Each line represents a rule that allows one to derive a new judgment from existing ones. The symbols and notation are highly specialized, suggesting a deep understanding of the underlying formal system is required to fully interpret the meaning of each expression. The grid format suggests a systematic exploration of different possible rules or derivations. The expressions seem to be building up a system for reasoning about types, values, and computations. The presence of both "V" and "V'" in many expressions suggests a relationship between an original value and a transformed or evaluated value. The bullet point in the top-center may indicate a starting point or a central concept within the system. Without further context, it's difficult to determine the specific purpose or application of this formal system.

## Formal Inference Rules: Type System Subtyping Relations ### Overview The image displays a collection of formal inference rules, likely from a type system or programming language theory paper. These rules define a subtyping or ordering relation (denoted by `⊑`) between terms (`V`, `M`) and types (`A`, `B`). The rules are presented in a standard natural deduction style, with premises above a horizontal line and the conclusion below. The notation uses a typing context `Γ`. ### Components/Axes * **Primary Symbols:** * `Γ`: Typing context. * `⊢`: Turnstile, denoting "entails" or "proves". * `⊑`: Subtyping or ordering relation. * `: A`, `: B`: Type annotations. * `⊆`: Appears to be a variant or specific form of the subtyping relation, often used with variables (`x ⊆ x`). * **Type Constructors:** * `A1 + A2`: Sum type (disjoint union). * `A1 × A2`: Product type (tuple/record). * `A[μX.A/X]`: Recursive type unfolding. * `μX.A`: Recursive type. * `U B`: Likely a "thunk" or suspended computation type. * `F A`: Likely a "future" or monadic type. * `A → B`: Function type. * `B1 & B2`: Intersection type. * `vY.B`: Appears to be a form of recursive type or binder (possibly "v" for "recursive variable"). * **Term Formers/Constructors:** * `let x = V; M`: Let binding. * `abort V`: Abort operation. * `inl V`, `inr V`: Injections into sum types. * `case V{x1.M1 | x2.M2}`: Case analysis on sum types. * `(V1, V2)`: Tuple construction. * `split V to (x,y).M`: Destructuring a product. * `roll_μX.A V`, `unroll V to roll x.M`: Rolling/unrolling recursive types. * `thunk M`, `force V`: Thunking and forcing delayed computations. * `ret V`: Returning a value in a monadic context. * `bind x ← M; N`: Monadic bind. * `λx:A.M`: Lambda abstraction (function definition). * `M V`: Function application. * `{π ↦ M1 | π' ↦ M2}`: Record construction with labels `π`, `π'`. * `πM`, `π'M`: Projection from a record. * `roll_vY.B M`, `unroll M`: Another form of rolling/unrolling, possibly for a different recursive type construct. ### Detailed Analysis / Content Details The image contains 24 distinct inference rules. Below is a transcription of each rule's conclusion (below the line), grouped by the type constructor they primarily involve. The premises are omitted for brevity but follow the standard pattern of requiring subtyping relations for the components. **1. Base & Variable Rules:** * `Γ ⊢ x ⊆ x : A` (Variable reflexivity) * `Γ ⊢ • : B ⊢ • ⊆ • : B` (Empty context/base case) * `Γ ⊢ U ⊆ U : B` (Thunk type subtyping) **2. Let Binding & Abort:** * `Γ ⊢ let x = V; M ⊆ let x = V'; M' : B` * `Γ ⊢ abort V ⊆ abort V' : 0` **3. Sum Types (+):** * `Γ ⊢ inl V ⊆ inl V' : A1 + A2` * `Γ ⊢ inr V ⊆ inr V' : A1 + A2` * `Γ ⊢ case V{x1.M1 | x2.M2} ⊆ case V'{x1.M1' | x2.M2'} : B` **4. Product Types (×):** * `Γ ⊢ (V1, V2) ⊆ (V1', V2') : A1 × A2` * `Γ ⊢ split V to (x,y).M ⊆ split V' to (x,y).M' : B` **5. Recursive Types (μ):** * `Γ ⊢ roll_μX.A V ⊆ roll_μX.A V' : μX.A` * `Γ ⊢ unroll V to roll x.M ⊆ unroll V' to roll x.M' : B` **6. Computational/Effect Types (U, F):** * `Γ ⊢ thunk M ⊆ thunk M' : U B` * `Γ ⊢ force V ⊆ force V' : B` * `Γ ⊢ ret V ⊆ ret V' : F A` * `Γ ⊢ bind x ← M; N ⊆ bind x ← M'; N' : B` **7. Function Types (→):** * `Γ ⊢ λx:A.M ⊆ λx:A.M' : A → B` * `Γ ⊢ M V ⊆ M' V' : B` **8. Intersection Types (&):** * `Γ ⊢ {π ↦ M1 | π' ↦ M2} ⊆ {π ↦ M1' | π' ↦ M2'} : B1 & B2` * `Γ ⊢ πM ⊆ πM' : B1` * `Γ ⊢ π'M ⊆ π'M' : B2` **9. Advanced Recursive/Unrolling (vY.B):** * `Γ ⊢ roll_vY.B M ⊆ roll_vY.B M' : vY.B` * `Γ ⊢ unroll M ⊆ unroll M' : B[vY.B/Y]` ### Key Observations 1. **Systematic Structure:** Every rule follows the same pattern: if the subtyping relation `⊑` holds for all components in the premises, then it holds for the constructed term in the conclusion. This is characteristic of a **coinductive** or **equational** definition of a relation. 2. **Underlined `B`:** The type `B` in the conclusion of many rules is underlined. This is a non-standard notation and may indicate that `B` is a specific, fixed type (like a "answer type" or "result type") in this system, or it could be a typographical emphasis from the source document. 3. **Two Flavors of Recursion:** The rules distinguish between `μX.A` (a standard recursive type) and `vY.B` (a less common construct, possibly a "recursive type in negative position" or a "recursive computation type"). The unrolling rule for `vY.B` involves a substitution `B[vY.B/Y]`. 4. **Effect System:** The presence of `U` (thunk), `F` (future/monad), `ret`, and `bind` strongly suggests this is a **type system for a language with computational effects** (like state, exceptions, or I/O), managed via monads or similar constructs. 5. **No Axiom for `⊑` Itself:** The image does not show a reflexivity or transitivity rule for `⊑` as a standalone relation. Its properties are entirely defined by its interaction with the term and type formers. ### Interpretation This image presents the **core equational theory or subtyping rules for a sophisticated type system**. The system appears designed for a functional programming language with: * **Algebraic Data Types:** Sum (`+`) and Product (`×`) types. * **Recursive Types:** At least two distinct forms (`μ` and `v`). * **Effect Handling:** Via thunks (`U`), monads (`F`, `ret`, `bind`), and explicit `abort`. * **Intersection Types:** (`&`), allowing terms to have multiple types simultaneously. The relation `⊑` likely represents **contextual equivalence**, **bisimulation**, or a **preorder on terms** that is sound with respect to some notion of program behavior. The rules are **compositional**: the relation on complex terms is defined purely from the relation on their immediate subterms. This is a foundational piece for proving properties like type safety, compiler optimizations (e.g., inlining, dead code elimination), or program equivalence in a language with effects and recursion. The underlined `B` might be a key technical device, perhaps representing the "type of observations" or "return type" in a coinductive definition of behavioral equivalence.

## Logical Rules Diagram: Type System Inference Rules ### Overview The image depicts a formal system of logical inference rules, likely from a type theory or programming language semantics context. It consists of 25+ rules organized in a grid-like structure, each representing a type-preserving transformation or operational behavior. Rules involve variables (`x`, `M`, `V`), types (`A`, `B`), and operations (`let`, `case`, `split`, `roll`, `unroll`, etc.). ### Components/Axes - **Structure**: Rules are presented as horizontal lines with premises (above the line) and conclusions (below the line). - **Symbols**: - `Γ ⊢ ...` : Type context entailment - `⊆` : Subtyping or inclusion - `→` : Function type - `∧` : Logical conjunction (and) - `∨` : Logical disjunction (or) - `μ` : Type constructor (e.g., for recursive types) - `λ` : Lambda abstraction - `∀` : Universal quantification - **Operations**: - `let`, `case`, `split`, `roll`, `unroll`, `thunk`, `force`, `bind`, `ret`, `abort`, `inl`, `inr` ### Detailed Analysis 1. **Substitution Rule**: ``` Γ ⊢ V ⊆ V' : A Γ, x : A, M ⊆ M' : B ------------------------ Γ ⊢ let x = V; M ⊆ let x = V'; M' : B ``` Preserves subtyping under variable binding. 2. **Case Analysis**: ``` Γ ⊢ V ⊆ V' : A₁ + A₂ Γ, x₁ : A₁, M₁ ⊆ M'₁ : B Γ, x₂ : A₂, M₂ ⊆ M'₂ : B ----------------------------------------- Γ ⊢ case V{x₁.M₁ | x₂.M₂} ⊆ case V'{x₁.M'₁ | x₂.M'₂} : B ``` Handles sum types (`A₁ + A₂`) with pattern matching. 3. **Pair Splitting**: ``` Γ ⊢ V ⊆ V' : A₁ × A₂ Γ, x : A₁, y : A₂, M ⊆ M' : B ---------------------------------------- Γ ⊢ split V to (x,y).M ⊆ split V' to (x,y).M' : B ``` Deconstructs pairs into components. 4. **Monadic Operations**: - **Roll/Unroll**: ``` Γ ⊢ V ⊆ V' : μX.A Γ ⊢ roll V ⊆ roll V' : μX.A ``` Encapsulates values in a monad (`μX.A`). - **Thunk/Force**: ``` Γ ⊢ M ⊆ M' : U B Γ ⊢ thunk M ⊆ thunk M' : U B Γ ⊢ force V ⊆ force V' : B ``` Manages lazy evaluation. 5. **Error Handling**: ``` Γ ⊢ () ⊆ () : 1 Γ ⊢ abort V ⊆ abort V' : B ``` Represents unit type and error propagation. 6. **Binding/Return**: ``` Γ ⊢ M ⊆ M' : F A Γ, x : A, N ⊆ N' : B ---------------------------------------- Γ ⊢ bind x ← M; N ⊆ bind x ← M'; N' : B ``` Chains monadic actions. ### Key Observations - **Type Preservation**: All rules ensure that operations preserve subtyping (`⊆`). - **Monadic Structure**: Rules for `roll`, `unroll`, `bind`, and `force` suggest a monadic type system (e.g., for IO or state). - **Sum/Prod Types**: Explicit handling of `A₁ + A₂` (sum) and `A₁ × A₂` (product) types. - **Error Propagation**: `abort` and `ret` rules indicate explicit error handling. ### Interpretation This system formalizes a **strongly typed, effectful programming language** with: 1. **Type Safety**: Subtyping ensures operations respect type constraints. 2. **Computational Effects**: Monadic operations (`roll`, `bind`) manage side effects (e.g., IO, state). 3. **Pattern Matching**: `case` and `split` rules enable algebraic data type deconstruction. 4. **Lazy Evaluation**: `thunk`/`force` rules support non-strict semantics. The rules collectively define a **calculus of constructions** or **dependent type system**, where types can depend on terms (e.g., `μX.A`). The presence of `abort` and `ret` suggests a **sum type for errors** (`A + B`), common in total functional languages. No numerical data or trends are present; the focus is on syntactic and semantic rules for type checking and program behavior.