Features and Types in Type-Theoretical Natural Language Semantics

Abstract

Features and types are two possible ways to classify phenomena related to the formalization of natural language grammar and semantics. Features are frequently used in linguistically oriented theories. However, they do not accord with type theoretical semantics due to the notion of subtype to which they lead. The article suggests a way to coordinate these two approaches through defining types based on the classification by features. An example of formalization for a small fragment of English language is provided for demonstration. General formal theory of syntax and semantics for this language is developed, which is of a separate interest. The language of formalization is Agda. Agda serves simultaneously as (1) a metalanguage that formalizes the syntax of the natural language and (2) a semantical/ontological language that interprets the natural language. This allows to formalize interpretation as a function that maps Agda expressions presenting syntax into Agda expressions comprising semantics. The concept of subtype is based on the notion of coercion. Defining types through features leads to the automatic definition of coercion between them. Agda's mechanism of instance arguments allows in many cases to provide coercion automatically. The article ends with examples of the natural language expression formalizations showing the theory in action. Despite Agda's primary orientation towards mathematics, it contains tools and instruments that render it applicable to natural language studies in the framework of type theoretical semantics.