问题标签 [recursion-schemes]

当转换器函数中需要给定项目的位置（索引或路径）时，使用哪一个是合适的态射（递归方案）？

一个简单的示例是将列表["foo", "bar", "qux"]转换为字符串"foo, bar, and qux"。需要当前元素的位置来知道何时插入and.

自然数的著名 Church 编码可以推广到使用任意函子F。结果是类型，称为它C，定义为

在这里和下面，为简单起见，我们将假设它F是一个固定的、已经定义的函子。

众所周知，类型C是函子的固定点F，也是C初始F代数。例如，如果函子F a定义为

然后是F ais的固定点[a]（类型的值列表a）。另外，[a]是初始代数。列表的 Church 编码是众所周知的。但是我找不到这些陈述中的任何一个的严格证明（C是一个固定点，并且C是初始代数）。

问题是，如何严格证明两个陈述之一：

1. 该类型C是类型 isomorphism 的固定点F C ≅ C。换句话说，我们需要证明存在两个函数，fix :: F C -> C并且unfix :: C -> F C使得fix . unfix = id和unfix . fix = id。
2. 类型C是函子的初始代数F；即-F代数范畴中的初始对象。换句话说，对于任何给定A函数p :: F A -> A的类型（即是-A代数F），我们都可以找到一个唯一的函数q :: C -> A，它是 F-代数态射。这意味着，q必须使法律q . fix = p . fmap q成立。我们需要证明，给定A和p，这样q的存在并且是唯一的。

这两个语句不等价；但证明（2）意味着（1）。（Lambek 定理说初始代数是同构。）

fix函数的代码unfix可以相对容易地编写：

给定一个函数p :: F A -> A，函数的代码q写成

然而，似乎很难直接证明函数fix, unfix,q满足所需的性质。我找不到完整的证明。

C证明它是一个初始代数，即它q是唯一的，比证明它更容易fix . unfix = id吗？

在这个问题的其余部分，我将展示一些我能够为证明fix . unfix = id.

仅通过使用给定的函数代码来证明 (1) 或 (2) 是不可能的。我们需要额外的假设。与米田身份相似，

我们需要假设函数的代码是完全参数化的（没有副作用，没有特别选择的值或固定类型），以便可以应用参数化定理。所以，我们需要假设类型只包含满足适当自然法则C的类型函数。forall r. (F r -> r) -> r

参数化定理为这种类型签名给出了以下自然法则：对于任何类型Aand B，以及对于任何函数p :: F B -> Aand f :: A -> B，函数c :: forall r. (F r -> r) -> r必须满足等式

Using this naturality law with appropriately chosen pand f, one can show that the composition fix . unfixis a certain function of type C -> Cthat must be equal to \c -> (run c) fix.

然而，证明的进一步进展似乎是不可能的。不清楚为什么这个函数必须等于id。

让我们暂时定义函数m：

然后我得到的结果写成

也可以证明这一点unfix . fix = fmap (m fix)。

这还有待证明m fix = id。一旦证明了这一点，我们就证明了F C ≅ C。

相同的自然规律c与不同的选择p并f赋予了奇怪的身份

但不知如何从这个身份中推导出来m fix = id。

在 Haskell 中，我可以写

但 Idris 似乎不允许使用data. 他们确实合作record，即我可以写作

但是如果我理解正确的话，我不能有多个变体。有解决办法吗？

通过共同递归，我的意思是展开一棵树，例如使用anaEd Kmett递归方案中的态射

通过重新组合树，我的意思是共享结构的图。例如，二项式期权定价树或帕斯卡三角形。这两者都有一些对称性，所以为了效率，我们希望避免重新计算树的一部分，而是重新使用已经计算过的分支。

注意这个问题不是关于计算上述示例中的值的一些聪明方法；这是关于递归的一般问题。

例如，对于期权定价，可以像这样生成树：

因此，“向上”分支中p * x的值为 ，“向下”分支中的值为(1-p) * x。由于这种对称性，“up”后跟“down”节点将具有与“down”后跟“up”分支相同的值。它也是整个子树。

我认为有可能以State某种方式传递包含已计算节点的哈希图。

或者，如果我能以某种方式访问​​已经计算过的子树，我可以将它作为态射中的 aLeft传入apo。

是否有一些现有的态射允许这样做？或者我可以自己编码吗？

我对编写递归代码的高阶方式（递归方案）感兴趣，其中递归调用之间可能存在依赖关系。

作为一个简化的例子，考虑一个遍历整数树的函数，检查总和是否小于某个值。我们可以对整棵树求和，并将其与最大值进行比较。或者，我们可以在超过最大值后立即保持运行总和并短路：

有没有办法用递归方案来表达这个想法——本质上是一个有序的遍历？我对尽可能一般地编写这样的有序遍历感兴趣。

理想情况下，我想要某种方式来编写遍历，其中在数据结构上折叠（或展开）的函数决定了遍历的顺序。无论我最终得到什么抽象，我都希望能够编写sumLT'上面遍历的逆序版本，而不是从右到左：

对于此代码，我收到以下错误：

对于这个简单的间接递归示例，可能的错误是什么？我什至尝试改变函数的顺序。

我有这个算法：

如何将其转换为动态规划算法？我尝试了几个想法，但似乎没有一个可行。所以我被困住了。

PS w 和 v 只是简单的数字数组，没什么特别的。W 只是一个数字。这个算法没有实现任何特定的任务，我刚刚在一本书中找到了它，他们要求为给定的公式实现算法。

更新：

这给出了与递归算法不匹配的错误答案。而且它似乎仍然使用递归......

我绘制的递归树

如果我们有一个函子固定点： Fix f = Con (f (Fix f))

then 该函数out : Fix f -> f (Fix f)使用起来不安全，因为 if fis not a Functorthen 您可以轻松编写无限循环（例如 with f x = x -> x）。

我的问题：如果我们只能Fix用 Mendler 式的超态来消除（即使f不是 a Functor），是否可以编写一个无限循环？

对于 Mendler 式的超态，我正在考虑以下类型：

我的预感是答案是否定的，因为我们只能写outiff实际上是一个函子：

所以这意味着它mpara可以安全地与任何f. 我对么？

我的问题是如何将递归的 F 代数风格的递归类型定义与单子/应用风格的解析器结合起来，以适应现实的编程语言。

我刚刚从以下Expr定义开始：

我正在尝试将它与使用变形的解析器结合起来：

据我所知，在我的示例中，psi应该只解析一个整数，或者它应该确定字符串是 a<expr> + <expr>然后（通过递归调用fmap (ana psi)），它应该解析左侧和右侧表达式.

但是，（monadic/applicative）解析器不是这样工作的：

• 他们首先尝试解析左边的表达式，
• +, _
• 和右手表达式

我看到的一种解决方案是更改 to 的类型定义，Plus a a以便Plus Integer a它反映解析过程，但这似乎不是最好的途径。

欢迎任何建议（或阅读指导）！

关于 Haskell 中的递归方案，我最喜欢的事情之一是广义态射（gcata等），它允许使用 monad 转换器库来交叉（co-）monadic 计算与递归。例如，如这篇精彩的博客文章中所述。

但是，我遇到了一个问题；为了能够使用这些函数，我们需要 (co-)monads 是 (co-)sequentiable。考虑一个类型签名gana：

第一个参数本质上说m必须有一个sequence运算符。

不幸的是，我发现在实践中，有些单子不是可分配的。例如：

• 表示数据库事务的 monad。中止时，事务可以回滚；如果已排序，则只能回滚到已排序的点。
• 一个并发单子，表示资源上的锁或原子计算。排序后，锁会暂时丢失。

在这种情况下，仍然可以编写一个专门的递归方案来交错单子执行；但是你失去了使用单子变压器融合它的能力。即，如果你想组合这样的非分配单子，它们不能使用变压器与 f-(co) 代数中的单子/共单子进行融合。具体来说，我不能使用 monad 转换器将DBTransactionmonad 与 apomorphism ( ExceptT/EitherT) 结合起来；我需要从头开始编写自定义递归方案。

我的问题是是否有人有解决此限制的建议。