22

RDBMS は、リレーショナル代数と Codd のモデルに基づいています。プログラミング言語や OOP に似たものはありますか?

4

11 に答える 11

41

プログラミング言語の [基礎となるモデル] はありますか?

天国、はい。また、非常に多くのプログラミング言語があるため、複数のモデルから選択できます。最初に最も重要なこと:

  • チャーチの型なしラムダ計算は、チューリング マシンと同じくらい強力な計算モデルです (それ以上でもそれ以下でもありません)。有名な "Church-Turing 仮説" は、これら 2 つの同等のモデルが、私たちが実装方法を知っている最も一般的な計算モデルを表しているというものです。ラムダ計算は非常に単純です。全体として、言語は

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

    変数、関数適用、および関数定義を構成します。ラムダ計算には、式を単純化するための「簡約規則」のかなり大きなコレクションも付属しています。還元できない式を見つけた場合、それは「正規形」と呼ばれ、値を表します。

    ラムダ計算は非常に一般的であるため、いくつかの方向に進むことができます。

    • 利用可能なすべてのルールを使用したい場合は、部分評価器やコンパイラの一部などの特殊なツールを作成できます。

    • ラムダの下で部分式を減らすことを避け、利用可能なすべてのルールを使用すると、Haskellや Clean のような遅延関数型言語のモデルになってしまいます。このモデルでは、リダクションが終了できる場合は終了することが保証されており、無限のデータ構造を簡単に表現できます。とてもパワフルな。

    • ラムダの下で部分式を縮小することを避け、関数が適用される前に各引数を通常の形式に縮小することを主張する場合、F#、Lisp、Objective Caml、Scheme、または標準ML。

  • 型付きラムダ計算にはいくつかの種類があり、その中で最も有名なものはSystem Fという名前でグループ化されており、Girard (ロジック) と Reynolds (コンピューター サイエンス) によって個別に発見されました。System F は、CLU、Haskell、および ML などの言語の優れたモデルです。これらの言語はポリモーフィックですが、コンパイル時に型チェックを行います。Hindley (論理学) と Milner (コンピューター サイエンス) は、型指定されていないラムダ計算のいくつかの式から System F 式を推論できるようにする System F の制限された形式 (現在 Hindley-Milner 型システムと呼ばれる) を発見しました。Damas と Milner は、この推論を行うアルゴリズムを開発しました。これは標準 ML で使用され、他の言語で一般化されています。

  • ラムダ計算は、記号を押し付けているだけです。Dana Scott の表示意味論における先駆的な研究は、ラムダ計算の式が実際に数学関数に対応することを示し、彼はどの関数かを特定しました。Scott の研究は、コンピューター サイエンスでは一般的ですが、数学的な観点からは無意味な「再帰的定義」を理解する上で特に重要です。Scott と Christopher Strachey は、再帰的定義が再帰方程式の最小定義解と同等であることを示し、さらに、その解を構築する方法を示しました。再帰を許可するすべての言語、特に任意の型で再帰を許可する言語 (Haskell や Clean など) は、Scott のモデルに負っています。

  • 抽象機械に基づくモデルのファミリー全体があります。ここでは、テクニックほど個々のモデルはありません。ステート マシンを使用し、マシン上で遷移を定義することで、言語を定義できます。この定義には、チューリング マシンからフォン ノイマン マシン、用語書き換えシステムまですべてが含まれますが、一般的に、抽象マシンは「可能な限り言語に近い」ように設計されています。そのような機械の設計と、それらに関する定理を証明する業務は、操作上のセマンティクスの見出しに含まれます。

オブジェクト指向プログラミングはどうですか？

私は、OOP に使用される抽象モデルについて十分な教育を受けていません。私が最もよく知っているモデルは、実装戦略に非常に密接に関連しています。この分野をさらに調査したい場合は、William Cook の Smalltalk の表示セマンティクスから始めます。(言語としての Smalltalk は非常に単純で、ラムダ計算とほぼ同じくらい単純であるため、より複雑なオブジェクト指向言語をモデル化するための良いケース スタディになります。)

Wei Hu は、Martin Abadi と Luca Cardelli が、オブジェクト指向言語の基礎計算 (ラムダ計算に類似) に関する野心的な一連の作業をまとめたことを思い出させてくれます。私はそれを要約するのに十分なほどよく理解していませんが、引用する価値があると思われる彼らの本のプロローグからの一節を次に示します。

手続き型言語は一般的によく理解されています。それらの構造は現在では標準的であり、正式な基盤はしっかりしています。これらの言語の基本的な機能は、実装、静的分析、セマンティクス、および検証の問題を特定して説明するのに役立つことが証明されている形式主義に蒸留されています。

オブジェクト指向言語についても、同様の理解はまだ確立されていません。基本的な構成要素の集合とその特性については、広く合意されているわけではありません... オブジェクト指向言語の基礎をよりよく理解していれば、この状況は改善されるかもしれません。

...私たちはオブジェクトを原始的なものと見なし、オブジェクトが従うべき固有の規則に集中します。オブジェクト計算を導入し、それらの周りのオブジェクトの理論を開発します。これらのオブジェクト計算は、関数計算と同じくらい単純ですが、オブジェクトを直接表現します。

この引用で作品の趣を感じていただければ幸いです。

于 2010-03-18T22:10:10.630 に答える
10

Lisp はラムダ計算に基づいており、今日の現代言語で見られるものの多くのインスピレーションとなっています。

フォンノイマン マシンは現代のコンピューターの基礎であり、最初はアセンブラー言語でプログラムされ、次に FORmula TRANslator でプログラムされました。その後、文脈自由文法の正式な言語理論が適用され、すべての現代言語の構文の基礎となっています。

計算可能性理論 (形式オートマトン) には、形式文法の階層に対応するマシンタイプの階層があります。チューリングマシン。

シャノンとコルモゴロフの 2 種類の情報理論もあり、コンピューティングに適用できます。

再帰関数理論、レジスタマシン、ポストマシンなど、あまり知られていないコンピューティングモデルがあります。

そして、さまざまな形式の述語論理を忘れないでください。

追加: 離散数学 - 群論と格子論について言及するのを忘れていました。特に、格子は (IMHO) すべてのブール論理の根底にある特に気の利いた概念であり、表示セマンティクスなどの一部の計算モデルです。

于 2010-03-18T12:59:25.863 に答える
6

Lisp のような関数型言語は、Church の「ラムダ計算」 (ウィキペディアの記事はこちら) から基本的な概念を継承しています。よろしく

于 2010-03-18T12:47:17.257 に答える
5

1 つの概念はチューリング マシンかもしれません。

于 2010-03-18T12:41:56.830 に答える
3

プログラミング言語を勉強している場合 (例: 大学で)、かなり多くの理論があり、少なからず数学が含まれています。

例は次のとおりです。

于 2010-03-18T13:10:22.483 に答える
2

ウィキペディアのオブジェクト指向プログラミングの歴史のセクションは、啓蒙的かもしれません。

于 2010-03-18T12:48:48.113 に答える
2

私が考えることができる最も近い類推は、最近では「Gurevich Abstract State Machines」（GASM）の名前でより知られているGurevich Evolving Algebrasです。

Gurevich が Microsoft に入社したとき、私は長い間、この理論がより実際に適用されることを望んでいましたが、出てきたものはほとんどないようです。Microsoft サイトの ASML ページを確認できます。

GASM の良い点は、セマンティックが正式に指定されていても、疑似コードによく似ていることです。これは、実践者がそれらを簡単に把握できることを意味します。

結局のところ、リレーショナル代数の成功の一部は、テーブル、外部キー、結合など、簡単に把握できる概念の正式な基盤であることにあると思います。

ソフトウェアシステムの動的コンポーネントにも同様のものが必要だと思います。

于 2010-03-18T12:56:29.440 に答える
2

あなたの質問に対処するための多くの側面があり、回答が散らばっています。

まず、言語の構文を記述し、パーサーがどのように機能するかを指定するために、文脈自由文法を使用します。

次に、構文に意味を割り当てる必要があります。正式なセマンティクスは役に立ちます。主なプレーヤーは、操作上のセマンティクス、表示上のセマンティクス、および公理的なセマンティクスです。

悪いプログラムを排除するために、型システムがあります。

最終的に、すべてのコンピューター プログラムは、非常に単純な計算モデルに縮小 (または、必要に応じてコンパイル) できます。命令型プログラムはより簡単にチューリング マシンにマッピングされ、関数型プログラムはラムダ計算にマッピングされます。

これらすべてを自分で学習している場合は、http://www.uni-koblenz.de/~laemmel/paradigms0910/を強くお勧めします。講義は録画され、オンラインで公開されているからです。

于 2010-03-19T06:13:30.723 に答える
0

私が知っているように、形式文法は構文の記述に使用されます。

于 2010-03-18T12:45:08.040 に答える