[TYPES] subject reduction

[J. R. Hindley]

Dear All, 

Simone and Tarmo and Herman are right.  A typing judgment M:A can be thought of as an analogy to the English sentence "John is happy", where "John" is the subject and "happy" is the predicate. (Or perhaps better, John is the subject and happiness is the predicate.)  

The subject/predicate notation is introduced in Curry and Feys "Combinatory Logic Volume 1" (1958) pp. 272--3 (Section 8E5), followed by a discussion on pp.274--5 (Section 8S2) of the analogy between type-theory (which Curry calls "functionality") and traditional grammar. 

Happy Christmas,  
Roger Hindley 

----------------------- 
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear types-announce and types-list,

As a moderator of both list, I mistakenly accepted this
"Subject reductoin" email on the types-announce list,
which is only for announces.

Apologies for the noise.

If you wish to reply to Peter, please use types-list instead.

Below is a collection of the excellent responses already received:

From: Simone Martini <simone.martini at unibo.it>
> 
> Types, for H.B. Curry, are properties, which are asserted on a subject.
> Hence: M:T may be read as “the subject M has the property T”.
> 
> I am sure others on this list may be more philologically precise.

From: Tarmo Uustalu <tarmo at cs.ioc.ee>
> 
> Hi Peter,
> 
> It's about 'subject' vs 'predicate' where the subject is the term and
> the predicate is the type in a typing judgement s : P.
> 
> Best wishes,
> 
> Tarmo U

From: Sophia Drossopoulou <s.drossopoulou at imperial.ac.uk>
> 
> I do not know why “subject”. But I think that the first use of the technique in CS as
>    Mitchell & Plotkin: Abstract types has existential type, POPL 1985
> 
> And they attributed the technique to
>    Curry & Feys, Combinatory Logic I, North Holland, 1958


Cheers

On Tue, Dec 5, 2017 at 9:26 PM, Peter Selinger <selinger at mathstat.dal.ca> wrote:
> [ The Types Forum (announcements only),
>     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
> 
> Dear type theorists,
> 
> what is the origin of the term "subject reduction"? I am of course
> referring to the property that if M:A and M -> N, then N:A, also
> known as type preservation.
> 
> I can sort of see where "reduction" comes into it, but why "subject"?
> 
> Thanks, -- Peter