问题标签 [fixpoint-combinators]

在 Haskell 中关于不动点的文本中，经常提到最小和最大不动点。例如在Data.Functor.Fixedpoint文档或这里。

最小和最大暗示所涉及类型的顺序（或者仅在固定点上定义它就足够了吗？）无论如何，我从来没有看到这个顺序被明确表示。

在 Haskell 中，一个固定点大于另一个固定点的正式含义是什么？

我已经意识到以下程序

速度惊人。它比递归定义快得多：

我很难理解定点定义实际上归结为哪种程序算法。仅仅是因为 Haskell 的编译器做了一些巧妙的优化，还是它本质上很快？

让我们稍微解开固定点：

Haskell 编译器是否识别 x = y 和“short-fuse”？它会更多地了解列表 x，还是会从头开始重新计算 y 的所有内容？

我觉得短融合会产生一个快速的算法，而重新计算 y 会给出大致相当于递归算法的东西？

是否有任何技巧/思维方式可以更轻松地确定使用固定点的算法的复杂性？它对编译器的评估策略敏感吗？

编辑：fix在这篇文章中，它代表一般用 Haskell 写下的定点组合，而不仅仅是Data.Function.fix.

众所周知，fix可能是非共享的，因为 GHC 并不总是消除常见的子表达式：

长话短说：“如果您关心 CSE，请亲自动手。”

fix使用 -combinator 可以很容易地写下无点S：

如果我们返回积分，我们将得到众所周知的非共享实现：

我相信，在这种情况下，GHC 无法完成 CSE，因为它fix f取决于f第一个论点中的懒惰。事实上，正如Daniel Wagner所建议的，请看以下代码段：

fix f = let x = f x in x它用完了〜54,5 kB，而用-〜615 kB fix = ($) <*> fix。

是否有可能以fix某种方式免费写下共享点？

我一直在尝试mfix使用Control.Arrow.loop. 我想出了不同的定义，并mfix想看看哪一个是实际工作相似的。

因此，我认为正确的解决方案如下：

可以看到，loop . Kleisli' 的论点适用于Applicative实例。我发现这是一个好兆头，因为在正确的论点中，我们的打结大多被(>>=)' 严格性破坏了。

这是另一个功能。我可以说这不是mfix完全一样的，但我发现的唯一情况不是很自然。看一看：

据我了解，并非所有严格的右手绑定都完全强制其论点。例如，在以下情况下IO：

所以，我决定解决这个问题。我只是接受Maybe并强行x加入Just x >>= k：

我们手上有这个：

所以，这是我的问题：

1. 有没有其他例子可以证明这mfix''不是完全的mfix？
2. 具有如此严格绑定的 monadMaybe'在实践中是否有趣？
3. 是否有任何例子表明我没有找到mfix'不完全是？mfix

关于IO：

不要担心所有的returns 和joins - 它们在这里只是为了让mfix3's 和mfix' 类型匹配。这个想法是我们传递d自己而不是传递return d到(>>=)右手边。它为我们提供了以下信息：

然而，例如（感谢Li-yao Xia的评论）：

编辑：感谢HTNW 在评论中对模式匹配的重要说明：最好使用\ ~(_, d) -> ...，而不是\ (_, d) -> ....

我真的很喜欢这个repmin问题：

写下repmin :: Tree Int -> Tree Int，它在一次通过中将树中的所有数字替换为它们的最小值。

如果我在 python 中编写这样的东西，我会通过引用传递值（假设单元素列表而不是数字就足够了）：

在我看来，这似乎是一种合适的方式来围绕 Haskell 中的打结解决方案（我从 为玫瑰树Data.Tree写了这个）：

然而，我认为解决方案的工作方式非常不同。以下是我对后一种的理解：

让我们重写loop一下(->)：

我认为它与loopfor(->)的工作相似，因为snd它给出了与let.

因此，当repmin遍历树时，它是：

• 在树中建立最小值，作为该对的第二个元素返回。
• snd $ copyRose (tree, m)在每个节点中留下。

因此，当遍历结束时，程序知道snd $ copyRose (tree, m)（即树中的最小值）的值，并且能够在计算树的某个节点时显示它。

我repmin在 Haskell 中理解正确吗？

自然数的著名 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。

fix f = let {x = f x} in x

谈到let，我认为let P = Q in R会评估 Q -> Q' 然后 P 被 R 中的 Q' 替换，或者：R[P -> Q']。

但是在fix定义上Q取决于R，那么如何评估呢？

我想这是关于惰性评估的。Q'变成了一个重击，但我无法在我的脑海中推理。

作为上下文，我正在查看Y组合器，它应该找到函数的固定点，所以如果我有这个函数one x = 1，那么 fix one == 1必须保持，对吗？

所以fix one = let {x = one x} in x，但我看不出1会如何出现。

我试图证明这里描述的队列实现的正确性：

在这里提琴

我想证明的一件事是排空队列，所以我定义了这个函数来进行计算：

推理queue_dump_all具有挑战性，所以我试图证明这个引理以允许更直接的计算：

不过，我一直无法使用 取得进展queue_dump_all_elim。我怀疑问题可能是“手动”匹配，worker而不是依赖于Equation' 模式匹配构造，但是我在以这种方式证明格式良好时遇到了麻烦。有没有办法推动这个证明？

（最初是用写的，Program Fixpoint但我也无法得到这个答案）。

我正在尝试将这个 JS 定点运算符翻译成 Haskell。

JS：

我的尝试是（Haskell）：

但是，我收到以下错误：

有人知道这里发生了什么吗？

我是 Haskell 的新手，我有以下代码：

我希望xs被评估为[1,2,3,4,2,4,4]，因为那是固定点，即[1,2,3,4,2,4,4] == [1,2,3,4] ++ second [1,2,3,4,2,4,4]。

但是，当我尝试xs在 GHCi 中进行评估时，我得到

但它不会停止计算。

谁能解释为什么这不会停止，是否有一种简单的方法可以使计算停止并返回[1,2,3,4,2,4,4]？