问Agda中数据结构的导数

EN

我目前正在Agda中实现常规数据结构的派生，如Conor McBride 5的One-Hole Context论文中所述。

在直接从OHC论文中实现它时，Löh & Magalhães 3,4也这样做了，我们留下了用红色突出显示的⟦_⟧函数，因为Agda不能判断μ和I案例是否会一起终止。Löh & Magalhães在their repository上对此发表了评论。

其他论文也在他们的论文7,8中包含了类似的实现或定义，但没有repo (至少我还没有找到它) 1,2,6，或者他们遵循不同的方法9，其中μ与Reg，⟦_⟧和derive分开定义(或者在他们的案例中是derive)，没有环境，并且操作在堆栈上执行。

不希望使用{-# TERMINATING #-}或{-# NON_TERMINATING #-}标志。特别是，使用⟦_⟧的任何东西都不会规范化，因此我不能使用这个函数来证明任何东西。

下面的实现是对OHC实现的细微修改。它删除了作为Reg结构定义的一部分的弱化和替换。一开始，这让⟦_⟧很高兴！但我在实现derive时发现了一个类似的问题-- Agda的终止检查器对μ的情况不满意。

我还没有成功地说服Agda相信derive已经终止了。我想知道是否有人用签名derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n成功地实现了derive

下面的代码只显示了一些重要的部分。我已经在其余的定义中包含了一个要点，其中包括替换和弱化的定义以及无法终止的派生。

 -- Regular universe, multivariate.
 -- n defines the number of variables
 data Reg : ℕ → Set₁ where
   0′    : {n : ℕ} → Reg n
   1′    : {n : ℕ} → Reg n
   I     : {n : ℕ} → Fin n → Reg n 
   _⨁_  : {n : ℕ} → (l r : Reg n) → Reg n
   _⨂_  : {n : ℕ} → (l r : Reg n) → Reg n
   μ′    : {n : ℕ} → Reg (suc n)   → Reg n

 infixl 30 _⨁_
 infixl 40 _⨂_

 data Env : ℕ → Set₁ where
   []  : Env 0
   _,_ : {n : ℕ} → Reg n → Env n → Env (suc n)

 mutual
   ⟦_⟧ : {n : ℕ} → Reg n → Env n → Set
   ⟦ 0′ ⟧  _ = ⊥
   ⟦ 1′ ⟧  _ = ⊤
   ⟦ I zero  ⟧   (X , Xs) = ⟦ X ⟧  Xs   
   ⟦ I (suc n) ⟧ (X , Xs) = ⟦ I n ⟧ Xs  
   ⟦ L ⨁ R ⟧ Xs = ⟦ L ⟧ Xs ⊎ ⟦ R ⟧ Xs
   ⟦ L ⨂ R ⟧ Xs = ⟦ L ⟧ Xs × ⟦ R ⟧ Xs
   ⟦  μ′ F  ⟧ Xs =  μ F Xs

   data μ {n : ℕ} (F : Reg (suc n)) (Xs : Env n) : Set where
     ⟨_⟩ : ⟦ F ⟧ (μ′ F , Xs) → μ F Xs

 infixl 50 _[_]
 infixl 50 ^_

 _[_]  : {n : ℕ} → Reg (suc n) → Reg n → Reg n
 ^_    : {n : ℕ} → Reg n → Reg (suc n)

 derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n
 derive = {!!}

完整代码：https://pastebin.com/awr9Bc0R

1 Abbott，M.，Altenkirch，T.，Ghani，N.和McBride，C. (2003年)。容器的衍生物。在类型Lambda演算和应用国际会议上，第16-30页。斯普林格。

2雅培，M.，Altenkirch，T.，McBride，C.和加尼，N. (2005)。数据的δ:区分数据结构。基础信息，65(1-2)：1-28。

3 Löh，A. & Magalhães JP (2011)。带索引函数器的泛型编程。在第七届ACM SIGPLAN泛型编程研讨会(WGP'11)论文集中。

4 Magalhães JP.& Löh，A。(2012) Datatype泛型编程方法的正式比较。在Proceedings第四次数学结构函数式编程研讨会(MSFP '12)中。

5 McBride，C. (2001)。正则类型的导数是它的单孔上下文类型。未发表的手稿，第74-88页。

6 McBride，C. (2008)。我左边的小丑，右边的小丑(珍珠)：剖析数据结构。在ACM SIGPLAN通知中，第43卷，第287-295页。ACM。

7 Morris，P.，Altenkirch，T.，& McBride，C. (2004年12月)。探索常规的树类型。在关于校样和程序类型的国际研讨会上(第252-267页)。施普林格，柏林，海德堡。

8 Sefl，V. (2019)。拉链的性能分析。arXiv预印本arXiv:1908.10926。

9 Tome Cortinas，C.和Swierstra，W. (2018)。从代数到抽象机:一种经过验证的通用结构。在第三届ACM SIGPLAN类型驱动开发国际研讨会论文集，第78-90页。ACM。