Reducible expression
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
A reducible expression (redex for short) is an expression which matches the left-hand-side of some reduction rule or definition.
For example, given the definitions:
fac 0 = 1
fac n = n * fac (n-1)
then "fac 3" is a redex (because it matches left-hand-side of the second definition) but "fac" is not.
Operationally, a redex is any expression whose evaluation requires work to be done. For example, a function call with all of its arguments supplied is a redex, but a constant is not. This is useful, for example, in common subexpression elimination, which only saves work if the common subexpression is a redex.