コンピューター工学、言語学、数学を合わせる

プログラムを書いてからデイバッギングと言う作業で直す事が普通です。でも書いたプログラムを観て確実に正しく動く事を証明出来ればシステムの設計がよくなるはずです。数学の計算式をを確かめる検算がよく使われます。この考え方をコンピューターサイエンスに実施した方がC.A.R. Hoare （An Axiomatic Basis for Computer Programming)だったどうです。彼のやり方によって定理を使ってプログラムの結果を予測出来ます。この学問は今software verificationと呼ばれているそうです。For Loop, IF, assignment, Arrays, etc can be encompassed in axioms and rules of inference describing the initial state of the system, the program, and the resulting state of the system. その後はAIで有名になったJohn McCarthy (Towards a Mathematical Science of Computation)がRecursionの結果を証明しました。Recursive Inductionと言うルールによって二つのプログラムが同じな影響になると確かめる方法を見つけました。
However, the discussion does not conclude at proofs regarding the correctness and equivalence of computer programs. Once a program is known to be correct, given that its syntax can be understood, it must be shown to conform to the syntax of its language. 統語を表すトリー図を作ってこれでプログラムを確認します。意味も分析しなければいけません。関数の意味がシステムの変化になるからです。If the program conforms to the syntactical specification of the language, we might obtain an accurate prediction of its behavior down to its impact on the hardware. 先のプログラムが検算で確かめた場合に無駄な変数などがないはずだから言語の仕様書を使って自動的にCPUのコードに翻訳出来る。これはコンパイルとリンクの作業です。
However, this systematization of computer language has strong parallels to formal grammars and syntax trees in linguistics. Computational linguistics, in particular, indicates significant influence of the above principles. Machine translation involves basically mapping one abstract representation of a text into another one. 以上のMcCarthyの文書がコンピューター言語の翻訳を確認する方法を書いた。だから人間の言語をコンピューターで翻訳する事が現在のコンパイラーの動き方と似ています。