coop ∷ C → ((Int, Int), String, (Int, Int) → C)
coop self = (position self, name self, setPosition self)
类型((Int, Int), String, (Int, Int) → c)-for anyc-是一个函子,所以coop确实具有我们想要的形式:Functor f ⇒ C → f C . 这样,C沿着coop形成了一个余代数,它指定了我上面给出的类,你可以看到我们如何使用同样的技术来指定对象的任意数量的方法和属性。 这使得我们可以使用余代数推理来处理类。例如,我们可以引入“F-余代数同态”的概念来表示类之间的变换。这是一个听起来很可怕的术语,它只是意味着保持结构的余代数之间的变换。这使得考虑将类Map到其他类变得容易得多。 简而言之,F-余代数通过拥有一堆属性和方法来表示类,这些属性和方法都依赖于包含每个对象内部状态的self参数。
其他类别
到目前为止,我们已经讨论了Haskell类型的代数和余代数,一个代数就是τ型,其中有一个函数f τ → τ,余代数就是τ型,其中有一个函数τ → f τ。 然而,这些概念与Haskell * 本身 * 并没有什么真正的联系。事实上,它们通常是以集合和数学函数的形式引入的,而不是类型和Haskell函数。实际上,我们可以将这些概念推广到 * 任何 * 范畴! 我们可以为某个范畴C定义一个F-代数,首先,我们需要一个函子F : C → C,也就是一个 endofunctor。(所有 haskell Functor实际上都是Hask → Hask的内函子。)那么,一个代数就是从C得到的具有态射F A → A的对象A。余代数除了A → F A之外是相同的。 我们考虑其他范畴会得到什么呢?我们可以在不同的上下文中使用相同的概念,比如单子,在Haskell中,单子是M ∷ ★ → ★类型,有三个运算:
map ∷ (α → β) → (M α → M β)
return ∷ α → M α
join ∷ M (M α) → M α
instance (Functor f, Functor g) ⇒ Functor (f ∘ g) where
fmap fun x = fmap (fmap fun) x
这有助于我们把join看作是f ∘ f → f的Map,join的类型是∀α. f (f α) → f α,直观地,我们可以看到一个对 * 所有 * 类型α有效的函数可以被看作是f的变换。 return是一个类似的变换。它的类型是∀α. α → f α。这看起来不同-第一个α不是“in”函子!幸运的是,我们可以通过在那里添加一个恒等函子来修复这个问题:所以return是个变换。
现在我们可以把一个单子看作是一个代数,它基于某个函子f和f ∘ f → f以及Identity → f,这看起来是不是很熟悉,它非常类似于一个单子,它只是一个类型τ和τ × τ → τ以及() → τ。 因此,单子就像幺半群,只是我们有函子而不是类型,它们是同一种代数,只是在不同的范畴中(据我所知,“单子就是内函子范畴中的幺半群”这句话就是从这里来的)。 现在,我们有两个操作:f ∘ f → f和Identity → f。要得到对应的余代数,我们只需翻转箭头。这给了我们两个新的操作:f → f ∘ f和f → Identity。我们可以通过添加如上所述的类型变量将它们转换为Haskell类型,得到∀α. f α → f (f α)和∀α. f α → α。这看起来就像comonad的定义:
class Functor f ⇒ Comonad f where
coreturn ∷ f α → α
cojoin ∷ f α → f (f α)
sumFold :: IntList -> Int
sumFold Nil = 0
sumFold (Cons x xs) = x + sumFold xs
我们看到这个函数由两部分组成:第一部分定义此函数在IntList的Nil部分上的行为,第二部分定义此函数在Cons部分上的行为。 现在假设我们不是用Haskell编程,而是用某种允许在类型签名中直接使用代数类型的语言(从技术上讲,Haskell允许通过元组和Either a b数据类型使用代数类型,但这会导致不必要的冗长)。
reductor :: () | (Int × Int) -> Int
reductor () = 0
reductor (x, s) = x + s
可以看出,reductor是F1 Int -> Int型函数,正如F-代数的定义一样!的确,对(Int, reductor)是F1-代数。
因为IntList是初始F1-代数,所以对于每个类型T和每个函数r :: F1 T -> T,存在一个函数,称为 * catamorphism * for r,它将IntList转换为T,并且这样的函数是唯一的。在我们的例子中,reductor的退化是sumFold。注意reductor和sumFold是如何相似的:它们具有几乎相同的结构!在reductor定义s中,参数用法(其类型对应于T)对应于sumFold定义中sumFold xs的计算结果的用法。 为了更清楚地说明这一点,帮助你理解其中的模式,下面是另一个例子,我们再次从得到的folding函数开始,考虑append函数,它将第一个参数附加到第二个参数上:
现在,* F-余代数 * 是对(T, g),其中T是类型,g是g :: T -> F T类型的函数。例如,(IntStream, head&tail)是F1-余代数。同样,正如在F-代数中,g和T可以是任意的,例如,(String, h :: String -> Int x String)也是某个h的F1-余代数。 在所有的F-余代数中,存在所谓的 * terminal F-余代数 *,它是初始F-代数的对偶,例如IntStream是一个terminal F-余代数,这意味着对于每个类型T和每个函数p :: T -> F1 T,存在一个函数,称为 * anamorphism *,它将T转换为IntStream,并且这个函数是唯一的。 考虑下面的函数,它生成从给定整数开始的连续整数流:
nats :: Int -> IntStream
nats n = Cons (n, nats (n+1))
现在让我们来检查一个函数natsBuilder :: Int -> F1 Int,即natsBuilder :: Int -> Int × Int:
natsBuilder :: Int -> Int × Int
natsBuilder n = (n, n+1)
通过阅读教程论文 * A tutorial on (co)algebras and (co)induction *,您将对计算机科学中的余代数有一些了解。 下面是它的一个引用来说服你, 一般来说,某种程序设计语言的程序操纵数据。在过去几十年计算机科学的发展过程中,很明显,这些数据的抽象描述是可取的,例如,为了确保程序不依赖于它所操作的数据的特定表示。而且,这种抽象性便于正确性证明。 这种愿望导致了代数方法在计算机科学中的应用,在一个分支称为代数规格说明或抽象数据类型理论。研究的对象是数据类型本身,使用的技术概念是从代数中熟悉的。计算机科学家使用的数据类型通常是从给定的数据类型集合中产生的。(构造函数)运算,也正是因为这个原因,代数的"初始性"才起到如此重要的作用。 标准的代数技术已被证明在捕捉计算机科学中使用的数据结构的各种基本方面是有用的。但结果证明难以用代数描述计算中出现的一些固有的动态结构。这样的结构通常涉及状态的概念,状态可以用各种方式转换。对这样的基于状态的动态系统的形式化方法通常使用自动机或转换系统。作为经典的早期参考文献。 在过去的十年里,人们逐渐认识到,这种基于状态的系统不应该被描述为代数,而应该被描述为所谓的余代数。这是代数的形式对偶,在本教程中将以一种精确的方式进行描述。代数的"初始性"的对偶性质,即终局性对这类余代数是至关重要的,而这类终局余代数所需要的逻辑推理原则不是归纳法,而是余-感应。
4条答案
按热度按时间tp5buhyn1#
代数
我认为首先应该理解代数的概念。这只是群、环、么半群等代数结构的一般化。大多数时候,这些东西都是以集合的形式介绍的,但既然我们是朋友,我就转而谈谈Haskell类型。(不过我忍不住要用一些希腊字母--它们让一切看起来更酷!)
因此,一个代数就是
τ
类型的代数,它包含一些函数和恒等式,这些函数接受不同数目的τ
类型的参数,并产生一个τ
:如果不加修饰,它们看起来都像(τ, τ,…, τ) → τ
,它们还可以具有“标识”-τ
的元素,这些元素对某些函数具有特殊的行为。最简单的例子是幺半群,幺半群是具有函数
mappend ∷ (τ, τ) → τ
和恒等式mzero ∷ τ
的任何类型τ
,其他例子包括群(除了多了一个invert ∷ τ → τ
函数之外,它们就像幺半群)、环、格等等。所有的函数都在
τ
上运行,但是可以有不同的arity,我们可以把它们写成τⁿ → τ
,这里τⁿ
Map到一个元组n
τ
,这样,将恒等式看作τ⁰ → τ
是有意义的,其中τ⁰
只是空元组()
。现在我们可以简化代数的概念了:它只是一种类型,上面有一些函数。代数只是数学中被“分解”出来的一种常见模式,就像我们处理代码一样。人们注意到一大堆有趣的东西--前面提到的幺半群、群、格等等--都遵循类似的模式,所以他们把它抽象出来。这样做的好处和编程中的一样:它创建可重用的证明,并使某些类型的推理更容易。
F-代数
然而,我们还没有完全完成因式分解,到目前为止,我们有一堆函数
τⁿ → τ
,我们实际上可以做一个巧妙的技巧把它们组合成一个函数,特别是让我们看看幺半群:我们有mappend ∷ (τ, τ) → τ
和mempty ∷ () → τ
,我们可以使用求和类型Either
将它们转换成一个函数,如下所示:实际上,我们可以重复使用这个变换,将 * 所有 *
τⁿ → τ
函数组合成一个单一的函数,用于 * 任意 * 代数(事实上,我们可以对 * 任意 *a, b,…
的任意数量的函数a → τ
、b → τ
等等这样做)。这让我们把代数当作一个类型
τ
,它有一个从Either
到单个τ
的 single 函数。对于幺半群,这个mess是:Either (τ, τ) ()
;对于组(具有额外的τ → τ
操作),它是:Either (Either (τ, τ) τ) ()
。每个不同的结构都有不同的类型。那么所有这些类型有什么共同点呢?最明显的是它们都是乘积和-代数数据类型。例如,对于幺半群,我们可以创建一个适用于 any monoid τ的幺半群参数类型:我们可以对群、环、格和所有其他可能的结构做同样的事情。
所有这些类型还有什么特别之处?它们都是
Functors
!因此,我们可以进一步推广代数的概念,它只是一个类型
τ
,其中的函数f τ → τ
对应于某个函子f
,实际上,我们可以把它写成一个类型类:这通常被称为“F代数”,因为它是由函子
F
决定的。如果我们可以部分地应用类型类,我们可以定义类似class Monoid = Algebra MonoidArgument
的东西。余代数
现在,希望你已经很好地理解了代数是什么,以及它如何只是正规代数结构的推广。那么什么是F-余代数呢?好吧,co意味着它是代数的“对偶”-也就是说,我们取一个代数,然后翻转一些箭头。在上面的定义中,我只看到一个箭头,所以我只翻转它:
就是这样!现在,这个结论可能看起来有点轻率(呵呵)。它告诉你余代数是什么,但并没有真正给予任何关于它如何有用或为什么我们关心它的见解。一旦我找到或想出一两个好例子,我会很快谈到这一点:P。
类和对象
在阅读了一些内容之后,我想我对如何使用余代数来表示类和对象有了一个很好的想法:我们有一个类型
C
,它包含了类中对象的所有可能的内部状态;类本身是X1 M38 N1 X上的余代数,其指定对象的方法和属性。如代数例子所示,如果我们有一堆函数,如
a → τ
和b → τ
,对于任何a, b,…
,我们可以使用求和类型Either
将它们组合成一个函数,对偶“概念”是组合一堆τ → a
类型的函数,τ → b
等等。我们可以使用sum类型的对偶类型--product类型来实现这一点。因此,给定上面的两个函数(称为f
和g
),我们可以创建一个如下所示的函数:(a, a)
类型是一个函子,所以它当然符合F-余代数的概念,这个特殊的技巧让我们可以把一堆不同的函数--或者,对于OOP来说,方法--打包成一个τ → f τ
类型的函数。C
类型的元素表示对象的 internal 状态。如果对象有一些可读属性,它们必须能够依赖于状态。最明显的方法是使它们成为C
的函数。因此,如果我们想要一个length属性(例如object.length
),我们将有一个函数C → Int
。我们希望方法能够接受参数并修改状态。为此,我们需要接受所有参数并生成一个新的
C
。让我们想象一个setPosition
方法,它接受x
和y
坐标:object.setPosition(1, 2)
。它看起来像这样:C → ((Int, Int) → C)
.这里的重要模式是对象的“方法”和“属性”将对象本身作为它们的第一个参数,这就像Python中的
self
参数,也像许多其他语言中的隐式this
,余代数本质上只是封装了接受self
参数的行为:这就是C → F C
中的第一个C
。让我们把所有的东西放在一起,想象一个类有一个
position
属性,一个name
属性和setPosition
函数:我们需要两个部分来表示这个类。首先,我们需要表示对象的内部状态;在本例中,它只包含两个
Int
和一个String
(这是我们的类型C
)。然后,我们需要给出表示该类的余代数。我们有两个属性要写,它们很简单:
现在,我们只需要能够更新位置:
这就像一个Python类有显式的
self
变量,现在我们有了一堆self →
函数,我们需要把它们组合成一个余代数函数,我们可以用一个简单的元组来完成:类型
((Int, Int), String, (Int, Int) → c)
-for anyc
-是一个函子,所以coop
确实具有我们想要的形式:Functor f ⇒ C → f C
.这样,
C
沿着coop
形成了一个余代数,它指定了我上面给出的类,你可以看到我们如何使用同样的技术来指定对象的任意数量的方法和属性。这使得我们可以使用余代数推理来处理类。例如,我们可以引入“F-余代数同态”的概念来表示类之间的变换。这是一个听起来很可怕的术语,它只是意味着保持结构的余代数之间的变换。这使得考虑将类Map到其他类变得容易得多。
简而言之,F-余代数通过拥有一堆属性和方法来表示类,这些属性和方法都依赖于包含每个对象内部状态的
self
参数。其他类别
到目前为止,我们已经讨论了Haskell类型的代数和余代数,一个代数就是
τ
型,其中有一个函数f τ → τ
,余代数就是τ
型,其中有一个函数τ → f τ
。然而,这些概念与Haskell * 本身 * 并没有什么真正的联系。事实上,它们通常是以集合和数学函数的形式引入的,而不是类型和Haskell函数。实际上,我们可以将这些概念推广到 * 任何 * 范畴!
我们可以为某个范畴
C
定义一个F-代数,首先,我们需要一个函子F : C → C
,也就是一个 endofunctor。(所有 haskellFunctor
实际上都是Hask → Hask
的内函子。)那么,一个代数就是从C
得到的具有态射F A → A
的对象A
。余代数除了A → F A
之外是相同的。我们考虑其他范畴会得到什么呢?我们可以在不同的上下文中使用相同的概念,比如单子,在Haskell中,单子是
M ∷ ★ → ★
类型,有三个运算:map
函数只是证明了M
是Functor
,所以我们可以说一个单子只是一个有 * 两个 * 运算的函子:x1米95英寸和x1米96英寸。函子本身形成了一个范畴,它们之间的态射被称为“自然变换”。自然变换就是将一个函子变换为另一个函子,同时保持其结构的一种方式。Here's是一篇很好的文章,有助于解释这个想法。它讨论了
concat
,这就是列表的join
。在Haskell函子中,两个函子的复合就是一个函子本身。在伪代码中,我们可以这样写:
这有助于我们把
join
看作是f ∘ f → f
的Map,join
的类型是∀α. f (f α) → f α
,直观地,我们可以看到一个对 * 所有 * 类型α
有效的函数可以被看作是f
的变换。return
是一个类似的变换。它的类型是∀α. α → f α
。这看起来不同-第一个α
不是“in”函子!幸运的是,我们可以通过在那里添加一个恒等函子来修复这个问题:所以return
是个变换。现在我们可以把一个单子看作是一个代数,它基于某个函子
f
和f ∘ f → f
以及Identity → f
,这看起来是不是很熟悉,它非常类似于一个单子,它只是一个类型τ
和τ × τ → τ
以及() → τ
。因此,单子就像幺半群,只是我们有函子而不是类型,它们是同一种代数,只是在不同的范畴中(据我所知,“单子就是内函子范畴中的幺半群”这句话就是从这里来的)。
现在,我们有两个操作:
f ∘ f → f
和Identity → f
。要得到对应的余代数,我们只需翻转箭头。这给了我们两个新的操作:f → f ∘ f
和f → Identity
。我们可以通过添加如上所述的类型变量将它们转换为Haskell类型,得到∀α. f α → f (f α)
和∀α. f α → α
。这看起来就像comonad的定义:所以一个余单子是一个内函子范畴中的 * 余代数 *。
g52tjvyc2#
F-代数和F-余代数是数学结构,它们在关于 * 归纳类型 *(或 * 递归类型 *)的推理中是有用的。
F-代数
我们先从F-代数开始,我会尽可能简单。
我猜你知道什么是递归类型。例如,这是一个整数列表的类型:
很明显它是递归的--事实上,它的定义是指它自己。它的定义由两个数据构造函数组成,它们有以下类型:
注意,我把
Nil
的类型写成() -> IntList
,而不是简单地写成IntList
,从理论的观点来看,它们实际上是等价的类型,因为()
类型只有一个居民。如果我们用集合论的方法写出这些函数的特征,我们将得到
其中
1
是单位集(具有一个元素的集),并且A × B
运算是两个集A
和B
的叉积(即,对(a, b)
的集,其中a
经过A
的所有元素,并且b
经过B
的所有元素)。两个集合
A
和B
的不相交并集是集合A | B
,它是集合{(a, 1) : a in A}
和{(b, 2) : b in B}
的并集。本质上,它是来自A
和B
的所有元素的集合,但是该元素中的每一个被“标记”为属于A
或B
,因此当我们从A | B
中选取任何元素时,我们将立即知道该元素是来自A
还是来自B
。我们可以'join'
Nil
和Cons
函数,这样它们就形成了一个作用于集合1 | (Int × IntList)
的函数:实际上,如果将
Nil|Cons
函数应用于()
值(显然,其属于1 | (Int × IntList)
集合),则其表现得好像它是Nil
;如果将Nil|Cons
应用于(Int, IntList)
类型的任何值(这样的值也在集合1 | (Int × IntList)
中),则其行为与Cons
相同。现在考虑另一种数据类型:
它具有以下构造函数:
它们也可以合并成一个函数:
可以看出,这两个
joined
函数具有相似的类型:他们看起来都像其中
F
是一种转换,它接受我们的类型并给出更复杂的类型,该类型由x
和|
操作、T
的用法以及可能的其他类型组成。例如,对于IntList
和IntTree
,F
如下所示:我们可以立即注意到,任何代数类型可以写在这种方式。的确,这就是为什么他们被称为'代数':它们由许多其它类型的“和”(并集)和“积”(叉积)组成。
现在我们可以定义F-代数。* F-代数 * 只是一对
(T, f)
,其中T
是某种类型,f
是f :: F T -> T
类型的函数。在我们的例子中,F-代数是(IntList, Nil|Cons)
和(IntTree, Leaf|Branch)
。然而,注意,尽管f
函数的类型对于每个F都是相同的,T
和f
本身可以是任意的,例如,对于某些g
和h
,(String, g :: 1 | (Int x String) -> String)
或(Double, h :: Int | (Double, Double) -> Double)
也是相应F的F-代数。然后我们可以引入 * F-代数同态 * 和 * 初始F-代数 *,它们具有非常有用的性质。事实上,
(IntList, Nil|Cons)
是初始F1-代数,(IntTree, Leaf|Branch)
是初始F2-代数。由于这些术语和性质比需要的更复杂和抽象,因此我将不给出它们的精确定义。尽管如此,假设
(IntList, Nil|Cons)
是F-代数,这一事实允许我们在这种类型上定义fold
-like函数,正如你所知道的,fold是一种操作,它将一些递归数据类型转换为一个有限值,例如,我们可以将一个整数列表折叠为一个值,该值是列表中所有元素的总和:可以在任何递归数据类型上推广这种操作。
以下是
foldr
函数的签名:注意,我用大括号将前两个参数和最后一个参数分开,这不是真实的的
foldr
函数,但它与它同构(也就是说,你可以很容易地从一个得到另一个,反之亦然),部分应用的foldr
将具有以下签名:我们可以看到这是一个接受一系列整数并返回一个整数的函数,让我们用
IntList
类型来定义这个函数。我们看到这个函数由两部分组成:第一部分定义此函数在
IntList
的Nil
部分上的行为,第二部分定义此函数在Cons
部分上的行为。现在假设我们不是用Haskell编程,而是用某种允许在类型签名中直接使用代数类型的语言(从技术上讲,Haskell允许通过元组和
Either a b
数据类型使用代数类型,但这会导致不必要的冗长)。可以看出,
reductor
是F1 Int -> Int
型函数,正如F-代数的定义一样!的确,对(Int, reductor)
是F1-代数。因为
IntList
是初始F1-代数,所以对于每个类型T
和每个函数r :: F1 T -> T
,存在一个函数,称为 * catamorphism * forr
,它将IntList
转换为T
,并且这样的函数是唯一的。在我们的例子中,reductor
的退化是sumFold
。注意reductor
和sumFold
是如何相似的:它们具有几乎相同的结构!在reductor
定义s
中,参数用法(其类型对应于T
)对应于sumFold
定义中sumFold xs
的计算结果的用法。为了更清楚地说明这一点,帮助你理解其中的模式,下面是另一个例子,我们再次从得到的folding函数开始,考虑
append
函数,它将第一个参数附加到第二个参数上:这是它在我们的
IntList
上的外观:同样,让我们试着写出归约式:
appendFold
是appendReductor
的一个变质作用,它将IntList
转变为IntList
。因此,本质上,F-代数允许我们定义递归数据结构上的"折叠",即把我们的结构简化为某个值的操作。
F-余代数
F-余代数是F-代数中所谓的"对偶"项,它允许我们定义递归数据类型的
unfolds
,即从某个值构造递归结构的一种方法。假设您具有以下类型:
这是一个无限的整数流。它唯一的构造函数具有以下类型:
或者说,用集合来表示
Haskell允许您对数据构造函数进行模式匹配,因此您可以定义以下在
IntStream
上工作的函数:您可以很自然地将这些函数"连接"成
IntStream -> Int × IntStream
类型的单个函数:请注意函数的结果如何与
IntStream
类型的代数表示一致。类似的事情也可以对其他递归数据类型进行。也许您已经注意到了这种模式。我指的是类型为其中
T
是某个类型。从现在开始,我们将定义现在,* F-余代数 * 是对
(T, g)
,其中T
是类型,g
是g :: T -> F T
类型的函数。例如,(IntStream, head&tail)
是F1-余代数。同样,正如在F-代数中,g
和T
可以是任意的,例如,(String, h :: String -> Int x String)
也是某个h的F1-余代数。在所有的F-余代数中,存在所谓的 * terminal F-余代数 *,它是初始F-代数的对偶,例如
IntStream
是一个terminal F-余代数,这意味着对于每个类型T
和每个函数p :: T -> F1 T
,存在一个函数,称为 * anamorphism *,它将T
转换为IntStream
,并且这个函数是唯一的。考虑下面的函数,它生成从给定整数开始的连续整数流:
现在让我们来检查一个函数
natsBuilder :: Int -> F1 Int
,即natsBuilder :: Int -> Int × Int
:同样,我们可以看到
nats
和natsBuilder
之间的一些相似之处。这与我们之前观察到的缩减体和褶皱之间的联系非常相似。nats
是natsBuilder
的一种变质作用。另一个例子是,一个函数接受一个值和一个函数,并返回一个函数对该值的连续应用流:
其生成器功能如下:
那么
iterate
是iterateBuilder
的一个变体。结论
因此,简而言之,F-代数允许定义folds,即把递归结构简化为单个值的运算,而F-余代数允许做相反的事情:从一个值构造一个[潜在的]无限结构。
事实上,在Haskell中F-代数和F-余代数是一致的。这是一个非常好的性质,它是每种类型中存在"底"值的结果。因此,在Haskell中,折叠和展开都可以为每种递归类型创建。然而,这背后的理论模型比我上面介绍的更复杂,所以我故意避免了它。
rnmwe5a23#
通过阅读教程论文 * A tutorial on (co)algebras and (co)induction *,您将对计算机科学中的余代数有一些了解。
下面是它的一个引用来说服你,
一般来说,某种程序设计语言的程序操纵数据。在过去几十年计算机科学的发展过程中,很明显,这些数据的抽象描述是可取的,例如,为了确保程序不依赖于它所操作的数据的特定表示。而且,这种抽象性便于正确性证明。
这种愿望导致了代数方法在计算机科学中的应用,在一个分支称为代数规格说明或抽象数据类型理论。研究的对象是数据类型本身,使用的技术概念是从代数中熟悉的。计算机科学家使用的数据类型通常是从给定的数据类型集合中产生的。(构造函数)运算,也正是因为这个原因,代数的"初始性"才起到如此重要的作用。
标准的代数技术已被证明在捕捉计算机科学中使用的数据结构的各种基本方面是有用的。但结果证明难以用代数描述计算中出现的一些固有的动态结构。这样的结构通常涉及状态的概念,状态可以用各种方式转换。对这样的基于状态的动态系统的形式化方法通常使用自动机或转换系统。作为经典的早期参考文献。
在过去的十年里,人们逐渐认识到,这种基于状态的系统不应该被描述为代数,而应该被描述为所谓的余代数。这是代数的形式对偶,在本教程中将以一种精确的方式进行描述。代数的"初始性"的对偶性质,即终局性对这类余代数是至关重要的,而这类终局余代数所需要的逻辑推理原则不是归纳法,而是余-感应。
那么在这个阶段,我想说,
在程序的生命周期中,数据和状态共存,相互补充,具有对偶性。
b4wnujal4#
我将从一些明显与编程相关的东西开始,然后添加一些数学的东西,以使它尽可能具体和脚踏实地。
让我们引用一些计算机科学家关于共归纳的观点......
http://www.cs.umd.edu/~micinski/posts/2012-09-04-on-understanding-coinduction.html
归纳是关于有限数据的,共归纳是关于无限数据的。
无限数据的典型例子是惰性列表类型(流),例如,假设内存中有以下对象:
计算机不能存储π的全部,因为它只有有限的内存!但它能做的是存储一个有限的程序,这个程序可以产生你想要的π的任意长的展开式。只要你只使用列表的有限部分,你就可以用这个无限列表计算你所需要的任何东西。
但是,请考虑以下程序:
这个程序应该打印出pi的第三位数字,但是在某些语言中,函数的任何参数在传入函数之前都要求值(严格的,不是懒惰的,求值)如果我们使用这个归约顺序,那么我们上面的程序将永远运行,计算圆周率的数字,然后才能传递给我们的打印机函数(这永远不会发生)。由于机器没有无限的内存,程序最终会耗尽内存并崩溃。这可能不是最佳的求值顺序。
http://adam.chlipala.net/cpdt/html/Coinductive.html
在像Haskell这样的惰性函数式编程语言中,无限数据结构无处不在。无限列表和更奇特的数据类型为程序各部分之间的通信提供了方便的抽象。在许多情况下,要想在没有无限惰性结构的情况下实现类似的方便,需要对控制流进行技巧性的反转。
http://www.alexandrasilva.org/#/talks.html
将环境数学上下文与常规编程任务关联起来
什么是"代数"?
代数结构一般看起来像:
1.东西
1.这些东西能做什么
这听起来应该像是有1个属性和2个方法的对象。或者更好的是,它应该听起来像类型签名。
标准的数学例子包括幺半群group vector-space an algebra。幺半群就像自动机:动词序列(如
f.g.h.h.nothing.f.g.f
)。一个总是添加历史而从不删除历史的git
日志是一个幺半群,但不是一个群。如果你添加逆元(如负数、分数、根、删除累积的历史、恢复破碎的镜子),你会得到一个群。组包含可以加在一起或减在一起的东西。例如
Duration
s可以加在一起。(但Date
s不能。)持续时间存在于向量空间(不仅仅是组)中,因为它们也可以由外部数字缩放。(scaling :: (Number,Duration) → Duration
的类型签名)代数向量空间还可以做另一件事:有一些
m :: (T,T) → T
,称之为"乘法"或不称之为"乘法",因为一旦离开Integers
,"乘法"(或"exponentiation")应该是什么就不那么明显了。(This这就是为什么人们关注(范畴理论的)普遍属性:告诉他们乘法应该做什么或应该是什么样子:
)
代数→余代数
复杂乘法比乘法更容易定义,因为从
T → (T,T)
开始,你可以重复相同的元素("对角Map"--类似于谱理论中的对角矩阵/算子)。计数通常是迹(对角线上的项的和),尽管重要的是你的计数做了什么;
trace
正好是矩阵的一个很好的答案。一般来说,之所以要研究dual space,是因为在那个空间中更容易思考,例如,有时候考虑法向量比考虑它所垂直的平面更容易,但是你可以用向量来控制平面(包括超平面)(现在我说的是熟悉的几何向量,就像在光线追踪器中一样)。
驯服(非)结构化数据
数学家们可能正在为TQFT's这样有趣的东西建模,而程序员们却不得不为
+ :: (Date,Duration) → Date
),Paris
≠(+48.8567,+2.3508)
!这是一个形状,不是一个点),计算机科学家在谈到余代数时,通常会想到set-ish运算,比如笛卡尔积。我相信这就是人们说"代数是Haskell中的余代数"时的意思。但就程序员必须对
Place
,Date/Time
等复杂数据类型建模而言,和Customer
-并使这些模型看起来尽可能像真实世界(或者至少是最终用户对真实世界的看法)-我相信duals的用处可能不仅仅限于set-world。