修复和Mu同构

Question

修复和Mu同构

haskellrecursion-schemesfixpoint-combinators

9

在 recursion-schemes 包中定义了以下类型：

newtype Fix f = Fix (f (Fix f))

newtype Mu f = Mu (forall a. (f a -> a) -> a)

它们是同构的吗？如果是，如何证明？

- marcosh

3

相关内容：Ed Kmett的递归方案包中Fix、Mu和Nu有什么区别（那里的答案唯一没有明确写下的是同构） - duplode

在 Haskell 中是 yes（因为它是惰性求值语言），而在严格的语言中则为 Mu f < Fix f < Nu f。 - xgrommx

3

关于同构；从Fix到Mu本质上是cata，而从Mu到Fix是mu2fix(Mu x) = x Fix。棘手的部分在于证明它们是相互逆的，利用参数性。 - chi

你也可以解决这个编程题 https://www.codewars.com/kata/folding-through-a-fixed-point - xgrommx

@chi 是的。mu2fix . fix2mu 是简单的方向，而 fix2mu . mu2fix 则需要这样的一个参数。 - duplode

1

@xgrommx，在严格的上下文中，可以用Fix表示但不能用Mu表示的术语的例子是什么？我认为Fix应该是最小的（直观地因为它是一个“数据结构”，不包含底部）。 - luqui

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- duplode · Accepted Answer

它们同构吗？

是的，在Haskell中它们是同构的。有关一些附加说明，请参见Ed Kmett递归方案包中Fix、Mu和Nu之间的区别是什么。

如果是这样，你如何证明它呢？

让我们开始定义函数来执行转换：

muToFix :: Mu f -> Fix f
muToFix (Mu s) = s Fix

fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)

为了展示这些函数见证同构，我们必须展示以下内容：

muToFix . fixToMu = id
fixToMu . muToFix = id

从`Fix`到回溯

同构的一个方向比另一个方向更加简单明了:

muToFix (fixToMu t) = t
muToFix (fixToMu t)  -- LHS
muToFix (Mu (\f -> cata f t))
(\f -> cata f t) Fix
cata Fix t  -- See below.
t  -- LHS = RHS

上述最后一段代码可以通过的定义进行验证：

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix

cata Fix t的意思是Fix (fmap (cata Fix) (unfix t))。我们可以使用归纳法来证明它必须是t，至少对于有限的t是成立的（对于无限结构，情况会更加微妙--请参见本答案末尾的补充说明）。有两种可能性需要考虑：

unfix t :: f (Fix f) is empty, having no recursive positions to dig into. In that case, it must be equal to fmap absurd z for some z :: f Void, and thus:

cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (fmap (cata Fix) (fmap absurd z))
Fix (fmap (cata Fix . absurd) z)
-- fmap doesn't do anything on an empty structure.
Fix (fmap absurd z)
Fix (unfix t)
t

unfix t is not empty. In that case, we at least know that fmap (cata Fix) can't do anything beyond applying cata Fix on the recursive positions. The induction hypothesis here is that doing so will leave those positions unchanged. We then have:
```
cata Fix t
Fix (fmap (cata Fix) (unfix t))
Fix (unfix t)  -- Induction hypothesis.
t
```

(最终，cata Fix = id 是 Fix :: f (Fix f) -> Fix x 是一个初始 F-代数的必然结果。在证明中直接诉诸该事实可能是太过于捷径。)

从 `Mu` 到 `Fix` 再到 `Mu`

给定 muToFix . fixToMu = id，为了证明 fixToMu . muToFix = id，我们只需要证明：

muToFix 是单射；或者
fixToMu 是满射。

我们选择第二个选项，并回顾相关定义：

newtype Mu f = Mu (forall a. (f a -> a) -> a)

fixToMu :: Functor f => Fix f -> Mu f
fixToMu t = Mu (\alg -> cata alg t)

fixToMu是满射的，这意味着，对于任何特定的Functor f，所有类型为forall a. (f a -> a) -> a的函数都可以定义为\alg -> cata alg t，其中t :: Fix f。因此，任务变成了记录forall a. (f a -> a) -> a函数，并查看它们是否都可以用这种形式表达。

如果不依赖于fixToMu，我们如何定义一个forall a. (f a -> a) -> a函数？无论如何，它都必须使用作为参数提供的f a -> a代数来获得a结果。直接的方法是将其应用于某个f a值。一个重要的限制是，由于a是多态的，我们必须能够为任何选择的a产生所需的f a值。只要f-值存在，这是可行的策略。在这种情况下，我们可以执行以下操作：

fromEmpty :: Functor f => f Void -> forall a. (f a -> a) -> a
fromEmpty z = \alg -> alg (fmap absurd z)

为了让符号更加清晰，让我们定义一种类型来表示可以用来定义 forall a. (f a -> a) -> a 函数的东西：

data Moo f = Empty (f Void)

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Empty z) = \alg -> alg (fmap absurd z)

除了直接的路线外，还有另一种可能性。假设 f 是一个 Functor，如果我们以某种方式拥有一个 f (Moo f) 值，我们可以在外层 f 层下通过 fmap 和 fromMoo 进行两次代数应用，第一次应用是在外部 f 层下进行的。

fromLayered :: Functor f => f (Moo f) -> forall a. (f a -> a) -> a
fromLayered u = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

考虑到我们也可以从f (Moo f)的值中得出forall a. (f a -> a) -> a，因此将它们作为Moo的一种情况添加是有意义的:

data Moo f = Empty (f Void) | Layered (f (Moo f))

因此，可以将fromLayered合并到fromMoo中：

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo = \case
    Empty z -> \alg -> alg (fmap absurd z)
    Layered u -> \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

请注意，通过这样做，我们已经巧妙地从在一个f层下应用alg转而递归地在任意数量的f层下应用alg。

接下来，我们可以注意到一个f Void值可以注入到Layered构造函数中：

emptyLayered :: Functor f => f Void -> Moo f
emptyLayered z = Layered (fmap absurd z)

这意味着我们实际上不需要 Empty 构造函数:

newtype Moo f = Moo (f (Moo f))

unMoo :: Moo f -> f (Moo f)
unMoo (Moo u) = u

fromMoo函数中的Empty情况怎么处理？两种情况唯一的区别在于，在Empty情况下，我们使用absurd而不是\moo -> fromMoo moo alg。由于所有的Void -> a函数都是absurd，因此我们也不需要单独处理Empty情况：

fromMoo :: Functor f => Moo f -> forall a. (f a -> a) -> a
fromMoo (Moo u) = \alg -> alg (fmap (\moo -> fromMoo moo alg) u)

一种可能的美化调整是翻转fromMoo参数，这样我们就不需要将参数写成lambda传递给fmap了：

foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg (Moo u) = alg (fmap (foldMoo alg) u)

或者更点无关:

foldMoo :: Functor f => (f a -> a) -> Moo f -> a
foldMoo alg = alg . fmap (foldMoo alg) . unMoo

此时，我们的定义需要进行一些重命名：

newtype Fix f = Fix (f (Fix f))

unfix :: Fix f -> f (Fix f)
unfix (Fix u) = u

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix

fromFix :: Functor f => Fix f -> forall a. (f a -> a) -> a
fromFix t = \alg -> cata alg t

这就是所有 forall a. (f a -> a) -> a 函数的形式：\alg -> cata alg t，其中t :: Fix f。因此，fixToMu 是满射的，我们得到了所需的同构。

补充说明

在评论中，有人提出了关于推导cata Fix t = t中归纳论证适用性的相关问题。至少在函数子范畴和参数化方面，fmap (cata Fix)不会产生额外的工作（例如，它不会扩大结构或引入额外的递归位置），这解释了为什么进入递归位置是推导归纳步骤中唯一需要考虑的事情。因此，如果t是一个有限结构，将最终达到空的f (Fix t)基本情况，一切都很清楚。然而，如果我们允许t是无限的，那么我们可以不断下降,fmap后的fmap后的fmap，永远不会达到基本情况。

无限结构的情况并不像一开始看起来那么糟糕。懒惰原则使得无限结构在第一时间就变得可行，它允许我们懒惰地消耗无限结构。

GHCi> :info ListF
data ListF a b = Nil | Cons a b
    -- etc.
GHCi> ones = Fix (Cons 1 ones)
GHCi> (\(Fix (Cons a _)) -> a) (cata Fix ones)
1
GHCi> (\(Fix (Cons _ (Fix (Cons a _)))) -> a) (cata Fix ones)
1

虽然递归位置的继承是无限的，但我们可以在任何时候停止，并从周围的 ListF 函子上下文中获得有用的结果。这些上下文不受 fmap 的影响，因此我们可能消耗的结构的任何有限部分都不会受 cata Fix 的影响。

这种惰性缓解反映了如何在本讨论的其他地方提到的那样，惰性折叠了固定点 Mu、Fix 和 Nu 之间的区别。没有惰性，Fix 不足以编码生产性的核心递归，因此我们必须切换到最大固定点 Nu。以下是一个小差异的演示：

GHCi> :set -XBangPatterns
GHCi> -- Like ListF, but strict in the recursive position.
GHCi> data SListF a b = SNil | SCons a !b deriving Functor
GHCi> ones = Nu (\() -> SCons 1 ()) ()
GHCi> (\(Nu c a) -> (\(SCons a _) -> a) (c a)) ones
1
GHCi> ones' = Fix (SCons 1 ones')
GHCi> (\(Fix (SCons a _)) -> a) ones'
^CInterrupted.

修复和Mu同构

从Fix到回溯

从 Mu 到 Fix 再到 Mu

补充说明

从`Fix`到回溯

从 `Mu` 到 `Fix` 再到 `Mu`