Programming in Haskell by Hutton says:
An expression that has the form of a function applied to one or more arguments that can be ‘reduced’ by performing the application is called a reducible expression, or redex for short.
Is a reducible expression i.e. redex exactly
a function application where the function is not the result of another function application,
equivalently, a function application where the function is either a function name or a lambda expression?
Is either of the above two points an answer to my previous question at How does the outermost evaluation strategy evaluate partial application of a function and application of a curried function?
What counts as a redex generally depends on the language. The syntax of expressions comes in pairs of introduction and elimination forms of various constructs; a redex is when a particular kind of construct's introduction and elimination forms are juxtaposed appropriately.
For functions, lambdas are introductions (they are the canonical way to create a function when there wasn't one before) and applications are eliminations (they are the canonical way to use a function). So a function redex is the application of a lambda to something, e.g. something of the form (\x -> e1) e2
. (And only this! The application of a variable to something is not a function redex. Normally I would assume this is implied, but your question explicitly asks about this, so...)
For declarations, let
-bindings or similar are introductions (they are the canonical way to declare that a name has a given value) and variables are eliminations (they are the canonical way to use a declared value). So a declaration redex is a term in the scope of a let
binding that references a let
-bound variable, e.g. something of the form let x = e1 in e2
where e2
mentions x
.
For algebraic data types, the type's data constructors are introductions (they are the canonical way to create a value in the type) and case
expressions are eliminations (they are the canonical way to use a value of algebraic type). So an algebraic data type redex is a case
whose scrutinee is a fully-saturated constructor application, e.g. case Constructor arg1 arg2 arg3 ... of pat1 -> e1; pat2 -> e2; ...
.
These are just some examples of pairings. Not all languages have all three of these constructs; and there are languages with additional constructs (e.g. mutable references, exceptions, and the like, each with their own introduction and elimination forms). But I think this should give you a flavor of what is meant by "redex": it is a construction in which some computation can be done to make forward progress in figuring out the value of an expression.