[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
