问题标签 [induction]

以下是结构归纳的定义吗？

有人可以给我一个 Haskell 结构归纳的例子吗？

我有两种算法。

我如何归纳证明B 比 A 快。

有人告诉我 2^n > 2n+1 for n>2 可能对这个问题有用。我一直在绞尽脑汁，无法解决这个问题。谢谢。

“n”相当于程序的大小。

编辑：对于所有 n > 19。

解决方案：

前提：n^2 + 1,000,000 < 2^n

基础：
n = 20
1000400 < 1048576 真

就职：

最后一行暗示 B 总是大于 A。

我正在准备编译器考试，我在过去的论文中发现了以下两个我不知道如何回答的问题：

我知道不变量和归纳变量的含义，但我真的不知道在解释这两种解决方案方面对我的期望是什么。

如果有人帮助我解释，我将不胜感激。

谢谢！

我实现了一种用于字符串排列的递归方法。但是我有一个问题：如何用归纳法证明这段代码的正确性？我真的不知道。

假设我有一个非常简单的归纳类型：

我想证明某些价值观是不存在的。具体来说，不能有没有根据的价值观：~exists i, i = ind1 i.

我在互联网上环顾了一下，什么也没想到。我能够写：

这有效，但看起来真的很丑陋且不一般。

我需要在 ACSL 中编写一个归纳谓词，说明一个链表是另一个链表的子表。

谓词的签名应该是这样的：

所以基本上我想要一个谓词来说明状态 L1 上的链表 l 是同一个链表 l 的子列表，但在这种情况下是状态 L2。

我是 Coq 的新手，但通过一些努力，我能够证明各种归纳引理。但是，我卡在所有使用以下归纳定义的练习中：

我得到的最远的是以下引理：

以下两个引理我无法通过第一步，因为我exists在使用intros.

任何帮助，将不胜感激！

在Arthur 的建议下，我将我的Fixpoint关系改为一种相互Inductive关系，这种关系“建立”了游戏之间的不同比较，而不是“向下钻取”。

但现在我收到一条全新的错误消息：

我认为错误消息是说我需要为所有这些互归纳定义使用相同的确切参数。

我意识到有一些简单的技巧可以解决这个问题（未使用的虚拟变量，长函数类型，其中包含所有内容forall），但我不明白为什么我应该这样做。

有人可以解释这种对互归纳类型的限制背后的逻辑吗？有没有更优雅的方式来写这个？这种限制是否还意味着对彼此的归纳调用都必须使用相同的参数（在这种情况下，我不知道有任何黑客可以节省大量的代码重复）？

（所有类型和术语的定义，例如 compare_quest、game、g1side 等，与我在第一个问题中的定义没有变化。

在 CGT 中，通常两个玩家（名为Left和Right）轮流玩游戏，最后一步的玩家获胜。每个游戏（意味着游戏中的每个位置）都可以读为一组Left' 选项和一组Right' 选项写为{G_L | G_R}。在比较两个游戏时，他们可以通过以下四种不同方式中的任何一种进行比较：<、>、=或||。

一个游戏是A < BifB绝对比Afor好Left，不管谁先走。A > BifA比Bfor好Left。A = B如果两个游戏是等价的（从某种意义上说，游戏的总和A + -B是零游戏，所以先走的玩家输了）。而且，A || B如果哪个游戏更适合Left取决于谁先走。

检查两个游戏之间比较的一种方法如下：

• A <= B如果所有A的Left孩子都是<| B并且A <|所有的孩子都是B正确的孩子。

• A <| BifA有一个右孩子，<= B或者如果A <=有任何一个B左孩子。

• 并且，同样对于>=和>|。

因此，然后通过查看这对关系中的哪一对适用于两个游戏Aand B，可以确定是A < B( A<=Band A<|B)、A=B( A<=Band A>=B)、A > B( A>=Band A>|B) 还是A || B( A<|Band A>|B)。

这是关于 CGT 的 wiki 文章。

在我的 rails 4 应用程序目录中，我在终端中键入“heroku pg:credentials DATABASE”以获取有关部署在 heroku 上的应用程序的数据库的所有信息。由于我想查看我的 postgresql 数据库中的数据，我尝试将信息输入到 Induction 中，但它最终没有响应，我被迫进入活动监视器并强制退出。我又重复了几次相同的程序，结果都是一样的。我的 Induction 版本有问题吗？我应该使用不同的程序来查看我的数据库吗？还是我做错了什么？

我是rails新手，谢谢你的帮助！

我正在尝试连接到来宾机器内部的 PostgreSQL 数据库（使用 Vagrant 和 VirtualBox）。

我正在尝试使用Induction连接它，但我收到一条错误消息：

我让 Vagrant 在我的主机上将端口转发到端口 1234。

我对感应连接的设置是：

开发数据库是由 Rails 使用创建的rake db:create:all，我知道它可以工作，因为我从 Rails db 控制台看到它。

在我的 postgresql.conf 文件中，我也设置listen_addresses为'*'监听外部机器。

我究竟做错了什么？

编辑（添加我的 pg_hba.conf）：

编辑（这是尝试连接时从 Induction 应用程序显示的错误）