20.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 Gallina language. 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'' polynomial

((V₁ Ä V₂) Å V₂) Å (V₀ Ä 2)

In our example the normal form is:

(2 Ä V₀) Å (V₁ Ä V₂) Å (V₂ Ä V₂)

Then substitute the variables by their values in the variables map to get the concrete normal polynomial:

(plus (mult (2) (if b then (4) else (f (3)))) 
      (plus (mult (f (5)) x) (mult x x)))