## Diagram: Result Orderings (Fig. 17) ### Overview The image displays five separate Hasse diagrams illustrating different ordering relations on a set of result values. These diagrams are labeled as "Fig. 17. Result Orderings" and appear to be from a technical document on formal methods, programming language semantics, or verification, where different notions of approximation or error are being compared. The diagrams use nodes labeled with specific return values and special symbols, connected by lines indicating an ordering relationship (typically from a more specific to a more general or erroneous value). ### Components/Axes The image is composed of five distinct diagrams, each with a title and a set of nodes connected by lines. There are no traditional chart axes. The key components are the node labels and the diagram titles. **Common Node Labels:** * `ret false`: Represents a return value of boolean `false`. * `ret true`: Represents a return value of boolean `true`. * `ϒ` (Greek letter Upsilon): Likely represents an "undefined" or "unspecified" value. * `Ω` (Greek letter Omega): Likely represents a "divergent", "error", or "bottom" value in a semantic ordering. **Diagram Titles (in order of appearance, top to bottom, left to right):** 1. **Top-Left:** `Diverge Approx. ≤` 2. **Top-Right:** `Error Approx. ⊑` 3. **Middle-Left:** `Error Approx. up to left-divergence ≤⊑` 4. **Middle-Right:** `Error Approx. up to right-divergence ⊒≥` 5. **Bottom-Center:** `Error Approx. up to right-divergence Op ≤⊑` ### Detailed Analysis Each diagram shows a partial order. Lines connect nodes, with the upper node being "greater than" or "more general/approximating" the lower node in the context of the diagram's title. **1. Diverge Approx. ≤ (Top-Left)** * **Structure:** A V-shape. * **Nodes & Order:** `ret false` and `ret true` are both below `Ω`. `ϒ` is also below `Ω`. `ret false` and `ret true` are not connected to each other or to `ϒ`. * **Interpretation:** Under the "Diverge Approximation" order (`≤`), both definite boolean results (`ret false`, `ret true`) and the unspecified value (`ϒ`) are considered less than or equal to the divergent/error value (`Ω`). This suggests `Ω` is the top element, representing the most uncertain or erroneous outcome. **2. Error Approx. ⊑ (Top-Right)** * **Structure:** A V-shape, inverted relative to the first diagram. * **Nodes & Order:** `ret false`, `ret true`, and `Ω` are all below `ϒ`. * **Interpretation:** Under the "Error Approximation" order (`⊑`), the boolean results and the divergent value are all considered less than or equal to the unspecified value (`ϒ`). Here, `ϒ` is the top element. **3. Error Approx. up to left-divergence ≤⊑ (Middle-Left)** * **Structure:** A V-shape. * **Nodes & Order:** `ret false` and `ret true` are both below a combined node labeled `ϒ,Ω`. * **Interpretation:** This order (`≤⊑`) treats `ϒ` and `Ω` as equivalent or merged at the top. Both boolean results are less than this combined "error/undefined" state. **4. Error Approx. up to right-divergence ⊒≥ (Middle-Right)** * **Structure:** A diamond shape. * **Nodes & Order:** * Top: `Ω` * Middle: `ret false` and `ret true` (connected to both top and bottom). * Bottom: `ϒ` * **Flow/Relationships:** `ϒ` is below both `ret false` and `ret true`. Both `ret false` and `ret true` are below `Ω`. There is no direct line between `ret false` and `ret true`. * **Interpretation:** This order (`⊒≥`) creates a diamond where `ϒ` is the bottom (least defined), the boolean results are intermediate, and `Ω` is the top (most erroneous/divergent). **5. Error Approx. up to right-divergence Op ≤⊑ (Bottom-Center)** * **Structure:** A diamond shape, inverted relative to the previous diagram. * **Nodes & Order:** * Top: `ϒ` * Middle: `ret false` and `ret true` (connected to both top and bottom). * Bottom: `Ω` * **Flow/Relationships:** `Ω` is below both `ret false` and `ret true`. Both `ret false` and `ret true` are below `ϒ`. There is no direct line between `ret false` and `ret true`. * **Interpretation:** This order (`Op ≤⊑`) inverts the previous diamond. `Ω` is the bottom, the boolean results are intermediate, and `ϒ` is the top. ### Key Observations * **Symbol Consistency:** The same four symbols (`ret false`, `ret true`, `ϒ`, `Ω`) are used across all diagrams, but their hierarchical relationships change fundamentally based on the defined order. * **Structural Variety:** The diagrams explore different lattice structures: simple V-shapes (1, 2, 3) and diamond shapes (4, 5). * **Role of `ϒ` and `Ω`:** These two special values swap positions as the top or bottom element depending on the approximation strategy. In diagram 3, they are merged. * **Boolean Results:** `ret false` and `ret true` are always treated as peer values at the same level within any given ordering; they are never compared directly to each other. ### Interpretation This figure is a comparative study of different formal semantics for handling approximation, error, and divergence in computational results. It visually defines five distinct "result orderings." * **What it demonstrates:** The diagrams show how the same set of possible outcomes (two boolean values, an unspecified value, and a divergent/error value) can be organized into different hierarchies of "informativeness" or "correctness." The choice of ordering (`≤`, `⊑`, `≤⊑`, `⊒≥`, `Op ≤⊑`) reflects different philosophical or practical approaches to error modeling. * **Relationship between elements:** The lines represent a "less than or equal to" relation in the context of approximation. A value lower in the diagram is considered more precise, more defined, or "better" than a value above it, which represents a more approximate, less defined, or erroneous state. * **Notable patterns:** The contrast between the "Diverge Approx." (where `Ω` is worst) and "Error Approx." (where `ϒ` is worst) is fundamental. The "up to..." variants create hybrid or inverted structures. The diamond shapes (4 & 5) are particularly interesting as they place the boolean results as intermediates between two different kinds of non-value (`ϒ` and `Ω`), suggesting a nuanced spectrum from undefined (`ϒ`) through defined-but-finite (`ret true/false`) to non-terminating/error (`Ω`), or vice-versa. * **Underlying purpose:** This is likely used to formally specify and compare the behavior of program analysis techniques, type systems, or abstract interpretation methods. The figure allows a reader to quickly contrast how different formalisms treat the relationship between normal results, unspecified behavior, and outright errors or divergence.