dfe*_*uer 7 haskell types calculus
pigworker曾经问过如何表达一种类型是无限可分的.这个问题让人联想到这样一个事实:在复杂的分析中,一个可微分的函数(在开集上)必须是无限可微的(在那个集合上).有没有办法谈论数据类型的复杂差异？如果是这样,类似的定理是否成立？
不是一个真正的答案......但是这个咆哮对于评论来说太长了.
我觉得复杂的差异性只意味着无限的差异性,这有点误导.事实上它比这更强大:如果一个函数是复杂可微的,那么它的导数在任何点都决定了整个函数.由于无限可微性为您提供完整的泰勒级数,因此您具有与您的函数相等的分析函数,即您的函数本身.因此,从某种意义上说,复杂的可微分函数是分析性的...因为它们是.
从(标准)微积分的角度来看,实际可扩展性与复杂可扩展性之间的关键对比是,在实际中,只有一个方向可以取得差异商的极限(f(x + δ) -fx)/ δ.您只需要左边界限等于右边界限.但是因为这是在限制之后的平等,所以这只在本地产生影响.(从拓扑学的角度来说,约束只是比较两个离散值,因此它根本不会真正处理连续性属性.)
OTOH,对于复杂的可微性,如果我们从任何方向接近x,我们要求差商的极限是相同的在整个复杂的平面上.这是一个完全连续的自由度受限制.然后,您可以继续执行拓扑技巧(Cauchy积分本质上是这样)以在整个域中"扩展"约束.
我认为这在哲学上有点问题.全纯函数根本不是真正的函数,例如:它们不是通过整个域中的整个结果值定义的,而是通过某种方式用分析公式来编写它们(即可能无限的代数表达式/多项式) ).
大多数数学家和物理学家显然都喜欢这样 - 这种表达只是他们通常编写功能的方式.
我真的不喜欢它:对我来说,一个函数应该是一个函数,一个由各个值定义的东西,比如你可以在空间中测量的场强或你可以在Haskell中定义的结果.
无论如何,我离题了......
如果我们将这个问题从数字上的函数转换为Haskell类型的仿函数,我认为结果是复杂的diff_ability只是意味着:一个类型可以写成(可能是无限的？)ADT多项式.在你链接的帖子中显示了如何为这些ADT获得无限的可区分性.
Haskell类型的这些"衍生物"在微积分意义上并不是真正的衍生物.如同,它们不受小扰动反应分析概念的启发†.碰巧你可以在数学上证明,对于一个非常特殊的函数类 - 由代数表达式定义的函数 - 微积分导数可以再次用简单的代数方式编写(由众所周知的微分规则给出).这意味着你可以经常无限地区分.
这种象征性差异化的有用性也促使人们将其视为一种更抽象的运作.当你区分Haskell类型时,它主要只是你要追求的代数定义,而不是原始的微积分定义.
这很好......但是一旦你做代数而不是微积分,区分"真实"和"复杂"并不是很有意义 - 它实际上也不是,因为你不是处理价值而是象征性的价值表征.一种无类型的语言,如果你愿意的话(事实上,Haskell的类型语言仍然是无类型的,一切都很好*).
† 无论是传统的收敛极限还是NSA -infinitesimals.