19.2 The variables map
19.2 The variables map
It is frequent to have an expression built with + and
×, but rarely on variables only.
Let us associate a number to each subterm of a ring
expression in the Gallinalangage. For example in the ring
nat, consider the expression:
(plus (mult (plus (f (5)) x) x)
(mult (if b then (4) else (f (3))) (2)))
As a ring expression, is has 3 subterms. Give each subterm a
number in an arbitrary order :
0 |
|¬ |
if b then (4) else (f (3)) |
1 |
|¬ |
(f (5)) |
2 |
|¬ |
x |
Then normalize the ``abstract'' polynom ((V1 Ä V2) Å V2) Å (V0 Ä 2)
In our example the normal form is:(2 Ä V0) Å (V1 Ä V2) Å (V2 Ä V2)
Then substitute the variables by their values in the variables map to
get the concrete normalized polynom:
(plus (mult (2) (if b then (4) else (f (3))))
(plus (mult (f (5)) x) (mult x x)))
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.8.1.html at 8/10/98