[TYPES] subject reduction

[Herman Geuvers]

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).