logo标签列表

编程语言背后是否有任何数学模型或理论？

oopmathprogramming-languagesmodelalgebra
21
RDBMS是基于关系代数和Codd模型的。编程语言或OOP中是否有类似的东西呢？
回答太简略了，但类型理论和范畴论肯定适用。 - Erik Kaplun
11个回答
阿里云服务器只需要99元/年，新老用户同享，点击查看详情
41

编程语言是否有[基础模型]？

当然有。由于存在众多编程语言，因此可以选择多种模型。首先最重要的是：

  • Church's untyped lambda calculus is a model of computation that is as powerful as a Turing machine (no more and no less). The famous "Church-Turing hypothesis" is that these two equivalent models represent the most general model of computation that we know how to implement. The lambda calculus is extremely simple; in its entirety the language is

    e ::= x | e1 e2 | \x.e

    which constitute variables, function applications, and function definitions. The lambda calculus also comes with a fairly large collection of "reduction rules" for simplifying expressions. If you find an expression that can't be reduced, that is called a "normal form" and represents a value.

    The lambda calculus is so general that you can take it in several directions.

    • If you want to use all the available rules, you can write specialized tools like partial evaluators and parts of compilers.

    • If you avoid reducing any subexpression under a lambda, but otherwise use all the rules available, you wind up with a model of a lazy functional language like Haskell or Clean. In this model, if a reduction can terminate, it is guaranteed to, and it is easy to represent infinite data structures. Very powerful.

    • If you avoid reducing any subexpression under a lambda, and if you also insist on reducing each argument to a normal form before a function is applied, then you have a model of an eager functional language like F#, Lisp, Objective Caml, Scheme, or Standard ML.

  • There are also several flavors of typed lambda calculi, of which the most famous are grouped under the name System F, which were discovered independently by Girard (in logic) and by Reynolds (in computer science). System F is an excellent model for languages like CLU, Haskell, and ML, which are polymorphic but have compile-time type checking. Hindley (in logic) and Milner (in computer science) discovered a restricted form of System F (now called the Hindley-Milner type system) which makes it possible to infer System F expressions from some expressions of the untyped lambda calculus. Damas and Milner developed an algorithm do this inference, which is used in Standard ML and has been generalized in other languages.

  • Lambda calculus is just pushing symbols around. Dana Scott's pioneering work in denotational semantics showed that expressions in the lambda calculus actually correspond to mathematical functions—and he identified which ones. Scott's work is especially important in making sense of "recursive definitions", which are commonplace in computer science but are nonsensical from a mathematical point of view. Scott and Christopher Strachey showed that a recursive definition is equivalent to the least defined solution to a recursion equation, and furthermore showed how that solution could be constructed. Any language that allows recursion, and especially languages that allow recursion at arbitrary type (like Haskell and Clean) owes something to Scott's model.

  • There is a whole family of models based on abstract machines. Here there is not so much an individual model as a technique. You can define a language by using a state machine and defining transitions on the machine. This definition encompasses everything from Turing machines to Von Neumann machines to term-rewriting systems, but generally the abstract machine is designed to be "as close to the language as possible." The design of such machines, and the business of proving theorems about them, comes under the heading of operational semantics.

关于面向对象编程，你有什么看法？

我对用于OOP的抽象模型不够了解。我最熟悉的模型与实现策略密切相关。如果我想进一步研究这个领域，我会从William Cook的Smalltalk指称语义开始。（Smalltalk作为一种语言非常简单，几乎与λ演算一样简单，因此它是建模更复杂的面向对象语言的好案例研究。）

Wei Hu提醒我，Martin Abadi和Luca Cardelli已经为面向对象语言制定了一个雄心勃勃的基础演算（类似于λ演算）。我不理解这项工作的内容，但这里有一段他们书中的序言值得引用：

过程式语言通常都很容易理解；它们的构造已经成为标准，它们的形式基础也很坚实。这些语言的基本特性已被提炼成形式化方法，可用于识别和解释实现、静态分析、语义和验证问题。

相比之下，关于面向对象语言的理解还没有达成广泛共识。人们对基本结构及其属性没有普遍的认识……如果我们对面向对象语言的基础有更好的理解，这种情况可能会改善。

……我们将对象作为原始元素，并集中研究对象应遵守的内在规则。我们引入对象演算并围绕它们发展对象理论。这些对象演算与函数演算一样简单，但直接表示对象。

我希望这个引用能让你了解到这项工作的风格。

@Norman - 非常感谢您详尽而丰富的回答。 - Padmarag
非常全面的回答。虽然如果您也提到公理语义会更好。我还没有阅读过两位著名微软研究员的书籍《对象的理论》（http://lucacardelli.name/TheoryOfObjects.html），但我的直觉是这本书应该涵盖面向对象编程背后的理论。 - Wei Hu
++ 很好的答案，Norman，特别是Lambda演算部分。我知道Scott-Strachey的工作，但它超出了我的理解范围。当我在AI实验室时，像Carl Hewitt这样的人试图将其扩展到涵盖副作用（Actor理论-与Smalltalk＆OOP相结合），但我不确定最终结果走得很远。 - Mike Dunlavey
+1：一如既往的出色回答 :) - Juliet
@Profjim：是的。在我看来，决定何时何地可以执行β还原的各种“结构规则”是将高度不确定的基础演算法与通常的确定性编程语言区分开来的关键。 - Norman Ramsey
显示剩余3条评论
10

Lisp基于λ演算，是现代语言中很多特性的灵感来源。

Von-Neumann机是现代计算机的基础，最初使用汇编语言进行编程，然后使用FORmula TRANslator语言。接着应用了上下文无关文法的形式语言理论，并构成了所有现代语言的句法基础。

可计算性理论（形式自动机）有一系列与形式文法相似的机器类型，例如正则文法 = 有限状态机，上下文无关文法 = 下推自动机，上下文相关文法 = 图灵机。

此外还有信息论，分为Shannon和Kolmogorov两种类型，可以应用于计算。

还有一些不太知名的计算模型，例如递归函数论、寄存器机和Post机。

别忘了各种形式的谓词逻辑。

添加：我忘记提到离散数学——群论和格论。格论特别是一个非常巧妙的概念，是所有布尔逻辑以及某些计算模型（如指称语义）的基础。

1
然后，上下文无关文法的正式语言理论被应用，并构成了所有现代语言的语法基础——有点像说西方古典音乐理论是披头士乐队作品的基础一样。 :) 它可以用来分析结果，但这并不意味着创作者有意识地应用了它。也许令人惊讶的是，许多现代语言最初都是使用“手写”的自顶向下解析器实现的，BNF表示方法稍后才出现，而且很少单独使用。C++以难以通过学术解析理论而闻名。 - Daniel Earwicker
@Daniel：你正在完善我的翻转句子。谢谢。 - Mike Dunlavey
6

函数式编程语言（如lisp）的基本概念继承自Church的“lambda演算”（维基百科文章在这里）。 祝好。

我不一定会称lisp为函数式语言。它可以用函数式的方式编写，但更多是一种多范式语言。 - Vatine
5
3
2

面向对象编程（OOP）没有数学模型。

关系代数是SQL的数学模型，由E.F. Codd创建。C.J. Date也是一位著名的科学家，他帮助制定了这个理论。整个想法是您可以将每个操作作为集合操作执行，同时影响许多值。当然，这意味着必须告诉数据库引擎要获取什么，并且数据库能够优化查询。

Codd和Date都批评了SQL，因为他们参与了该理论，但并未参与SQL的创建。

请参见此视频：http://player.oreilly.com/videos/9781491908853?toc_id=182164

Chris Date提供了大量信息。我记得Date批评SQL编程语言是一种糟糕的语言，但我找不到这篇论文。

批评基本上是大多数语言允许编写表达式并将变量分配给这些表达式，但SQL不允许。

由于SQL是一种逻辑语言，我猜你可以在Prolog中编写关系代数。至少这样你就有了一个真正的语言。因此，你可以在Prolog中编写查询。由于在Prolog中有很多程序可以解释自然语言，因此你可以使用自然语言查询你的数据库。 根据Bob大叔的说法，当每个人都拥有SSD时，数据库将不再需要，因为SSD的架构意味着访问速度像RAM一样快。因此，你可以将所有对象保存在RAM中。

https://www.youtube.com/watch?feature=player_detailpage&v=t86v3N4OshQ#t=3287

放弃使用SQL的唯一问题是你最终会没有数据库查询语言。因此，可以说SQL是受关系代数启发而来，但它并不是关系代数的实现。而对于Lisp，情况则不同。主要思想是在Lisp中实现eval函数，就可以实现整个语言。这就是为什么第一个Lisp实现只有半页代码的原因。

http://www.michaelnielsen.org/ddi/lisp-as-the-maxwells-equations-of-software/

笑一笑：https://www.youtube.com/watch?v=hzf3hTUKk8U 函数式编程的重要性在于柯里化函数和惰性调用。不要忘记环境和闭包，还有 map-reduce。这意味着我们将在 20 年内使用函数式语言进行编码。 现在回到面向对象编程，没有正式的面向对象编程规范。 有趣的是，第二个创建的面向对象语言 Smalltalk 只有对象，没有原语或类似的东西。创造者 Alan Kay 明确地创建了块，以完全像 Lisp 函数那样工作。 有些人声称可以使用范畴论来形式化面向对象编程，范畴论是一种带有态射的集合论。态射是在对象之间保持结构的映射。因此，通常您可以使用 map(f, collection) 并返回应用 f 的所有元素的集合。 我很确定 Lisp 有这个功能，但 Lisp 还具有返回集合中一个元素的函数，这会破坏结构，因此态射是一种特殊类型的函数，因此，您需要减少并限制 Lisp 中的函数，使它们都成为态射。

https://www.youtube.com/watch?feature=player_detailpage&v=o6L6XeNdd_k#t=250

这种方法的主要问题在于，OOP中的函数不存在于对象之外，但在范畴论中是存在的。因此它们是不兼容的。你可以开发一种新的语言来表达范畴论。 一个专门为尝试形式化OOP而创建的实验性理论语言是Z。Z源自需求形式化。 另一种尝试是Luca Cardelli的形式化方法：

Javahttp://lucacardelli.name/Papers/PrimObjImp.pdf Javahttp://lucacardelli.name/Papers/PrimObj1stOrder.A4.pdf Javahttp://lucacardelli.name/Papers/PrimObjSemLICS.A4.pdf

我无法阅读和理解那个符号。这似乎是一个无用的练习，因为据我所知，没有人像Lisp中实现lambda演算一样实现过它。
2

维基百科的面向对象编程的历史部分可能会很有启发性。

2

我能想到的最接近的类比是Gurevich Evolving Algebras，现在更为人所知的名称是“Gurevich Abstract State Machines”（GASM）。

我一直希望看到更多关于该理论实际应用的案例，当Gurevich加入微软后，但似乎很少有成果。你可以在微软网站上检查关于ASML的页面。

GASM的好处在于它们与伪代码非常相似，即使其语义已被正式指定。这意味着从业者可以轻松掌握。

毕竟，我认为关系代数的成功部分原因是它是易于理解概念的正式基础，即表格、外键、连接等。

我认为我们需要类似的东西来处理软件系统的动态组件。

2
回答如下：

回答您的问题有很多方面需要考虑，答案分散在不同的地方。

首先，为了描述一种语言的语法并指定解析器的工作方式，我们使用上下文无关文法。

然后您需要为语法赋予意义。形式语义非常有用；主要的参与者是操作语义、指称语义和公理语义。

为了排除错误程序，您需要类型系统。

最终，所有计算机程序都可以简化为（或编译为）非常简单的计算模型。命令式程序更容易映射到图灵机，而函数式程序则映射到λ演算。

如果您正在自学所有这些东西，我强烈推荐http://www.uni-koblenz.de/~laemmel/paradigms0910/，因为讲座被录像并放在网上。

2

已经有很多关于将数学应用于计算理论和语义学的讨论。我喜欢提到类型理论，很高兴有人提到格理论。这里还有一些。

没有人明确提到范畴论，它在函数式语言中比其他地方更常见，例如通过单子和函子的概念。然后还有模型理论以及实际出现在定理证明器或逻辑语言Prolog中的各种逻辑形式。数学应用还可以用于并发语言的基础和问题。

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，