我明白你在Agda里处理递归终止性时遇到的头疼问题——明明知道pre f在语义上比lam f更小，但Agda的默认终止检查只认语法上的直接子项递减，死活不买账。咱们一步步用良基归纳（Well-Founded Induction）来解决这个问题，从梳理核心逻辑到实现可通过检查的递归函数。

Agda的默认终止检查非常“死板”：它只会看递归调用的参数是不是原参数的直接子结构（比如lam (x::xs)的子结构是x或xs）。但你的递归里，第二个参数从lam (b::bs)变成了pre (b::bs)——这是一个函数计算后的结果，不属于直接子项，所以Agda没法自动识别它的递减性。这时候必须手动定义良基关系，证明不存在无限递减的参数链，从而让Agda信服递归一定会终止。

首先先把你代码里的小错误修正，比如_u_的返回类型笔误，还有用标准库的乘积类型更方便：

open import Level
open import Data.Product using (_×_; _,_) renaming (<_,_> to ⟨_,_⟩)
open import Relation.Binary using (Rel)
open import Relation.Binary.WellFounded using (WellFounded; Acc; acc)

-- 配对类型（或直接用标准库_×_）
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')

-- 修正后的邻域定义（补全_u_的所有case）
data UniNbh : Set where
  bot : UniNbh
  lam : FinFun UniNbh UniNbh → UniNbh
  _u_ : 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')
x u (y u z) = (x u y) u z  -- 补充结合律
(x u y) u z = x u (y u z)

-- pre函数定义
pre : FinFun UniNbh UniNbh → UniNbh
pre nil = bot
pre (< x , y > :: f) = x u pre f

我们需要定义一个_≺_关系，描述“一个UniNbh比另一个更小”，必须包含你需要的pre f ≺ lam f规则，同时覆盖其他可能的递减场景：

data _≺_ : Rel UniNbh lzero where
  -- bot比任何非bot的项小
  bot≺nonbot : ∀ {n} → n ≢ bot → bot ≺ n
  -- pre f严格小于lam f（这是你递归的核心递减规则）
  pre≺lam : ∀ {f} → pre f ≺ lam f
  -- 上确界的左右分量都比上确界本身小
  left≺u : ∀ {x y} → x ≺ x u y
  right≺u : ∀ {x y} → y ≺ x u y
  -- lam构造子中的每个配对元素都比lam整体小
  elem≺lam : ∀ {x y f} → x ≺ lam (< x , y > :: f)
  elem'≺lam : ∀ {x y f} → y ≺ lam (< x , y > :: f)
  -- 传递性：a≺b且b≺c则a≺c
  trans : ∀ {a b c} → a ≺ b → b ≺ c → a ≺ c

接下来要证明_≺_是良基的——也就是不存在无限递减的n₁ ≺ n₂ ≺ n₃ ≺ ...链。我们递归证明每个UniNbh都是可访问的（Acc）：

wf-≺ : WellFounded _≺_
-- bot没有更小的项，直接返回可访问性
wf-≺ bot = acc (λ _ ())
-- 处理lam f的情况：所有比lam f小的项都已被证明可访问
wf-≺ (lam f) = acc helper
  where
    helper : ∀ {n} → n ≺ lam f → Acc _≺_ n
    helper pre≺lam = wf-≺ (pre f)  -- pre f的可访问性递归调用
    helper (elem≺lam {x}) = wf-≺ x
    helper (elem'≺lam {y}) = wf-≺ y
    helper (trans p q) = helper q  -- 传递性归约到子case
    helper (bot≺nonbot _) = wf-≺ bot
-- 处理上确界x u y的情况
wf-≺ (x u y) = acc helper
  where
    helper : ∀ {n} → n ≺ x u y → Acc _≺_ n
    helper left≺u = wf-≺ x
    helper right≺u = wf-≺ y
    helper (trans p q) = helper q
    helper (bot≺nonbot _) = wf-≺ bot

你的f是三元函数，所以我们需要把三个参数打包成元组，定义元组上的良基关系：

open import Data.Product using (proj₁)

-- 三元组的良基关系：只要任意一个参数更小，元组就更小
data _≺₃_ : Rel (UniNbh × UniNbh × UniNbh) lzero where
  first≺ : ∀ {a a' b c} → a ≺ a' → (a , b , c) ≺₃ (a' , b , c)
  second≺ : ∀ {a b b' c} → b ≺ b' → (a , b , c) ≺₃ (a , b' , c)
  third≺ : ∀ {a b c c'} → c ≺ c' → (a , b , c) ≺₃ (a , b , c')

-- 证明三元组关系的良基性
wf-≺₃ : WellFounded _≺₃_
wf-≺₃ (a , b , c) = acc helper
  where
    helper : ∀ {p} → p ≺₃ (a , b , c) → Acc _≺₃_ p
    helper (first≺ p) = wf-≺₃ (proj₁ p , b , c)
    helper (second≺ p) = wf-≺₃ (a , proj₁ p , c)
    helper (third≺ p) = wf-≺₃ (a , b , proj₁ p)

现在可以定义f的核心函数，依赖可访问性证明来保证终止：

-- 先定义你的Result类型（这里假设是UniNbh，你可以替换成实际类型）
data Result : Set where
  -- 你的Result构造子，比如：
  res : UniNbh → Result

-- 核心函数：接收参数元组和可访问性证明
f-core : ∀ (p : UniNbh × UniNbh × UniNbh) → Acc _≺₃_ p → Result
-- 基准case：处理bot或lam nil的情况
f-core (bot , b , c) _ = res bot
f-core (a , bot , c) _ = res bot
f-core (a , b , bot) _ = res bot
f-core (lam nil , b , c) _ = res bot
f-core (a , lam nil , c) _ = res bot
f-core (a , b , lam nil) _ = res bot
-- 你的递归case：第二个参数从lam(b::bs)变成pre(b::bs)
f-core (lam (a₁ :: as) , lam (b₁ :: bs) , lam (c₁ :: cs)) (acc rec) =
  let new-p = (lam (a₁ :: as) , pre (b₁ :: bs) , lam (c₁ :: cs))
      -- 证明新参数元组比原元组小：第二个参数满足pre≺lam
      rel = second≺ pre≺lam
  in f-core new-p (rec rel)

-- 最终的f函数：用良基性证明触发核心逻辑
f : UniNbh → UniNbh → UniNbh → Result
f a b c = f-core (a , b , c) (wf-≺₃ (a , b , c))

如果你觉得良基归纳太繁琐，也可以给UniNbh加自然数大小索引，让pre f的大小比lam f小1，让Agda自动识别终止性：

open import Data.Nat

data UniNbh : ℕ → Set where
  bot : ∀ {n} → UniNbh n
  lam : ∀ {n} → FinFun (UniNbh n) (UniNbh n) → UniNbh (suc n)
  _u_ : ∀ {n} → UniNbh n → UniNbh n → UniNbh n

pre : ∀ {n} → FinFun (UniNbh n) (UniNbh n) → UniNbh n
pre nil = bot
pre (< x , y > :: f) = x u pre f

-- 此时pre f的大小是n，lam f的大小是suc n，递归调用时Agda能自动识别递减

这种方式需要修改所有相关函数的类型，适合从头设计的场景，如果你已经写了大量代码，良基归纳会更灵活。

内容的提问来源于stack exchange，提问作者DoppeDee