对 trie 函数的终止检查

Question

我很难说服 Agda 终止 - 检查下面的函数 fmap 以及在 Trie 的结构上递归定义的类似函数。 Trie 是 trie，其域是 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 : Set ????} (a : A) : Cxt A → Set ???? where
      here : ∀ {Δ} → a ∈ Δ ∷ᵣ a
      there : ∀ {Δ a′} → a ∈ Δ → a ∈ Δ ∷ᵣ a′
   infix 3 _∈_

   -- Well-formed types, using de Bruijn indices.
   data _⊦ (Δ : Cxt ⊤) : Set where
      nat : Δ ⊦
      ???? : Δ ⊦
      var : _ ∈ Δ → Δ ⊦
      _+_ _⨰_ : Δ ⊦ → Δ ⊦ → Δ ⊦
      μ : Δ ∷ᵣ _ ⊦ → Δ ⊦
   infix 3 _⊦

   -- A closed type.
   Type : Set
   Type = ε ⊦

   -- Type-level substitutions and renamings.
   Sub Ren : Rel (Cxt ⊤) zero
   Sub Δ Δ′ = _ ∈ Δ → Δ′ ⊦
   Ren Δ Δ′ = ∀ {x} → x ∈ Δ → x ∈ Δ′

   -- Renaming extension.
   extendᵣ : ∀ {Δ Δ′} → Ren Δ Δ′ → Ren (Δ ∷ᵣ _) (Δ′ ∷ᵣ _)
   extendᵣ ρ here = here
   extendᵣ ρ (there x) = there (ρ x)

   -- Lift a type renaming to a type.
   _*ᵣ_ : ∀ {Δ Δ′} → Ren Δ Δ′ → Δ ⊦ → Δ′ ⊦
   _ *ᵣ nat = nat
   _ *ᵣ ???? = ????
   ρ *ᵣ (var x) = var (ρ x)
   ρ *ᵣ (τ₁ + τ₂) = (ρ *ᵣ τ₁) + (ρ *ᵣ τ₂)
   ρ *ᵣ (τ₁ ⨰ τ₂) = (ρ *ᵣ τ₁) ⨰ (ρ *ᵣ τ₂)
   ρ *ᵣ (μ τ) = μ (extendᵣ ρ *ᵣ τ)

   -- Substitution extension.
   extend : ∀ {Δ Δ′} → Sub Δ Δ′ → Sub (Δ ∷ᵣ _) (Δ′ ∷ᵣ _)
   extend θ here = var here
   extend θ (there x) = there *ᵣ (θ x)

   -- Lift a type substitution to a type.
   _*_ : ∀ {Δ Δ′} → Sub Δ Δ′ → Δ ⊦ → Δ′ ⊦
   θ * nat = nat
   θ * ???? = ????
   θ * var x = θ x
   θ * (τ₁ + τ₂) = (θ * τ₁) + (θ * τ₂)
   θ * (τ₁ ⨰ τ₂) = (θ * τ₁) ⨰ (θ * τ₂)
   θ * μ τ = μ (extend θ * τ)

   data Trie {????} (A : Set ????) : Type → Set ???? where
      〈〉 : A → ???? ▷ A
      〔_,_〕 : ∀ {τ₁ τ₂} → τ₁ ▷ A → τ₂ ▷ A → τ₁ + τ₂ ▷ A
      ↑_ : ∀ {τ₁ τ₂} → τ₁ ▷ τ₂ ▷ A → τ₁ ⨰ τ₂ ▷ A
      roll : ∀ {τ} → (const (μ τ) * τ) ▷ A → μ τ ▷ A

   infixr 5 Trie
   syntax Trie A τ = τ ▷ A

   {-# NO_TERMINATION_CHECK #-}
   fmap : ∀ {a} {A B : Set a} {τ} → (A → B) → τ ▷ A → τ ▷ B
   fmap f (〈〉 x)    = 〈〉 (f x)
   fmap f 〔 σ₁ , σ₂ 〕 = 〔 fmap f σ₁ , fmap f σ₂ 〕
   fmap f (↑ σ)    = ↑ (fmap (fmap f) σ)
   fmap f (roll σ) = roll (fmap f σ)

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

这里最简单的方法是什么？ inline/fuse trick 看起来并不特别适用，但也许确实适用。还是我应该寻找另一种方法来处理 Trie 定义中的替换？

Answer 1

内联/熔断技巧可以（也许）以令人惊讶的方式应用。此技巧适用于此类问题：

data Trie (A : Set) : Set where
  nil  :                     Trie A
  node : A → List (Trie A) → Trie A

map-trie : {A B : Set} → (A → B) → Trie A → Trie B
map-trie f nil = nil
map-trie f (node x xs) = node (f x) (map (map-trie f) xs)

这个函数在结构上是递归的，但是以一种隐藏的方式。 map 只是将map-trie f 应用于xs 的元素，因此map-trie 应用于较小的（子）尝试。但是 Agda 并没有通过 map 的定义来查看它没有做任何时髦的事情。所以我们必须应用 inline/fuse 技巧让它通过终止检查器：

map-trie : {A B : Set} → (A → B) → Trie A → Trie B
map-trie         f nil = nil
map-trie {A} {B} f (node x xs) = node (f x) (map′ xs)
  where
  map′ : List (Trie A) → List (Trie B)
  map′ [] = []
  map′ (x ∷ xs) = map-trie f x ∷ map′ xs

---

您的fmap 函数具有相同的结构，您映射了某种提升的函数。但是要内联什么呢？如果我们按照上面的例子，我们应该内联fmap 本身。这看起来和感觉有点奇怪，但确实有效：

fmap fmap′ : ∀ {a} {A B : Set a} {τ} → (A → B) → τ ▷ A → τ ▷ B

fmap  f (〈〉 x) = 〈〉 (f x)
fmap  f 〔 σ₁ , σ₂ 〕 = 〔 fmap f σ₁ , fmap f σ₂ 〕
fmap  f (↑ σ) = ↑ (fmap (fmap′ f) σ)
fmap  f (roll σ) = roll (fmap f σ)

fmap′ f (〈〉 x) = 〈〉 (f x)
fmap′ f 〔 σ₁ , σ₂ 〕 = 〔 fmap′ f σ₁ , fmap′ f σ₂ 〕
fmap′ f (↑ σ) = ↑ (fmap′ (fmap f) σ)
fmap′ f (roll σ) = roll (fmap′ f σ)

---

您可以应用另一种技术：它称为尺寸类型。与其依赖编译器来确定某个东西何时是或不是结构递归的，不如直接指定它。但是，您必须通过 Size 类型来索引您的数据类型，因此这种方法相当具有侵入性，不能应用于已经存在的类型，但我认为值得一提。

在其最简单的形式中，已调整大小的类型表现为由自然数索引的类型。该索引指定结构大小的上限。您可以将其视为树高度的上限（假设数据类型是某个函子 F 的 F 分支树）。 List 的大小版本看起来几乎像 Vec，例如：

data SizedList (A : Set) : ℕ → Set where
  []  : ∀ {n} → SizedList A n
  _∷_ : ∀ {n} → A → SizedList A n → SizedList A (suc n)

但大小类型添加了一些使它们更易于使用的功能。当您不关心大小时，您有一个常量∞。 suc 被称为↑，Agda 实现的规则很少，例如↑ ∞ = ∞。

让我们重写Trie 示例以使用大小类型。我们需要在文件顶部有一个编译指示和一个导入：

{-# OPTIONS --sized-types #-}
open import Size

这是修改后的数据类型：

data Trie (A : Set) : {i : Size} → Set where
  nil  : ∀ {i}                         → Trie A {↑ i}
  node : ∀ {i} → A → List (Trie A {i}) → Trie A {↑ i}

如果您将map-trie 函数保持原样，终止检查器仍会抱怨。那是因为当你不指定任何大小时，Agda 会填入无穷大（即 don't-care 值），我们又回到了起点。

但是，我们可以将map-trie 标记为保留大小：

map-trie : ∀ {i A B} → (A → B) → Trie A {i} → Trie B {i}
map-trie f nil         = nil
map-trie f (node x xs) = node (f x) (map (map-trie f) xs)

所以，如果你给它一个以i 为边界的Trie，它也会给你另一个以i 为边界的Trie。所以map-trie 永远不能让Trie 变大，只能变大或变小。这足以让终止检查器确定map (map-trie f) xs 没问题。

---

这个技巧也可以应用到你的Trie：

open import Size
  renaming (↑_ to ^_)

data Trie {?} (A : Set ?) : {i : Size} → Type → Set ? where
  〈〉    : ∀ {i} → A →
    Trie A {^ i} ?
  〔_,_〕 : ∀ {i τ₁ τ₂} → Trie A {i} τ₁ → Trie A {i} τ₂ →
    Trie A {^ i} (τ₁ + τ₂)
  ↑_    : ∀ {i τ₁ τ₂} → Trie (Trie A {i} τ₂) {i} τ₁ →
    Trie A {^ i} (τ₁ ⨰ τ₂)
  roll  : ∀ {i τ} → Trie A {i} (const (μ τ) * τ) →
    Trie A {^ i} (μ τ)

infixr 5 Trie
syntax Trie A τ = τ ▷ A

fmap : ∀ {i ?} {A B : Set ?} {τ} → (A → B) → Trie A {i} τ → Trie B {i} τ
fmap f (〈〉 x) = 〈〉 (f x)
fmap f 〔 σ₁ , σ₂ 〕 = 〔 fmap f σ₁ , fmap f σ₂ 〕
fmap f (↑ σ) = ↑ fmap (fmap f) σ
fmap f (roll σ) = roll (fmap f σ)