[TYPES/announce] subject reduction

[Gabriel Scherer]

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