问题标签 [forall]

在使用 z3-solver 模块 (4.8.0.0) 在 Python 3.6.7 上运行此代码时，z3 返回的模型似乎对公理无效。

为什么我们没有达到预期的 42 ？公理或函数有问题吗？

我是 PL/SQL 的初学者，从不同的表中获取大量记录，并希望使用带有 BULK COLLECT 和 FORALL 的匿名块插入到 PL/SQL 中的单个表中。任何人都可以帮助我确定以下代码是否正确。我参考了很多链接

http://uksanjay.blogspot.com/2012/08/difference-between-bulk-collect-and.html?m=1

如何在 Pl/SQl 中使用批量收集和插入

有两个表 'ABC' 和 'BCD' 从中获取记录并插入到目标表 'DEF'

ABC 表（A、B、C 是列名）

BCD 表

在目标表“DEF”中，我必须插入两个表记录。

代码如下：

PS：实际代码中select语句比较复杂，源表'ABC'和'DEF'由百万条记录组成。所以请帮助我编写有效的代码。

我想使用 DBLINK - @FMATLINK 将来自不同表的大量记录插入目标远程表“Audition_Detail”。我使用了批量收集，但它的抛出错误。我也浏览了一些链接：

克服通过数据库链接进行批量插入的限制

PLS-00394：提取语句的 INTO 列表中的值数量错误

代码如下：

错误报告 -

ORA-06550：第 39 行，第 3 列：

PLS-00394：FETCH 语句的 INTO 列表中的值数量错误

ORA-06550：第 39 行，第 3 列：

PL/SQL：忽略 SQL 语句

ORA-06550：第 40 行，第 4 列：

PLS-00739：远程表 06550 不支持 FORALL INSERT/UPDATE/DELETE。00000 -“行 %s，列 %s：\n%s”

*原因：通常是 PL/SQL 编译错误。*行动：

从 ghc-8.0 开始，我们有一个非常好的扩展名为TypeApplications. 这允许我们而不是：

这样做：

这真的很酷。当我们添加更多类型变量时，它会变得更加复杂，但是有一些规则可以用来确定确切的顺序，并且它们有很好的文档记录：

所以在上面的函数中，我们首先提供a然后b：

很好，但是如果我想更改顺序怎么办？没问题，我们可以使用ExplicitForAll扩展（或其他暗示它）来指定它：

现在我们颠倒了我们要应用的类型的顺序：

问题是我似乎无法弄清楚如何对属于类型类的函数实现相同的影响。考虑这个例子：

我现在不能forall使用函数（例如fooBarClassFunc :: forall a b . a -> b -> ..，因为这会改变函数的含义并且显然无法编译。

所以，问题是，如何TypeApplication在类型类方法内部更改类型变量的顺序？

编辑

以防万一，我尝试InstanceSigs了扩展，它完全忽略了forall类型变量的顺序TypeApplications，这是一件好事，否则我们最终会得到由实例而不是类决定的行为。

我试图了解如何用forallRuby 或 JavaScript 等过程或 OO 语言来实现。例如（这是 Coq）：

我这样做的尝试只是定义一个诸如此类的类（调用MainAxiom == ax）。

这有各种各样的错误。它本质上是说“对于你用点 p1 和 p2 创建的每个公理，它必须满足在一条线上的属性等。”这并不完全符合我的要求。我希望它完成定义实际公理的数学目标。

想知道如何用像 Ruby 或 JavaScript 这样的语言来实现这一点，如果不能直接实现的话，就尽可能接近。即使它只是一个 DSL 或定义一些数据的对象，知道如何作为替代方案也会很有帮助。

让我印象深刻的第一部分是，attr :p1和 attr 定义似乎适用于每个实例。也就是说，它似乎说了一些关于forall的内容，但我无法确定它。

也许更像这样的东西更接近：

我只想让任何东西都接近forall过程/OO语言的定义。

使用案例

首先，我想解释一下我的使用案例：我想将一个领域划分为不同的扇区，所有的植物都应该由机器人分析（每个扇区只有一个机器人）。我想检查：前提条件是已经分析了一个部门的所有植物，以便机器人返回“家”。

问题

这是域 PDDL。我的问题是放在“tracker-back-home”动作的前提下。现在我正在检查是否已经分析了所有植物，但我需要知道是否分析了特定部门的所有植物？可以使用 forall 语句吗？

我是 Haskell 的初学者，我被undefined函数的类型签名吓了一跳。

我期待一些更简单的东西，但我在 Hackage 上找到了这个：

错误的特殊情况。预计编译器将认识到这一点并插入更适合undefined出现的上下文的错误消息。

你能解释一下这个签名是什么意思吗？

谢谢！

我有以下类表示类别，其中对象类由一种表示，并且每个 hom 类由由上述种类的类型索引的类型表示。

一个简单的实例示例是：

现在我想为产品类别建模。作为一个简单的起点，这里有一个类型，它对对应于->with 自身乘积的类别的态射进行建模：

下面是相应的操作：

但是当我尝试将操作粘贴到类的实例中时：

我遇到以下问题：

我相信消息的重要部分如下：

特别是它不能将 typeforall x y. Bifunction '(x, y) '(x, y)与 type统一起来forall (a :: (*, *)). Bifunction a a。

剥离大部分领域特定的东西，我们只剩下以下问题的最小重现：

有没有办法可以bifunction_id与bifunction_id'上面统一？

我尝试过的另一种方法是使用类型族，但这仍然不能完全解决问题：

但是我真的不明白为什么这个相同的表达式有效，并且宁愿不必在代码的其余部分中管理像这样的有点不明显的区别。

I want to write a class like this:

Here, c is a type restricted by C and this restriction will be used in func2. But this cannot be compiler. Type c is not a real type. I try to add forall or using TypeFamilies, but none of them can do this. TypeFamilies looks good, but it cannot use with restriction in funcion definition like C c => b -> c or `type X x :: C * => *.

Must I use (A b, C c) => B b c to define this class? I have another class using with B like B b => D d b. If adding a param for class B, the D class needs one more param as well. In fact, Seq a will be used with class D, which cannot match D d b.

EDIT: one more description.

Compiler will complain with the line a2f :: b -> Bool:

EDIT2: Use type families

It will show error with:

如果我有一组名称，如何使用 forall （或其他功能）检查它们是否都以大写字母开头？

这是错误的，我还不太熟悉高阶函数，所以我可以使用一些帮助。