Backtracking in Standard ML

Question

I have seen in my SML manual the following function, which computes how many coins of a particular kind are needed for a particular change. For example change [5,2] 16 =[5,5,2,2,2] because with two 5-coins and three 2-coins one gets 16.

the following code is a backtracking approach:

exception Change;
fun change _ 0 = nil|
    change nil _ = raise Change|
    change (coin::coins)=
if coin>amt then change coins amt
else (coin:: change (coin::coins) (amt-coin))

handle Change=> change coins amt;

It works, but I don't understand how exactly. I know what backtracking is, I just don't understand this particular function.

What I understood so far: If amt is 0, it means our change is computed, and there is nothing to be cons'd onto the final list.

If there are no more coins in our 'coin-list', we need to go back one step.

This is where I get lost: how exactly does raising an exception helps us go back?

as I see it, the handler tries to make a call to the change function, but shouldn't the "coins" parameter be nil? therefore entering an infinite loop? why does it "go back"?

The last clause is pretty obvious to me: if the coin-value is greater than the amount left to change, we use the remaining coins to build the change. If it is smaller than the amount left, we cons it onto the result list.

Answer 1

You can rewrite this use of exceptions into using the 'a option type instead. The original function:

exception Change;
fun change _ 0 = []
  | change [] _ = raise Change
  | change (coin::coins) amt =
    if coin > amt
    then change coins amt
    else coin :: change (coin::coins) (amt-coin)
         handle Change => change coins amt;

In the modified function below, instead of the exception bubbling up, it becomes a NONE. One thing that becomes slightly more apparent here is that coin only occurs in one of the two cases (where in the code above it always occurs but is reverted in case of backtracking).

fun change' _ 0 = SOME []
  | change' [] _ = NONE
  | change' (coin::coins) amt =
    if coin > amt
    then change' coins amt
    else case change' (coin::coins) (amt-coin) of
             SOME result => SOME (coin :: result)
           | NONE        => change' coins amt

Another way to demonstrate what happens is by drawing a call tree. This does not gather the result as Andreas Rossberg's evaluation by hand, but it does show that only the times change is taking an else-branch is there a possibility to backtrack, and if a backtrack occurs (i.e. NONE is returned or an exception is thrown), don't include coin in the result.

  (original call ->)  change [2,5] 7
                      \ (else)
                       `-change [2,5] 5
                      /  \ (else)
  ___________________/    `-change [2,5] 3
 /                       /  \ (else)
/                       /    `-change [2,5] 1
`-change [5] 5         /       \ (then)
  \ (else)            /         `-change [5] 1
   `-change [] 0     /            \ (then)
     \              /              `-change [] 1
      `-SOME []     `-change [5] 3   \ (base)
                     \ (then)         `-NONE
                      `-change [] 3
                        \
                         `-NONE

Answer 2

This is best seen by writing out how evaluation proceeds for a simple example. In each step, I just replace a call to change by the respective right-hand side (I added extra parentheses for extra clarity):

  change [3, 2] 4
= if 3 > 4 then ... else ((3 :: change [3, 2] (4 - 3)) handle Change => change [2] 4)
= (3 :: change [3, 2] 1) handle Change => change [2] 4
= (3 :: (if 3 > 1 then change [2] 1 else ...)) handle Change => change [2] 4
= (3 :: change [2] 1) handle Change => change [2] 4
= (3 :: (if 2 > 1 then change [] 1 else ...)) handle Change => change [2] 4
= (3 :: (raise Change)) handle Change => change [2] 4

At this point an exception has been raised. It bubbles up to the current handler so that evaluation proceeds as follows:

= change [2] 4
= if 2 > 4 then ... else ((2 :: change [2] (4 - 2)) handle Change => change [] 4)
= (2 :: change [2] 2) handle Change => change [] 4
= (2 :: (if 2 > 2 then ... else ((2 :: change [2] (2 - 2)) handle Change => change [] 2)) handle Change => change [] 4
= (2 :: ((2 :: change [2] 0) handle Change => change [] 2)) handle Change => change [] 4
= (2 :: ((2 :: []) handle Change => change [] 2)) handle Change => change [] 4
= (2 :: (2 :: [])) handle Change => change [] 4
= 2 :: 2 :: []

No more failures up to here, so we terminate successfully.

In short, every handler is a backtracking point. At each failure (i.e., raise) you proceed at the innermost handler, which is the last backtracking point. Each handler itself is set up such that it contains the respective call to try instead.

Answer 3

Source: https://www.cs.cmu.edu/~rwh/introsml/core/exceptions.htm

The expression exp handle match is an exception handler. It is evaluated by attempting to evaluate exp. If it returns a value, then that is the value of the entire expression; the handler plays no role in this case. If, however, exp raises an exception exn, then the exception value is matched against the clauses of the match (exactly as in the application of a clausal function to an argument) to determine how to proceed. If the pattern of a clause matches the exception exn, then evaluation resumes with the expression part of that clause. If no pattern matches, the exception exn is re-raised so that outer exception handlers may dispatch on it. If no handler handles the exception, then the uncaught exception is signaled as the final result of evaluation. That is, computation is aborted with the uncaught exception exn.

In more operational terms, evaluation of exp handle match proceeds by installing an exception handler determined by match, then evaluating exp. The previous binding of the exception handler is preserved so that it may be restored once the given handler is no longer needed. Raising an exception consists of passing a value of type exn to the current exception handler. Passing an exception to a handler de-installs that handler, and re-installs the previously active handler. This ensures that if the handler itself raises an exception, or fails to handle the given exception, then the exception is propagated to the handler active prior to evaluation of the handle expression. If the expression does not raise an exception, the previous handler is restored as part of completing the evaluation of the handle expression.