高階邏輯

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

基本介紹

• 中文名：高階邏輯
• 釋義：接受其他謂詞作為參數的謂詞
• 套用：數學
• 實例：構造演算

套用

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

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

性質

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

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

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

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

演算

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

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

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