相关疑难解决方法(0)

假设我们定义了一个函数

f : N \to N
f 0 = 0
f (s n) = f (n/2) -- this / operator is implemented as floored division.

Agda将在三文鱼中绘制f,因为它无法判断n/2是否小于n.我不知道怎么告诉Agda的终止检查器.我在标准库中看到它们有一个2的分区和n/2 <n的证明.但是,我仍然没有看到如何让终止检查器意识到已经在较小的子问题上进行了递归.

Agda 2.3.2.1无法看到以下函数终止:

open import Data.Nat
open import Data.List
open import Relation.Nullary

merge : List ? ? List ? ? List ?
merge (x ? xs) (y ? ys) with x ?? y
... | yes p = x ? merge xs (y ? ys)
... | _     = y ? merge (x ? xs) ys 
merge xs ys = xs ++ ys

Agda wiki说,如果递归调用的参数按字典顺序减少,那么终止检查器就可以了.基于此,似乎这个功能也应该通过.那我在这里错过了什么？此外,在以前版本的Agda中它可能还可以吗？我在互联网上看过类似的代码,没有人提到那里的终止问题.

我很难说服Agda终止检查fmap下面的函数,并且在a的结构上递归地定义了类似的函数Trie.A Trie是一个trie,其域是a Type,是一个由单元,产品和固定点组成的对象级类型(我省略了副产品以保持代码最小).问题似乎与我在定义中使用的类型级替换有关Trie.(表达式const (?? ?) * ?表示将替换const (?? ?)应用于类型?.)

module Temp where

   open import Data.Unit
   open import Category.Functor
   open import Function
   open import Level
   open import Relation.Binary

   -- A context is just a snoc-list.
   data Cxt {} (A : Set ) : Set  where
      ? : Cxt A
      _??_ : Cxt A ? A ? Cxt A

   -- Context membership.
   data _?_ {} {A …