Higher-order grammar is a grammar theory based on higher-order logic. HOG does not force you to choose between the proof-theoretic (a la Categorial Grammar) and model-theoretic (a la HPSG or LFG) type of grammar.

Key features

• In HOG, a grammar is an axiomatic theory written in a certain kind of higher-order logic (HOL).
• The types of the HOL provide a logic for the proof-theoretic aspects of grammatical analysis. A type denotes a set of linguistic (phonological, syntactic, or semantic) entities; e.g. the type NP denotes the set of NPs.
• The (typed) terms of the HOL provide a logic for the model-theoretic aspects of grammatical analysis. A term denotes a linguistic (phonological, syntactic, or semantic) entity, and can be thought of as a derivation of the entity it denotes. E.g. the term runs(Kim) of type S_fin denotes denotes a finite sentence, a member of the set denoted by S_fin.
• The two logics are intimately connected to each other by the Curry-Howard isomorphism.
• Unsaturated syntactic entities, such as verbs, are literally functions, and what are (usually metaphorically) called their "grammatical arguments" (i.e. the subject and complements) are literally the arguments of the function. E.g. the basic constant runs of type NP_nom => S_fin denotes a function from the set of nominative noun phrases to the set of finite sentences.
• Semantic interpretation is analyzed as a (polymorphic) structure preserving function sem from syntactic entities to semantic ones, e.g. sem(runs(Kim)) = run'(Kim').
• Phonological interpretation is analyzed as a (polymorphic) structure preserving function phon from syntactic entities to phonological ones, e.g. phon(runs(Kim)) = /kim/^/ranz/.

External links

• Higher-Order Grammar (http://www.ling.ohio-state.edu/~hana/hog/), Ohio State