[TYPES] What is the term after reduction called?

[Fritz Henglein]

Commonly 'reduct' is used, which is English and derived from the Latin
'reductum'.  But since Latin is arguably a conditio sine qua non of erudite
discourse, 'reductum' is clearly an option.  (Writing the remainder of
one's paper in Latin may be a challenge and not an H-index friendly
strategy, though.  It hasn't been done much since Gauss's Disquisitiones
Arithmeticae.)

On Thu, Jun 9, 2022 at 2:38 PM Fangyi Zhou <fangyi.zhou15 at imperial.ac.uk>
wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Dear TYPES mailing list
>
> Let M -> N.
>
> It appears to me that the terminology for terms before reduction (M) is
> sometimes called a reducible expression (redex), although the concept of
> redex
> seems to be more general than that.
>
> Is there an agreed terminology for the term after reduction (N)?
> The wikipedia page for lambda calculus (without giving any sources) calls
> the
> expression to which a redex reduces to a 'reduct', but I've seen other
> words
> used such as 'reductum'.
>
> Apologies if the question is silly.
>
> Best,
> Fangyi
>
> --
> Fangyi Zhou (Pronouns: they/them)
> PhD Student
> Mobility Reading Group
> Department of Computing
> Imperial College London
>
>