问题标签 [totality]

假设我有一些自然数d ≥ 2和n > 0；在这种情况下，我可以从n中分离出d并得到n = m * d ^k，其中m不能被d整除。

我想使用这种重复删除d可分部分作为递归方案；所以我想我会为Steps通往m的数据类型：

并编写一个递归函数，计算Steps给定对的d和n：

但是，steps不被接受为全部，因为没有明显的理由说明递归调用是有充分根据的（q和之间没有结构关系n）。

但我也有一个功能

用一个无聊的证明。

我可以用towf的定义steps来向Idris解释那steps是total吗？

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues指出：

其次，目前的实现到目前为止所做的努力有限，因此可能仍然存在它认为一个函数是完全的但不是的情况。不要依赖它来做你的证明！

这是否意味着不能依赖 Idris 来提供证明，或者有没有一种方法可以创建不需要整体检查器的证明？

我有以下代码：

我收到关于最后一行的错误消息：

该函数应始终给出结果，因为最终 fromInteger 的参数将变得足够小以选择第一种情况。但伊德里斯似乎并不理解这一点。这个功能有什么问题，我该如何解决这个错误？

我对术语有以下定义：

和一个函数pos_list，它获取一个术语列表并为每个子术语返回一个“位置”列表。例如，[Var "e"; Func "f" [Var "x"; Func "i" [Var "x"]]]我应该得到[[1]; [2]; [2; 1]; [2; 2]; [2; 2; 1]]每个元素代表子项树层次结构中的位置的位置。

使用上面的代码，我得到了错误

错误：无法猜测fix

在第一个let fix构造上，但在我看来，调用(pos_list_aux args' [] new_head)（导致问题）将其作为参数args'，该参数(Func _ args')本身就是ts.

怎么了 ？

和一个beq_term比较两个术语的函数定义如下：

该函数的定义beq_term产生错误消息：

错误：无法猜测 的递减参数fix。

所以我对如何说服 Coq 终止感兴趣。

I'm writing (for myself) an explanation of how to do well-founded recursion in Coq. (see i.e. the Coq'Art book, chapter 15.2). First I made an example function based on nat and that worked fine, but then I did it again for Z, and when I use Compute to evaluate it, it doesn't reduce all the way down to a Z value. Why?

Here is my example (I put the text inside comments so one can copy-paste the whole thing into your editor):

(* Test of well-founded recursion *)

(* TL;DR: To do well-founded recursion, first create 'functional' and then create the recursive function using Acc_iter, the iterator for accessible relations *)

(* As an example, compute the sum of the series from 1 to n, something like this sketch:

fix f n := (if n = 0 then 0 else n + f (n-1))

Now, let's not use structural recursion on n.

Instead, we use well-founded recursion on n, using that the relation less-than ('lt') is wellfounded. The function f terminates because the recursive call is made on a structurally smaller term (in the decreasing Acc-chain). *)

(* First we do it for nat *)

(* From a proof that a relation is wellfounded, we can get a proof that a particular element in its domain is accessible.

The Check commands here are not necessary, just for documentation, dear reader. *)

(* First define a 'functional' F for f. It is a function that takes a function F_rec for the 'recursive call' as an argument. Because we need to know n <> 0 in the second branch we use 'dec' to turn the boolean if-condition into a sumbool. This we get info about it into the branches.

We write most of it with refine, and leave some holes to be filled in with tactics later. *)

(* The functional can be used by an iterator to call f as many times as is needed.

Side note: One can either make an iterator that takes the maximal recursive depth d as a nat argument, and recurses on d, but then one has to provide d, and also a 'default value' to return in case d reaches zero and one must terminate early.

The neat thing with well-founded recursion is that the iterator can recurse on the proof of wellfoundedness and doesnt need any other structure or default value to guarantee it will terminate. *)

(* The type of Acc_iter is pretty hairy *)

(* P is there because the return type could be dependent on the argument,
but in our case, f:nat->nat, and R = lt, so we have *)

(* Here the first argument is the functional that the iterator takes, the second argument n is the input to f, and the third argument is a proof that n is accessible. The iterator returns the value of f applied to n.

Several of Acc_iter's arguments are implicit, and some can be inferred. Thus we can define f simply as follows: *)

(* It works like a charm *)

(* Now let's do it for Z. Here we can't use lt, or lt_wf because they are for nat. For Z we can use Zle and (Zwf c) which takes a lower bound. It needs a lower bound under which we know that the function will always terminate to guarantee termination. Here we use (Zwf 0) to say that our function will always terminate at or below 0. We also have to change the if-statement to 'if n <= 0 then 0 else ...' so we return zero for arguments less than zero. *)

(* Now we define the function g based on the functional G *)

(* But now we can't compute! *)

(* We just get a huge term starting with

Comment: I noticed that Zwf_well_founded is defined as Opaque in the library, so I tried to make it Transparent by copying the proof and ending the lemma with Defined. instead of Qed. but that didn't help...

Added observation:

If I define f' for nat with Fixpoint instead, and recurse on the accesibility proof, and end with Defined. then it computes. But if I end with Qed. it doesn't reduce. Is this related? I guess there is an issue of transparency in the definition of G or g somewhere... Or am I completely mistaken?

Anyway, my problem persists for Z.

它们似乎有类似的目的。到目前为止，我注意到的一个区别是，虽然Program Fixpoint会接受复合措施，例如{measure (length l1 + length l2) }，Function似乎拒绝这一点，并且只会允许{measure length l1}。

Program Fixpoint严格来说比 更强大Function，还是更适合不同的用例？

使用 Idris 进行测试驱动开发的第 9 章介绍了以下数据类型和removeElem功能。

以下作品：

但是，几分钟后以下调用仍在运行：

我猜为什么编译这么慢？

考虑以下无类型 lambda 演算的玩具表示：

类型检查print失败并出现以下错误：

什么是最易读/符合人体工程学/最有效的实现方式？

我正在研究 Idris 中的快速搜索字符串搜索算法的一个版本，并提出了这个：

（lookupChar 和 makeBadShift 在别处。）

这很好用，但我想让它更正式地正确。首先，由于使用了 strIndex，它并不完全。创建 strIndex 的总版本并不难（通过 List Char 或这个:)

但是我必须有一种方法来证明 (n + i) 小于 h。（是的，因为那时 i < h - n。）

如果我直接将“>”和“==”替换为它们的表亲，我最终会看到否定：

和

这让我很难过。

另一方面，我可以颠倒条件，最终得到

但在这一点上，我完全糊涂了，不知道如何前进。

现在最好的事情是什么？