问题标签 [formal-semantics]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
1 回答
175 浏览

haskell - 如何在 Haskell 中创建格型数据结构?

我正在尝试在 Haskell 中构建 FCA 类型的格型数据结构,我可以在其中检查两个实体是否有连接。实际上,我什至不确定晶格是正确的结构,因为它可能有点“太多”。

这是上下文。在 COBOL 程序分析器中,我有一个数据集名称、文件、记录和字段的本体。根据程序,一个数据集名称可以有多个文件名,一个文件可以有多个记录,一个记录可以有多个字段。我希望这种层次结构反映在 Haskell 数据结构中。但我也希望能够为 file1 和 file2 继承关系,以便我可以检查 file1 和 file2 是否属于相同的数据集名称。实际上,这种关系几乎可以是“==”的关系。但是,例如,它们可能只是在 dsn0 中有一个连接。

在这种情况下,我还有其他可以从格或 FCA 数据结构中受益的本体。例如,我有属于作业步骤的程序和属于作业的作业步骤。如果我能很容易地弄清楚两个程序是否属于同一个工作,那就太好了。在这里,它似乎也是一个“加入”运算符。获取某个实体的扩展名(代码)也会很有用。

我对 Haskell 还是有点陌生​​。我试图查看Lattice 库,但具体而言,我不确定从那里去哪里。知道如何开始吗?Haskell 中格子的一个小例子会很有帮助。非常感谢您的帮助(和耐心)。

更新:如评论中所述,Lattice 可能不是最好的形式。我意识到我可能只需要按照这些思路使用常规类类型的数据结构:

我想我使用树/格/FCA 类型结构的最初意图是充分利用 Haskell 中的函子潜力,这应该会导致有趣的格操作,包括获得一个概念的所有扩展,检查两个概念是否属于相同的更高级别的概念,通过它们的 DSN 检查两个文件的相等性“==”,...

也许非二叉树结构会更好?在 Haskell 中很容易做到这一点吗?

0 投票
1 回答
172 浏览

rust - 为什么我不必声明 x 对于仿射语义和函数类型是可重用/可复制的?

有人告诉我,Rust 在仿射逻辑中有一种语义——所以它有删除/弱化但没有复制/收缩。

以下编译:

由于不允许重复,因此无法编译以下内容:

同样,这些都不编译:

减弱也有目共睹

我们没有返回fn(A, C) -> B,而是返回impl Fn(A, C) -> B。有没有办法返回fn(A, C) -> B呢?如果没有也没关系;我只是好奇。

我期望的另一件事是你可以提升A() -> A. 但是,Rust 中的函数可以多次复制和使用。例如,

假设实际上有一个 function lift(x: A) -> fn() -> A,那么我们可以打破 move 语义。例如,这将允许

因此要提升Afn() -> A,我们需要知道该函数是“线性/仿射”或只能使用一次。Rust 为此提供了一种类型:FnOnce() -> A. 在下文中,第一个编译,第二个不编译。

以下函数是互逆的(可能我不太了解 Rust 的语义,无法说它们实际上是互逆的):

由于fn dup<A>(x: A) -> (A, A) { (x,x) }无法编译,我认为以下可能是一个问题:

似乎 Rust 正在为fn(A) -> B类型做一些特别的事情。

为什么我不必在上面声明 x 是可重用/可复制的?

也许正在发生一些不同的事情。声明的函数有点特殊fn f(x: A) -> B { ... },就是特别的见证A -> B。因此,如果f需要多次使用,可以根据需要进行多次批评,但fn(A) -> B完全不同:它不是构造的东西,而是假设的东西,并且必须使用fn(A) -> B可复制的东西。事实上,我一直认为它更像是一个可自由复制的实体。这是我的粗略类比:

  • fn my_fun<A,B>(x :A) -> B { M } “是” x:A |- M:B
  • fn(A) -> B"is" !(A -o B) 因此可以自由复制
  • 因此fn() -> A“是” !(() -o A) = !A 因此fn () -> A是 A 上的 (co)free 重复
  • fn dup_arg<A: Copy>(x: A) -> B { M }“说” A 有重复或者是一个类固醇
  • impl FnOnce (A) -> B“是” A -o B

但这不可能是正确的......为了什么impl Fn(A) -> B?从玩了一下,似乎fn(A) -> B比 更严格Fn(A) -> B。我错过了什么?

0 投票
1 回答
57 浏览

coq - Coq:证明 while 等价于重复

我是 Coq 的新手,要学习形式语义,我正在关注 Software Foundations 这本书。目前我在本章中:https ://softwarefoundations.cis.upenn.edu/lf-current/Imp.html 。它定义了简单命令式语言的命令。作为练习,我尝试向定义如下的语言添加重复命令:

但我一直试图证明该命令repeat c until b end等同于c; while ~b do c end,在以下意义上:

我在 Coq 中定义的定理如下:

我已经设法证明了评估在下一步中结束的情况,但是当我尝试证明另一种情况时,我陷入了循环。我想应用归纳假设来解决它,但我不知道该怎么做。我认为也许依赖归纳可以帮助我,但我无法使用它来证明它。