我正在尝试编写一些推理规则,但我无法理解通常用于编写它们的符号的含义。
例如: 我为某种类型表达式编写了以下规则:
class(r) ∈ t, \there_exists v ⊢ r ∈ type(v)
-------------------------------------------------------------
Γ, m:n -> r ⊢ n:(Γ, r, {}) <- r
m
是一个声明,其中 n
被 r
替换。
(如果表达式中的r
属于t
(类型表达式)并且存在v
使得r
属于 v
类型)。
可能我的方程完全错误。
至少请有人解释一下 ⊢
和 :
运算符的含义。
同样在 Benjamin Pierce 的书中,他将 Γ
称为打字上下文。
有人可以用一个例子解释它的含义吗(如果这个例子是用 Haskell、Lisp 或 C++ 编写的,我会很感激)
谢谢
PS:这不是作业。
最佳答案
在较高层次上,符号很简单:假设行上方的条件成立,则行下方的表达式为真。
Γ 是一个类型上下文——也就是说,它是一组变量和类型对。这些对将变量映射到类型。 ⊢ 的意思是“在上下文中”。冒号只是将变量与类型组合起来——就像 ::
在 Haskell 中或 :
在 Scala 或 Ocaml 中。所以类似 Γ ⊢ x:σ
意味着“在上下文 Γ 中,x 具有类型 σ”。类似 Γ,x:σ
表示由 Γ
组成的上下文和x:σ
.
本质上,上下文代表了其他变量所具有的所有类型。所以x:σ ∈ Γ
意味着x
类型为σ
在Γ
,这可以让您轻松解决 Γ ⊢ x:σ
。这一切都说明如果 x
绑定(bind)到上下文中的某种类型,它在该上下文中具有该类型。
您可以将类型上下文视为来自“外部”的所有类型信息。因此,上一段中的简单陈述基本上告诉您,如果您看到 x
和x
已经有类型 σ
,你可以推断 x
类型为σ
。不是很有趣,但非常重要!
您可以将此规则写为:
x:σ ∈ Γ
-------
Γ ⊢ x:σ
如果我们有 LaTeX 就好了:P。我想我们没有 math.se 或 cstheory.se 那么酷。
这是一个稍微复杂一点的例子。本质上,我们想要在简单类型的 lambda 演算中对应用程序的工作方式进行编码。其实很简单:给定一个函数f
类型 τ → τ'
和一个值x
类型 τ
然后f x
类型为τ'
。在 Haskell 中,这看起来像应用 f :: Int -> Bool
上x :: Int
。很明显 f x :: Bool
。所以让我们把这个写出来。
条件(最高位)是,在某些上下文中,f
有一个类型 τ → τ'
:Γ ⊢ f:τ → τ'
。此外,在同一上下文中,x
类型为τ
:Γ ⊢ x:τ
。放在一起,我们得到:Γ ⊢ f:τ → τ' Γ ⊢ x:τ
.
现在到最后一点。鉴于这两种类型,我们知道什么?我们知道应用程序的类型f x
但仅在相同的上下文中。 (这就是为什么 Γ
很重要。)所以我们得到: Γ ⊢ f x:τ'
.
现在,把所有这些放在一起,我们有:
Γ ⊢ f:τ → τ' Γ ⊢ x:τ
--------------------
Γ ⊢ f x:τ'
看到 StackOverflow 语法荧光笔与最后一个示例的斗争很有趣。我想知道它认为是哪种语言。
关于haskell - 表达操作语义时遇到符号问题,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/11465966/