[TYPES] What is the term after reduction called?

[Jon Sterling]

I think I have also heard 'contractum'. But maybe that refers to the result of applying a single reduction rule? Not sure.

Best,
Jon


On Thu, Jun 9, 2022, at 5:10 PM, Hendrik Boom wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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.
>
> The word that came to mind when I had just read the title of this post 
> was 'reduct'.
>
>> 
>> 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'.
>
> I suspect that is for writers that use latin to give their writing a 
> classical sound.
>
> -- hendrik
>
>> 
>> Apologies if the question is silly.
>> 
>> Best,
>> Fangyi
>> 
>> -- 
>> Fangyi Zhou (Pronouns: they/them)
>> PhD Student
>> Mobility Reading Group
>> Department of Computing
>> Imperial College London
>>