functional-programming - 说服 Agda 递归函数正在终止

Question

我很难让 Agda 相信递归调用函数中的参数在结构上小于传入参数。

我已经定义了对、对列表(将有限函数表示为输入/输出对的“集合”)以及这些列表的并集，如下所示:

data _x_ {l : Level} (A B : Set l) : Set l where
  <_,_> : A -> B → A x B

data FinFun (A B : Set) : Set where
  nil : FinFun A B
  _::_ : A x B → FinFun A B → FinFun A B

_U_ : {A B : Set} -> FinFun A B -> FinFun A B -> FinFun A B
nil U f' = f'
(x :: xs) U f' = x :: (xs U f')

我还定义了“社区”和两个这样的社区的最高层:

data UniNbh : Set where
  bot : UniNbh
  lam : FinFun UniNbh UniNbh -> UniNbh

_u_ : UniNbh -> UniNbh -> UniNbh
bot u bot = bot
bot u (lam f) = lam f
(lam f) u bot = lam f
(lam f) u (lam f') = lam (f U f')

最后，对于这个问题，最重要的是，我定义了一个函数，在给定邻域对列表的情况下，该函数取列表中对的所有第一个分量的最高值:

pre : FinFun UniNbh UniNbh -> UniNbh
pre nil = bot
pre (< x , y > :: f) = x u pre f

给我带来麻烦的相互递归函数本质上是这样的:

f : UniNbh -> UniNbh -> UniNbh -> Result
-- Base cases here. When any argument is bot or lam nil, no
-- recursion is needed.
f (lam (a ∷ as)) (lam (b ∷ bs)) (lam (c ∷ cs)) =
  f (lam (a ∷ as)) (pre (b ∷ bs)) (lam (c ∷ cs))

很明显，要么 pre f 小于 lam f，要么基本情况之一将结束递归，但 Agda 无法理解这一点。为了解决这个问题，我尝试了很多不同的想法，但都没有奏效。在这一点上，我认为唯一的方法是使用标准库中的 Induction.WellFounded，但我不知道如何。

我试图证明以下数据类型是有根据的，但没有成功:

data preSmaller : UniNbh -> UniNbh -> Set where
  pre-base : preSmaller (pre nil) (lam nil)
  pre-step : ∀ (x y f f') ->
             preSmaller (pre f) (lam f') ->
             preSmaller  (pre (< x , y > :: f')) (lam (< x , y > :: f'))

我什至不确定这种数据类型是否有用，即使我可以证明它是有根据的。

在四处寻找有关如何使用 Induction.WellFounded 的信息时，我只能找到非常简单的示例，表明 < for natural numbers 是有根据的，而且我无法将这些想法推广到这种情况。

抱歉，帖子太长了。任何帮助将不胜感激!

Answer 1

由于某些 unicode，我无法看到整个定义 - 您引入的许多字符都呈现为正方形。 WellFounded的基本思想不是某些数据类型变小的证据。基本思路是Agda可以看到Acc _<_ x由包装在 Acc _<_ y 中的访问器函数构造变小。

在你的情况下，似乎 preSmaller是这样的_<_ .很难判断是否是这样，因为缺少很多文字。然后你需要构造一个可以构建 Acc preSmaller y 的函数。对于任意两个给定的 x y : UniNbh .

编辑后的问题仍然缺少一些定义(例如，什么是 post nil 。但我明白了正在发生的事情的要点。

您对 preSmaller 的定义类似于以下 _<_ 的定义为 Nat :

data _<_ : Nat -> Nat -> Set where
   z<  : {n : Nat} -> zero < (succ n)
   s<s : {m n : Nat} -> m < n -> (succ m) < (succ n)

注意它与标准定义不同，因为两者都是 m和 n变得更大。这会影响 WellFounded的证明的构建。 - 内。

-- may just as well import, but let me be self-contained:
data Acc {A : Set} (_<_ : A -> A -> Set) (x : A) : Set where
   acc : ((y : A) -> y < x -> Acc _<_ y) -> Acc _<_ x

Well-founded : (A : Set) -> (R : A -> A -> Set) -> Set
Well-founded A _<_ = (x : A) -> Acc _<_ x

{-# BUILTIN EQUALITY _==_ #-} -- rewrite rule needs this, if I am not using
-- Unicode version of it from Prelude
<-Well-founded : Well-founded Nat _<_
<-Well-founded zero     = acc \_ ()
<-Well-founded (succ x) = acc aux where
   aux : (y : Nat) -> y < (succ x) -> Acc _<_ y
   aux zero     _                                 = <-Well-founded zero
   aux (succ y) (s<s y<x) with <-Well-founded x | is-eq? (succ y) x
   ...          | acc f | no  sy!=x               = f (succ y) (neq y<x sy!=x)
   ...          | wf-x  | yes sy==x rewrite sy==x = wf-x

辅助功能:

data False : Set where

false-elim : {A : Set} -> False -> A
false-elim ()

data Dec (A : Set) : Set where
   yes : A -> Dec A
   no  : (A -> False) -> Dec A

_==?_ : {A : Set} -> A -> A -> Set
_==?_ x y = Dec (x == y)

s== : {m n : Nat} -> (succ m) == (succ n) -> m == n
s== refl = refl

is-eq? : (m n : Nat) -> m ==? n
is-eq? zero     zero     = yes refl
is-eq? (succ m) zero     = no \()
is-eq? zero     (succ n) = no \()
is-eq? (succ m) (succ n) with is-eq? m n
...                        | no  f   = no \sm=sn -> f (s== sm=sn)
...                        | yes m=n = yes (cong succ m=n)

-- if m < n and m+1 /= n, then m+1 < n
neq : {m n : Nat} -> m < n -> ((succ m) == n -> False) -> (succ m) < n
neq {_}      {zero}          ()
neq {zero}   {succ zero}     z<        f = false-elim (f refl)
neq {zero}   {succ (succ n)} z<        f = s<s z<
neq {succ m} {succ n}        (s<s m<n) f = s<s (neq m<n \m=n -> f (cong succ m=n))

要带走的重要事项:
_<_的标准定义允许构建 WellFounded 的更简单证明-ness，因为可以一次减少一个参数。 _<_的不同定义需要减少两者，这似乎是一个问题。然而，使用辅助函数 neq可以构造一个递归，其中只有一个相同的参数变小。
_==_的可判定性为 Nat允许我建立这样的递归。 Agda 可以看到对 <-WellFounded 的递归调用用于结构更小的 x , 这样就结束了。然后根据相等测试的结果不同地使用它的结果。使用 neq 的分支计算必要的 Acc给定函数 <-WellFounded发现较小的 x : 函数终止，因为 Agda 允许构造这样的函数。另一个分支，其中 x == (succ y) , 按原样使用值，因为 rewrite让 Agda 相信它是正确的类型。

通过构造 <-WellFounded 的实例，可以使用有根据的证明函数终止。 :

_-|-_ : Bin -> Bin -> Bin
x -|- y with max-len x y
...   | n , (x<n , y<n) = Sigma.fst (a (<-Well-founded n) b (x , x<n) (y , y<n)) where
  a : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ n)
  a+O : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ (succ n))
  a+I : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ (succ n))

  a+O f c m n with a f c m n
  ...                | r , r<n = r O , s<s r<n

  a+I f c m n with a f c m n
  ...                | r , r<n = r I , s<s r<n

  a {zero} _ _ (_ , ())
  a {succ sz} (acc f) cc mm nn with cc | mm | nn
  ... | b | m O , s<s m< | n O , s<s n< = a+O (f sz n<n1) b (m , m<) (n , n<)
  ... | b | m O , s<s m< | n I , s<s n< = a+I (f sz n<n1) b (m , m<) (n , n<)
   ....-- not including the whole thing here - it is too long.

我不包括两个二进制数相加的整个构造(也不是一个有效的 - 只是证明有根据的练习)。这里要注意的重要一点是递归是如何开始的，以及如何重用它来构造 Acc 的新实例。匹配类型 - 此处 S-Bin表示位长最多为 n 的二进制数, Agda 深信 Acc _<_ n变小了，即使它不能证明 S-Bin n变小。