Agda中数据结构的导数

Question

我目前正在阿格达（Agda）实现常规数据结构的派生，如Conor McBride [5]在“单孔上下文”论文中所介绍的。

[直接从OHC文件中实施，这也是Löh＆Magalhães[3,4]所做的，剩下的是⟦_⟧功能以红色突出显示，因为Agda无法判断μ和I案例是否会一起终止。Löh＆Magalhães在their repository中对此发表了评论。

[其他论文在其论文中也包含类似的实现或定义[7,8]，但没有有一个仓库（至少我找不到它）[1,2,6]，或者他们遵循不同的方法[9]，其中μ分别定义从Reg，⟦_⟧和derive（在其情况下为解剖）中获取，没有环境，并且操作在堆栈上执行。

使用{-# TERMINATING #-}或{-# NON_TERMINATING #-}标志是不可取的。特别是，任何使用⟦_⟧的内容都不会规范化，因此，我无法使用此功能来证明任何事情。

以下实施是对OHC实施的略微修改。作为Reg的结构定义，它删除了弱化和替换。首先让⟦_⟧开心！但是我在实施时发现了类似的问题derive-Agda的终止检查器对μ情况不满意。

我未能成功说服Agda derive终止。我想知道是否有人成功实施了derive签名derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n

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

 -- 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] Abbott，M.，Altenkirch，T.，McBride，C.，and Ghani，N.（2005）。数据的δ：不同的数据结构。 Fundamenta Informaticae，65（1-2）：1–28。

[3]Löh，A.＆MagalhãesJP（2011）。带索引函子的泛型编程。在第七届ACM SIGPLAN泛型编程讲习班（WGP'11）的会议记录中。

[4]MagalhãesJP。 ＆Löh，A.（2012）数据类型通用编程方法的形式比较。在《第四届数学结构函数编程》研讨会上（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。

我目前正在Agda中实现常规数据结构的派生，如Conor McBride的“一孔上下文”论文所介绍的[5]。在直接从OHC文件中实施时，...

Answer 1

derive的定义终止，您只是错误地改写了repo中的代码。如果在derive情况下仅在F上调用μ′ F，那显然是结构性的。在code sample中，您尝试对^ (F [ μ′ F ])进行递归。