[TYPES] What is the term after reduction called?

Fangyi Zhou fangyi.zhou15 at imperial.ac.uk
Thu Jun 9 08:31:33 EDT 2022


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



More information about the Types-list mailing list