Re: [TYPES] What is the term after reduction called?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I've seen "reduct", but also "contractum". See e.g. "Semantics Engineering with PLT Redex".

As with much terminology and notation, I doubt you will find one true answer.

--
William J. Bowman

On Thu, Jun 09, 2022 at 01:31:33PM +0100, Fangyi Zhou 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
>