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

Question

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?

Answer 1

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.

Answer 2

You also ask (in the comments on the linked entry) "Isn't mult(3) a partial application, so it makes sense?"

I thought I've answered this concern in my answer to one of your previous questions.

No, the type of mult is (Int, Int) -> Int, i.e. its argument must have type (Int, Int). But 3 can't have that type; its type is simply Int. To calculate the result of mult 3, the definition of

mult :: (Int, Int) -> Int
mult (x, y) = x * y

is consulted, and the calculation proceeds as follows:

mult 3
= case 3 of (x, y) -> x * y
***error: pattern match failure

Actually, this would be the case if Haskell were an untyped language. Since it's got types, the type mismatch of 3 and (Int, Int) is detected during compilation, and the program is rejected. (*)

---

_{(*) 3 :: Num a => a, i.e. its type can be Int, Float, etc., but certainly it can't be a tuple ... well, without having a Num instance defined for tuples it can't, but let's say there isn't one. This also means the program will actually be rejected at run time after having found no Num instances were defined for any tuple types in any of the imported modules... but let's leave it as a footnote.}