Agda：构造递归记录值？

Question

我想知道，是否有可能具有values相互依赖的记录，而不必按类型递归定义？基本上，我的记录类型如下：

record SomeRec (a : Set) : Set where   
  method1 : a -> a -> Foo   
  method2 : a -> a -> Bar  
  ...  
  method n : a -> a -> Baz

其中n足够大，我实际上希望将所有这些捆绑在一起作为记录，而不仅仅是一堆相互递归的函数。 （此外，我使用SomeRec作为实例参数）。值得注意的是，SomeRec不是递归的：它的任何字段类型都不引用SomeRec。

现在，我有一个描述D，其中FD：Set-> Set是D描述的函子。我想显示的是以下内容：

muRec : ( FRec : (a : Set) -> SomeRec a -> SomeRec (FD a) ) -> SomeRec (mu D)

也就是说，如果我可以将（SomeRec a）取为（SomeRec（F a）），那么我可以递归地打结，并显示整个实例。原则上可以做到这一点：对SomeRec字段的每个递归调用都将使用严格较小的参数进行。如果我只有10个相互递归的方法，那将起作用。但是，如果我尝试建立记录，最终我会将muRec传递给FRec 而其参数不会减少。

所以，我想知道的是：有没有办法证明这是有根据的？即使记录类型不是归纳或共归的，归纳或共归也可以帮助吗？

我当前的方法是制作D的大小索引版本，并从大小

谢谢！

Answer 1

FRec : (a : Set) -> SomeRec a -> SomeRec (FD a)参数要求太多。它不应该要求完整的SomeRec a，而只是要求在某些x : FD a的子项上调用这些方法的结果。

如果方法真的很简单，您可以定义]

record Results : Set where   
  field1 : Foo   
  field2 : Bar  
  ...  
  fieldn : Baz
然后有muRec具有类似的类型

muRec : (FRec : (a : Set) (x : FD a) (y : FD a) 
                 (IH : (t1 t2 : a) -> In t1 x -> In t2 y -> Results)
                 -> Results)
        -> mu D -> mu D -> Results
IH的类型可能需要根据递归模式进行调整。In : {a : Set} -> a -> FD a -> Set是一些谓词，您应该可以使用D进行定义，该谓词应将子树与其父树相关联。