形式語義學

形式語義學是指用數學方法精確刻畫計算機語言的語義；尤其指用形式系統嚴格定義出的語言的語義。形式語義學是軟件工程學的基礎理論之一；語言的形式語法和形式語義已成為程序設計語言的必要組成部分。在形式語義學基礎上；形式規範、程序變換、編譯自動化等研究都取得了豐碩的成果。程序設計語言的語義通常是由設計者用一種自然語言非形式地解釋的；實現者和使用者依據各自的理解去實現和使用這種語言。人們發現對過程調用語句的非形式解釋可能導致各種不同的理解；產生多種不同的效果。為了正確、有效地使用程序設計語言；必須瞭解語言中各個成分的含義；並要求計算機系統執行這些成分所產生的效果與其含義完全一致；人們這種對語義精確解釋的要求便產生了形式語義學。形式語義學是對形式語言及其句子採用形式系統方法進行語義定義的學問。需要形式語義研究的原因有以下幾點：1、幫助理解語言；2、支持語言標準化；3、指導語言設計；4、幫助編寫編譯器和語言系統 ；5、支持程序驗證和軟件可靠性；6、有助於軟件規範化 ^[1]  。

為了正確、有效地使用程序設計語言，必須弄清語言中各成分的含義，並且要求計算機系統執行這些成分所產生的效果和它的語義完全一致。由於自然語言存在歧義性，故用自然語言解釋程序設計語言的含義容易造成誤解，影響語言的正確實現和有效使用。實踐證明，必須用形式化的語言和方法精確解釋程序設計語言。這種需求產生了形式語義學。20世紀60年代初，在程序設計語言ALGOL60的設計中，第一次明確區分了語言的語法和語義，圍繞ALGOL60的語義問題出現了形式語義學早期的研究高潮。

70年代，形式語義學取得重大進展，指稱語義、代數語義等理論和方法對程序設計理論有深刻的影響。操作語義、公理語義等研究也開創了新的局面。形式語義學是軟件工程學的基礎理論之一，語言的形式語法和形式語義已成為程序設計語言的必要組成部分。在形式語義學基礎上，形式規範、程序變換、編譯自動化等研究都取得了豐碩的成果。

用程序設計語言編寫的程序，規定了計算機對數據的加工過程。形式語義學的基本方法是用一種元語言將程序加工數據的過程及其結果形式化，從而定義程序的語義。根據所用數學工具和研究重點，形式語義學可分為四大類。

通過語言的實現方式定義語言的語義，也就是將語言成分所對應的計算機的操作作為語言成分的語義。因為語言的語義應該是標準的，不應依賴於特定的計算機系統，或一種具體的實現方式，因此，操作語義學使用抽象機和抽象解釋程序來定義語言的語義。

通過執行語言成分所要得到的最終效果來定義該語言成分的語義。指稱語義學方法認為語言成分的含義是語言成分本身固有的，不依賴於具體實現該語言成分的計算機。對同一種語言成分，不同的計算機的執行實現過程可以不同，但所產生的最終效果應該是相同的。這種最終效果被看作是語言成分所指稱的外在物體，稱作語言成分的指稱物。指稱物多為數學對象，如整數、集合、函數等。指稱語義學方法在定義語言的語義時，先確定指稱物，然後給出語言成分到指稱物的語義映射，這種映射必須滿足兩個條件：每個語言成分都對應有指稱；複合成分的指稱只依賴於它的子成分的指稱。論域理論是指稱語義學方法的數學基礎。

用代數公理刻劃語言成分的語義，只要研究抽象數據類型的代數規範。抽象數據類型的代數規範通過構造算子和一組有關運算的代數公理刻劃類型操作的行為。在論證這種規範滿足協調性和完全性的基礎上，通過尋找適當的模型代數，可以定義一個抽象類型的不同層次的語義，如初始語義、終止語義等，然後就可以用普通的代數方法論證規範的正確性和實現的正確性，從而形成的一門專業的自然學科。

通過使用數學中的公理化方法，用公理系統定義程序設計語言的語義。另外，公理語義學還研究和尋求適用於描述程序語義、便於語義推導的邏輯語言。例如，用時態邏輯定義的語言的公理語義又稱為時態語義。典型的公理語義方法是Hoare公理系統。代表人物有R.W.Floyd和C.A.R Hoare;如果掌握了形式語義學裏面的數學理論、方法和概念，就可以用它們去創造規則、刻畫規則和證明規則，從而可以描述和推導各類程序設計語言的各種成分和性質。

回顧過去，計算語言學主 要停留在語形處理上，而理論語言學可以為句法結構分析提供成熟的理論支持，因而語言學和計算語言學合作很多。隨着語形處理技術日趨成熟，其技術潛力也基本被挖掘殆盡，比如詞性標註、漢語詞的切分、機器翻譯等，近年以來，進展緩慢。互聯網上的信息搜索，主要採用的是語詞匹配技術語音識別與合成軟件，也多是基於對語音的物理屬性分析。計算語言學家馮志偉教授曾指出形式語義是理論語言學與計算語言學之間的橋樑。沒有形式語義學做中介，理論語言學很難直接與計算語言學中的自然語言語義處理做“無縫對接”，這使得形式語義學在這個信息技術時代顯得尤為重要。