问题标签 [agda]

我很难说服 Agda 终止检查fmap下面的函数以及在 a 的结构上递归定义的类似函数Trie。ATrie是一个域为 a的trieType ，它是由单元、乘积和固定点组成的对象级类型（我省略了副乘积以保持代码最小化）。这个问题似乎与我在定义中使用的类型级替换有关Trie。（表达式const (μₜ τ) * τ意味着将替换const (μₜ τ)应用于类型τ。）

似乎fmap在每种情况下都递归成一个严格较小的论点；如果我删除递归类型，产品案例当然很好。另一方面，如果我删除产品，定义可以很好地处理递归类型。

在这里进行最简单的方法是什么？内联/熔断技巧看起来并不特别适用，但也许确实适用。还是我应该寻找另一种方法来处理定义中的替换Trie？

假设我们有一个排序列表的数据类型，带有与证明无关的排序见证。我们将使用 Agda 的实验性大小类型特性，这样我们就有希望在数据类型上获得一些递归函数来通过 Agda 的终止检查器。

现在，一个想要在这样的数据结构上定义的经典函数是merge，它接受两个排序列表，并输出一个排序列表，其中包含输入列表的元素。

这个函数看起来很无害，但要让 Agda 相信它是完全的可能很棘手。实际上，如果没有任何明确的大小索引，该函数就无法进行终止检查。一种选择是将函数拆分为两个相互递归的定义。这可行，但给定义和相关证明增加了一定量的冗余。

但同样，我不确定是否甚至可以明确给出大小索引，以便merge具有 Agda 接受的签名。这些幻灯片mergesort明确讨论；那里给出的签名表明以下应该有效：

在这里，我们正在做的是允许输入具有任意（和不同）大小，并指定输出的大小为 ∞。

.ι != ∞ of type Size不幸的是，有了这个签名，Agda在检查xs定义的第一个子句的正文时抱怨说。我并没有声称非常了解大小类型，但我的印象是任何大小 ι 都会与 ∞ 统一。自从编写这些幻灯片以来，可能大小类型的语义已经发生了变化。

那么，我的场景是否是预期大小类型的用例？如果是这样，我应该如何使用它们？如果大小类型在这里不合适，为什么merge上面的第一个版本不终止检查，因为以下是：

我试图证明以下几点：

我是 Adga 的新手，甚至不知道从哪里开始。有什么建议或指导吗？显然很容易在纸上证明，但我不确定要告诉 Agda 什么。

我将我的 pow 函数定义如下：

我在我的 Mac 上安装 agda 时遇到问题。我从这里接受我的指示：

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX

我能够安装 Haskell 平台，并且当我运行 cabal update 时它可以工作。当我运行时：

它最初是安装的，现在它为我提供了重新安装的选项，所以我相信这是正确的。当我运行最后一个命令时出现问题，

它输出

我也尝试在我的虚拟机上安装，因为 Windows 安装似乎要容易得多，但是当我尝试运行 .msi 文件时，我收到“此文件与您的处理器不兼容”的错误消息。我允许虚拟窗口最多使用 8 个处理器（最大值），所以这似乎不是一个选择。任何帮助将不胜感激。

除非我弄错了，否则没有证据

在阿格达。

这意味着您不能使用矛盾证明。

许多数学教科书都使用这些证明，所以我想知道：是否总是有可能找到替代的建设性证明？例如，你能用建设性逻辑写一本代数教科书吗？

如果答案是否定的。这是否意味着建设性逻辑在某种意义上不如经典逻辑强大？

我正在尝试编写一个简单的程序，它从标准输入中读取一行，将其反转，然后打印反转的字符串。

不幸的是，本机getLine函数读取的是Costring; 我只能反转Strings；并且没有将 aCostring带到 a 的函数String。

我怎样才能修改这个程序来编译？

我试图证明这个引理

但是另一个功能 reverse-helper 不断出现在我的目标中，我不知道如何摆脱它。有什么指导或建议吗？

我是 Agda 的新手，我正在尝试定义一个prod类型的常量： Z → (Z → ((Z → Set) → Set))

现在，我编写了以下 Agda 代码：

当我对它进行类型检查时，agda 会产生以下错误消息：

非常感谢任何帮助