高階邏輯檢視原始碼討論檢視歷史

來自 搜狐網 的圖片

高階邏輯是全國科學技術名詞審定委員會審定、公布的科技類名詞。

關於中國文字的起源主要有兩種觀點：起源於刻畫符號和「圖畫文字」起源說。我們現在已知的最早的文字是安陽殷墟出土的甲骨文。

名詞解釋

高階邏輯亦稱「廣義謂詞邏輯」、「高階謂詞邏輯」。一階邏輯的推廣系統，謂詞邏輯的重要組成部分。謂詞邏輯有一階邏輯和高階邏輯之分。在一階邏輯中，量詞只能用於個體變元，取消這一限制條件，允許量詞也可用於命題變元和謂詞變元，由此構造起來的謂詞邏輯就是高階邏輯。公理化的高階邏輯系統或高階邏輯的自然推理系統又稱為廣義謂詞演算或高階謂詞演算。

在數學中，高階邏輯在很多方面有別於一階邏輯。其一是變量類型出現在量化中；粗略的說，一階邏輯中禁止量化謂詞。允許這麼做的系統請參見二階邏輯。

高階邏輯區別於一階邏輯的其他方式是在構造中允許下層的類型論。高階謂詞是接受其他謂詞作為參數的謂詞。一般的，階為n的高階謂詞接受一個或多個（n− 1）階的謂詞作為參數，這裡的n> 1。對高階函數類似的評述也成立。

高階邏輯更加富有表達力，但是它們的性質，特別是有關模型論的，使它們對很多應用不能表現良好。作為哥德爾的結論，經典高階邏輯不容許（遞歸的公理化的）可靠的和完備的證明演算；這個缺陷可以通過使用Henkin模型來修補。

高階邏輯的一個實例是構造演算。

應用

高階邏輯在數學中，高階邏輯在很多方面有別於一階邏輯。其一是變量類型出現在量化中；粗略的說，一階邏輯中禁止量化謂詞。允許這麼做的系統請參見二階邏輯。

高階邏輯區別於一階邏輯的其他方式是在構造中允許下層的類型論。

性質

高階邏輯更加富有表達力，但是它們的性質，特別是有關模型論的，使它們對很多應用不能表現良好。作為哥德爾的結論，經典高階邏輯不容許(遞歸的公理化的)可靠的和完備的證明演算；這個缺陷可以通過使用 Henkin 模型來修補。

高階邏輯的一個實例是構造演算。

高階函數在數學和計算機科學中，高階函數是至少滿足下列一個條件的函數:

接受一個或多個函數作為輸入輸出一個函數在數學中它們也叫做算子(運算符)或泛函。微積分中的導數就是常見的例子，因為它映射一個函數到另一個函數。

演算

在無類型 lambda 演算，所有函數都是高階的；在有類型 lambda 演算（大多數函數式編程語言都從中演化而來）中，高階函數一般是那些函數型別包含多於一個箭頭的函數。在函數式編程中，返回另一個函數的高階函數被稱為Curry化的函數。

在很多函數式編程語言中能找到的 map 函數是高階函數的一個例子。它接受一個函數 f 作為參數，並返回接受一個列表並應用 f 到它的每個元素的一個函數。

高階函數的其他例子包括函數複合、積分和常量函數 λx.λy.x。