形式化語言

背景

  以前並無學習過語言形式化理論這門課，最多也就是了解編譯原理，知道有個符號系統可以抽象詞法，語法。經過研究這套符合系統的內在規律，給出了驗證模型和相應的算法。恩，這就是我所瞭解的計算機程序原理。本科畢業以後，我覺的本身已經很好地掌握了計算機（組成，結構和程序）。但我不太懂：計算機幹了什麼，以至咱們須要它？
  首先，這不是一個好問題？爲何，由於這個問題有問題，有歧義，不一樣的人有不一樣的理解？
有人認爲大數據計算，有人認爲自動化，有人說是信息時代，下降生活成本，提升工做效率，還有人喊科技，創新等等。

  其實個人意思是站在歷史的角度，當時沒有人知道有這麼個東西的時候，最開始有這個想法的人，是如何定義它呢？
提及來這我的和計算機壓根不要緊，還不是他沒見過計算機，而是他的貢獻離咱們太遠了。韋達，這個十六世紀的法國數學家，第一次有意識地、系統地在數學中使用字母的學者。什麼？這個不是常識嗎，小學學的一元一次方程都是字母表示變量的好麼。可是，在以前確實還真不是，並且我國在在辛亥革命以前，也不是啊，1906年，京師大學堂使用的教科書上，仍然用天、地、人、元表示未知數，用符號「⊥」和「|」分別表示加和減，分數則自上而下讀。
  不要說什麼貢獻小，事實上他的努力不只推進了代數學的發展，並且對十七世紀的數學家和邏輯學家萊布尼茨啓發很大。所以，使數學自己有一套完美的、通用的符號，成爲萊布尼茨在數學研究中的努力追求。萊布尼茨本人創立的微積分符號體系。在他的符號體系中， dx 表示 x 的微分， ddx 和 dddx 分別表示 x 的二階和三階微分。儘管在建立微積分的過程當中，牛頓也曾創立了另外一種不一樣的符號體系。因爲民族的偏見，英國的數學家曾在很長的時間內對萊布尼茨的符號體系進行抵制並堅持採用牛頓的符號。但終因萊布尼茨的符號體系更爲便利，從而獲得了廣泛的應用並一直沿用至今。萊布尼茨的工做，致使了他在數學符號發展史上佔據着重要的地位。直到今天，許多數學家都認爲完美的符號系統促進了整個數學的發展。特別地，數學家克萊因對代數學的狀況寫道：代數學上的進步是引進了較好的符號體系，這對它自己和分析的發展比 16 世紀技術的進步遠爲重要。事實上，採起了這一步，才使代數有可能成爲一門科學。」 （《古今數學思想》，第一冊，第 301 頁）。
  不少人其實不太懂，爲何大師會這麼推崇符號系統呢？其實有點開始引進咱們的目的了。當時的符號體系就是今天的數學語言，這個本質上就是數學語言相對比天然語言有什麼優點？

1. 無窮性 就拿最簡單的算術語言來講，它研究的對象是 0,1 ， 2 ，…， n ，…這些天然數的性質。以前的定理或當時的知識都有侷限性，爲何，就是它驗證的數據是有限的，天然語言喜歡來個整數，再說也研究不到那麼多數啊！

2. 統一性 因爲數學語言中使用了特定的記號，從而使數學語言成爲一種半形式化的符號語言，這樣以來，數學語言比任何一種天然語言更具備「統一性」。這就更明顯了，之前一個村裏兩我的都還有分歧，更別說數學能夠跨種族的，全世界的人都認識符號「∫」表示積分。

3. 可操做性 與天然語言相比，它與算法創建了聯繫。法國數學家違達提出：咱們能夠用字母（即符號）表示已知量和未知量，並對此進行純形式的操做，也即咱們能夠擺脫問題的具體內容，而從通常角度總結出廣泛的算法。好比求得任何一個一元一次方程的解須要5步：①去分母；②去括號；③移項；④合併同類項；⑤同除以未知數的係數。也就是抽象，把一個具體問題從它自己的場景中剝離，不論是土地啊仍是黃金，都無論！你想一想咱們小學考試小明但是把全部水果啊、書本啊以及掃帚都算了一遍，可咱們也就只會解一元一次方程（想一想本身小時候不會寫做業的時候的抱怨，可不就是笨嘛）。
   另外數學語言與任何一種天然語言相比較，除了具備以上特色外，還具備無歧異性、簡明性等特色。

  恩，數學語言好，但不是最好的！啊，還有更好的呢！1879年，邏輯學家弗雷格就想了，數學好是好，可是有一點缺點，可操做性。不錯這個可操做性很差，由於人太懶嘛！你說你雖然定下了一元一次方程的5步求解法，可是你每次都讓我算一遍。我去，想起小明成天買這買那忙着給咱們出題，也是辛苦極了。那能不能在增長一個可計算性呢，對不對！我一輸入數字，你就被答案告訴我了。有算法（可操做性），有計算，恩！邏輯學家弗雷格越想越興奮，發表了名著《概念文字——一種模仿算術語言構造的純思惟的形式語言》。

在這本書中，弗雷格借鑑了兩種語言，一種是傳統邏輯使用的語言，另外一種是數學語言。從而成功地構造了一種邏輯的形式語言，即：一種表意的符號語言，而且用這種語言創建了一個一階謂詞演算系統，實現了萊布尼茨提出創建一種廣泛語言的思想。

有同窗看了上面的引用，借鑑兩種語言，數學語言我懂，但傳統邏輯使用的語言，我去什麼鬼。其實這這樣的，弗雷格想了想，人類是怎麼計算的呢？通常人有了數學的可操做性以後，而後在人腦中進行計算，按照5步操做一步一步來。哎，這不就是人腦的邏輯嘛。說幹就幹：

他用「?-」表示判斷符號，用「 ?﹁- 」表示否認符號，用「≡」表示內容統一符號，用「 F(A）」表示函數符號，等等。弗雷格使用這些符號，不只表達了推理的形式和規則，並且還成功構造了第一個初步自足地邏輯演算系統。可是，他使用的符號不利於印刷。1910-1913年，羅素和懷特海發表了《數學原理》。在這部邏輯著做中，他們改進了弗雷格的表述方式，發展和完善了弗雷格的形式語言和形式推理系統。

  可是有了邏輯，誰是大腦。沒有大腦，怎麼執行邏輯啊。因此就有了計算模型（爲了可計算性）。你們一分析，人類全部的計算模型都包括以下四個要素：

1. 輸入集合或者輸入變量（I）；

2. 輸出集合或者輸出變量（O）；

3. 處理或者變化（P）；

4. 數據或者狀態（D）。

即ComputingModel =（I，O，P，D）–注意其中用的是逗號（，），其中的輸入輸出是處理或者變化元素的輸入輸出。
當時正值兩次事件大戰，關於密碼的破解和導彈管道計算迫在眉睫。圖靈提出了一種計算模型：圖靈機在已知輸入輸出狀況下研究處理和數據的實現問題，即Turing’s machine = （I，O；P，D）–注意其中用的是分號（;），處理就是算法、程序Programming，數據是DataStructure。圖靈機的工程化技術已經成熟，包括從彙編語言到UML語言在內的全系列軟件工程和程序設計語言，核心是結構化程序設計語言。
  後來咱們也有一些不須要計算結果的須要，可是也須要計算。好比：一個機器，我按個按鈕，它就唱歌，再按一些就中止唱歌。我瞭解它的狀態，而且不須要計算結果。就提出了另外一個計算模型： Petri網在已知變化狀態條件下研究輸入和輸出的網絡結構問題，即Petri nets =（P，D；I，O）–注意其中用的是分號（；）。 圖靈機是「從蛋（I，O）開始研究蛋（I，O）孵雞（P，D）」問題，而Petri網是「從雞（P，D）開始研究雞（P，D）生蛋（I，O）」問題。二者精確對偶，統一塊兒來就能夠徹底解決了「蛋（I，O）孵雞（P，D）、雞（P，D）生蛋（I，O）」的天然循環，所以被我統稱爲天然（或實）計算模型，目的是區別於我預計10年後纔有可能研究成熟並公開的「虛計算模型」。
  對偶定律告訴咱們，對偶模型能夠相互解決它倆各自所不能解決的問題。Petri網的實踐（語用網）能夠解決Turing機所不能解決的「軟件模塊複用（也就是計算協做）」問題；而 Turing機的實踐（算法分析-也就是軟件工程）解決了Petri網所不能解決的「節點爆炸」問題。這就是我把它倆統一塊兒來研究的緣由。

參考資料

邏輯學語言
計算模型的統一分析