Dependent Types for Program Termination Verification.
Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic examples, which are all verified in a prototype implementation, to support the effectiveness of our approach to program termination verification as well as its unobtrusiveness to programming. The main contribution of the paper lies in the design of an approach to program termination verification that smoothly combines types with metrics, yielding a type system capable of guaranteeing program termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic datatypes, and polymorphism.
Introduction
Programming is notoriously error-prone. As a conse-
quence, a great number of approaches have been developed
to facilitate program error detection. In practice, the programmer
often knows certain program properties that must
hold in a correct implementation; it is therefore an indication
of program errors if the actual implementation violates some
of these properties. For instance, various type systems have
been designed to detect program errors that cause violations
of the supported type disciplines.
It is common in practice that the programmer often knows
for some reasons that a particular program should terminate
if implemented correctly. This immediately implies
that a termination checker can be of great value for detecting
program errors that cause nonterminating program ex-
Partially supported by NSF grant no. CCR-0092703
ecution. However, termination checking in a realistic programming
language that supports general recursion is often
prohibitively expensive given that (a) program termination
in such a language is in general undecidable, (b) termination
checking often requires interactive theorem proving that can
be too involved for the programmer, (c) a minor change in a
program can readily demand a renewed effort in termination
checking, and (d) a large number of changes are likely to be
made in a program development cycle. In order to design a
termination checker for practical use, these issues must be
properly addressed.
There is already a rich literature on termination verifica-
tion. Most approaches to automated termination proofs for
either programs or term rewriting systems (TRSs) use various
heuristics, some of which can be highly involved, to
synthesize well-founded orderings (e.g., various path orderings
[3], polynomial interpretation [1], etc. While these
approaches are mainly developed for first-order languages,
the work in higher-order settings can also be found (e.g.,
[7]). When a program, which should be terminating if implemented
correctly, cannot be proven terminating, it is often
difficult for the programmer to determine whether this
is caused by a program error or by the limitation of the
heuristics involved. Therefore, such automated approaches
are likely to offer little help in detecting program errors that
cause nonterminating program execution. In addition, automated
approaches often have difficulty handling realistic (not
necessarily large) programs.
The programmer can also prove program termination in
various (interactive) theorem proving systems such as NuPrl
[2], Coq [4], Isabelle [8] and PVS [9]. This is a viable practice
and various successes have been reported. However, the
main problem with this practice is that the programmer may
often need to spend so much time on proving the termination
of a program compared with the time spent on simply implementing
the program. In addition, a renewed effort may
be required each time when some changes, which are likely
in a program development cycle, are made to the program.
Therefore, the programmer can often feel hesitant to adopt
(interactive) theorem proving for detecting program errors in
general programming.
We are primarily interested in finding a middle ground. In
particular, we are interested in forming a mechanism in a programming
language that allows the programmer to provide
information needed for establishing program termination
else if
withtype {i:nat,j:nat} <i,j> => int(i) -> int(j) -> [k:nat] int(k)

Figure

1. An implementation of Ackerman function
and then automatically verifies that the provided information
indeed suffices. An analogy would be like allowing the user
to provide induction hypotheses in inductive theorem proving
and then proving theorems with the provided induction
hypotheses. Clearly, the challenging question is how such
information for establishing program termination can be
formalized and then expressed. The main contribution of this
paper lies in our attempt to address the question by presenting
a design that allows the programmer to provide through
dependent types such key information in a (relatively) simple
and clean way.
It is common in practice to prove the termination of recursive
functions with metrics. Roughly speaking, we attach a
metric in a well-founded ordering to a recursive function and
verify that the metric is always decreasing when a recursive
function call is made. In this paper, we present an approach
that uses the dependent types developed in DML [18, 14] to
carry metrics for proving program termination. We form a
type system in which metrics can be encoded into types and
prove that every well-typed program is terminating. It should
be emphasized that we are not here advocating the design
of a programming language in which only terminating programs
can be written. Instead, we are interested in designing
a mechanism in a programming language, which, if the programmer
chooses to use it, can facilitate program termination
verification. This is to be manifested in that the type system
we form can be smoothly embedded into the type system of
DML. We now illustrate the basic idea with a concrete example
before going into further details.
In

Figure

1, an implementation of Ackerman function is
given. The withtype clause is a type annotation, which
states that for natural numbers i and j, this function takes
an argument of type int(i) and another argument of type
and returns a natural number as a result. Note that
we have refined the usual integer type int into infinitely
many singleton types int(a) for
such that int(a) is precisely the type for integer expressions
with value equal to a. We write fi:nat,j:natg
for universally quantifying over index variables i and j of
nat , that is, the sort for index expressions with values
being natural numbers. Also, we write [k:nat] int(k)
which represents the sum of all types
:. The novelty here is the pair hi; ji
in the type annotation, which indicates that this is the metric
to be used for termination checking. We now informally
explain how termination checking is performed in this case;
assume that i and j are two natural numbers and m and n
have types int(i) and int(j), respectively, and attach the
metric hi; ji to ack m n; note that there are three recursive
function calls to ack in the body of ack; we attach the metric
hi 1; 1i to the first ack since m 1 and 1 have types
int(i 1) and int(1), respectively; similarly, we attach the
metric hi 1; ki to the second ack, where k is assumed to
be some natural number, and the metric hi; j 1i to the third
ack; it is obvious that hi
and hi; j 1i < hi; ji hold, where < is the usual lexicographic
ordering on pairs of natural numbers; we thus claim
that the function ack is terminating (by a theorem proven in
this paper). Note that although this is a simple example, its
termination cannot be proven with (lexicographical) structural
ordering (as the semantic meaning of both addition
and subtraction is needed). 1
More realistic examples are to be presented in Section
5, involving dependent datatypes [15], mutual recursion,
higher-order functions and polymorphism. The reader may
read some of these examples before studying the sections on
technical development so as to get a feel as to what can actually
be handled by our approach.
Combining metrics with the dependent types in DML
poses a number of theoretical and pragmatic questions. We
briefly outline our results and design choices.
The first question that arises is to decide what metrics we
should support. Clearly, the variety of metrics for establishing
program termination is endless in practice. In this pa-
per, we only consider metrics that are tuples of index expressions
of sort nat and use the usual lexicographic ordering
to compare metrics. The main reasons for this decision are
that (a) such metrics are commonly used in practice to establish
termination proofs for a large variety of programs and
(b) constraints generated from comparing such metrics can
be readily handled by the constraint solver already built for
type-checking DML programs. Note that the usual structural
ordering on first-order terms can be obtained by attaching to
the term the number of constructors in the term, which can be
readily accomplished by using the dependent datatype mechanism
in DML. However, we are currently unable to capture
structural ordering on higher-order terms.
The second question is about establishing the soundness
of our approach, that is, proving every well-typed program
in the type system we design is terminating. Though the idea
mentioned in the example of Ackerman function seems intu-
itive, this task is far from being trivial because of the presence
of higher-order functions. The reader may take a look
at the higher-order example in Section 5 to understand this.
We seek a method that can be readily adapted to handle various
common programming features when they are added,
1 There is an implementation of Ackerman function that involves only
primitive recursion and can thus be easily proven terminating, but the point
we drive here is that this particular implementation can be proven terminating
with our approach.
including mutual recursion, datatypes, polymorphism, etc.
This naturally leads us to the reducibility method [12]. We
are to form a notion of reducibility for the dependent types
extended with metrics, in which the novelty lies in the treatment
of general recursion. This formation, which is novel to
our knowledge, constitutes the main technical contribution
of the paper.
The third question is about integrating our termination
checking mechanism with DML. In practice, it is common
to encounter a case where the termination of a function f depends
on the termination of another function g, which, unfor-
tunately, is not proven for various reasons, e.g., it is beyond
the reach of the adopted mechanism for termination checking
or the programmer is simply unwilling to spend the effort
proving it. Our approach is designed in a way that allows the
programmer to provide a metric in this case for verifying the
termination of f conditional on the termination of g, which
can still be useful for detecting program errors.
The presented work builds upon our previous work on the
use of dependent types in practical programming [18, 14].
While the work has its roots in DML, it is largely unclear,
a priori, how dependent types in DML can be used for establishing
program termination. We thus believe that it is a
significant effort to actually design a type system that combines
types with metrics and then prove that the type system
guarantees program termination. This effort is further
strengthened with a prototype implementation and a variety
of verified examples.
The rest of the paper is organized as follows. We form
a language ML ;
0 in Section 2, which essentially extends
the simply typed call-by-value -calculus with a form of dependent
types, developed in DML, and recursion. We then
extend ML ;to ML ;
in Section 3, combining metrics
with types, and prove that every program in ML ;
0; is termi-
nating. In Section 4, we enrich ML ;
with some significant
programming features such as datatypes, mutual recursion
and polymorphism. We present some examples in Section 5,
illustrating how our approach to program termination verification
is applied in practice. We then mention some related
work and conclude.
There is a full paper available on-line [16] in which the
reader can find details omitted here.
start with a language ML ;
0 , which essentially extends
the simply typed call-by-value -calculus with a form
of dependent types and (general) recursion. The syntax for
ML ;is given in Figure 2.
2.1 Syntax
We fix an integer domain and restrict type index expres-
sions, namely, the expressions that can be used to index a
type, to this domain. This is a sorted domain and subset sorts
can be formed. For instance, we use nat for the subset sort
0g. We use (~) for a base type indexed with
a sequence of index expressions~, which may be empty. For
instance, bool(0) and bool(1) are types for boolean values
false and true, respectively; for each integer i, int(i) is the
singleton type for integer expressions with value equal to i.
We use  satisfaction relation, which means
P holds under , that is, the formula ()P , defined below, is
satisfied in the domain of integers.
For instance, the satisfaction relation
holds since the following formula is true in the integer domain

Note that the decidability of the satisfaction relation depends
on the constraint domain. For the integer constraint domain
we use here, the satisfaction relation is decidable (as we do
not accept nonlinear integer constraints).
We use a :
: for the usual dependent
function and sum types, respectively. A type of form
: is essentially equivalent to a
where we use ~a : ~
for
n . 2 We also introduce
-variables and -variables in ML ;and use x and
f for them, respectively. A lambda-abstraction can only be
formed over a -variable while recursion (via fixed point op-
erator) must be formed over a -variable. A -variable is a
value but a -variable is not.
We use  for abstracting over index variables, lam for abstracting
over variables, and fun for forming recursive func-
tions. Note that the body after either  or fun must be a
value. We use hi j ei for packing an index i with an expression
e to form an expression of a dependent sum type, and
open for unpacking an expression of a dependent sum type.
2.2 Static Semantics
We write  '  :  to mean that  is a legally formed type
under  and omit the standard rules for such judgments.
index substitutions  I ::= [] j  I [a 7! i]
substitutions  ::= [] j [x 7! e] j [f 7! e]
A substitution is a finite mapping and [] represents an empty
mapping. We use  I for a substitution mapping index variables
to index expressions and dom( I ) for the domain of
I . Similar notations are used for substitutions on variables.
We write [ I ] ([]) for the result from applying  I
() to
, where  can be a type, an expression, etc. The standard
In practice, we also have types of form ~a : ~
: , which we omit here
for simplifying the presentation.
index constants c I ::=
index expressions i ::= a j c I j
index propositions P
index sorts
index variable contexts  ::=
index constraints  ::=
types  ::= (~)
contexts
constants c ::= true
expressions e ::= c j x
values

Figure

2. The syntax for ML ;;

Figure

3. Typing Rules for ML ;definition is omitted. The following rules are for judgments
of form  '  I :  0 , which roughly means that  I has "type"
We write dom() for the domain of , that is, the set of
variables declared in . Given substitutions  I
and , we say
We write  for the congruent extension of
index expressions to types, determined by
the following rules. It is the application of these rules that
generates constraints during type-checking.
We present the typing rules for ML ;in

Figure

3. Some
of these rules have obvious side conditions, which are omit-
ted. For instance, in the rule (type-ilam), ~a cannot have free
occurrences in . The following lemma plays a pivotal r"ole
in proving the subject reduction theorem for ML ;, whose
standard proof is available in [14].
Lemma 2.1 Assume ;  derivable and
holds. Then we can derive ; '
2.3 Dynamic Semantics
We present the dynamic semantics of ML ;through the
use of evaluation contexts defined below. Certainly, there are
other possibilities for this purpose, which we do not explore
here. 3
evaluation contexts E ::=
We write E[e] for the expression resulting from replacing
the hole [] in E with e. Note that this replacement can never
result in capturing free variables.
Definition 2.2 A redex is defined below.
are redexes for false , which reduce
to e 1 and e 2 , respectively.
(lam x : :e)(v) is a redex, which reduces to e[x 7! v].
Let e be fun f [~a : ~
e is a redex, which
reduces to ~a : ~
:v[f 7! e].
:v)[~] is a redex, which reduces to v[~a 7!~].
open hi j vi as ha j xi in e is a redex, which reduces
to e[a 7! i][x 7! v].
We use r for a redex and write r ,! e if r reduces to e. If
e, we write e 1 ,! e 2 and say
reduces to e 2 in one step.
Let ,!  be the reflexive and transitive closure of ,!. We say
reduces to e 2 (in many steps) if e 1 ,!  e 2 . We omit the
standard proof for the following subject reduction theorem,
which uses Lemma 2.1.
Theorem 2.3 (Subject Reduction) Assume ;
derivable in ML ;
derivable in ML ;2.4 Erasure
We can simply transform ML ;into a language ML 0
by erasing all syntax related to type index expressions in
. Then ML 0 basically extends simply typed -
calculus with recursion. Let jej be the erasure of expression
e. We have e 1 reducing to e 2 in ML ;
reducing
to je 2 j in ML 0 . Therefore, if e is terminating in ML ;then jej is terminating in ML 0 . This is a crucial point since
the evaluation of a program in ML ;
0 is (most likely) done
through the evaluation of its erasure in ML 0 . Please find
more details on this issue in [18, 14].
3 For instance, it is suggested that one present the dynamic semantics in
the style of natural semantics and then later form the notion of reducibility
for evaluation rules.
We combine metrics with the dependent types in ML ;,
forming a language ML ;
. We then prove that every well-typed
program in ML ;
is terminating, which is the main
technical contribution of the paper.
3.1
We use  for the usual lexicographic ordering on tuples
of natural numbers and < for the strict part of . Given
two tuples of natural numbers hi
holds if
. Evi-
dently, < is a well-founded. We stress that (in theory) there
is no difficulty supporting various other well-founded orderings
on natural numbers such as the usual multiset ordering.
We fix an ordering solely for easing the presentation.
Definition 3.1 (Metric) Let be a tuple of
index expressions and  be an index variable context. We
say  is a metric under  if  ' are derivable for
to mean  is a metric
under .
A decorated type in ML ;
0; is of form ~a : ~
the following rule is for forming such types.
The syntax of ML ;
is the same as that of ML ;except
that a context in ML ;
maps every -variable f in its domain
to a decorated type and a recursive function in ML ;
is of form fun f [~a : ~
v. The process of
translating a source program into an expression in ML ;
is
what we call elaboration, which is thoroughly explained in
[18, 14]. Our approach to program termination verification
is to be applied to elaborated programs.
3.2 Dynamic and Static Semantics
The dynamic semantics of ML ;
is formed in precisely
the same manner as that of ML ;
0 and we thus omit all the
details.
The difference between ML ;
and ML ;lies in static
semantics. There are two kinds of typing judgments in
ML ;, which are of forms
0 . We call the latter a metric typing judgment, for which
we give some explanation. Suppose
and
roughly speaking, for each
free occurrence of f in e, f is followed by a sequence of
index expressions [~] such that [~a 7! ~], which we call
the label of this occurrence of f , is less than  0 under .
Now suppose we have a well-typed closed recursive function
0; and~ are of sorts ~
then f [~][f 7! holds; by the
rule (type-fun), we know that all labels of f in v are less than
[~a 7!~], which is the label of f in f [~]; since labels cannot
decrease forever, this yields some basic intuition on why all
recursive functions in ML ;
are terminating. However, this
intuitive argument is difficult to be formalized directly in the
presence of high-order functions.
The typing rules in ML ;
for a judgment of form ; '
are essentially the same as those in ML ;except the
following ones.
We present the rules for deriving metric typing judgments in

Figure

4. Given
means that for some 1  k <
are satisfied for all 1  j < k
is also satisfied.
Lemma 3.2 We have the following.
1. Assume ;
holds. Then we can derive ; '
2. Assume ;  derivable and
dom(). Then
we can derive
Proof (1) and (2) are proven simultaneously by structural
induction on derivations of ;
Theorem 3.3 (Subject Reduction) Assume ;
derivable in ML ;
0; . If e ,!  e 0 , then ;  ' e
derivable in ML ;
Obviously, we have the following.
Proposition 3.4 Assume that D is a derivation ;
f  0 . Then then there is a derivation of ;
with the same height 4 as D.
3.3 Reducibility
We define the notion of reducibility for well-typed closed
expressions.
Definition 3.5 (Reducibility) Suppose that e is a closed expression
of type  and e ,!  v holds for some value v. The
reducibility of e is defined by induction on the complexity of
.
4 For a minor technicality reason, we count neither of the rules
(type-var) and (-var) when calculating the height of a derivation.
1.  is a base type. Then e is reducible.
2. are reducible
for all reducible values v 1 of type  .
3.
reducible if e[~] are reducible
4.
some i and v 1 such that v 1 is a reducible value of type
Note that reducibility is only defined for closed expressions
that reduce to values.
Proposition 3.6 Assume that e is a closed expression of type
and e ,! e 0 holds. Then e is reducible if and only if e 0 is
reducible.
Proof By induction on the complexity of  .
The following is a key notion for handling recursion,
which, though natural, requires some technical insights.
Definition 3.7 (-Reducibility). Let e be a well-typed closed
recursive function fun f [~a : ~
be a
closed metric. e is  0 -reducible if e[~] are reducible for all
satisfying [~a 7!~] <  0 .
Definition 3.8 Let  be a substitution that maps variables to
expressions; for every x 2 dom(),  is x-reducible if (x)
is reducible; for every f 2 dom(),  is (f;  f )-reducible if
(f) is  f -reducible.
In some sense, the following lemma verifies whether the
notion of reducibility is formed correctly, where the difficulty
probably lies in its formulation rather than in its proof.
Lemma 3.9 (Main Lemma) Assume that ; ' e :  and
are derivable. Also assume that
is x-reducible for every x 2 dom() and for every f 2
derivable and
is (f;  f )-reducible. Then e[ I ][] is reducible.
Proof Let D be a derivation of ; ' e :  and we proceed
by induction on the height of D. We present the most
interesting case below. All other cases can be found in [16].
Assume that the following rule (type-fun) is last applied in
D,
where we have
and
Suppose that e I ][] is
not reducible. Then by definition there exist ~
1 such
that e  [~ 0 ] is not reducible but e  [~] are reducible for all
satisfying
~
In other words, e  is  f1 -
reducible for
that we can derive

Figure

4. Metric Typing Rules for ML ;
. By Proposition 3.4, there is a derivation D 1 of
such that the
height of D 1 is less than that of D. By induction hypothesis,
we have that v
Note that e  [~ 0 ] ,!  v and thus e  [~ 0 ] is reducible, contradicting
the definition of~ 0 . Therefore, e  is reducible.
The following is the main result of the paper.
Corollary 3.10 If ;  ' e :  is derivable in ML ;
in ML ;
is reducible and thus reduces to a value.
Proof The corollary follows from Lemma 3.9.
Extensions
We can extend ML ;
with some significant programming
features such as mutual recursion, datatypes and poly-
morphism, defining the notion of reducibility for each extension
and thus making it clear that Lemma 3.9 still holds
after the extension. We present in this section the treatment
of mutual recursion and currying, leaving the details in [16].
4.1 Mutual Recursion
The treatment of mutual recursion is slightly different
from the standard one. The syntax and typing rules for
handling mutual recursion are given in Figure 5. We use
the type of an expression representing n mutually
recursive functions of types  respectively,
which should not be confused with the product of types
. Also, the n in e:n must be a positive (constant)
integer. Let v be the following expression.
funs
Then for every 1  k  n, v:k is a redex, which reduces to
and we form a metric typing judgment ; ' e  ~
f
0 for
verifying that all labels of f in e are less than  0 under
. The rules for deriving such a judgment are essentially
the same as those in Figure 4 except (-lab), which is given
below.
f in ~
f
The rule (-funs) for handling mutual recursion is straight-forward
and thus omitted.
Definition 4.1 (Reducibility) Let e be a closed expression of
reduces to v. e is reducible if e:k are
reducible for
4.2 Currying
A decorated type must so far be of form ~a : ~
and this restriction has a rather unpleasant consequence. For
types  ::=    j
expressions e ::=    j e:n j funs f 1
values v ::=    j funs f 1
~
f
f
(type-funs)

Figure

5. The Syntax and Typing Rules for Mutual Recursion
instance, we may want to assign the following type  to the
implementation of Ackerman function in Figure 1:
fi:natg int(i) -> fj:natg int(j) -> int;
which is formally written as
If we decorate  with a metric , then  can only involve
the index variable a 1 , making it impossible to verify that the
implementation is terminating.
We generalize the form of decorated types to the following
so as to address the problem.
Also, we introduce the following form of expression e for
representing a recursive function.
We require that e 0 be a value if In the following, we
only deal with the case 1. For n > 1, the treatment is
similar. For
have e ,!
:e 0 and the following
typing rule
, and the following
metric typing rule
Definition 4.2 (-reducibility) Let e be a closed recursive
function
a closed metric. e is  0 -reducible if e[~ 1 ](v)[~] are reducible
for all reducible values
1 and
5 Practice
We have implemented a type-checker for ML ;
in a prototype
implementation of DML and experimented with various
examples, some of which are presented below. We also
address the practicality issue at the end of this section.
5.1 Examples
We demonstrate how various programming features are
handled in practice by our approach to program termination
verification.
Primitive Recursion The following is an implementation
of the primitive recursion operator R in Godel's T , which is
clearly typable in ML ;
. Note that Z and S are assigned
the types Nat(0) and
respectively.
datatype Nat with
Z(0) | {n:nat} S(n+1) of Nat(n)
u | R (S n) u (R n u v)
withtype
{n:nat}   =>
(* Nat is for [n:nat] Nat(n) in a type *)
By Corollary 3.10, it is clear that every term in T is terminating
(or weakly normalizing). This is the only example in
this paper that can be proven terminating with a structural
ordering. The point we make is that though it seems
"evident" that the use of R cannot cause non-termination, it
is not trivial at all to prove every term in T is terminating.
Notice that such a proof cannot be obtained in Peano
arithmetic. The notion of reducibility is precisely invented
for overcoming the difficulty [12]. Actually, every term in
T is strongly normalizing, but this obviously is untrue in
0; .
Nested Recursive Function Call The program in Figure 6
involving a nested recursive function call implements Mc-
Carthy's ``91'' function. The withtype clause indicates
that for every integer x, f91(x) returns integer 91 if x  100
We informally explain why the
metric in the type annotation suffices to establish the termination
of f91; for the inner call to f91, we need to prove that
for which is obvious; for the outer
call to f91, we need to verify that  1
and max(0; 101 assumed
in ). Clearly, this example can not be handled with a
structural ordering.
Mutual Recursion The program in Figure 7 implements
quicksort on a list, where the functions qs and par are defined
mutually recursively. We informally explain why this
program is typable in ML ;
0; and thus qs is a terminating
function by Corollary 3.10.
For the call to par in the body of qs, the label is (0
1), where a is the length of xs 0 . So we need to
verify that  is satisfied for
obvious.
For the two calls to qs in the body of par, we need to
verify that
of which hold since
This also indicates why we need r
of r in the metric for par.
For the two calls to par in the body of par, we need
to verify that
and
both of
which hold since
this example can not be handled with a structural ordering.
Higher-order Function The program in Figure 8 implements
a function accept that takes a pattern p and a string
s and checks whether s matches p, where the meaning of a
pattern is given in the comments.
The auxiliary function acc is implemented in continuation
passing style, which takes a pattern p, a list of characters
cs and a continuation k and matches a prefix of cs
against p and call k on the rest of characters. Note that k
is given a type that allows k to be applied only to a character
list not longer than cs. The metric used for proving
the termination of acc is hn; ii, where n is the size of p,
that is the number constructors in p (excluding Empty) and
i is the length of cs. Notice the call acc p cs 0 k in the
last pattern matching clause; the label attached to this call is
is the length of cs 0 ; we have i 0  i since the
continuation has the type a
where
must be false when this call hap-
pens; therefore we have It
is straightforward to see that the labels attached to other calls
to acc are less than hn; ii. By Corollary 3.10, acc is termi-
nating, which implies that accept is terminating (assuming
explode is terminating). In every aspect, this is a non-trivial
example even for interactive theorem proving systems.
Notice that the test length(cs 0 in the body
of acc can be time-consuming. This can be resolved by using
a continuation that accepts as its arguments both a character
list and its length. In [5], there is an elegant implementation
of accept that does some processing on the pattern to be
matched and then eliminates the test.
Run-time Check There are also realistic cases where termination
depends on a program invariant that cannot (or is difficult
to) be captured in the type system of DML. For instance,
the following example is adopted from an implementation of
bit reversing, which is a part of an implementation of fast
Fourier transform (FFT).
fun loop (j,
if (k<j) then loop (j-k, k/2) else j+k
withtype
{a:nat,b:nat} int(a) * int(b) -> int
Obviously, loop(1; 0) is not terminating. However, we may
know for some reason that the second argument of loop can
never be 0 during execution. This leads to the following im-
plementation, in which we need to check that k > 1 holds
before calling loop(j k; k=2) so as to guarantee that k=2 is
a positive integer.
fun loop (j,
else raise Impossible
withtype {a:nat,b:pos} <max(0, a-b)> =>
int(a) * int(b) -> int
It can now be readily verified that loop is a terminating func-
tion. This example indicates that we can insert run-time
checks to verify program termination, sometimes, approximating
a liveness property with a safety property.
5.2 Practicality
There are two separate issues concerning the practicality
of our approach to program termination verification, which
are (a) the practicality of the termination verification process
and (b) the applicability of the approach to realistic programs

5 Note that length(cs 0 ) and length(cs) have the types int(i 0 ) and
int(i), respectively, and thus length(cs has the type
depending on whether i 0 equals i.
Thus, can be inferred in the type system.
withtype

Figure

6. An implementation of McCarthy's ``91'' function
case xs of [] => [] | x :: xs' => par cmp (x, [], [], xs')
withtype ('a * 'a -> bool) -> {n:nat} <n,0> => 'a list(n) -> 'a list(n)
and('a) par cmp (x, l, r,
case xs of
| x' :: xs' => if cmp(x', x) then par cmp (x, x' :: l, r, xs')
else par cmp (x, l, x' :: r, xs')
withtype ('a * 'a -> bool) -> {p:nat,q:nat,r:nat} <p+q+r,r+1> =>
'a * 'a list(p) * 'a list(q) * 'a list(r) -> 'a list(p+q+r+1)

Figure

7. An implementation of quicksort on a list
It is easy to observe that the complexity of type-checking
in ML ;
is basically the same as in ML ;since the only
added work is to verify that metrics (provided by the pro-
are decreasing, which requires solving some extra
constraints. The number of extra constraints generated from
type-checking a function is proportional to the number of recursive
calls in the body of the function and therefore is likely
small. Based on our experience with DML, we thus feel that
type-checking in ML ;
is suitable for practical use.
As for the applicability of our approach to realistic pro-
grams, we use the type system of the programming language
C as an example to illustrate a design decision. Obviously,
the type system of C is unsound because of (unsafe) type
casts, which are often needed in C for typing programs that
would otherwise not be possible. In spite of this practice, the
type system of C is still of great help for capturing program
errors. Clearly, a similar design is to allow the programmer
to assert the termination of a function in DML if it cannot be
verified, which we may call termination cast. Combining termination
verification, run-time checks and termination cast,
we feel that our approach is promising to be put into practice.
6 Related Work
The amount of research work related to program termination
is simply vast. In this section, we mainly mention some
related work with which our work shares some similarity either
in design or in technique.
Most approaches to automated termination proofs for either
programs or term rewriting systems (TRSs) use various
heuristics to synthesize well-founded orderings. Such ap-
proaches, however, often have difficulty reporting comprehensible
information when a program cannot be proven ter-
minating. Following [13], there is also a large amount of
work on proving termination of logic programs. In [11], it is
reported that the Mercury compiler can perform automated
termination checking on realistic logic programs.
However, we address a different question here. We are
interested in checking whether a given metric suffices to establish
the termination of a program and not in synthesizing
such a metric. This design is essentially the same as the
one adopted in [10], where it checks whether a given structural
ordering (possibly on high-order terms) is decreasing in
an inductive proof or a logic program. Clearly, approaches
based on checking complements those based on synthesis.
Our approach also relates to the semantic labelling approach
[19] designed to prove termination for term rewriting
systems (TRSs). The essential idea is to differentiate
function calls with labels and show that labels are always
decreasing when a function call unfolds. The semantic labelling
approach requires constructing a model for a TRS to
verify whether labelling is done correctly while our approach
does this by type-checking.
The notion of sized types is introduced in [6] for proving
the correctness of reactive systems. There, the type system
is capable of guaranteeing the termination of well-typed
programs. The language presented in [6], which is designed
for embedded functional programming, contains a significant
restriction as it only supports (a minor variant) of primitive
recursion, which can cause inconvenience in programming.
For instance, it seems difficult to implement quicksort by using
only primitive recursion. From our experience, general
recursion is really a major programming feature that greatly
complicates program termination verification. Also, the notion
of existential dependent types, which we deem indispensable
in practical programming, does not exist in [6].
When compared to various (interactive) theorem proving
datatype pattern with
string matches Empty *)
| Char(1) of char (* "c" matches Char (c) *)
| {i:nat,j:nat} Plus(i+j+1) of pattern(i) * pattern(j)
(* cs matches Plus(p1, p2) if cs matches either p1 or p2 *)
| {i:nat,j:nat} Times(i+j+1) of pattern(i) * pattern(j)
(* cs matches Times(p1, p2) if a prefix of cs matches p1 and
the rest matches p2 *)
| {i:nat} Star(i+1) of pattern(i)
(* cs matches Star(p) if cs matches some, possibly 0, copies of p *)
(* 'length' computes the length of a list *)
length
| len
withtype
in
len (xs,
withtype {i:nat} <> => 'a list(i) -> int(i)
(* empty tuple <> is used since 'length' is not recursive *)
case p of
Empty => k (cs)
| Char(c) =>
(case cs of
| c' :: cs' => if
| Plus(p1, p2) => (* in this case, k is used for backtracking *)
if acc p1 cs k then true else acc p2 cs k
| Times(p1, p2) => acc p1 cs (fn cs' => acc p2 cs'
|
if k (cs) then true
else acc p0 cs (fn cs' =>
else acc p cs'
withtype {n:nat} pattern(n) ->
{i:nat} <n, i> => char list(i) ->
({i':nat | i' <= i} char list(i') -> bool) -> bool
(* 'explode' turns a string into a list of characters *)
withtype <> => pattern -> string -> bool

Figure

8. An implementation of pattern matching on strings
systems such as NuPrl [2], Coq [4], Isabelle [8] and PVS [9],
our approach to program termination is weaker (in the sense
that [many] fewer programs can be verified terminating) but
more automatic and less obtrusive to programming. We have
essentially designed a mechanism for program termination
verification with a language interface that is to be used during
program development cycle. We consider this as the main
contribution of the paper. When applied, the designed mechanism
intends to facilitate program error detection, leading
to the construction of more robust programs.
7 Conclusion and Future Work
We have presented an approach based on dependent types
in DML that allows the programmer to supply metrics for
verifying program termination and proven its correctness.
We have also applied this approach to various examples that
involve significant programming features such as a general
form of recursion (including mutual recursion), higher-order
functions, algebraic datatypes and polymorphism, supporting
its usefulness in practice.
A program property is often classified as either a safety
property or a liveness property. That a program never performs
out-of-bounds array subscripting at run-time is a safety
property. It is demonstrated in [17] that dependent types in
DML can guarantee that every well-typed program in DML
possesses such a safety property, effectively facilitating run-time
array bound check elimination. It is, however, unclear
(a priori) whether dependent types in DML can also be used
for establishing liveness properties. In this paper, we have
formally addressed the question, demonstrating that dependent
types in DML can be combined with metrics to establish
program termination, one of the most significant liveness
properties.
Termination checking is also useful for compiler opti-
mization. For instance, if one decides to change the execution
order of two programs, it may be required to prove
that the first program always terminates. Also, it seems feasible
to use metrics for estimating the time complexity of
programs. In lazy function programming, such information
may allow a compiler to decide whether a thunk should be
formed. In future, we expect to explore along these lines of
research.
Although we have presented many interesting examples
that cannot be proven terminating with structural orderings,
we emphasize that structural orderings are often effective in
practice for establishing program termination. Therefore, it
seems fruitful to study a combination of our approach with
structural orderings that handles simple cases with either automatically
synthesized or manually provided structural orderings
and verifies more difficult cases with metrics supplied
by the programmer.



--R

Termination of rewriting systems by polynomial interpretations and its implementation.
Implementing Mathematics with the NuPrl Proof Development System.
Orderings for term rewriting systems.


Proving the correctness of reactive systems using sized types.
The higher-order recursive path ordering
A Generic Theorem Prover.
PVS: Combining specification
Termination and Reduction Checking in the Logical Framework.
Termination Analysis for Mercury.
Intensional Interpretations of Functionals of Finite Type I.
Efficient tests for top-down termination of logic rules
Dependent Types in Practical Programming.
Dependently Typed Data Structures.
Dependent Types for Program Termination Verifica- tion
Eliminating array bound checking through dependent types.
Dependent types in practical program- ming
Termination of term rewriting by semantic la- belling
--TR

--CTR
Kevin Donnelly , Hongwei Xi, A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.5, p.109-125, June, 2007
Chiyan Chen , Hongwei Xi, Combining programming with theorem proving, ACM SIGPLAN Notices, v.40 n.9, September 2005
Kevin Donnelly , Hongwei Xi, Combining higher-order abstract syntax with first-order abstract syntax in ATS, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.58-63, September 30-30, 2005, Tallinn, Estonia
Amir M. Ben-Amram , Chin Soon Lee, Program termination analysis in polynomial time, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.1, p.5-es, January 2007
Arne John Glenstrup , Neil D. Jones, Termination analysis and specialization-point insertion in offline partial evaluation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1147-1215, November 2005
dependent types;termination