Next: Cartesion Product
Up: Class note 28
Previous: Remarks on Subject
We would like to show that reduction terminates. To do so, we will
need a bit of machinery. The first concept to consider will be
the depth of a term.
- Definition: Suppose
Type. Define the depth of
, denoted 
by cases as follows:. If is some variable 
,
then 
. If is a compound type, i.e. 
then
.
Examples:
.
- Definition: The depth of a redex
is 
.
We now wish to consider a notion of the measure of a term
in the 
-calculus, using the depth of the type of its redices as
defined above:
- Definition: Suppose
. We define the measure of 
denoted 
as 
where 
is the maximum depth redex in and 
is the number of such redices.
For example, suppose 
, then 
.
Thus, to calculate 
, look at , find all its redices and then compute
their depths. Find the maximum of all of these depths to get and then
count how many redices of that depth there are to find . We will use the
standard lexicographical
ordering on 
to find an ordering on . Namely,
if and only if
or, if 
and 
. Note that if we take
then we're just
using the ordinary ordinal ordering. Fact: We know that this
ordering is well-founded. Thus, there is no infinite decreasing sequence
of measures on a term.
Our goal now is
to find a reduction strategy (choice of which 
-redex to reduce) which
will guarantee that (redex) > (contractum). That is, we need
some reduction strategy where:
We know two reduction strategies already which we could consider,
namely lazy (leftmost outermost) and eager (leftmost innermost).
So, what sort of strategy do we choose? If we have 
,
then our goal is to reduce in such a way such that 
.
When we consider , our first thought might be to find the maximum
depth redex and then reduce it. However, we see that this strategy
won't work. Supose 
is the maximum depth redex.
Also suppose that itself is duplicated in 
. Then, if we do the
substitution 
we end up replicating , possibly many times.
This clearly does not decrease the number of maximum depth
redices. In fact it will often increase the number of maximum depth redices.
Thus is not decreasing. So this reduction strategy does not work.
It turns out that we need to find the rightmost innermost maximum depth
redex, and then reduce that one. In this case,
the redices in will be of smaller depth, and if the reduction creates
a redex in , say 
reduces
to 
; then the depth of the new redex is , which is
smaller than 
.
We will
call this strategy maximum depth rightmost innermost redex reduction.
We have thus demonstrated the following theorem:
- Theorem:
such that 
Type where
the maximum depth rightmost innermost redex reduction
strategy terminates.
We should note that we have said nothing about how many steps will be
required until this strategy terminates. Suppose and . Suppose also 
and 
.
Then one of the following will be true:
-
; this implies that the latest reduction ``used up'' the
redices of depth .
-
and 
; this implies that we have reduced one
occurrence of a maximum depth redex, but there are still others of
this depth left which need to be reduced.
The theorem we stated above is a weak theorem. The stronger statement
of this theorem is to say that every reduction terminates, not only the
maximum depth rightmost innermost redex reduction as demonstrated
above. The proof of this theorem can be found in CN91 11.
Next: Cartesion Product
Up: Class note 28
Previous: Remarks on Subject