4.3 Conversion rules
b-reduction.
We want to be able to identify some terms as we can identify the application of a function to a given argument with its result. For instance the identity function over a given type T can be written [x:T]x. We want to identify any object a (of type T) with the application ([x:T]x a). We define for this a reduction (or a conversion) rule we call b:| ([x:T]t u) |> |
|
t{x/u} |
We say that t{x/u} is the b-contraction of ([x:T]t u) and, conversely, that ([x:T]t u) is the b-expansion of t{x/u}.
According to b-reduction, terms of the Calculus of Inductive Constructions enjoy some fundamental properties such as confluence, strong normalization, subject reduction. These results are theoretically of great importance but we will not detail them here and refer the interested reader to [17].
i-reduction.
A specific conversion rule is associated to the inductive objects in the environment. We shall give later on (section 4.5.4) the precise rules but it just says that a destructor applied to an object built from a constructor behaves as expected. This reduction is called i-reduction and is more precisely studied in [86, 98].d-reduction.
In the environment we also have constants representing abbreviations for terms. It is legal to identify a constant with its value. This reduction will be precised in section 4.4.1 where we define well-formed environments. This reduction will be called d-reduction.Convertibility.
Let us write t |> u for the relation t reduces to u with one of the previous reduction b,i or d.We say that two terms t1 and t2 are convertible (or equivalent) iff there exists a term u such that t1 |> ... |> u and t2 |> ... |> u. We note t1 =bdi t2.
The convertibility relation allows to introduce a new typing rule which says that two convertible well-formed types have the same inhabitants.
At the moment, we did not take into account one rule between universes which says that any term in a universe of index i is also a term in the universe of index i+1. This property is included into the conversion rule by extending the equivalence relation of convertibility into an order inductively defined by:
- if M=bdi N then M£bdi N,
- if i £ j then Type(i)£bdiType(j),
- if T =bdi U and M£bdi N then (x:T)M£bdi (x:U)N.
The conversion rule is now exactly:
h-conversion.
An other important rule is the h-conversion. It is to identify terms over a dummy abstraction of a variable followed by an application of this variable. Let T be a type, t be a term in which the variable x doesn't occurs free. We have [x:T](t x) |> t
Indeed, as x doesn't occurs free in t, for any u one
applies to [x:T](t x), it b-reduces to (t u). So
[x:T](t x) and t can be identified.Remark: The h-reduction is not taken into account in the convertibility rule of Coq.
Normal form.
A term which cannot be any more reduced is said to be in normal form. There are several ways (or strategies) to apply the reduction rule. Among them, we have to mention the head reduction which will play an important role (see chapter 7). Any term can be written as [x1:T1]...[xk:Tk](t0 t1... tn) where t0 is not an application. We say then that t0 is the head of t. If we assume that t0 is [x:T]u0 then one step of b-head reduction of t is:[x1:T1]...[xk:Tk]([x:T]u0 t1... tn) |> [x1:T1]...[xk:Tk](u0{x/t1} t2 ... tn)
Iterating the process of head reduction until the head of the reduced
term is no more an abstraction leads to the b-head normal
form of t:
t |> ... |> [x1:T1]...[xk:Tk](v u1... um)
where v is not an abstraction (nor an application). Note that the
head normal form must not be confused with the normal form since some
ui can be reducible.Similar notions of head-normal forms involving d and i reductions or any combination of those can also be defined.