[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear all,
I think the terminology comes from the research on Illative Combinatory
Logic (ILC).
The notions "subject" and "predicate", respectively for the term M and
the type A in a judgment M:A are explained in the publication [Seldin
1919], see below.
(I am not sure it is the original source though, Seldin refers to
[Curry, Hindley, Seldin, 1972] when talking about subject-reduction, in
Section 2.2.2)
In ILC, one writes AM for the typing M:A, where A and M are both
lambda-terms and A is interpreted as the type (predicate) and M as the
term (subject) we want to give a type to.
Hindley and Seldin also use the terminology in their 1986 classic book.
Best
Herman
[Seldin 1979]
J. P. Seldin.
Progress report on generalized functionality. Annals of Mathematical
Logic, 17:29–59, 1979.
Condensed from manuscript Theory of Generalized functionality informally
circulated 1975. Journal now called "Annals of Pure and Applied Logic".
see https://www.sciencedirect.com/science/article/pii/0003484379900202
[Hindley and Seldin, 1986]
J. R. Hindley and J. P. Seldin.
Introduction to Combinators and λ-calculus. Cambridge Univ. Press,
England, 1986.
[Curry, Hindley, Seldin, 1972]
Curry, Haskell B., Hindley, Roger, and Seldin, Jonathan P.
Combinatory Logic, vol. II. (North-Holland, Amsterdam, 1972).
