表达操作语义时出现符号问题

Question

我正在尝试编写一些推理规则,但我无法理解通常用于编写它们的符号的含义.

例如:我为某个类型表达式编写了以下规则:

 class(r) ? t,  \there_exists v ? r ? type(v)
-------------------------------------------------------------
 ?, m:n -> r ? n:(?, r, {}) <-  r

m是一个声明n被替换为r.

(如果r在表达式属于t(类型表达)并且存在v使得r属于的类型v).

可能是我的等式是完全错误的.至少有人请解释?和:运营商的意思.同样在本杰明皮尔斯的书中,他称之为?打字环境.有人可以通过一个例子来解释它的含义(如果例子是在Haskell或Lisp或C++中,我会很感激)

谢谢

PS:这不是作业.

Answer 1

在高级别,符号很简单:假设线条上方的条件保持不变,则线条下方的表达式为真.

Γ是一个打字上下文 - 也就是说,它是一组变量和类型.这些对将变量映射到类型.⊢仅仅意味着"在上下文中".冒号只是将变量与类型组合在一起 - 就像::在Haskell或:Scala或Ocaml中一样.所以类似? ? x:?意味着"在上下文中,Γ,x具有类型σ".类似的东西?,x:?意味着由?和组成的背景x:?.

本质上,上下文表示其他变量具有的所有类型.因此,x:? ? ?这意味着x已经输入?的?,它可以让你平凡的解决? ? x:?.所有这一切都在说,如果x在上下文中绑定某种类型,它在该上下文中具有该类型.

您可以将输入上下文视为"外部"中的所有类型信息.所以在上面的段落中的琐碎的声明基本上告诉你,如果你看到一个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语法高亮显示器与最后一个例子斗争是有趣的.我想知道它认为的是哪种语言.