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

Question

Closed. This question needs to be more focused。它当前不接受答案。












想改善这个问题吗？更新问题，使其仅关注 editing this post的一个问题。

5年前关闭。



Improve this question




RDBMS基于 Relational Algebra和Codd模型。我们有类似于编程语言或OOP的东西吗？

最佳答案

Do we have [an underlying model] for programming languages?

天哪由于编程语言太多，因此有多种模型可供选择。最重要的第一:

Church的无类型lambda演算是一种计算模型，其功能与图灵机一样强大(不多也不少)。著名的“Church-Turing假设”是这两个等效模型代表了我们知道如何实现的最通用的计算模型。 λ演算非常简单。整个语言是

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

构成变量，函数应用程序和函数定义。 lambda演算还带有大量的“简化规则”，用于简化表达式。如果找到无法归约的表达式，则称为“正常形式”并表示一个值。

Lambda演算是如此笼统，您可以沿多个方向进行操作。

如果要使用所有可用规则，则可以编写专用工具，例如部分求值器和部分编译器。

如果要避免在lambda下减少任何子表达式，而要使用所有可用规则，那么您最终会使用诸如Haskell或Clean之类的惰性功能语言模型。在此模型中，如果缩减可以终止，则可以保证缩减，并且很容易表示无限的数据结构。很强大。

如果您避免在lambda下减少任何子表达式，并且如果您还坚持在应用函数之前将每个参数减少为正常形式，那么您将拥有一个热切的函数语言模型，例如F＃，Lisp，Objective Caml，Scheme，或标准ML。

也有几种类型的lambda calculi，其中最著名的是 System F 命名的，这是由Girard(在逻辑上)和Reynolds(在计算机科学中)独立发现的。系统F是CLU，Haskell和ML等语言的出色模型，这些语言是多态的，但具有编译时类型检查功能。 Hindley(逻辑上)和Milner(计算机科学上)发现了系统F(现在称为Hindley-Milner类型系统)的受限形式，这使得可以从未类型化lambda演算的某些表达式中推断出System F表达式。 Damas和Milner开发了一种执行此推断的算法，该算法在标准ML中使用，并已在其他语言中得到了推广。

Lambda微积分只是在 push 符号。达娜·斯科特(Dana Scott)在指称语义方面的开创性工作表明，lambda演算中的表达式实际上与数学函数相对应，并且他确定了哪些表达式。 Scott的工作对于弄清“递归定义”尤其重要，“递归定义”在计算机科学中很常见，但从数学 Angular 来看却毫无意义。 Scott和Christopher Strachey证明了递归定义等同于递归方程的最小定义解，并且进一步说明了如何构造该解。任何允许递归的语言，尤其是允许以任意类型递归的语言(例如Haskell和Clean)都应归功于Scott的模型。

有一系列基于抽象机的模型。这里没有那么多的个体模型作为一种技术。您可以通过使用状态机并在机器上定义转换来定义语言。这个定义涵盖了从图灵机到冯·诺依曼机再到术语重写系统的所有内容，但是抽象机通常被设计为“尽可能接近语言”。此类机器的设计以及有关它们的证明定理的业务都在操作语义的标题下进行。

What about object-oriented programming?

我对受过OOP训练的抽象模型的了解程度不高。我最熟悉的模型与实现策略紧密相关。如果我想进一步研究这一 Realm ，我将从William Cook的Smalltalk指称语义开始。 (Smalltalk作为一种语言非常简单，几乎与lambda演算一样简单，因此它为建模更复杂的面向对象语言提供了一个很好的案例研究。)

胡维提醒我，马丁·阿巴迪(Martin Abadi)和卢卡·卡德利(Luca Cardelli)在面向对象语言的基础演算(类似于lambda演算)上进行了雄心勃勃的工作。我对这项工作的理解不够充分，无法对其进行总结，但是这里是他们的书序言中的一段，我觉得值得一提:

Procedural languages are generally well understood; their constructs are by now standard, and their formal underpinnings are solid. The fundamental features of these languages have been distilled into formalisms that prove useful in identifying and explaining issues of implementation, static analysis, semantics, and verification.

An analogous understanding has not yet emerged for object-oriented languages. There is no widespread agreement on a collection of basic constructs and on their properties... This situation might improve if we had a better understanding of the foundations of object-oriented languages.

... we take objects as primitive and concentrate on the intrinsic rules that objects should obey. We introduce object calculi and develop a theory of objects around them. These object calculi are as simple as function calculi, but represent objects directly.

我希望这段报价能使您对作品的风格有所了解。

关于oop - 编程语言背后是否有任何数学模型或理论？ ，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/2469824/

上一篇：xslt - 使用xsl :choose for updating a single element attribute

下一篇：json - 在 Windows 上的 Excel VBA 中，对于解析的 JSON 变量，这个 JScriptTypeInfo 到底是什么？

相关文章：

java - 比较对象不起作用

python - 编写一个引用实例和类的python方法

sql - Firebird 2.1 TIMESTAMP 算术和民用间隔

c - 如何在 FUSE 中创建符号链接(symbolic link)？

programming-languages - 响应式(Reactive)编程和函数式响应式(Reactive)编程之间的区别

c# - 'GET OR SET ACCESSOR EXPECTED' 是什么意思？

perl - 在 Perl 中递归打印数据结构

algorithm - 如果数字是小数，如何检查某个数字是否可以表示为 x^y？

java - 我是否正确地将这段伪代码翻译成Java？

language-agnostic - 支持 "partial specialization"的其他语言有哪些？

Answer 1

Do we have [an underlying model] for programming languages?

天哪由于编程语言太多，因此有多种模型可供选择。最重要的第一:

Church的无类型lambda演算是一种计算模型，其功能与图灵机一样强大(不多也不少)。著名的“Church-Turing假设”是这两个等效模型代表了我们知道如何实现的最通用的计算模型。 λ演算非常简单。整个语言是

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

构成变量，函数应用程序和函数定义。 lambda演算还带有大量的“简化规则”，用于简化表达式。如果找到无法归约的表达式，则称为“正常形式”并表示一个值。

Lambda演算是如此笼统，您可以沿多个方向进行操作。

如果要使用所有可用规则，则可以编写专用工具，例如部分求值器和部分编译器。

如果要避免在lambda下减少任何子表达式，而要使用所有可用规则，那么您最终会使用诸如Haskell或Clean之类的惰性功能语言模型。在此模型中，如果缩减可以终止，则可以保证缩减，并且很容易表示无限的数据结构。很强大。

如果您避免在lambda下减少任何子表达式，并且如果您还坚持在应用函数之前将每个参数减少为正常形式，那么您将拥有一个热切的函数语言模型，例如F＃，Lisp，Objective Caml，Scheme，或标准ML。

也有几种类型的lambda calculi，其中最著名的是 System F 命名的，这是由Girard(在逻辑上)和Reynolds(在计算机科学中)独立发现的。系统F是CLU，Haskell和ML等语言的出色模型，这些语言是多态的，但具有编译时类型检查功能。 Hindley(逻辑上)和Milner(计算机科学上)发现了系统F(现在称为Hindley-Milner类型系统)的受限形式，这使得可以从未类型化lambda演算的某些表达式中推断出System F表达式。 Damas和Milner开发了一种执行此推断的算法，该算法在标准ML中使用，并已在其他语言中得到了推广。

Lambda微积分只是在 push 符号。达娜·斯科特(Dana Scott)在指称语义方面的开创性工作表明，lambda演算中的表达式实际上与数学函数相对应，并且他确定了哪些表达式。 Scott的工作对于弄清“递归定义”尤其重要，“递归定义”在计算机科学中很常见，但从数学 Angular 来看却毫无意义。 Scott和Christopher Strachey证明了递归定义等同于递归方程的最小定义解，并且进一步说明了如何构造该解。任何允许递归的语言，尤其是允许以任意类型递归的语言(例如Haskell和Clean)都应归功于Scott的模型。

有一系列基于抽象机的模型。这里没有那么多的个体模型作为一种技术。您可以通过使用状态机并在机器上定义转换来定义语言。这个定义涵盖了从图灵机到冯·诺依曼机再到术语重写系统的所有内容，但是抽象机通常被设计为“尽可能接近语言”。此类机器的设计以及有关它们的证明定理的业务都在操作语义的标题下进行。

What about object-oriented programming?

我对受过OOP训练的抽象模型的了解程度不高。我最熟悉的模型与实现策略紧密相关。如果我想进一步研究这一 Realm ，我将从William Cook的Smalltalk指称语义开始。 (Smalltalk作为一种语言非常简单，几乎与lambda演算一样简单，因此它为建模更复杂的面向对象语言提供了一个很好的案例研究。)

胡维提醒我，马丁·阿巴迪(Martin Abadi)和卢卡·卡德利(Luca Cardelli)在面向对象语言的基础演算(类似于lambda演算)上进行了雄心勃勃的工作。我对这项工作的理解不够充分，无法对其进行总结，但是这里是他们的书序言中的一段，我觉得值得一提:

Procedural languages are generally well understood; their constructs are by now standard, and their formal underpinnings are solid. The fundamental features of these languages have been distilled into formalisms that prove useful in identifying and explaining issues of implementation, static analysis, semantics, and verification.

An analogous understanding has not yet emerged for object-oriented languages. There is no widespread agreement on a collection of basic constructs and on their properties... This situation might improve if we had a better understanding of the foundations of object-oriented languages.

... we take objects as primitive and concentrate on the intrinsic rules that objects should obey. We introduce object calculi and develop a theory of objects around them. These object calculi are as simple as function calculi, but represent objects directly.

我希望这段报价能使您对作品的风格有所了解。