Agda 中数据结构的导数

Question

I am currently implementing derivatives of regular data structures, in Agda, as presented in the One-Hole Context paper by Conor McBride [5].

In implementing it straight out of the OHC paper, which has also been done by Löh & Magalhães [3,4], we are left with the ?_? function highlighted in red, as Agda can't tell if the ? and I cases will terminate together. Löh & Magalhães made a comment of this in their repository.

Other papers have also included a similar implementation or definitions in their papers [7,8] but do not have a repo (at least I haven't been able to find it) [1,2,6], or they follow a different approach [9] in which ? is defined separately from Reg, ?_?, and derive (or dissection in their case), with no environment, and the operations are performed on a stack.

Using the {-# TERMINATING #-} or {-# NON_TERMINATING #-} flags is undesirable. Particularly, anything using ?_? will not normalize, and thus I can't use this function to prove anything.

The implementation below is a slight modification to the OHC implementation. It removes weakening and substitution as part of the structural definition of Reg. Which, at first, makes ?_? happy! But I find a similar problem when implementing derive -- Agda's termination checker is not happy with the ? case.

I haven't been successful at convincing Agda that derive terminates. I was wondering if anyone had successfully implemented derive with the signature derive : {n : ?} ? (i : Fin n) ? Reg n ? Reg n

The code below only shows some of the important pieces. I have included a gist with the rest of the definitions, which includes definitions of substitution and weakening and the derive that fails to terminate.

 -- 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 = {!!}

Complete code: https://pastebin.com/awr9Bc0R

[1] Abbott, M., Altenkirch, T., Ghani, N., and McBride, C. (2003). Derivatives of con- tainers. In International Conference on Typed Lambda Calculi and Applications, pages 16–30. Springer.

[2] Abbott, M., Altenkirch, T., McBride, C., and Ghani, N. (2005). ? for data: Differ- entiating data structures. Fundamenta Informaticae, 65(1-2):1–28.

[3] Löh, A. & Magalhães JP (2011). Generic Programming with Indexed Functors. In Proceedings of the seventh ACM SIGPLAN Workshop on Generic Programming (WGP'11).

[4] Magalhães JP. & Löh, A. (2012) A Formal Comparison of Approaches to Datatype-Generic Programming. In Proceedings Fourth Workshop on Mathematically Structured Functional Programming (MSFP '12).

[5] McBride, C. (2001). The derivative of a regular type is its type of one-hole contexts. Unpublished manuscript, pages 74–88.

[6] 麦克布莱德，C.（2008 年）。我左边的小丑，右边的小丑（珍珠）：剖析数据结构。在 ACM SIGPLAN Notices，第 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)。从代数到抽象机器：经过验证的泛型构造。在第 3 届 ACM SIGPLAN 类型驱动开发国际研讨会论文集，第 78-90 页。ACM。

Answer 1

derive终止的定义，您只是错误地修改了repo 中的代码。如果derive仅F在?? F案例中调用，那显然是结构性的。在您尝试递归的代码示例中^ (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