编辑“︁Lean格”︁（章节）

== 应用案例 ==

=== 类型系统中的应用 ===

在类型系统中，格用于描述类型之间的子类型关系。例如，考虑以下类型层次结构：

<syntaxhighlight lang="lean">
inductive Animal
| dog | cat | bird

inductive Pet
| dog | cat
</syntaxhighlight>

这里可以定义一个子类型格，其中：
* 并运算表示最具体的共同超类型
* 交运算表示最一般的共同子类型

=== 程序分析中的应用 ===

在抽象解释中，格用于表示程序状态的可能值。例如，一个整数变量可能的状态可以构成如下格：

<mermaid>
graph TD
    Top[⊤ = any integer] --> Pos[positive]
    Top --> Neg[negative]
    Top --> Zero[zero]
    Pos --> Bottom[⊥ = no value]
    Neg --> Bottom
    Zero --> Bottom
</mermaid>