## Logical Rules: Type Systems and Properties ### Overview The image presents a collection of logical rules, likely related to type systems or program semantics. These rules are expressed using mathematical notation and logical symbols, defining relationships between types, expressions, and contexts. The rules are grouped into categories such as "Cast Universal Properties", "Type Universal Properties", and "Error Properties". ### Components/Axes **1. Cast Universal Properties:** - Located at the top of the image. - Subdivided into "Bound" and "Best" categories. - Contains rules involving type casting or subtyping, denoted by symbols like "⊢" and "⊏". **2. Retract Axiom:** - Located below "Cast Universal Properties". - Presents axioms related to retracting or unwrapping types. **3. Type Universal Properties:** - Located in the center of the image. - Organized in a table format with columns for "Type", "β" (beta reduction), and "η" (eta conversion). - Lists rules for various types such as +, 0, ×, 1, U, F, →, &, and ⊤. **4. Error Properties:** - Located at the bottom of the image. - Contains rules related to error handling or type checking in erroneous situations. - Includes labels "ERRBOT" and "STKSTRICT". ### Detailed Analysis or ### Content Details **Cast Universal Properties:** * **Up (Bound):** x: A ⊢ x ⊏ (A' ⇦ A) x: A ⊏ A' * **Up (Best):** x ⊏ x': A ⊏ A' ⊢ (A' ⇦ A) x ⊏ x': A' * **Down (Bound):** •: B' ⊢ (B ⇦ B') • ⊏: B ⊏ B' * **Down (Best):** • ⊏: B ⊏ B' ⊢ (B ⇦ B') •: B **Retract Axiom:** * x: A ⊢ (FA ⇐ F?) (ret (? ⇐ A) x)) ⊏ ret x: FA * x: UB ⊢ (B ⇐) (force (U¿ ⊏ UB) x)) ⊏ force x: B **Type Universal Properties:** | Type | β AND THE LIST GOES ON!

\n ## Table: Universal Properties ### Overview The image presents a table detailing Universal Properties, categorized into "Cast Universal Properties" and "Type Universal Properties". The table uses logical symbols and mathematical notation to define relationships between types and functions. The table is divided into columns representing "Bound", "Best", and additional columns specific to Type Universal Properties (β, η). A section at the bottom details "Error Properties" and "StkStrict". ### Components/Axes The table has the following structure: * **Header:** Divided into two main sections: "Cast Universal Properties" and "Type Universal Properties". * **Rows:** Represent different types or operations (+, 0, ×, 1, U, F, →, & , T, ERRor, StkStrict). * **Columns:** * "Up" and "Down" (under Cast Universal Properties) * "Bound", "Best" (under Cast Universal Properties) * "β", "η" (under Type Universal Properties) * **Footer:** Contains "Error Properties" and "StkStrict" sections. ### Detailed Analysis or Content Details **Cast Universal Properties:** * **Up:** `x: A ⊢ x ∈ (A' ↔ A) x: A ⊢ x ∈ A' ↔ (A' ↔ A) x ∈ A'` * **Down:** `•: B' ⊢ (B ↔ B') •: B ⊢ B' •: B ⊢ (B ↔ B') •: B` * **Retract Axiom:** `x: A ⊢ (FA ∈ E?)ret(⟨? A⟩x) ⊆ ret x: FA x: UB ⊢ (B ⊆ ¿)(force (U¿ ⊆ UB)x) ⊆ force x: B` * **Bound:** `x: A ⊢ x ∈ A' ↔ (A' ↔ A) x ∈ A'` * **Best:** `x ∈ A' ↔ (A' ↔ A) x ∈ A'` **Type Universal Properties:** * **+:** `case inL V{x1.E1 | ...} ∃E [V[x]] case inr V{x2.E2} ∃E [V[x2]]` * **0:** `E ∃E case x{0.E} : T where x: A₁ + A₂ ∈ E : T` * **×:** `split (V₁, V₂) to (x₁, x₂).E ∃E [V[x₁, V₂]] E ∃E split x to (x₁, x₂).E[x₁, x₂]` where `x: A₁ × A₂ + E : T` * **1:** `split (0) to .E ∃E E x: 1 + E ∃E split x to (0).E[0] : T where x: 1 + E : T` * **U:** `force thunk M ∃E M` * **F:** `bind x ← ret V; M ∃E M[V[x]]` * **→:** `(λx.A M)V ∃E M[V/x]` * **&:** `π(π → M') ∃E M' π(π → M') ∃E M'` * **T:** `•: T + • ∃E {}: T` **Error Properties:** * `Γ ⊢ + ⊢ U ∈ M' : B ⊆ B'` * `Γ ⊢ + ⊢ U ∈ M' : B ⊆ B'` **StkStrict:** * `Γ ⊢ x: B + S : B'` * `Γ ⊢ x: S[UB] ⊆ U : B'` ### Key Observations The table is densely packed with logical notation. The "Type Universal Properties" section appears to define how different type constructors (like +, 0, ×, etc.) interact with universal quantification (∃E) and substitution. The "Error Properties" and "StkStrict" sections seem to define constraints or conditions related to error handling and stack safety. The notation `∃E` appears frequently, suggesting a focus on existential quantification over environments. ### Interpretation This table likely comes from a formal semantics or type theory context, possibly related to a programming language or logic system. It defines the universal properties of various type constructors and operations. These properties are crucial for reasoning about the behavior of programs and ensuring type safety. The "Cast Universal Properties" section deals with type conversions and relationships, while the "Type Universal Properties" section defines the fundamental behavior of type-forming operations. The "Error Properties" and "StkStrict" sections are likely related to ensuring the correctness and safety of the system, particularly in the presence of errors or stack overflows. The notation is highly specialized and requires a strong background in formal methods to fully understand. The table is a precise specification of the rules governing type manipulation and evaluation within the system.

## Formal Logic/Type Theory Notation: Universal Properties and Error Rules ### Overview The image displays a set of formal mathematical/logical notation tables and inference rules, likely from a paper on programming language semantics, type theory, or formal verification. It defines properties related to type casting, type constructors, and error handling. The content is presented in three distinct sections: "Cast Universal Properties", "Type Universal Properties", and "Error Properties". ### Components/Axes The image is structured into three main horizontal sections, each with a title in a box: 1. **Cast Universal Properties**: A 2x2 table with row labels "Up" and "Down", and column labels "Bound" and "Best". Below it is a "Retract Axiom". 2. **Type Universal Properties**: A large table with three columns labeled "Type", "β" (beta), and "η" (eta). The "Type" column lists symbols for type constructors: `+`, `0`, `×`, `1`, `U`, `F`, `→`, `&`, `⊤`. 3. **Error Properties**: Two inference rules labeled "ErrBot" and "STKSTRICT". The notation uses standard symbols from logic and type theory: `:` (type annotation), `⊆` (subset/subtype), `⊢` (entails), `⊓` (meet/greatest lower bound), `⊔` (join/least upper bound), `×` (product type), `+` (sum type), `→` (function type), `&` (intersection type), `⊤` (top type), `U` (a type constructor, possibly for "thunk" or "universal"), `F` (a type constructor, possibly for "computation" or "effectful"), `abort`, `force`, `thunk`, `bind`, `ret`, `split`, `case`, `inl`, `inr`. ### Detailed Analysis #### Section 1: Cast Universal Properties This section defines properties for a "cast" operation, possibly between types or values. * **Table Structure**: * **Columns**: `Bound`, `Best` * **Rows**: `Up`, `Down` * **Content**: | | Bound | Best | |---|---|---| | **Up** | `x : A ⊓ x ⊆ ⟨A' ↣ A⟩x : A ⊆ A'` | `x ⊆ x' : A ⊆ A' ⊢ ⟨A' ↣ A⟩x ⊆ x' : A'` | | **Down** | `• : B' ⊢ (B ↣ B') • : B ⊆ B'` | `• : • : B' ⊢ • : (B ↣ B') • : B` | * **Retract Axiom**: * `x : A ⊢ ⟨FA ↣ E?⟩(ret ((? ↣ A)x)) ⊆ ret x : FA` * `x : UB ⊢ (B ↣ ?)(force ((U↣ UB)x)) ⊆ force x : B` #### Section 2: Type Universal Properties This table defines "β" (reduction) and "η" (expansion/extensionality) rules for various type constructors. * **Table Structure**: * **Columns**: `Type`, `β`, `η` * **Rows** (by Type symbol): | Type | β | η | |---|---|---| | `+` (Sum Type) | `case inl V{x₁, E₁ \| ...} ⊇ E₁[V/x₁]` and `case inr V{... \| x₂, E₂} ⊇ E₂[V/x₂]` | `E ⊇ case x{x₁, E[inl x₁/x] \| x₂, E[inr x₂/x]}` where `x : A₁ + A₂ ⊢ E : T` | | `0` (Empty/Bottom Type) | `-` (No rule) | `E ⊇ abort x` where `x : 0 ⊢ E : T` | | `×` (Product Type) | `split (V₁, V₂) to (x₁, x₂).E ⊇ E[V₁/x₁, V₂/x₂]` | `E ⊇ split x to (x₁, x₂).E((x₁, x₂)/x)` where `x : A₁ × A₂ ⊢ E : T` | | `1` (Unit Type) | `split () to ().E ⊇ E` | `x : 1 ⊢ E ⊇ split x to ().E(()/x) : T` where `x : 1 ⊢ E : T` | | `U` (Likely "Thunk" or "Universal" type) | `force thunk M ⊇ M` | `x : UB ⊢ x ⊇ thunk force x : UB` | | `F` (Likely "Computation" or "Effectful" type) | `bind x ← ret V; M ⊇ M[V/x]` | `• : FA ⊢ M ⊇ bind x ← M;[ret x/•] : B` and `• : A → B ⊢ • ⊇ λx:A. x : A → B` | | `→` (Function Type) | `(λx:A.M) V ⊇ M[V/x]` | (No explicit η rule listed in this cell) | | `&` (Intersection Type) | `π(π ↦ M \| π' ↦ M') ⊇ M` and `π'(π ↦ M \| π' ↦ M') ⊇ M'` | `• : B₁ & B₂ ⊢ • ⊇ {π ↦ π \| π' ↦ π'} : B₁ & B₂` | | `⊤` (Top Type) | `-` (No rule) | `• : T ⊇ • ⊇ {} : T` | #### Section 3: Error Properties Two inference rules defining properties of an error type `UB`. * **ErrBot**: * Premise: `Γ' | ⊢ M' : B'` * Conclusion: `Γ ⊆ Γ' | ⊢ UB ⊆ M' : B ⊆ B'` * **STKSTRICT**: * Premise: `Γ | x : B ⊢ S : B'` * Conclusion: `Γ | ⊢ S[UB/x] ⊆ UB_B : B'` ### Key Observations 1. **Symmetry in Cast Rules**: The "Up" and "Down" rules for "Bound" and "Best" show a symmetric structure, suggesting a duality in the casting or subtyping relationship being defined. 2. **Pattern in Type Rules**: For each type constructor, the β-rule describes how to eliminate a value of that type (e.g., pattern matching on `inl`/`inr` for `+`, projecting from a pair for `×`), while the η-rule describes how any value of that type can be expressed in a canonical form (e.g., any term of type `0` is equivalent to `abort`). 3. **Special Handling of `U` and `F`**: These constructors have rules involving `thunk`/`force` and `ret`/`bind`, respectively, which are characteristic of languages with effects, laziness, or computational types (like monads). 4. **Error Typing**: The "Error Properties" section defines how the type `UB` (likely a type for errors or undefined values) interacts with the typing context (`Γ`) and subtyping (`⊆`). The `STKSTRICT` rule suggests strictness in how errors are handled within a stack or context `S`. ### Interpretation This image presents a formal specification for a type system with sophisticated features. The "Universal Properties" likely refer to rules that must hold for all types or casts within the system, ensuring consistency and safety. * **The Cast Properties** define a disciplined way to convert between types (`A` and `A'`), possibly accounting for both "upcasting" (to a more general type) and "downcasting" (to a more specific type), with "Bound" representing a safe limit and "Best" representing an optimal or precise conversion. The "Retract Axiom" ensures that casting and then performing an operation (like `ret` or `force`) is equivalent to performing the operation directly, which is a form of coherence. * **The Type Universal Properties** are the core operational semantics of the language. The β-rules define computation (how programs run), while the η-rules define extensionality (when two programs are considered observationally equivalent). This separation is fundamental in defining a well-behaved programming language. The presence of rules for `abort`, `thunk`, and `bind` indicates the system models non-termination, laziness, and side effects. * **The Error Properties** integrate a special error type `UB` into the subtyping and typing rules. The `ErrBot` rule suggests `UB` is a subtype of all other types (`B ⊆ B'`), meaning an error can be used wherever any other type is expected—a common but potentially unsafe design choice that this formalism is making explicit. The `STKSTRICT` rule governs how substituting an error into a term `S` affects the resulting type. In summary, this is a dense, formal snapshot of a programming language's theoretical foundation, specifying how types, values, casts, computations, and errors interact according to strict logical rules. It would be used by programming language researchers or implementers to prove properties like type safety ("well-typed programs don't go wrong") or to guide the correct implementation of a compiler or interpreter.

## Technical Document: Type System Properties and Error Handling ### Overview The image presents a formal specification of type system properties, error handling rules, and type universal properties in a programming language context. It combines logical assertions, type operations, and error propagation mechanisms using mathematical notation and type theory constructs. ### Components/Axes 1. **Cast Universal Properties Table** - **Columns**: Bound, Best, Retract Axiom - **Rows**: Up, Down - **Notation**: Uses type casts (`⊆`), logical implications (`⇒`), and set operations (`⊆`, `⊇`) 2. **Type Universal Properties Table** - **Columns**: β (beta), η (eta) - **Rows**: Type constructors (`+`, `0`, `×`, `1`, `U`, `F`, `→`, `&`, `T`) - **Notation**: Case analysis, type splitting, and monadic operations 3. **Error Properties Section** - **Subsections**: ErrBot, StkStrict - **Notation**: Type refinement (`⊆`), error propagation (`⊆`), and strictness annotations ### Detailed Analysis #### Cast Universal Properties | Bound | Best | Retract Axiom | |-------|------|---------------| | Up: `x : A - x ⊆ ⟨A' ⇸ A⟩x : A ⊆ A'` | Up: `x ⊆ x' : A ⊆ A' - ⟨A' ⇸ A⟩x ⊆ x' : A` | `x : A ↦ ⟨FA ⇸ F?⟩(ret (⟨? ⇸ A⟩x)) ⊆ ret x : FA` | | Down: `• : B' - ⟨B ⇸ B'⟩• ⊆ • : B ⊆ B'` | Down: `• ⊆ • : B ⊆ B' - ⟨B ⇸ B'⟩• : B` | `x : U_B ↦ ⟨B ⇸ ?⟩(force (⟨U_? ⇸ U_B⟩x)) ⊆ force x : B` | #### Type Universal Properties | Type | β (Beta) | η (Eta) | |------|----------|---------| | `+` | `case inl V{x1.E1 | ...} ⇒ E1[V/x1]` | `E ⇒ case x{x1.E[inl x1/x] | x2.E[inr x2/x]}` | | `0` | - | `E ⇒ abort x` | | `×` | `split (V1,V2) to (x1,x2).E ⇒ E[V1/x1,V2/x2]` | `E ⇒ split x to (x1,x2).E[(x1,x2)/x]` | | `1` | `split () to ().E ⇒ E` | `x : 1 ↦ split x to ().E[()]/x : T` | | `U` | `force M ⇒ M` | `x : U_B ↦ x ⇒ thunk force x : U_B` | | `F` | `bind x ← ret V; M ⇒ M[V/x]` | `• : FA ↦ bind x ← •; M[ret x/•] : B` | | `→` | `(λx : A.M) V ⇒ M[V/x]` | `• : A → B ↦ λx : A. • x : A → B` | | `&` | `π{π ↦ M | π' ↦ M'} ⇒ M` | `• : B₁ & B₂ ↦ {π ↦ π • | π' ↦ π' •} : B₁ & B₂` | | `T` | - | `• : T ↦ { } : T` | #### Error Properties - **ErrBot**: - `Γ' | · ↦ M' : B'` - `Γ ⊆ Γ' | · ↦ U ⊆ M' : B ⊆ B'` - **StkStrict**: - `Γ | x : B ↦ S : B'` - `Γ | · ↦ S[U_B] ⊆ U_B' : B'` ### Key Observations 1. **Type Safety**: The Cast Universal Properties enforce safe type casting through bidirectional implications between source and target types. 2. **Monadic Operations**: The `bind` and `force` operations in the `F` and `U` rows implement monadic behavior for effect handling. 3. **Product/Union Types**: The `×` and `+` rows define tuple and sum type operations with explicit case analysis. 4. **Error Propagation**: The ErrBot and StkStrict sections formalize error handling through type refinement and strictness annotations. ### Interpretation This document formalizes a type system with: 1. **Type Casting Rules**: Ensuring safe upcasts (`A ⊆ A'`) and downcasts (`B' ⊆ B`) through logical implications. 2. **Effect Handling**: Using monadic operations (`bind`, `force`) to manage side effects and errors. 3. **Error Handling**: Differentiating between recoverable errors (`ErrBot`) and strict error propagation (`StkStrict`). 4. **Type Theory Foundations**: Employing dependent types (`π`, `λ`) and case analysis for algebraic data types. The specifications appear to implement a **graded type system** with: - **Bounded Casting**: Restricting casts to subtypes (`A ⊆ A'`) - **Error Annotations**: Explicit error handling through type refinements - **Strictness Control**: Differentiating between lazy (`U`) and strict (`F`) evaluation contexts The document likely serves as a formal verification of a programming language's type system, ensuring type safety while allowing controlled type casting and error handling.