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