haskell - 我如何解释这篇论文上的打字规则？

Question

"On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy" 上有这些输入规则。纸:



来自 “What part of Milner-Hindley do you not understand?” Stack Overflow 问题，我可以阅读其中的一些英文，但仍然很难弄清楚如何从中制作类型检查器。这是我阅读前 4 条规则的尝试:

斧头 : 作为一个公理，如果 x 具有类型 A，则 x 具有类型 A。(这不是很明显吗？)

切 : 如果一个上下文 Γ证明 t has type A , 和另一个上下文 ∆ , 用断言 x has type A 扩展, 证明 u has type B ，那么这两个上下文一起证明了所有出现的 x 的替换通过 t在 u有类型 B . (这是什么意思？为什么有两个上下文，额外的一个来自哪里？另外，这似乎是替换的规则，但是，如果替换不是一个术语，而是一个操作呢？经典的 Milner- Hindley 没有这样的东西；它只有一个非常简单的 App 规则。)

弱 : 如果上下文证明 t has type A , 然后用语句 x has type B 扩展该上下文仍然证明t has type A . (同样，这不是很明显吗？)

控制 : 如果上下文扩展为 x1 has type !A和 x2 has type !A证明 t has type B ，然后是上下文，扩展为 x has type !A证明替换所有出现的x1和 x2通过 x在 t有类型 B . (似乎是另一个替换规则？但是为什么上面有两个术语，下面有一个术语？另外，为什么那些 ! s？所有这些都会显示在类型检查器上吗？)

我很明白这些规则想说什么，但是在它真正点击之前我错过了一些东西，我能够实现相应的类型检查器。我怎样才能理解这些规则？

Answer 1

这有点太宽泛了，但是从您的评论来看，我猜您缺乏线性类型系统的一些基础知识。这个系统有弱化(在线性逻辑中通常不允许)，所以它实际上对应于仿射直觉逻辑。

关键思想是:您最多可以使用您拥有的每个值(例如变量)一次。

类型A (x) B (张量积)大致代表pair值的类型，从中可以投影出A值和 B值(value)。

类型A -o B代表一个线性函数，它消耗一个值 A (记住:最多使用一次!)并生成单个 B .

你可以有例如\x.x : A -o A但你不能有任何术语: A -o (A (x) A)因为那将要求您使用该参数两次。

类型!A ("of course A!") 代表 A 类型的值可以随意复制——就像你在非线性 lambda 演算中通常可以做的那样。这是由收缩规则完成的。

例如，!A -o !B表示一个普通函数:它需要一个值(无限数量的副本)并产生一个值(无限数量的副本)。你可以写一个函数!A -o (!A (x) !A)如下:

\a. (a (x) a)

请注意，每个具有多个前提的线性类型规则都必须在前提之间拆分环境变量(例如，一个得到 Gamma，另一个得到 Delta)，没有重叠。否则，您可能会复制线性变量。因此，Cut 有两个上下文。非线性切割将是:

G |- t: A        G, x:A |- u: B
--------------------------------
  G |- u[t/x]: B

但这里两个术语t和 u可以使用G中的变量，因此 u[t/x]可以使用两次变量——不好。相反，线性切割

G1 |- t: A        G2, x:A |- u: B
--------------------------------
  G1,G2 |- u[t/x]: B

强制您在两个前提之间拆分变量:您在 t 中使用的内容对 u 不可用.