Otto Jespersen (1924).
The present paper begins with a new exposition of the theory of syntactic types. It is addressed to mathematicians with at most an amateur interest in linguistics. The choice of sample languages is therefore restricted to English and mathematical logic. For the same reason, technical terms have been borrowed from the field of high school grammar. Only a fragmentary treatment of English grammar is presented here. This should not be taken too seriously, but is meant to provide familiar illustrations for our general methods. The reader should not be surprised if he discovers considerable leakage across the line dividing sentences from nonsentences. It is only fair to warn him that some authorities think that such difficulties are inherent in the present methods3. We take consolation in the words of Sapir: ``All grammars leak.''
The second part of this paper is concerned with a development of the technique of Ajdukiewicz and Bar-Hillel in a mathematical direction. We introduce a calculus of types, which is related to the well-known calculus of residuals4. The decision problem for this system is solved affirmatively, following a procedure first proposed by Gentzen for the intuitionistic propositional calculus5.
The methods described here may be applied in several fields. For the teaching of English they provide a rigorous version of the traditional activity known as diagramming and parsing. For introductory logic courses they offer an effective definition of well-formed formulas. For the mechanical translation of languages (Locke and Booth 1955), they may help with the syntactic analysis of the input material and indicate how to arrange the output into grammatical sentences of the target language. For the construction of an auxiliary language, they tell how to achieve a completely regular syntax; this is of special importance when the auxiliary is to act as an intermediate language in mechanical translation.
We begin by introducing two primitive types: s, the type of sentences, and n, the type of names. For the sake of simplicity, we here restrict sentence to denote complete declarative sentences, ruling out requests and questions (as well as most replies, which are usually incomplete). By a name we understand primarily a proper name, such as `John' or `Napoleon'. But we shall also assign type n to all expressions which can occur in any context in which all proper names can occur. Thus type n is ascribed to the so-called class-nouns `milk', `rice',. . ., which can occur without article, and to compound expressions such as `poor John', `fresh milk', . . .6. We do not need to assign type n to the so-called count-nouns `king', `chair', . . ., which require an article, nor to the pronoun `he', as it cannot replace `John' in `poor John works, or `milk' in `John likes milk'.
From the primitive types we form compound types, by the recursive definition: If x and y are types, then so are x/y (read x over y) and y\x (read y under x). The meaning of these two kinds of division will be made clear by two examples. The adjective `poor' modifies the name `John' from the left, producing the noun-phrase `poor John'. We assign to it type n/n. The predicate (intransitive verb) `works' transforms the name `John' from the right into the sentence `John works'. We assign to it type n\s.
In general, an expression of type x/y when followed by an expression
of type y produces an expression of type x, and so does an
expression of type
y\x when preceded by an expression of type y.
We write symbolically
This remains a sentence if `John' is replaced by any other name, hence `works' has type n\s.
Here `poor John' takes the place of the name in (1) ; in fact `poor John' can occur in any context in which all names can occur, hence it has type n. Moreover, so has `poor Tom', `poor Jane', . . ., thus `poor' has type n/n.
The word `here' transforms (l), or any other sentence, into a new sentence, hence it has type s\s. The question may be raised whether `here, can be attached to a sentence such as (3) itself. While `John works here here, is open to stylistic objections, we shall consider it grammatically well-formed.
Since `John' can be replaced by any name here, `never works' has type n\s, and so has `never sleeps', . . .; hence `never' has type (n\s)/(n\s). It may be argued that (3) could also have been grouped `John (works here)' suggesting the type (n\s)\(n\s) for `here'. It will be shown later that every adverbial expression of type s\s also has type (n\s)\(n\s).
This indicates that `for Jane' should have the same type as `here' in (3), namely s\s, and, since `Jane' can be replaced by any other name, `for' has type (s\s)/n.
This illustrates how `and' can join two arbitrary sentences to form a new sentence; its type is therefore (s\s)/s.
Here `likes Jane' has the same type as `works' in (1), hence `likes' has type (n\s)/n. Similarly we may write `John (likes milk)' and even `milk (likes John)'. The latter is a grammatical sentence, though open to semantic objections. Example (7) raises an important point. Let us group this sentence
Here `John likes' has type s/n, hence `likes' must be given the
new type n\(s/n). We would regard the two types of `likes' in (7)
and (7') as in some sense equivalent. Abstracting from this particular
situation, we write symbolically (II)
In practical applications it is often tedious to distinguish between
equivalent types, we then write x\y/z for either side of (II). Further
examples of this convention are afforded by the types of `never', `for'
and `and' [see Table I]. To avoid multiplication of parentheses, we may
also abbreviate (x/y)/z as x/y/z, and, symmetrically, z\(y\x)
as z\y\x. However, parentheses must not be omitted in such compounds
as x/(y/z), (z\y)\x, (x/y)\z and z/(y\x). Table I compares
the syntactic types of the words discussed above with the traditional parts
of speech and the recent classification of Fries (1952)).
It is fairly clear that in this manner we can build up a type list for a gradually increasing portion of English vocabulary. This should be subject to possible revision, as more information becomes available. To distinguish between different forms such as `works' and `work', usually represented by a single dictionary entry, it is necessary to allow for more than two primitive types. Thus we might assign the type n* to all noun-plurals, such as `men', `chairs',. . . In contrast to examples (1), (2), (5), (7) we then have
This assignment successfully distinguishes between the forms `work' and `works', `like' and `likes', but it introduces an undesirable multiplicity of types for `poor', `for', and `likes'. While French distinguishes the forms `pauvre' and `pauvres', English fails to make a corresponding distinction. A more thorough analysis of the English verb phrase would compel us to introduce further primitive types for the infinitive and the two kinds of participles of intransitive verbs. This would lead to some revision of the type list embodied in Table I. While giving a more adequate treatment of English grammar, such a program would not directly serve the purpose of the present paper.
The indicated computation can also be written in one line:
In the formal languages studied by logicians, this process offers an
effective test whether a given grouped string of symbols is a well-formed
formula. For in these languages each word (usually consisting of a single
sign) has just one pre-assigned type, and the use of brackets is obligatory.
Let us call expressions with built-in brackets formulas; then formulas
may be defined recursively: Each word is a formula, and if A and
B are formulas, so is (AB). Brackets are usually omitted when this
can be done without introducing ambiguity. Brackets are regularly omitted
in accordance with Rule (II). Thus logicians write
rather than
Allowance being made for this convention, the sentence structure of a formalized language is completely determined by its type list. A number of examples will illustrate this.
The Polish school of logicians prefer to write all functors on the
left of their arguments; it is well-known (Rosenbloom 1950,
IV) that all brackets can then he omitted without introducing ambiguity.
The implication sign in the Polish notation is therefore of type s/s/s.
i. Insert brackets in all admissible ways.
ii. To each word assign all types permitted by a given finite type list. (We ignore for the moment the difficulty arising from words which possess a potentially infinite number of types, as do the chameleons `and' and `only').
iii. For each grouping and type assignment compute the type of the total expression.
iv. Select that method of grouping and that type assignment which yields the desired type s.A simple example, in which the problem of grouping does not arise, is
Only the assignment
produces a declarative sentence. This may be contrasted with
and
To give a heuristic introduction for the consideration of further rules, we enter into a short discussion of English pronouns.
Since `he' transforms such expressions as `works,, `likes Jane,, . . ., of type n\s into sentences, we assign to it type s/(n\s). We could of course enlarge the class of names to include pronouns, but then we should be hard put to explain why `poor he works' and `Jane likes he' are not sentences. At any rate, the assignment of type s/(n\s) to `he' is valid, irrespective of whether we regard pronouns as names. In fact, by the same argument, the name `John' also has type s/(n\s). This point will be discussed later.
Jane works for him n n\s s\s/n (s/n)\s The expressions `that's', `Jane likes' and `Jane works for' all have type s/n, hence we have ascribed type (s/n)\s to `him'. (This assignment is not quite correct:7 The example `Jane likes poor John' indicates that the expression `Jane likes poor' also has type s/n, yet `Jane likes poor him' is not a sentence. Moreover the present assignment does not explain why `that's he' is a sentence in the speech of some people. We shall overlook these defects here.) We observe that the difference in form between `he' and `him' is reflected by a difference in type, indicating that the former operates from the left, while the latter operates from the right. Sapir (1949), vii) has called these two forms the pre-verbal and >post-verbal case of the pronoun respectively. A difficulty arises when we try to show the sentencehood of
for
cannot be simplified any further by the Rules (I) and (II). We introduce
two new rules
We may then assign type
to `he likes' and type
to `likes him', permitting two equivalent resolutions
Rules (III) also allow alternative, though equivalent, resolutions of
expressions considered earlier; e.g., the sentence
can now also be grouped
where the predicate has type
We have seen above that the name `John' also has the type of the pronoun
`he'. For the same reason, it also has the type of the pronoun `him'. We
symbolize the situation by writing
and more generally
These new rules may actually be required for computations. Suppose that
from sample sentences such as `books by him bore' we arrived at the type
n*\n*/n' for by, where n' is short for (s/n)\s. The
phrase `books by John' then requires the computation
which utilizes rules (I), (IV) and (I) in this order. While Ajdukiewicz (1935) makes use of (III), Rules (IV) suggest that the mathematical apparatus used hitherto may have to be expanded.
Rules (a), (b), (b'), (e) hold trivially. Rules (c') and (d') are symmetric duals of (c) and (d), hence it suffices to prove the latter. Assume xy -> z, and let A have type x. Then for any B of type y, AB has type z. Thus xy -> z. The system presented above may be viewed abstractly as a formal language with a number of primitive type symbols of type n, three connectives .,/,\ of type n\n/n, and a relation symbol -> of type n\s/n. If we furthermore regard (a), (b) and (b') as axiom schemes and (c) to (e) as rules of inference, we obtain a deductive system which may be called syntactic calculus. A number of rules are provable in the system; for example,
Here (f) follows from xy -> xy by (c), (g) follows from
z/y -> z/y by (d), (h) follows from (g) by (c'), (j) follows
from (i) by (c). Proofs of (i), (k) and (l) are a bit longer; we omit them
in view of the decision procedure established in Section 8.
Proofs of (m) and (n) are arranged in tree form.
The syntactic theorems (g), (h), (i), and (k) coincide with the Rules
(I), (IV), (III), and (II), respectively. An illustration of (j), or rather
its symmetric dual, appeared in Section 3,
where it was pointed out that every sentence-modifying adverb is also a
predicate-modifying adverb, symbolically,
Rule (1) is due to Schönfinkel (1924),
who observed that a function of two variables may be regarded as an ordinary
function of one variable whose value is again an ordinary function, so
that
If a, b and f(a,b) have types x, y and z respectively, then f occurs in f(a, b) with type z/(xy) and in (fa)b with type (z/y)/x, these two types being equivalent by (1).
to stand for
where x1, . . ., xn,
y are types. Now let x be any of the possible products of
the xi obtained from some way of
grouping the string x1x2
. . . xn. Then it follows by repeated
application of rules (b), (b'), (m) and (e) that
Hence the above sequent is also equivalent to the formula x -> y.
Let capitals denote sequences of types, possibly empty sequences. By ``U, V'' we mean the sequence obtained by juxtaposing U and V; if U is empty it means V, and if V is empty it means U. The following rules are consequences of (a) to (e), provided T, P and Q are not empty.
Note that each of Rules (2) to (5) introduces an occurrence of one of
the connectives .,/,\ into the conclusion. To derive Rules (1) to (5) from
(a) to (e), we observe that (1) is the same as (a), (2) becomes (c), (2')
becomes (c'), (4) is immediate, and (5) becomes (m), if the sequences T'
U' V, P, and Q are replaced by the products of the terms in
them. It remains only to prove (3), since (3') is its symmetric dual. First
let us take the case where U and V are empty sequences. We
replace T by some product t of its terms. Then (3) takes
the form: if t -> y and x -> z then (x/y)t
-> z. This may be shown thus:
Next suppose U is empty but V is not. Replace the latter
by a product v of its terms. Then (3) takes the form: if t
-> y and xv -> z then ((x/y)t)v -> z.
This is established thus:
Similarly we deal with the remaining two cases in which U is not empty. Conversely, we shall deduce rules (a) to (e) from (1) to (5), so that the two sets of rules are equivalent. For the moment we assume one additional rule, the so-called cut,
It will appear later (Gentzen's theorem) that this new rule does not
increase the set of theorems deducible from (1) to (5). Now (a) coincides
with (1), and (e) is a special case of (6), hence it suffices to prove
(b), (c) and (d). Proofs are arranged in tree form.
Let us verify that we have, in fact, a decision procedure. Given a sequent U -> x, we attempt to construct a proof in tree form, working from the bottom up, using Rules (1) to (5), but not (6). Every upward step eliminates an occurrence of one of the connectives .,/,\, and there are only a finite number of ways of making this step. Therefore the total number of proofs that can be attempted is finite. The sequent U -> x is deducible if and only if one of the attempted proofs is successful.
We prove this by reduction on the degree of the cut, which is defined
thus: Let d(x) be the number of separate occurrences of the connectives
.,/,\ in the type formula x, and let
then the degree of the above cut is
We will now show that in any cut, whose premises have been proved without cut,the conclusion is either identical with one of the premises, or else the cut can be replaced by one or two such cuts of smaller degree. Since no degree is negative, this will establish Gentzen's theorem. We consider seven cases, which need not be mutually exclusive.
Case 1. T -> x is an instance of (1); then T = x and the conclusion coincides with the other premise.
Case 2. U,x,V -> y is an instance of (1); then U and V are empty and x = y. Hence the conclusion coincides with the premise T -> x.
Case 3.The last step in the proof of T -> x uses one of
Rules (2) to (5), but does not introduce the main connective of x.
Then T -> x is inferred by Rule (3), (3') or (4) from one or two
sequents, one of which has the form T' -> x with d(T') < d(T).
The cut
has smaller degree than the given cut. More over the rule which led from T' -> x to T -> x will also lead from U,T',V -> y to U,T,V -> y, as may be easily verified in the different subcases.
Case 4. The last step in the proof of U,x,V -> y uses
one of Rules (2) to (5), but does not introduce the main connective of
x. Then U,x,V -> y is inferred from one or two sequents,
one of which has the form U',x,V' -> y'. Since the inference introduces
an occurrence of one connective,
Therefore the cut
has smaller degree than the given cut. Moreover, the same rule which led from U',x,V' -> y' to U,x,V -> y will lead from U',T,V' -> y' to U,T,V -> y, as is easily verified in the different subcases.
Case 5. The last steps in the proofs of both premises introduce
the main connective of x = x'x'' = x'.x''. We may replace
by
where both new cuts have smaller degree.
Case 6. The last steps in the proofs of both premises introduce
the main connective of x = x'/x''. We may replace
by
Case 7. This last case is like Case 6, except that x = x''\x', and is treated symmetrically.
or equivalently
This result is easily proved by induction on the length of the given
sequence connecting x with y, once the equivalence of (1)
and (2) has been established. Assuming (1), we put
and verify (2) by computation; assuming (2), we put
and verify (1) by computation.
* This paper was written while the author held a summer Research Associateship from the National Research Council of Canada. The present discussion of English grammar, in its final form, owes much to the careful reading and helpful criticism of earlier versions by Bar-Hillel and Chomsky.
1) An English translation of Adjukiewicz (1935) is available in: McCall, S. (1967): Polish Logic 1920-1939, Oxford: Clarendon Press.
2) Historically, these types can be traced back to the semantic types attributed by Tarski (1956: 215) to E. Husserl and S. Lesniewski. A similar technique for logical systems was developed independently by Church (1940). Closely related is also the work by Curry (1952) on functional characters. These correspond approximately to syntactic types for languages in which functors are always written on the left of their arguments.
3) Chomsky (1956, 1957) believes that such methods can describe only a small proportion of the sentences of a natural language and that other sentences should be obtained from these by certain transformations.
4) See Birkhoff (1948). The calculus presented here is formally identical with a calculus constructed by G.D. Findlay and the present author for a discussion of canonical mappings in linear and multilinear algebra.
5) See [Gentzen 1934; Curry 1950, 1952; Kleene 1952, xv]. Curry [1952, appendix] has also observed the close analogy between the theory of functional characters and the propositional calculus.
6) There is a difficulty here: Of course we cannot check all admissible name contexts (whose number is infinite) to see whether poor John can be fitted in. Our assignment of types is tentative and subject to future revision.
7) This was kindly pointed out to the author by N. Chomsky.
- Ajdukiewicz, K. (1935):
- ``Die syntaktische Konnexität.'' Studia Philosophica 1, 1-27.
- Bar-Hillel, Y. (1953):
- ``A quasi-arithmetical notation for syntactic description.'' Language 29 47-58.
- Birkhoff, G. (1948):
- Lattice Theory. New York: Amer. Math. Soc. Coll. Publ 25.
- Bloomfield, L. (1933):
- Language. New York: Henry Holt & Co.
- Carnap, R. (1937):
- The Logical Syntax of Language. New York: Harcourt and Kegan.
- Chomsky, N. (1956):
- ``Three models for the description of language.'' I.R.E. Transactions on Information Theory IT-2, 113-124.
- Chomsky, N. (1957):
- Syntactic Structures. The Hague: Mouton.
- Church, A. (1940):
- ``A formulation of the simple theory of types.'' Journal of Symbolic Logic 5, 56-68.
- Church, A. (1956):
- Introduction to Mathematical Logic. Princeton: Princeton University Press.
- Curry, H.B. (1950):
- A Theory of Formal Deducibility. University of Notre Dame Mathematical Lectures 6.
- Curry, H.B. (1952):
- Leçons de Logique algébrique. Paris: Gauthier-Villars.
- Fries, C.C. (1952):
- The Structure of English. New York: Harcourt, Brace & Co.
- Gentzen, G. (1934):
- ``Untersuchungen üuber das Logische Schliessen.'' Mathematische Zeitschrift 39. 176-210, 405-431.
- Jespersen, O. (1924):
- The Philosophy of Grammar. New York: George Allen & Uniwin.
- Kleene, S.C. (1952):
- Introduction to Metamathematics. New York: Van Nostrand.
- Locke, W. and Booth, A., Eds. (1955):
- Machine Translation of Languages. Cambridge MA: MIT Press.
- Quine, W.V.O. (1951):
- Mathematical Logic. Revised edition. Cambridge: Cambridge University Press.
- Rosenbloom, P. (1950):
- The Elements of Mathematical Logic. New York: Dover.
- Sapir, E. (1949):
- Language. New York: Harcourt, Brace & World.
- Schönfinkel, M. (1924):
- ``Über die Bausteine der mathematischen Logik.'' Mathematische Annalen 92, 305-316.
- Tarski, A. (1956):
- Logic, Semantics, Metamathematics. Oxford: Clarendon Press.