recursion-schemes
包中定义了以下类型:newtype Fix f = Fix (f (Fix f))
newtype Mu f = Mu (forall a. (f a -> a) -> a)
它们是同构的吗?如果是,如何证明?
recursion-schemes
包中定义了以下类型:newtype Fix f = Fix (f (Fix f))
newtype Mu f = Mu (forall a. (f a -> a) -> a)
它们是同构的吗?如果是,如何证明?
它们同构吗?
是的,在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
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.
k
都必须通过直接应用代数(需要一个 f Void
值)或使用 fmap
递归应用它来获得,并且这两种情况都可以用 \alg -> cata alg t
的形式表达。因此,我相信我已经按照您的建议做到了,尽管“从头开始”可能不是最好的选择来描述它。 - duplodealg
必须应用于“某物”。这是正确的想法。 - Li-yao Xiacata Fix t = t
推导(实际上,考虑到这两个论点之间的相似之处,我现在觉得将其列出可以帮助为答案的第二部分做好准备)。感谢你指出需要改进的地方。 - duplodecata Fix t = t
也是证明 Fix f
是初始值所必需的。还有一个问题:您是否有任何关于为什么可以在 unfix t
上使用这样的归纳论证的参考/解释?对我来说,它仍然有点神秘。 - marcosh
yes
(因为它是惰性求值语言),而在严格的语言中则为Mu f < Fix f < Nu f
。 - xgrommxFix
到Mu
本质上是cata
,而从Mu
到Fix
是mu2fix(Mu x) = x Fix
。棘手的部分在于证明它们是相互逆的,利用参数性。 - chimu2fix . fix2mu
是简单的方向,而fix2mu . mu2fix
则需要这样的一个参数。 - duplodeFix
表示但不能用Mu
表示的术语的例子是什么?我认为Fix
应该是最小的(直观地因为它是一个“数据结构”,不包含底部)。 - luqui