I can't see the sense in reducing everything in a language to either an "e" or a "t".
Maybe this is a good place to start. Type theory (more accurately: so-called simple type theory with e and t as atomic types, which is what most linguists mean when they say "type theory") doesn't reduce everything to either e or t: It reduces everything to combinations of e and t. This may seem like nitpicking, but that's where the true power of type theory comes from: We can take existing types and build new ones from them, and there is no limit to the complexity of types we can build. Like syntax, semantics is recursive!
e and t are the atomic types that can not be decomposed any further.
e stands for "entity" and is the semantic type of terms, i.e. expressions which denote individuals: people, objects, numbers, ...
t stands for "truth value" and is the semantic type of sentences.
We can combine these types to function types: An expression of type ⟨a,b⟩ is something that takes an expression of type a as an input and outputs an expression of type b. Of course, a and b may themselves be complex, thereby allowing unlimited recursion.
- 1-place predicates like "is-a-woman" are of type ⟨e,t⟩: You put in an individual, you get out true or false.
- 2-place predicates like "love" are of type ⟨e,⟨e,t⟩⟩: You put in an individual, you get something where you put in another individual, and get out true or false.
- 1-place function symbols like "father-of" are of type ⟨e,e⟩: You put in an individual, you get out another individual.
Combining a function expression of type ⟨a,b⟩ with an appropriate argument of type a yields a new well-formed expression which has type b: For example, applying the 1-place function "father-of" of type ⟨e,e⟩ to the argument "Mary" of type e leads to a complex expression "father of Mary" which is another e, and using this term as an input to the predicate "is-a-woman" of type ⟨e,t⟩ leads to the sentence "The father of Mary is a woman" which has a truth value t.
is-a-woman (father-of (Mary))
| | |
| <e,e> e
| | |
| ------
| |
<e,t> e
| |
---------------
|
t
Up until now, this is nothing special: We just described the language of first-order logic. But we can build more types:
- Properties of properties such as "is-a-color" are of type ⟨⟨e,t⟩,t⟩:
You put in a 1-place predicate like "red", you get out a truth value.
- Predicate modifiers such as "quickly" are of type ⟨⟨e,t⟩, ⟨e,t⟩⟩, You
put in a 1-place predicate like "run", you get out a new 1-place
predicate, "run-quickly".
All the expressions in the first block only took inputs of type e: They are expressions of first order. The predicates, functions and quantifiers of first-order (~= standard) predicate logic only range over individuals.
But now we have expressions that allow predicates as arguments: We have expressions of second order. This is something new -- the language standard predicate logic does not allow for such expressions.¹ It is easy to see that we can iterate this further and get expressions of even higher order, i.e. properties of properties of properties and the like.
So here is the first advantage:
1. Standard predicate logic is too weak
Type theory has an explanatory advantage over formal semantics with standard predicate logic only, because it can account for the types of more expressions. Expressions that can not be systematically treated by standard predicate logic but by type theory include:
- properties and relations of properties and relations (such as "is a color", "is a brighter color than")
- predicate modifiers and adverbials (such as "quickly", "very")
- relative adjectives (such as "small")
- prepositions (such as "next to")
- quantifiers like "most", "more than", "infinitely many"
These are all expressions that are perfectly common natural language expressions, but can not be systematically analzyed with first-order logic. This is of course quite a limitation overcome.
Now translating natural language into a formal language doesn't yet explain anything. But one of the goals of building up a powerful enough formal language will be that this servers as a basis for a likewise powerful semantics: If we want to give a systematic account of sentences that speakers reason about, then we need a means to adequately express these sentences in the first place, on top of which a standard semantics for typed lambda calculus encorporating higher order logic is defined.
2. Type theory can explain semantic mismatches
It should be pointed out that it is not the language of type theory which makes these expressions formalizable: Rather, it is logics of higher order which provide the formal langauge as a basis for translation, most notably higher-order logic in lambda calculus, which may be attributed the status of the de facto lingua franca of formal semantics.
The role of type theory now is to
- 1) guide the syntax of these more powerful langauges: Complex expressions can only be built if the types of its components match, in the sense that an argument fits into the function according to their type specifications.
- 2) give an account of an aspect of the semantics of these more powerful langauges: The type of a complex expression can be computed from the type of its component expressions. A nice feature of this semantics is that it is compositional.
The cool thing about type theory is that we can systematically calculate why, for example, combining "red" with "is a color" leads to a sentence that has a truth value², or why "Mary is quickly" is not well-formed (namely because there is a type mismatch: "quickly" expects a property as an argument but gets an entity instead).
This is is the point where one could say there is some explanatory, rather than merely a descriptive value to this theory.
This also leads us to the next advantage:
3. Type-theoretic semantics works neatly with categorial grammar
Cateogrial grammar is a syntax theory developed to be tightly connected with a semantics as outlined above. The idea is to distinguish grammatical constituents by a semantic type, or category, that simultaneously describes the expressions it can syntactically combine with and its semantic value.
For instance, the category of a transitive verb like "eat" is (s\np)/np: It is an expression that becomes a sentence when it is first combined with an object on the right ("/np") and then a subject on the left ("\np"). Determiners like "a" are of category np/n: They are missing a noun to become an NP. Here is an exemplary syntax tree in categorial grammar:
Mary eats an apple
---- ---------- ---- -----
np (s\np)/np np/n n
----------/
np
---------------------/
s\np
--------------------------\
s
These categories can later be interpreted in terms of the standard type theoretic formalism.
- From a theoretical perspective, it is desirable to have a theory of syntax and a theory of semantics in systematic interaction with each other and expressible in a unified formalism, rather than syntax and semantics somewhat drifting apart, as has often been the case in the historical development of linguistic theories.
- Categorial grammar only has a few abstract rules; much of the syntax can be derived on the basis of the lexical items. (Whether this is indeed an advantage may be disputed.)
- Combinatory categorial grammar (some later improvement of pure categorial grammar) is supposed to be better at dealing with non-constituent-like strings and languages with more free word order than context-free grammars are, while at same time avoiding overgeneration issues known from transformational grammars.
- Categorial grammar is apparently straightforward to implement, in the same breath with a computation system for its type-theoretic semantics, due to its lexical nature can be trained with corpora to achieve wide coverage, and can be augmented with probabilistic components to make it more robust.
Upsides
In short,
- type theory can deal with the syntax and semantics of a number of expressions that standard predicate logic can't,
- it can explain certain syntactic/semantic mismatches,
- thereby in a natural way gives rise to a syntactic theory that performs well in some aspects that context-free or transformational grammars have problems with,
- type theoretic semantics is compositional, and
- its ontology is minimalist.
Downsides
Greater power comes with worse tractability. In the transition to higher-order logic and type theory, we lose a number of properties that keep standard predicate logic still relatively handleable; most notably:
- semi-decidability: There is no algorithm that detects for any valid inference in finite time that it is valid. In first-order logic we can at least detect the valid inferences (though not all the invalid ones, which is why FOL is said to be undecidable, but semi-decidable), but already for second-order logic it is not even possible to recursively enumerate all the inferenes that do hold. I.o.w., we can not possibly write a computer program that always confirms the validity of a given argument involving higher order expressions.
- completeness: There is no syntactic proof system like natural deduction that can formally derive all the semantically valid inferences. I.o.w., just because something holds doesn't always mean we can formally prove it.
- compactness: A valid inference may require infinitely many premises.
The computational complexity of higher order logic and type theories is one of the main concerns against them, not only for implementational purposes, but also in terms of psychological plausibility. Bluntly said, noone really understands logic and not even computers can fully handle it, so how could this be adequate as a model of how humans use natural langauge?
One can now argue against this by saying that one doesn't necessarily need full type theory, but only a fragment that may be less terrible; but defining precisely what kind of intermediate system constitutes a minimally complete theory of natural language, and determining its position on a complexity scale, is not a trivial problem.
Also, types can get big: The semantic type required to make coordination between NPs (such as "a man or woman") combine in a well-behaved manner is already as complex as ⟨⟨⟨e,t⟩,⟨⟨⟨e,t⟩,t⟩⟨⟨e,t⟩,t⟩⟩,⟨⟨⟨e,t⟩,⟨⟨⟨e,t⟩,t⟩⟨⟨e,t⟩,t⟩⟩,⟨⟨e,t⟩,⟨⟨e,t⟩,t⟩⟩,⟨⟨e,t⟩,t⟩⟩⟩.
Footnotes
¹ One may now wonder why one can't just model higher-order expressions in terms of first-order ones: For example, one may treat "is-a-color" as a 1-place first-order predicate that applies to a term "red" which serves as a first-order individual constant, just like "Mary" or "3" does. But this hack doesn't really do the trick:
For one, it doesn't do justice to the intuition that "red" is indeed not just an object, but rather a predicate that can be applied to objects, and just stipulating that there are two lexical items "red", one that behaves as a predicate and one that behaves as an object, is not a very satisfactory explanation of its syntax and semantics.
Second, even if such a trivialization does allow us to express higher-order expressions, it still doesn't allow to systematically analyze them. For example, from "Mars is red" and "Red is a color" we would want to infer that "Mars has a color". But if we assume that "red" in the second sentence is a term so that a first-order predicate "color" can be applied to it, then it can not simulataneously be a predicate in the first sentence. And if we claim that "red" and "red" in the two sentences are different expressions that aren't substitutible for one another, then we can not apply rules of inference to them to systematically derive the desired conclusion.
This limitaiton (amongst others) is precisely what is overcome by explicitly allowing for predicate and function symbols of higher order.
² Now justifying type theory because it allows us to calculate types may seem somehwat circular at first. But I think it is not illegitimate to claim that speakers do have intuitions like "Red is a color" being something they can judge as true or false, and certainly about something being off with "Mary is quickly". Type theory is one way of explaining why, and that with a really simple ontology consisting of just two basic types and one rule for composition, compared to much more heavy loaded syntax theories.
Literature
If you would like to read up more, I would recommend Gamut (see prash's comment); its chapter on type theory is essentially a more detailled exposition of what I outlined here. The book is rather technical, but provides accessibly written introductory motivations and comments on the introduced formalisms, and that combination makes it a pretty good resource IMO.
Partee, ter Meulen & Wall (1990), "Mathematical methods in linguistics", in their chapter on "English as a formal language" also give an introduction to type-theoretic semantics, explaining the type system directly starting with typed lambda calculus.
That being said, everything I wrote here is based on my rather old-school linguistics education; it may well be that some of the alleged advantages and possible shortcomings of type theory and categorial grammar by now have been overcome by better theories; and on the other hand I'm sure research over time has given rise to more phenomena being explained in terms of type-theoretic semantics. For the latter, the book linked by András Kovács in the comments looks promising.
