A/B + C/B -> (A+C)/B.In the case that the PT is

**1/3 + 1/3**, the CT obtained after application is

**2/3**.

So if this is the input, what is the output? You guessed (or read) it, a feedback-message! This feedback-message is supposed to contain more information then '

*this is incorrect*', but it can only use the CT, the PT and the allowed rules. Furthermore, the algorithm is assumed to only start when a mistake has been made.

## A first try

When we know that a mistake has been made, we also know that there is no path of rule-application which leads from the PT to the CT, otherwise there is a rule which is not valid. In order to get a path between the two terms we introduce a magic rule__R__which exactly encodes the rewrite between the PT and the CT. In the case that the PT is

**1/3 + 1/5**and the CT is

**3/15**, we have the following

__R__in which A != B != C != D:

A/B + A/D -> B/CNow lets assume that we have the following (conditional) rewrite-rules:

(1) A1/B1 + C1/B1 -> (A1 + C1)/B1Given this set, our task becomes to identify the rewrite-rule which the student wanted to apply, but in which he made a mistake. This can be translated into finding the allowed rule which is most similar to the

(2) A2/B2 + C2/D2 -> (A2*D2)/(B2*D2) + (C2*B2)/(D2*B2)

(3) A3/B3 + C3/D3 -> ((A3*N) + C3)/D3 where N = D3/B3

__R__. We can use some form of tree-edit distance for this problem, since the rules actually represent a structured action.

There exists many different tree-edit distance algorithms, for this algorithm we can use a rather simple one. When we encounter two intermediate or leaves nodes which cannot be matched we replace the one with the other. This operation costs 2, one node is deleted and one node is added. When we encounter a leave node which needs to be matched against an intermediate node we check whether the leaf node is a free variable. A variable is free if there is no previous match and the variable is not subject of any restrictions. When the variable is free we simply match it against the sub-tree, otherwise we replace the variable with the sub-tree which costs

*1 + size(inserted-tree)*.

To illustrate the distance we calculate the difference between (1) and

__R__. Within the LHS we need to replace

*B1*with

*B*which costs us 2. The rest of the variables can be matched against each other (so A = A!, etc). Within the RHS we need to replace

*A1+C1*with

*B*which costs 3 + 1 = 4. This replacement needs to be done because

*B*is already matched against

*B2*in the LHS. The last step is to replace the

*B1*with

*C*in the RHS which costs 2. This has to be done because we already matched

*B1*to

*B*in the LHS, and we know that B != C. This results in a total distance between

__R__and (1) of 8. If we perform the same algorithm for the other rules we end up with distance(

__R__,(2)) = 16, and distance(

__R__,(3)) = 8.

Even though (1) and (3) have a similar score, we end up with rule (3) as our guess. This is because rule (1) cannot be applied to the PT, so it is more unlikely that this was the intention of the student.

Unfortunately, we are not done yet because the student could have taken a correct step before making a mistake. To model this we calculate a new set of PT's by applying the rules where possible. This results in two new PT's, PT1' =

**(1*5)/(3*5) + (1*3)/(5*3)**and PT2' =

**((1*5)+1)/5**. Calculating the rules

__R1__,

__R2__and all the distances we get six new distances. None of these distances is smaller then the distance of 8 we already have (the proof of this claim is left as an exercise for the reader), therefore we stop the recursion and return a feedback-message containing the rule (3) as a guess.

Although I knew we needed to tests this algorithm more thoroughly, it seemed to be correct to me. However, the assumption that the recursion can be stopped when there is no distance <= the lowest distance up until now can not be made out of the blue. This has to do with confluence, a property that is not guaranteed for the set of rewrite-rules. Sigh, just when I thought that I had a fitting key for the lock, I could not turn it to unlock the door.

## Getting the facts

The concept of confluence came up Thursday and I have been trying to get around it until today. A first thing that I did was sum up some properties about the scope of the problem.- The terms are rather small (100 nodes or less)
- There are few steps between the start and the answer (15 or less)
- All rules are applied with a reason

*always*rewrite a term towards an answer.

With these assumptions in mind I noticed that the domain of fractions has only a few allowed rules. The same holds for the domain of equations and the domain of rewriting logic formulas to CNF, there are only 6 allowed rules for this last domain! Even if we combine rewrite-rules, by unifying the RHS of a rule with the LHS of another rule, we only get 9 rules for the domain of logic. These are not the kind of figures a computer cannot handle within a few milliseconds.

When we introduce new rules by unification this can be viewed as applying the rules after each other on the same (part of the) term. For example, if we unify the rules (2) and (1) from above we get:

1.2 A2/B2 + C2/D2 -> (A1+C1)/B1If we perform the same algorithm as above, this rule surfaces as the result with a distance of only 4. The only right thing to do now is to return both rules (1) and (2) as a result. We cannot deduce which of the two rules went wrong, but we know that the error is somewhere along this path.

where B1 = B2*D2, A1 = A2*D2

, C1 = C2*B , B1 = D2*B2

If we compare this with the first result of the algorithm we see that it is completely different. However, if we look at the example we see that it is indeed more likely that the student wanted to apply the rules (1) and (2). A guess which complies more with my intuition because of the matching denominators in the answer. Furthermore, this adapted version of the algorithm also work on the other examples that I tried, even the ones for the domain of rewriting logic!

## The solution?

Now that the improved algorithm seems to work it would be nice if we can prove the claim 'we can stop when the distance becomes greater'. We can view the path between the PT and the CT as a sequence of allowed rule application in which there is an error. This error can be anywhere on the path. So is*i*is an allowed rule, we have something like

*i*. The recursion in the algorithm strips of the first set of rules, so we end up with

_{n }..i_{m}. error . i_{k }..i_{j}*error . i*.

_{k }..i_{j}Because we assume that all rules rewrite the term towards an answer we argue that stripping of allowed rules results in a smaller distance. When we 'jump over' the error the distance becomes bigger because we get strange

__R__'s which do not look like an allowed rewrite rule at all, otherwise we could have stripped of another rule.

When we combine this reasoning with the fact that we only have a small sequence of steps, I believe that this algorithm will at least give better feedback in many practical situations. Whenever it is not possible to make a good guess we can always fall back to a message like:

*'We do not know what you did, can you try to do it in smaller steps?'*. I don't see a problem here because the tools are focused on practicing a task in small steps. Now lets see what my supervisor thinks of it.

## No comments:

Post a Comment