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

40

建设我们有[底层模型]编程语言？

天堂，是的。而且因为有这么多编程语言，有多种型号可供选择。最重要的是第一：

教会无类型演算是计算的模型是一样强大的图灵机（不能多也不能少）。着名的“Church-Turing假说”是这两个等价模型代表了我们知道如何实现的最一般计算模型。 lambda演算非常简单;其整体的语言是
```
e ::= x | e1 e2 | \x.e 
```
构成变量，功能的应用，和函数定义。 lambda演算还带有相当大量的简化表达式的“简化规则”。如果您发现无法缩小的表达式，那么称为“标准形式”并表示一个值。

的演算是太笼统，你可以把它在几个方向。
- 如果你想使用所有可用的规则，你可以编写专门的工具，如部分评估器和部分编译器。
- 如果您避免减少lambda下的任何子表达式，但是要使用所有可用的规则，则可以使用懒惰函数语言（如Haskell或Clean）的模型。在这个模型中，如果减少可以终止，那么保证，并且很容易表示无限的数据结构。很强大。
- 如果你避免拉姆达在还原任何子表达式，如果你还坚持减少每个参数应用功能之前正常的形式，那么你有一个像F＃，Lisp语言的渴望函数式语言模型，Objective Caml，Scheme或Standard ML。
也有几种口味的类型拉姆达结石，其中最有名的是名系统F，这是由吉拉德（逻辑）独立发现下分组和雷诺兹（以计算机科学）。系统F是CLU，Haskell和ML等语言的优秀模型，它们是多态的，但是具有编译时类型检查。辛德雷（在逻辑）和米尔纳（在计算机科学）发现的，这使得它能够从无类型演算的一些表达式推断系统F表达式系统F（现在称为辛德米尔纳类型的系统）中的受限形式。 Damas和Milner开发了一种算法来进行这种推断，该算法在标准ML中使用，并已在其他语言中推广。
LAMBDA演算只是推动周围的符号。达纳·斯科特在指称语义开创性的工作表明，在lambda演算表达式实际上对应于数学函数—和他辨认哪些。斯科特的工作对理解“递归定义”特别重要，这种定义在计算机科学中很常见，但从数学的角度来看是无意义的。 Scott和克里斯托弗斯特雷奇表明递归定义等效于至少所定义的解决方案来递归方程，进而表明，溶液可如何构造。任何允许递归的语言，尤其是允许以任意类型递归的语言（如Haskell和Clean）都会给Scott的模型带来一些东西。
有一个基于抽象机的整个系列的模型。这里没有太多的个人模式作为技术。您可以使用状态机定义语言并在机器上定义转换。这个定义从图灵机到冯·诺依曼机涵盖一切的术语重写系统，但一般的抽象机的设计是“尽可能接近的语言越好。”这种机器的设计，并证明对他们定理的业务，涉及的操作语义标题下。

那么面向对象编程呢？

我受教育程度不如我应该是关于面向对象的抽象模型。我最熟悉的模型与实施策略密切相关。如果我想进一步研究这个领域，我会从William Cook的Smalltalk的指称语义开始。（Smalltalk作为一门语言非常简单，几乎和lambda微积分一样简单，所以它为建模更复杂的面向对象语言提供了一个很好的案例研究。）

Wei Hu让我想起Martin Abadi和Luca Cardelli把共同为基于面向对象语言的基础计算（类似于lambda演算）开展了雄心勃勃的工作。我不明白这项工作是否足以概括它，但这里有一段来自他们的书的序言，我觉得值得引用：

程序语言通常是很好理解;他们的构造现在是标准的，他们的正式基础是坚实的。这些语言的基本特征已经被提炼出来，在识别和解释实现问题，静态分析，语义和验证等方面被证明是有用的。

面向对象的语言还没有出现类似的理解。关于基本构造集合及其属性并没有广泛的共识......如果我们更好地理解面向对象语言的基础，这种情况可能会有所改善。

......我们把对象看作是原始的，并专注于对象应该服从的内在规则。我们引入物体结石，并围绕它们发展物体的理论。这些对象结石与功能结石一样简单，但直接表示对象。

我希望这个报价给你的工作的味道的想法。

来源

2010-03-18 22:10:10

+0

@Norman - 非常感谢您提供丰富而全面的答案。 – Padmarag 2010-03-19 05:01:45

+0

非常全面的答案。虽然如果你提到公理语义也会很好。我没有读过两位知名微软研究人员的“物体理论”一书（http://lucacardelli.name/TheoryOfObjects.html），但我的直觉是，本书应该涵盖OOP背后的理论。 – 2010-03-19 06:04:28

+0

++好的答案，诺曼，特别是Lambda微积分部分。我已经知道斯科特 - 斯特拉奇的工作，但这是我理解的边界。当我在人工智能实验室时，像卡尔·休伊特这样的人试图扩展它以涵盖副作用（演员理论 - 与Smalltalk和OOP结盟），但我不确定最终结果是否走得太远。 – 2010-03-19 11:43:17

5

一个概念可能是Turing Machine。

来源

2010-03-18 12:41:56 Padmarag

1

据我所知，Formal grammars用于描述语法。

来源

2010-03-18 12:45:08 iburlakov

+1

哈哈。如果我理解你的英语，这可能是最好的答案。耻辱我不能在正确的轨道上投2分半。 – 2010-03-18 13:01:09

+0

不完全正确。形式语法只是指定语法部分。一个软件的完整语义不能用语法指定。相反，可以使用关系代数来完全指定数据库的工作方式。 – 2010-03-18 13:04:38

+0

“正式语法用于描述语法”究竟是“不完全正确”？你自己说的完全一样。 – EJP 2010-03-19 06:20:14

2

编程语言是继理论的应用产品：

算法理论
计算的理论
状态自动机
和像口齿不清更

来源

2010-03-18 12:45:34 Andrey

6

函数式语言继承来自教会“lambda calculs”的基本概念（维基百科文章here ）。关注

来源

2010-03-18 12:47:17

+0

我不会，必然会调用lisp功能。它可以用功能性方式编写，但更多是一种多范式语言。 – Vatine 2010-03-18 13:07:27

3

维基百科的history section面向对象的编程可能是有启发性的。

来源

2010-03-18 12:48:48 OverLex

2

我能想到的最接近的比喻是古列维奇进化代数的是，如今，更“古列维奇抽象状态机”（GASM）的名字为人所知。

我一直希望看到的时候古列维奇加入微软理论更实际的应用，但似乎很少是走出来。您可以检查Microsoft网站上的ASML页面。

约GASM好的一点是，即使它们的语义正式规定，他们酷似的伪代码。这意味着从业者可以轻松掌握它们。

毕竟，我觉得关系代数的成功的部分是，它是可以很容易地掌握概念，即表，外键的正式奠基，加入等

我认为我们需要对于软件系统的动态组件来说类似。

来源

2010-03-18 12:56:29

9

Lisp基于Lambda微积分，是我们今天在现代语言中看到的大部分灵感。

冯·诺依曼机是现代计算机的基础，这是首次在汇编语言编程，然后在公式翻译。然后，应用了上下文无关语法的形式语言学理论，并构成了所有现代语言的语法基础。

可计算性理论（形式自动机）具有与正式语法层次平行的机器类型层次结构，例如，规则语法=有限状态机，上下文无关语法=下推自动机，敏感语法=图灵机。

也有信息论两种类型，香农和Kolmogorov，可被施加到计算的。

有计算的鲜为人知的模型，如递归函数理论，寄存器机，和Post-机器。

而且不要忘了各种形式的谓词逻辑。

补充：我忘了提离散数学 - 群理论和晶格理论。特别是格（IMHO）是所有布尔逻辑下的一个特别漂亮的概念，以及一些计算模型，如指称语义。

来源

2010-03-18 12:59:25

+1

*然后，上下文无关语法的形式语言学理论被应用，并成为所有现代语言的语法基础* - 有点像说西方古典音乐理论是甲壳虫乐队工作的基础。 :)它可以用来分析结果，但这并不意味着它被创作者有意识地应用。也许令人惊讶的是，许多现代语言最初都是用“手写”自顶向下的语法分析器来实现的，而且BNF的表示形式来得晚，而且它本身很少有用。 C++因学术分析理论难以处理而臭名昭着。 – 2010-03-18 22:38:24

+0

@丹尼尔：你正在改进我的翻译句子。谢谢。 – 2010-03-19 01:40:11

3

如果你学习编程语言（例如：在一所大学），有相当多的理论，而不是一点点的数学参与。

的例子是：