问题标签 [denotational-semantics]

这里描述的 Haskell 中的底部据说是任何有错误、未终止或涉及无限循环的计算，是任何类型的......这是特定于 Haskell 的吗？我们知道在格理论中，还有一个概念Bottom……不应该根据定义的顺序来定义底部吗？

我发誓曾经有一件T 恤出售，上面印着不朽的文字：

哪一部分

你不明白吗？

就我而言，答案是……全部！

特别是，我经常在 Haskell 论文中看到这样的符号，但我不知道它是什么意思。我不知道它应该是什么数学分支。

我当然认识希腊字母表中的字母和诸如“∉”之类的符号（这通常意味着某物不是集合的元素）。

另一方面，我以前从未见过“⊢”（维基百科声称它可能意味着“分区”）。我也不熟悉这里的 vinculum 的使用。（通常，它表示分数，但这里似乎并非如此。）

如果有人至少可以告诉我从哪里开始寻找理解这个符号海洋的含义，那将很有帮助。

我正在编写语言规范，我需要解决以下基本问题。假设我有（诚然做作的）抽象语法：

这种语言的指称语义是什么样的？非终结符包含在 '<' 和 '>' 中，终结符不是。我想将1...映射6到自然数域。我完全不清楚的是我是否需要为非终端提供映射。似乎我不需要，因为，例如，<A> ::= <B> | <C>没有意义；它只是一个结构。忽略，暂时我们可以完全消除这条规则。

所以，就目前而言，这就是我认为完整的指称定义应该是这样的，其中右侧（斜体）表示自然数的相应值：

[[1]] =一

[[2]] =二

[[3]] =三

[[4]] =四

[[5]] =五

[[6]] =六

A从美学上讲，不提,B或根本不提似乎很奇怪C，但我认为这些符号永远不会出现在实际程序中（如4：），所以也许这就足够了。我所拥有的关于这个主题的所有材料都在他们的讨论中忽略了语言定义过程的这个非常简单的具体细节。

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

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

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

请告诉我，谢谢！

是否有函数式语言可以在类型检查器中指定某个计算是否保证终止？或者，您可以仅在 Haskell 中执行此操作吗？

关于 Haskell，在这个答案中，张贴者说

通常的思考方式是每个 Haskell 类型都被“提升”——它包含 ⊥。也就是说，Bool对应于{⊥, True, False}而不是仅仅{True, False}。这代表了 Haskell 程序不能保证终止并且可能有异常的事实。

另一方面，这篇关于 Agda的论文指出

一个正确的 Agda 程序是一个同时通过类型检查和终止检查的程序

即，所有的 Agda 程序都会终止，而BoolAgda 中的 a 正好对应{True, False}.

例如，在 Haskell 中你可以有一个 type 的值IO a，它告诉类型检查器需要 IO 来计算有问题的值。你能有一个类型Lifted a断言有问题的计算可能不会终止吗？也就是说，您允许不终止，但在类型系统中将其分开。（显然，就像在 Agda 中一样，您只能将值分为“绝对终止”和“可能不终止”）如果不是，是否有语言可以做到这一点？

我正在尝试在 Haskell 中编写一个程序来计算具有整数变量、一维（整数）数组和函数的命令式语言程序的指称语义。我开始使用的功能是以下类型：

其中状态如下：

第一部分是整数变量的值，而第二部分是特定索引处的数组变量的值。

该计划将具有以下品质：

• progsem 将在程序执行后返回结果状态

• 函数有两个参数列表，一个用于整数变量，一个用于数组变量。

• 函数按值调用结果

下面是命令式语言的抽象语法：

现在，我没有具体的问题，但我想知道是否有人可以为我指出如何编写语义的正确方向。

在过去，我为没有数组和函数的命令式编程语言做过类似的事情。它看起来像这样：

州属于那种类型

就像我说的那样，我不需要深入的答案，但任何帮助/提示/指针将不胜感激。

我正在阅读有关指称语义的 Haskell wikibook 部分，我有点坚持这个练习：

证明从 开始的不动点迭代得到的不动点也是最小的，它比任何其他不动点都小。（提示：是我们 cpo 的最小元素，g 是单调的）。

以下陈述定义了导致练习的概念的核心（我认为）：

其中 f 是阶乘函数，并且显示为 g 的不动点，假设 g 是连续的。

我想我基本上理解了显示 g(f) = f 的部分，但我真的不知道该练习什么。据我了解，阶乘函数 f 是最小不动点（至少基于运算符），但我完全不清楚将函数与 进行比较意味着什么（直观地），更不用说我如何找到不动点了除了示例中显示的最小不动点。

我知道这比其他所有事情都少，而且我知道由于 g(x) 是单调的，如果我将它应用于两件事，其中一个小于另一个，结果仍然会遵循这个顺序。

我想我会从取一些函数 f' 并假设开始证明。如果是这样，通过 g 的单调性，我可以证明. 如果我可以证明 g(f') = g(f) 或 f' = f 我认为证明是完整的，但我不知道如何证明这一点。

我理解（我认为）Haskell'sseq将（通常）将其第一个参数减少为WHNF，并在 GHCi 中看到这种行为：

然而，尽管for 的文档evaluate说它也将其参数简化为 WHNF，但看起来它实际上完全将其参数简化为正常形式：

我可以确认这个（明显的）差异

和

如果文档evaluate正确，seq和的行为不应该evaluate相同吗？我在这里缺少什么（作为 Haskell 初学者）？

这可能会去 cs 或 cstheory 堆栈交换，但我在这里看到了带有正式验证标记的大多数问题。

是否有大量关于使用指称语义进行程序验证的文献？

通过快速搜索，我发现

沃尔夫冈·波拉克。基于指称语义的程序验证。在第八届 ACM 编程语言原则研讨会的会议记录中，第 149-158 页。ACM，1981 年 1 月。

http://www.pocs.com/Papers/POPL-81.pdf

程序验证的基础，第 2 版 Jacques Loeckx，Kurt Sieber ISBN：978-0-471-91282-8

这门课程：

https://moves.rwth-aachen.de/teaching/ss-15/sv-sw/

此外，是否有使用指称语义的某些语言的实用程序验证工具？

我正在寻找一个准确且易于理解的定义。我发现的彼此不同：

• 来自一本关于函数式反应式编程的书

指称语义是编程语言形式含义的数学表达。

• 但是，维基百科将其称为一种方法而不是数学表达式

指称语义是一种通过构建描述语言表达式含义的数学对象（称为指称）来形式化编程语言含义的方法