小编jmi*_*ite的帖子

假设我有一个有向图 G，其中每个节点代表我拥有的某个集合。从 u 到 v 存在一条边，当且仅当 u 是 v 的子集。该图是传递且非循环的。有许多源节点（不包含任何其他节点的节点）和一个接收器（一个包含所有其他节点的并集的大“宇宙”集）。换句话说，该图是可比图的传递方向。

我想知道的是，我可以从这个图自动生成一个漂亮的欧拉图吗？

欧拉图类似于维恩图，但您不必显示集合之间重叠的每种组合。

一个例子是这样的（摘自维基百科）：

我确信我可以手工制作这样的图表，但我正在处理大量数据集，我将不断添加这些数据集，所以我想自动化该过程。请注意，图表的相对大小对我来说并不重要，重要的是两个区域是否重叠、互斥或者一个区域是否包含在另一个区域中。

是否有算法、工具或库可以让我做到这一点？

请注意，我在这里问过类似的问题，但我的大部分回答都是 LaTeX 根本不是适合这项工作的工具。因此，我在这里问。

我将在前言中说我对PyPy很新,虽然对Python很有经验.

我正在寻找运行不受信任的Python代码的Web应用程序.PyPy沙盒功能看起来非常适合我正在做的事情.

关于沙盒的PyPy文档表明您可以从Python或PyPy调用PyPy沙箱.这似乎意味着有一些单独的程序或可执行文件是沙盒.

我想知道,是否可以从非Python语言调用PyPy沙箱？我特别关注Haskell,但我也很可能使用C或C++作为中间体.

我有一个代码格式化扩展，启用了保存格式。不幸的是，每次我保存但我的程序无法解析时，它都会给我一个警告。此信息是多余的，因为还有其他软件包可以以一种侵入性更小的方式通知我该错误。

有什么方法可以阻止来自特定包的所有通知/警告吗？

有没有办法decide equality在Coq中使用相互递归类型的策略？

例如,如果我有这样的事情:

Inductive LTree : Set :=
  | LNil
  | LNode (x: LTree) (y: RTree)
  with RTree : Set :=
    | RNil
    | RNode (x: Tree) (y: RTree).

Lemma eq_LTree : forall (x y : LTree), {x = y} + {x <> y}.
Proof.
    decide equality; auto.

这让我有了目标:

y0: RTree
y1: RTree
{y0 = y1} + {y0 <> y1}

但是在我导出相等性之前我无法解决这个RTree问题,因为它会产生同样的问题.

我目前正在理论计算机科学方面做一些研究,我正在使用的主要工具之一是prolog.我发现编写非常快速的测试以反驳猜想特别方便.

但是,我已经到了蛮力搜索速度太慢的地步.虽然我可以使用不同的语言,但我使用prolog的重点是编写代码来测试假设是非常快/简单的.

我想知道,是否有Prolog的实现允许自动并行化？它不一定要快速剃刀,但理想情况下我正在寻找一些我可以将代码放入并获得至少一个小加速的东西.

我不知道这是否可行.谷歌搜索在Prolog中发现了很多关于自动并行的学术文章,但我没有遇到任何实现.但是,我真的只熟悉SWI-prolog,所以我绝对可以使用熟悉许多实现的人的建议.

我的代码使用剪切,但我相当确定我可以消除它们.至于IO,唯一的IO是打印到控制台,可能会移动到任何并行代码之外.

所以,我非常了解代数类型和类型类,但我对它的软件工程/最佳实践方面很感兴趣.

对于类型类,现代共识是什么？他们是邪恶的吗？它们方便吗？它们应该被使用吗？

这是我的案例研究.我正在写一个RTS风格的游戏,我有不同类型的"单位"(坦克,侦察等).说我想获得每个单位的最大健康状况.关于如何定义类型的两个想法如下:

ADT的不同构造函数:

data Unit = Scout ... | Tank ...

maxHealth :: Unit -> Int

maxHealth Scout  = 10

maxHealth Tank = 20

单元的类型类,每种类型都是一个实例

class Unit a where
    maxHealth :: a -> Int

instance Unit Scout where
    maxHealth scout = 10

instance Unit Tank where
    maxHealth tank = 20

显然,最终产品中会有更多的领域和功能.(例如,每个单元将具有不同的位置等,因此并非所有功能都是恒定的).

诀窍是,可能有些功能对某些单元有意义,但对其他单元则不然.例如,每个单位都有一个getPosition函数,但是坦克可能有一个getArmour函数,对于没有装甲的侦察兵来说没有意义.

如果我希望其他Haskeller能够理解并遵循我的代码,那么这种"普遍接受"的方式是什么？

以下代码:

Reserved Notation "g || t |- x < y" (at level 10).

Inductive SubtypeOf :
  GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set :=
| SubRefl :
    forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType) , gamma || theta |- u < u
where "g || t |- x < y" := (SubtypeOf g t x y).

给出以下错误:

Syntax error: '<' expected after [constr:operconstr level 200] (in [constr:operconstr])

如果我用<:它代替,我会收到类似的错误<.

但是这段代码运行正常:

Reserved Notation …

我想知道,coq中是否有一个常用的矢量库,即它们的类型长度索引.

有些教程引用了Bvector,但是当我尝试导入它时却找不到它.

有Coq.Vectors.Vectordef,但是那里定义的类型只是命名t,这使我认为它是供内部使用的.

对于不想推出自己的图书馆的人来说,最好或最常见的做法是什么？我对标准库中的向量有误吗？还是有另一个我失踪的自由人？或者人们只是使用列表,并与他们的长度证明配对？

我正在做一些验证工作,我将常规树语法作为基础理论.

Z3允许您使用未解释的函数定义自己的东西,但是在您的决策过程递归时,这并不能很好地工作.他们曾经允许使用插件,但我认为这已经被删除了.

我想知道,有没有人推荐过一个体面的SMT求解器,它允许你为自定义理论编写决策程序？

如果我试图证明 Nat 和 Bool 在 Agda 中不相等：

open import Data.Nat
open import Data.Bool
open import Data.Empty
open import Relation.Binary.PropositionalEquality

noteq : ? ? Bool -> ?
noteq () 

我收到错误：

Failed to solve the following constraints:
  Is empty: ? ? Bool

我知道不可能对类型本身进行模式匹配，但我很惊讶编译器看不到 Nat 和 Bool 具有不同的（类型）构造函数。

有没有办法在 Agda 中证明这样的事情？或者只是不支持 Agda 中涉及类型的不等式？