[TYPES] What is the term after reduction called?

[J. R. Hindley]

Dear Fangyi Zhou,

The name "redex" was invented by Haskell Curry, see Section 3D5 in the book "Combinatory Logic" by Curry and Feys 1958.  He called the result of contracting a redex "the contractum of the redex".

> Is there an agreed terminology for the term after reduction (N)?

No, I think there is no agreed terminology.  Perhaps the reason is that (in lambda-calculus) every term can be a reductum or contractum, but not every term can be a redex.  

For example, let T be any term; if we choose R to be the redex  (\x.x)T,   then R contracts to T, so T is a reductum.  

Good luck,
  Roger Hindley