问题标签 [bounded-quantification]
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.
scala - 理解 Scala 中的“类型参数不符合类型参数边界”错误
为什么以下不起作用？
在第一次尝试中，不是Hoo[B] with B <: Foo[B]吗？
在第二次尝试中，不是Hoo[B] <: Foo[B]吗？
为了激发这个问题，有一个图书馆：
我正在尝试在 TEXT 旁边引入一种名为 BYTEA 的新扩展方法，以便可以编写：
我的尝试：
但这遇到了与我上面较小的测试用例相同的问题。
scala - 无法将表示类型实现为类型成员
在思考另一个问题时，我遇到了似乎相关的不同谜语。这是其中之一：
其中错误如下：
为什么？（也尝试将 self-type 添加_:S =>到Sys，没关系）
虽然 Rex 的回答使构造Fenced对象成为可能，但它并没有真正解决我在使用类型投影 ( S#Peer) 时表示类型字符丢失的问题。我提出了另一种提出更严格限制的方案；我认为这是核心问题：
scala - 连接（投影）类型成员时，Scala 失去了对相关类型的跟踪
我正在解决一个问题，我发现类型投影和抽象类型有一个新的奇怪问题。假设我有一个产生交易的系统，并且有一个我想桥接的对等系统。以下对我来说看起来不错：
我可以使用直接系统：
但不知何故，peer交易的方法存在缺陷，如下所示：
我想变得聪明并解决它：
...但这也失败了，提供了更多关于问题所在的线索：
这一切都表明，要么def peer: S#Peer#Tx引入一个问题，要么（更有可能？）type Peer <: Sys[Peer]当不用作类型参数但类型成员时有问题。
scala - 通过类型成员而不是类型参数进行 F 有界量化？
我想将类型参数移动到类型成员。
这是有效的起点：
让我烦恼的是，我在[S <: Sys[S]]整个库中都携带了一个类型参数。所以我的想法是这样的：
哪个失败了......S#Tx并且S#Id变得不知何故分离：
任何使它起作用的技巧或改变？
编辑：为了澄清，我主要希望修复类型S以Sys使其工作。在我的案例中，使用路径相关类型存在许多问题。仅举一个反映 pedrofuria 和 Owen 答案的例子：
试着def foo: Foo[s.type]让你知道这无济于事。
scala - Scala将递归有界类型参数（F有界）转换为类型成员
我将如何转换：
类型成员？
即，我想要以下内容：
但我遇到了困难，因为名称 A 已经在类型细化中采用。这个问题是相似的（并且产生自）：F-bounded quantification through type member instead of type parameter?
scala - 存在类型或类型参数绑定失败
我有一个 F 有界类型Sys：
还有一些将其作为类型参数的特征：
假设我有一个要使用 a 调用的方法Foo：
假设我有一个模型更新类型和一个子类型，它带有Foo：
注册模型观察者的辅助函数：
现在以下失败：
和
如果Sys, Foo, invoke, Update,Opened和observe被给定，我如何修复偏函数。允许将值或类型成员添加到Foo.
smt - CVC4：使用量词在布尔值上合成函数的设置？
我目前正在使用 CVC4 来解决以下形式的公式：
在这里，f1...fn是从某个数量Bool到的函数Bool，以及
b1...bk是布尔值。
我的问题完全属于UFSMT 的片段：它有量词，但除了函数和布尔值之外没有其他种类。
当我尝试使用 CVC4 上的默认设置解决问题时，它立即返回未知，尽管事实上我所有的量化都是在有限域上的。
问题是，CVC4 有非常多的处理量词的选项：有一堆cegqi，一堆fmf，还有mbqi等等。我的印象是这些大部分是从特定的研究项目中添加的，我宁愿不必阅读 20 篇不同的论文就可以让我的解决方案继续下去。
我的问题：是否有一组推荐的选项来解决此类问题？
我知道 CVC4 是可能的，因为他们在 SMT 比赛的UF Track上竞争并表现相当出色，但我找不到用于该比赛的具体论据。
z3 - Dafny 作为 SAT-QBF 求解器没有给出正确的结果
我试图养成使用 Dafny 作为一些简单公式的友好 SAT-QBF 求解器的习惯，因为在 Z3 中这样做太不舒服了。
上下文是我已经实现了 Cooper 的量词消除算法，当所有变量都有界时，它可以用作决策过程：因此，我想知道在执行它之前应该得到哪个结果。
但是，我在 Dafny 中遇到了一个问题。
例如，让我们提出这个公式（用 Dafny 编写）：
在我的 Cooper 中，它返回False，而 Dafny 返回assertion violation（以及典型的triggers警告），我False也将其解释为。好的，所以这没有问题。
但如果我提出：
在我的 Cooper 中，它返回True，而 Dafny 也返回assertion violation。我已经完成了手动 Cooper 执行（铅笔和纸），我认为这True是正确的。
知道发生了什么吗？
PS：我还没有在Z3中尝试过，因为我在做其他理论的第一次尝试。
编辑
使用一个简单的技巧来实例化量化变量可以避免触发警告：创建一个未解释的函数。