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