haskellfunctional-programmingredex

Is my understanding of a reducible expression i.e. redex correct?


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

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?


Solution

  • 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.