How does the outermost evaluation strategy evaluat

2019-07-25 21:20发布

问题:

Programming in Haskell by Hutton says

When evaluating an expression, in what order should the reductions be performed? One common strategy, known as innermost evaluation, is to always choose a redex that is innermost, in the sense that it contains no other redex. If there is more than one innermost redex, by convention we choose the one that begins at the leftmost position in the expression.

Another common strategy for evaluating an expression, dual to innermost evaluation, is to always choose a redex that is outermost, in the sense that it is contained in no other redex. If there is more than one such redex then as previously we choose that which begins at the leftmost position. Not surprisingly, this evaluation strategy is known as outermost evaluation.

In partial application of a function, for example, mult(3)(4), where mult is defined as

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

innermost evaluation will first evaluate mult(3) as \y->3*y, and then evaluate (\y->3*y)4. How will outermost evaluation evaluate mult(3)(4)?

In application of a curried function, for example, mult'(3)(4), where

mult'   ::  Int ->  Int ->  Int
mult'   x   =   \y  ->  x   *   y

innermost evaluation will first evaluate mult'(3) as \y->3*y, and then evaluate (\y->3*y)4. How will outermost evaluation evaluate mult'(3)(4)?

回答1:

The only sensible way of interpreting:

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

in the context of your larger question is as an unary function that takes a single argument of tuple type (Int, Int). So, mult cannot be partially applied. In particular, mult(3) doesn't make any sense, because 3 is not a tuple of type (Int, Int).

As a result, the reduction of the expression mult (3,4) in the sense meant by Hutton is the same whether you use outermost or innermost reduction. There's only one redex/application here, the application of mult to (3,4), and both outermost and innermost reduction would give the reductions:

mult (3,4)
=>  3 * 4
=>  12

For the function:

mult' :: Int -> Int -> Int
mult' x y = x * y

or equivalently:

mult' = \x -> (\y -> x * y)

the expression mult' 3 4 or equivalently (mult' 3) 4 undergoes innermost reduction as:

(mult' 3) 4
= ((\x -> (\y -> x * y)) 3) 4
=> (\y -> 3 * y) 4
=> 3 * 4
=> 12

Curiously, outermost reduction proceeds in exactly the same manner:

(mult' 3) 4
= ((\x -> (\y -> x * y)) 3) 4     -- (1)
=> (\y -> 3 * y) 4
=> 3 * 4
=> 12

That's because the application of ((\x -> \y -> x * y) 3) to 4 in line (1), while it's the outermost application, is not a redex. It can't be reduced, because the thing being applied ((\x -> \y -> x * y) 3) isn't a lambda expression. (It's an application of a lambda expression to an argument.)

Therefore, contrary to first appearances, there's only one redex in line (1), and the innermost and outermost reduction strategies choose the same redex.