[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.mart...@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 <ta...@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.drossopou...@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 <selin...@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