agda - Agda 中数据结构的导数

Question

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

Löh & Magalhães [3,4] 也在 OHC 论文中直接实现了它，我们只剩下 ⟦_⟧以红色突出显示的功能，
因为 Agda 无法判断 μ和 I案件将一起终止。
Löh & Magalhães 在 their repository 中对此发表了评论.

其他论文也在他们的论文中包含了类似的实现或定义 [7,8] 但没有
有一个 repo (至少我没能找到)[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 演算和应用国际 session 上，第 16-30 页。斯普林格。

[2] Abbott, M.、Altenkirch, T.、McBride, C. 和 Ghani, N. (2005)。 δ 数据:区分数据结构。基础信息学，65(1-2):1-28。

[3] Löh, A. & Magalhães JP (2011)。带索引仿函数的泛型编程。在第七届 ACM SIGPLAN 泛型编程研讨会 (WGP'11) 的 session 记录中。

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

[5] 麦克布莱德，C.(2001 年)。常规类型的衍生物是它的单孔上下文类型。未发表的手稿，第 74-88 页。

[6] 麦克布莱德，C.(2008 年)。我左边的 clown ，右边的 clown (珍珠):剖析数据结构。在 ACM SIGPLAN Notices，第 43 卷，第 287-295 页。 ACM。

[7] Morris, P.、Altenkirch, T. 和 McBride, C.(2004 年，12 月)。探索常规树类型。在关于证明和程序类型的国际研讨会(第 252-267 页)中。斯普林格，柏林，海德堡。

[8] Sefl, V. (2019)。 zipper 的性能分析。 arXiv 预印本 arXiv:1908.10926。

[9] Tome Cortinas, C. 和 Swierstra, W. (2018)。从代数到抽象机器:经过验证的泛型构造。在第 3 届 ACM SIGPLAN 类型驱动开发国际研讨会论文集，第 78-90 页。 ACM。

Answer 1

derive的定义终止，您刚刚修改了 repo 中的代码不正确。如 derive仅在 F 上调用在 μ′ F情况，这显然是结构性的。在 code sample你试图在 ^ (F [ μ′ F ]) 上递归反而。

derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n
derive i 0′ = 0′
derive i 1′ = 0′
derive i (I j) with i ≟ j
derive i (I j) | yes refl = 1′
...            | no _     = 0′
derive i (L ⨁ R) = derive i L ⨁ derive i R
derive i (L ⨂ R) = (derive i L ⨂ R) ⨁ (L ⨂ derive i R)
derive i (μ′ F) = μ′ (    (^ (derive (suc i) F [ μ′ F ]))
                       ⨁ (^ (derive zero F [ μ′ F ])) ⨂ I zero)

我也建议调整 Reg如下，自 n因为索引是不必要的，并且 Set₁以及。

data Reg (n : ℕ) : Set where
  0′    : Reg n
  1′    : Reg n
  I     : Fin n → Reg n
  _⨁_  : (l r : Reg n) → Reg n
  _⨂_  : (l r : Reg n) → Reg n
  μ′    : Reg (suc n)  → Reg n