2
4

2 回答 2

5

在高层次上，符号很简单：假设行以上的条件成立，则行以下的表达式为真。

Γ 是一个类型化上下文——也就是说，它是一组变量和类型对。这些对将变量映射到类型。⊢ 仅表示“在上下文中”。冒号只是将变量与类型组合在一起——就像::在 Haskell 或:Scala 或 Ocaml 中一样。所以类似的Γ ⊢ x:σ意思是“在上下文Γ中，x具有类型σ”。like表示由andΓ,x:σ组成的上下文。Γx:σ

本质上，上下文代表了其他变量所具有的所有类型。Sox:σ ∈ Γ表示x具有类型σin Γ，这可以让您轻松解决该问题Γ ⊢ x:σ。这就是说，如果x在上下文中绑定到某种类型，那么它在该上下文中具有该类型。

您可以将输入上下文视为来自“外部”的所有类型信息。所以上一段中的简单陈述基本上告诉你，如果你看到一个x并且x已经有类型σ，你可以推断出那个x有类型σ。不是很有趣，但很重要！

你可以把这条规则写成：

x:σ ∈ Γ
-------
Γ ⊢ x:σ

如果我们有 LaTeX ：P。我想我们不如 math.se 或 cstheory.se 酷。

这是一个稍微复杂一点的例子。本质上，我们想在简单类型的 lambda 演算中编码应用程序的工作方式。它实际上非常简单：给定一个 type 的函数f和τ → τ'一个 type 的值x，τ然后f x有 type τ'。在 Haskell 中，这看起来像应用f :: Int -> Bool在x :: Int. 很明显f x :: Bool。所以让我们把这个写出来。

条件（最高位）是，在某些情况下，f有一个类型τ → τ': Γ ⊢ f:τ → τ'。此外，在相同的上下文中，x具有类型τ: Γ ⊢ x:τ。放在一起，我们得到：Γ ⊢ f:τ → τ' Γ ⊢ x:τ.

现在到底部。鉴于这两种类型，我们知道什么？我们知道应用程序的类型，f x 但仅在相同的上下文中。（这就是Γ重要的原因。）所以我们得到：Γ ⊢ f x:τ'.

现在，把它们放在一起，我们有：

Γ ⊢ f:τ → τ' Γ ⊢ x:τ 
--------------------
     Γ ⊢ f x:τ'

看到 StackOverflow 语法荧光笔与最后一个示例的斗争很有趣。我想知道它认为这是哪种语言。

于 2012-07-13T08:26:28.220 回答
3

（Γ如果有人知道如何嵌入 LaTeX，请留下评论或编辑评论）是输入上下文的符号：您可以将其视为表达式与其类型之间的映射。

例如，让我们看两个上下文：

  • Γ0空地图和
  • Γ1 = Γ0, x:Int前一个丰富了类型信息，说x有 type Int。因此，:这里代表类型分配。

现在，在空上下文 ( Γ0) 中，无法键入表达式x + x，因为您不知道类型x（它不存储在映射中）。但是，在另一种情况下，我们有一个类型 for x(that is Int)，所以我们可以说 that x + xhas type Int。

形式上，我们使用了这样的规则：

  x : σ ∈ Γ
______________
 Γ ⊢ x + x: σ

请注意在:Haskell::中的含义。并且A ⊢ B被理解为“在A B持有的情况下。

PS：我有一个关于类型系统的课程，你可以在这里找到一些材料（你可以看看 Typed_Lambda_Calculus.pdf）。

于 2012-07-13T08:28:46.923 回答