高次文法

高階文法（HOG）は、高階論理に基づいた文法理論です。^{[ 1 ] [ 2 ]}生成列挙的（範疇文法や原理とパラメータなど）またはモデル理論的（ヘッド駆動句構造文法や語彙機能文法など）として同時に見ることができます。

• 言語的（音韻的、統語的、または意味的）実体の集合を表す型という命題論理が存在する。例えば、型NPは名詞句の統語範疇（または形式クラス）を表す。
• HOGは、ハスケル・カリーが提唱したテクトグラム構造（抽象構文）とフェノグラム構造（具体構文）の区別を維持している。
• 抽象的な統語的実体は、構造主義的（ブルームフィールド＝ホケット）な自由形式（単語や句）と同一視される。例えば、名詞句your cat は、その音韻や意味とは区別される。
• 具体的な統語論は音韻論と同一視され、音韻論は広義には語順を含むものと解釈される。
• フレーゲの意味のモデル化はモンタギューのものと概ね似ているが、内包がより細かい超内包に置き換えられている。
• （カリー＝ハワード）証明項計算があり、その項は言語的（音韻論的、統語論的、または意味論的）実体を表す。
• 微積分という用語は、古典的な高階論理（HOL）の中に組み込まれている。
• HOLでは、統語論と音韻論、統語論と意味論のインターフェースは公理的理論として表現される。
• HOLは（分離型の）サブタイプを認めており、例えば、対格名詞句のタイプであるNPaccはNPのサブタイプであり、NPによって示されるカテゴリのサブセットを表します。

• 高次文法、オハイオ州立大学