haskell - 编写指称语义映射函数需要什么？

Question

我对指称语义的概念有点困惑。据我了解，指称语义应该描述函数和表达式在特定编程语言中的工作方式。用于描述这些功能以及它们如何工作的正确形式究竟是什么？ “域”到底是什么，如何构建映射功能？

例如，“do X while Y”的映射函数是什么？

我一直在网上阅读很多资料，但很难理解。这些描述会类似于上下文无关语法吗？

请告诉我，谢谢!

Answer 1

将外延视为从语法到“意义”的映射。您可能会看到它写在双括号中，以便您阅读 [[3]] = 3因为“语法 [数字 3] 的表示是数字 3”。

一个简单的例子是算术。通常你有一个像

[[x + y]] = [[x]] + [[y]]

+左边是句法加号和 +右边是算术加号。为了更清楚地说明这一点，我们可能会更改为 lispy 语法。

[[(+ x y)]] = [[x]] + [[y]]

现在要问的一个非常重要的问题是这个映射的范围(codomain)是多少？到目前为止，我一直假设将其视为“数字和加法存在的一些数学领域”就足够了，但这可能还不够。重要的是，您的示例将很快打破它。

[[do X while True]] = ???

因为我们不一定有一个包含不终止概念的数学域。

在 Haskell 中，这是通过将数学域称为“提升”域或 CPO 域来解决的，这基本上直接添加了非终止。例如，如果您的未提升域是整数 I那么提升的域是⊥ + I在哪里 ⊥被称为“底部”，它意味着不终止。

这意味着我们可以写(用 Haskell 语法)

[[let omega = 1 + omega in omega]] = ⊥

繁荣。我们有意义——无限循环的意义是……什么都没有!

在 Haskell 中提升域的技巧在于，因为 Haskell 是惰性的(非严格的)，所以可能会有数据类型和 ⊥ 的有趣交互。 .例如，如果我们有 type IntList = Cons Int IntList | Nil然后提升域超过 IntList包括⊥直接(一个完整的无限循环)以及像 Cons ⊥ ⊥ 这样的东西仍未完全解决，但提供比普通旧 ⊥ 更多的信息.

我故意写“更多信息”。 CPO 形成了“定义性”的部分顺序(即 PO)。 ⊥最大未定义，所以它是 <=到 CPO 中的任何其他内容。然后你会得到像 Cons ⊥ ⊥ <= Cons 3 ⊥ 这样的东西它以您的部分顺序形成一条链。你经常说如果 x <= y那么“y 包含比 x 更多的信息”或“y 比 x 定义更多”。

这对我来说最大的一点是，通过在我们的数学外延领域定义这种 CPO 结构，我们可以真正准确地讨论严格评估和非严格评估之间的区别。在严格的语言中(或者实际上，在您的语言可能有也可能没有的严格域中)，您的 CPO 都是“平坦的”，因为您要么有完全定义的结果，要么有 ⊥。没有别的了。当您的 CPO 不平坦时，就会发生懒惰。

另一个重要的一点是“你不能在底部进行模式匹配”的概念......如果我们将底部视为一个无限循环(尽管有了这个新的抽象模型，它并不一定意味着......例如，可能是段错误)那么这句格言只不过是表达停止问题的另一种方式。结果是所有可感知的函数都必须是“单调的”，如果 x <= y然后 f x <= f y .如果您花一些时间了解该概念，您会发现它禁止具有不同非底部行为的函数，无论它们的参数是否为底部。例如，停止预言机是非单调的

halting (⊥) = False     -- we can't pattern match on bottom!
halting _   = True

但是“断断续续的预言”是

hahahalting (⊥) = ⊥     -- we're still pattern matching, 
                            -- but at least the behavior is right
hahahalting _   = True

我们使用 seq 编写

hahahalting x = x `seq` True    -- valid Haskell

这也带来了明显的缓解the dangers of non-monotonic functions, like Haskell's spoon .我们可以通过利用不合理的异常捕获来编写它们……但如果我们不小心，它可能会导致非常不稳定的行为。

你可以从指称语义中学到很多东西，所以我将提供 Edward Z. Yang's notes关于指称语义。