1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
|
.. _Conversion-rules:
Conversion rules
--------------------
In |Cic|, there is an internal reduction mechanism. In particular, it
can decide if two programs are *intentionally* equal (one says
:term:`convertible`). Convertibility is described in this section.
α-conversion
~~~~~~~~~~~~
Two terms are :gdef:`α-convertible <alpha-convertible>` if they are syntactically
equal ignoring differences in the names of variables bound within the expression.
For example `forall x, x + 0 = x` is α-convertible with `forall y, y + 0 = y`.
.. _beta-reduction:
β-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 :math:`T` can be written
:math:`λx:T.~x`. In any global environment :math:`E` and local context
:math:`Γ`, we want to identify any object :math:`a` (of type
:math:`T`) with the application :math:`((λ x:T.~x)~a)`. We define for
this a *reduction* (or a *conversion*) rule we call :math:`β`:
.. math::
E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u}
We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of
:math:`((λx:T.~t)~u)` and, conversely, that :math:`((λ x:T.~t)~u)` is the
*β-expansion* of :math:`\subst{t}{x}{u}`.
According to β-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 :cite:`Coq85`.
.. _iota-reduction:
ι-reduction
~~~~~~~~~~~
A specific conversion rule is associated with the inductive objects in
the global environment. We shall give later on (see Section
:ref:`Well-formed-inductive-definitions`) 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 ι-reduction
and is more precisely studied in :cite:`Moh93,Wer94`.
.. _delta-reduction:
δ-reduction
~~~~~~~~~~~
We may have variables defined in local contexts or constants defined
in the global environment. It is legal to identify such a reference
with its value, that is to expand (or unfold) it into its value. This
reduction is called δ-reduction and shows as follows.
.. inference:: Delta-Local
\WFE{\Gamma}
(x:=t:T) ∈ Γ
--------------
E[Γ] ⊢ x~\triangleright_Δ~t
.. inference:: Delta-Global
\WFE{\Gamma}
(c:=t:T) ∈ E
--------------
E[Γ] ⊢ c~\triangleright_δ~t
.. _zeta-reduction:
ζ-reduction
~~~~~~~~~~~
Coq allows also to remove local definitions occurring in terms by
replacing the defined variable by its value. The declaration being
destroyed, this reduction differs from δ-reduction. It is called
ζ-reduction and shows as follows.
.. inference:: Zeta
\WFE{\Gamma}
\WTEG{u}{U}
\WTE{\Gamma::(x:=u:U)}{t}{T}
--------------
E[Γ] ⊢ \letin{x}{u:U}{t}~\triangleright_ζ~\subst{t}{x}{u}
.. _eta-expansion:
η-expansion
~~~~~~~~~~~
Another important concept is η-expansion. It is legal to identify any
term :math:`t` of functional type :math:`∀ x:T,~U` with its so-called η-expansion
.. math::
λx:T.~(t~x)
for :math:`x` an arbitrary variable name fresh in :math:`t`.
.. note::
We deliberately do not define η-reduction:
.. math::
λ x:T.~(t~x)~\not\triangleright_η~t
This is because, in general, the type of :math:`t` need not to be convertible
to the type of :math:`λ x:T.~(t~x)`. E.g., if we take :math:`f` such that:
.. math::
f ~:~ ∀ x:\Type(2),~\Type(1)
then
.. math::
λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1)
We could not allow
.. math::
λ x:\Type(1).~(f~x) ~\triangleright_η~ f
because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be
convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`.
.. _proof-irrelevance:
Proof Irrelevance
~~~~~~~~~~~~~~~~~
It is legal to identify any two terms whose common type is a strict
proposition :math:`A : \SProp`. Terms in a strict propositions are
therefore called *irrelevant*.
.. _convertibility:
Convertibility
~~~~~~~~~~~~~~
Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the
relation :math:`t` reduces to :math:`u` in the global environment
:math:`E` and local context :math:`Γ` with one of the previous
reductions β, δ, ι or ζ.
We say that two terms :math:`t_1` and :math:`t_2` are
*βδιζη-convertible*, or simply :gdef:`convertible`, or
:term:`definitionally equal <definitional equality>`, in the
global environment :math:`E` and local context :math:`Γ` iff there
exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
… \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and
:math:`u_2` are identical up to irrelevant subterms, or they are convertible up to η-expansion,
i.e. :math:`u_1` is :math:`λ x:T.~u_1'` and :math:`u_2 x` is
recursively convertible to :math:`u_1'`, or, symmetrically,
:math:`u_2` is :math:`λx:T.~u_2'`
and :math:`u_1 x` is recursively convertible to :math:`u_2'`. We then write
:math:`E[Γ] ⊢ t_1 =_{βδιζη} t_2`.
Apart from this we consider two instances of polymorphic and
cumulative (see Chapter :ref:`polymorphicuniverses`) inductive types
(see below) convertible
.. math::
E[Γ] ⊢ t~w_1 … w_m =_{βδιζη} t~w_1' … w_m'
if we have subtypings (see below) in both directions, i.e.,
.. math::
E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m'
and
.. math::
E[Γ] ⊢ t~w_1' … w_m' ≤_{βδιζη} t~w_1 … w_m.
Furthermore, we consider
.. math::
E[Γ] ⊢ c~v_1 … v_m =_{βδιζη} c'~v_1' … v_m'
convertible if
.. math::
E[Γ] ⊢ v_i =_{βδιζη} v_i'
and we have that :math:`c` and :math:`c'`
are the same constructors of different instances of the same inductive
types (differing only in universe levels) such that
.. math::
E[Γ] ⊢ c~v_1 … v_m : t~w_1 … w_m
and
.. math::
E[Γ] ⊢ c'~v_1' … v_m' : t'~ w_1' … w_m '
and we have
.. math::
E[Γ] ⊢ t~w_1 … w_m =_{βδιζη} t~w_1' … w_m'.
The convertibility relation allows introducing a new typing rule which
says that two convertible well-formed types have the same inhabitants.
|
