3

我很难说服 Agda 终止检查fmap下面的函数以及在 a 的结构上递归定义的类似函数Trie。ATrie是一个域为 a的trieType ，它是由单元、乘积和固定点组成的对象级类型（我省略了副乘积以保持代码最小化）。这个问题似乎与我在定义中使用的类型级替换有关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在每种情况下都递归成一个严格较小的论点；如果我删除递归类型，产品案例当然很好。另一方面，如果我删除产品，定义可以很好地处理递归类型。

在这里进行最简单的方法是什么？内联/熔断技巧看起来并不特别适用，但也许确实适用。还是我应该寻找另一种方法来处理定义中的替换Trie？

4

1 回答 1

5
于 2014-02-02T23:34:28.693 回答