Normalization

Perform some rewriting steps (with respect to a fixed set of rules) before the realization of a narrowing step.
Two level of rules:
- rules used during the narrowing process
- rules and negative rules (rules that force the computation to fail) used by rewriting.
Soundness: use only normalization rules that are logical consequences of the program.

Three kinds of rules that we can use for the simplification process

The rules of the program.
Inductive Consequences: rules that are valid in the least model of the program. The name comes from the fact that, usually the validity can only be proven by induction. For instance, if we consider the rules for the addition:
```
        X + 0 = X.
        X + (succ Y) = succ (X + Y).
```
the following rules are inductive consequences and can be used for simplification:
```
        0 + Y = Y.
        (succ X) + Y = succ (X + Y).
```
CWA-valid rules: rules that are a consequence of the program by using the Closed World Assumption. By using these rules, negation as failure can be simulated in some cases in a safe way.

Under certain conditions, some of these rules can be derived automatically.
We assume that the programmer marks the rules used only for simplification by using the directive norm.
Mainly used to improve the implementations (shorter computations).
Expressive power: Implemented strategies are not complete. The technique allows to write programs that compute an answer where the program alone cannot.

Expressivity of Normalization Rules

Example

Consider the program:


type letters = a | b | c.

pred on: letters * letters.
     on (a, b).
     on (b, c).

pred above: letters * letters.
     above (X, Y) :- on (X, Y).
     above (X, Y) :- above (X, Z), on (Z, Y).

solve above (a, a).
     ... infinite loop ...

solve above (a, c).
     ... infinite loop ...

With normalization we can reach a result:


pred on: letters * letters.
     on (a, b).
     on (b, c).

pred above: letters * letters.
     above (X, Y) :- on (X, Y).
     above (X, Y) :- above (X, Z), on (Z, Y).

norm ~ above (X, X).
norm ~ above (X, Y) :- above (Y, X).

solve above (a, a).
>     false.

solve above (a, c).
>     false.

The technique of normalization is also useful to handle equations between constructors, that cannot be handled by pure narrowing. The next example defined the function less-than-or-equal-to over integer numbers with a predecessor constructor:


type nat = 0 | succ nat | pre nat.

fun leq : nat -> nat -> bool.
    leq 0 0.
  ~ leq 0 (pre 0).
    leq 0 (succ X) :- leq 0 X.
  ~ leq 0 (pre X) :- ~ leq 0 X.
    leq (succ X) Y = leq X (pre Y).
    leq (pre X) Y = leq X (succ Y).

norm succ (pre X) = X.
norm pre (succ X) = X.

Normalization - Implementation -

Narrowing strategy

Normalizing narrowing have been studied in several papers Fribourg 84, 85, Hanus 92.
It has also been combined with lazy narrowing Hanus 94

Translation to PROLOG

Normalization was present in the SLOG interpreter Fribourg 84, 85

Abstract Machine Implementation

WAM extension: A-WAM for the ALF language
A preprocessor transforms programs into two groups of conditional equations, for narrowing steps and rewriting steps, respectively.
The abstract machine performs:

narrowing and
rewriting,

Rewriting is supported by a separate mechanism.

The combination of normalization into PROLOG has been studied in Fribourg, Cheong 91, but it is more difficult because the functional structure is not known.

Go to index