Least and greatest fixed points in intuitionistic natural deduction.
This paper is a comparative study of a number of (intensional-semantically distinct) least and greatest fixed point operators that natural-deduction proof systems for intuitionistic logics can be extended with in a proof-theoretically defendable way. Eight pairs of such operators are analysed. The exposition is centred around a cube-shaped classification where each node stands for an axiomatization of one pair of operators as logical constants by intended proof and reduction rules and each arc for a proof- and reduction-preserving encoding of one pair in terms of another. The three dimensions of the cube reflect three orthogonal binary options: conventional-style vs. Mendler-style, basic ("[co]iterative") vs. enhanced ("primitive-[co]recursive"), simple vs. course-of-value [co]induction. Some of the axiomatizations and encodings are well known; others, however, are novel; the classification into a cube is also new. The differences between the least fixed point operators considered are illustrated on the example of the corresponding natural number types.
Introduction
This paper is a comparative study of a number of least and greatest xed point
operators, or inductive and coinductive denition operators, that natural-
deduction (n.d.) proof systems for intuitionistic logics (typed lambda calculi
with product and sum types) can be extended with as logical constants
(type-language constants), either by an axiomatization by intended proof and
reduction rules (\implicit denition") or by a proof- and reduction-preserving
encoding in terms of some logical constants already present (\explicit deni-
tion"). One of the reasons why such logical or type-language constants are
interesting lies in their useful programming interpretation: inductive types
behave as data types, their introductions as data constructors and eliminations
as recursors; coinductive types may be viewed as codata types, their
introductions as corecursors and eliminations as codata destructors. In the
literature, a fairly large number of axiomatizations and encodings of both
particular [co]inductively dened types and general [co]inductive denition
operators can be found, see e.g., [1,14,19,20,24,25,15,7]. The paper grew out
of a wish to better understand their individual properties and their relations
to each other.
The contribution of the paper consists in a coordinated analysis of eight
intensional-semantically distinct pairs of [co]inductive denition operators, arranged
into a cube-shaped taxonomy, which resulted from an attempt to t
the various known axiomatizations and encodings into a single picture and to
nd llers for the holes. Each node of the cube stands for an axiomatization
by proof and reduction rules of one pair of logical constants and each arc for
a proof- and reduction-preserving encoding of one pair in terms of another.
Some axiomatizations and encodings rely on the presence in the system of certain
other logical constants (the standard propositional connectives, 2nd-order
quantiers, or a \retractive" recursive denition operator ). The three dimensions
of the cube re
ect three orthogonal binary choices: conventional-style vs.
Mendler-style, basic (\[co]iterative") vs. enhanced (\primitive-[co]recursive"),
simple vs. course-of-value [co]induction.
The cube looks as follows:
q
and  (with optional superscripts) are conventional-style inductive and coinductive
denition operators; m and n (with optional superscripts) are Mendler-
style operators. The superscript ' q ' marks the \enhanced" feature, the superscript
indicates the \course-of-value" feature.
The distinctions between basic and enhanced, simple and course-of-value [co]in-
duction are distinctions between essentially dierent forms of [co]induction,
with dierent associating schemes of (total) [co]recursion. Basic [co]induction
gives [co]iteration, enhanced [co]induction gives (full) primitive [co]recursion.
All axiomatizations and encodings we have found in the literature deal with
simple forms of [co]induction. The axiomatizations and encodings for course-
of-value [co]induction in this paper are ours, we think.
The dierence between conventional- and Mendler-style [co]induction (named
after Mendler [19,20]) is more technical and harder to spell out informally,
but not shallow. A conventional-style [co]inductive denition operator applies
to a proposition-function only if it is positive; the associating reduction rule
refers then to a proof of its monotonicity (all positive proposition-functions
are monotonic wrt the preorder of inclusion). Mendler-style operators apply
to any proposition-functions. The axiomatizations of enhanced and course-of-
value conventional-style operators rely on the presence in the system of other
logical constants, those of Mendler-style operators do not. Thus, in more than
one sense, Mendler-style operators are more uniform than conventional-style
operators; resorting to programming jargon, one might for instance want to
say that the Mendler-style operators are generic, whereas the conventional-
style ones are only polytypic. These uniformity features have a price
the proof rules of the Mendler-style operators involve implicit (\external")
2nd-order quantication at the level of premisses.
Throughout the paper, the semantics that we keep in mind is intensional, so
we only consider -reduction, not -conversion.
Some remarks are in order regarding the technical machinery that we use.
By natural deduction, we mean a proof system style where instead of axioms
involving implications and universal quantications we systematically prefer
to have proof rules involving hypothetical and schematic judgements (\exter-
nalized" implications and universal quantications), in sharp contrast to the
Hilbert style of proof systems. For us therefore, natural deduction is really
the \extended" natural deduction of Schroeder-Heister [30,31]: we allow proof
rules to be of order higher than two: not only may conclusions have premisses
and these have premisses in their turn, but even the latter may be hypo-
thetical. This choice makes axiomatizations of dierent logical constants very
compact, but on the expense of certain added complexity in their encodings
in terms of other logical constants.
In order to compactify the notation and to get around the technicalities related
to -conversion and substitution, we use a simple meta-syntax, a higher-oder
abstract syntax derived from logical frameworks such as de Bruijn's AUT-PI
and AUT-QE [5], Martin-Lof's system of arities [22, chapter 3], and Harper,
Honsell, and Plotkin's LF [12]. denotes the schematization of
s wrt. x denotes the instantiation of s with
Schematization and instantiation are stipulated to satisfy the following rules:
are not free
in s, then
We have made an eort to make the paper self-contained; for the omitted
details, we refer to Uustalu [35]. A preliminary report of the present work
appeared as [37]. We also refer to Matthes [17], an in-depth study of extensions
of system F with constructors of basic and enhanced conventional- and
Mendler-style inductive types, which in regard to the clarication of the relationship
between the conventional- and Mendler-style induction builds partly
upon our work.
The paper is organized as follows. In section 2, we lay down our starting point:
it is given by systems that we denote NI and NI 2 , the n.d. proof systems
for 1st- and 2nd-order intuitionistic propositional logics, optionally extended
with a \retractive" recursive denition operator . Then, in section 3, we rst
present the basic [co]induction operators, both in conventional and Mendler-
style and then continue with their encodings in terms of the 2nd-order quan-
tiers and each other. In sections 4 and 5, we describe enhanced [co]induction
and course-of-value [co]induction operators respectively and their encodings
via the operators of the basic kind. In section 6, we give a survey of related
work on inductive and coinductive types. Finally, in section 7, we conclude
and mention some directions for future work.
Preliminaries
In principle, the [co]inductive denition operators described below can be
added to the n.d. proof system of any intuitionistic propositional logic. (They
also admit a straightforward generalization for predicate logics.) The most
natural base system for such extensions however is NI, the standard n.d.
proof system for (full) 1st-order intuitionistic propositional logic. The logical
constants of NI are ^ (conjuction), _ (disjunction), > (verum), ? (falsum),
and ! (implication). These propositional connectives are axiomatized by the
proof and reduction rules listed in Figure 1. (To save space, the reduction rules
are given not for proofs, but for (untyped) term codes of proofs; the reduction
rules for proofs are easy to recover. The reduction relation on terms satises
subject reduction.)
^I
_I L
e
(c)  e   c(e)

Figure

1: Proof and reduction rules for standard propositional connectives.
Another important base system is NI 2 , the n.d. proof system for 2nd-order
intuitionistic propositional logic. This system extends NI with 8 2 and 9 2 , the
standard 2nd-order quantiers. The proof rules for 8 2 and 9 2 are presented in

Figure

2.
In the encodings of enhanced [co]induction in terms of basic [co]induction,
we shall need a logical constant , a \retractive" recursive denition oper-
ator. This is a proposition-valued operator on proposition-functions that are
positive. The proof and reduction rules for  appear in Figure 3. The introduction
and elimination rules for  behave as an embedding-retraction pair. The
c  c
e(c)  e(c)

Figure

2: Proof and reduction rules for 8 2 , 9 2 .
extensions of NI and NI 2 with  will be denoted by NI() and NI 2 ().
Of importance for us is the fact that NI 2 () is strongly normalizing (i.e.,
every proof of NI 2 () is strongly normalizing); consult Mendler [19,20] and
Urzyczyn [34].

Figure

3: Proof and reduction rules for .
The syntactic concepts of positivity and negativity of proposition-functions
are system-dependent. For any particular system, these concepts are dened
by mutual structural induction on proposition-functions denable in this sys-
tem. In NI and its extensions considered in this paper, a proposition-function
(X)F is dened to be positive [negative] if every occurrence of X in F appears
within an even [odd] number of antecedents of implications. Also for
any particular system and by a similar induction, explicit denitions can be
given for the derivable proof rules M and M + establishing that positive [neg-
ative] proposition-functions are monotonic [antimonotonic] wrt. the preorder
of proposition inclusion. These proof rules appear in Figure 4.
F
F positive F negative

Figure

4: Derivable proof rules M and M + .
As an example, we shall consider the proposition-function N dened by setting
N is obviously positive. The corresponding monotonicity witness map
N is dened
as follows:
3 Basic [co]induction
The logical constants from the two lower front nodes of the cube provide the
most fundamental forms of [co]inductive denition of propositions, viz. the
basic (in other words, \[co]iterative") forms of conventional- and Mendler-style
[co]inductive denition.  and  are operators of conventional-style induction
and coinduction and apply to positive proposition-functions
are their Mendler-style counterparts applicable without restrictions to any
proposition-functions. Their proof and reduction rules are given in Figures 5
and 6. The proof rules for m and n are more complex than those for  and
, but their reduction rules, in compensation, are simpler and more uniform:
their right-hand sides do not refer to the M + proof rule.
e(
cata F
cata F (wrap F (c); e)   e(map
F
()cata F (; e)))
e(
open
open F (ana F (c; e))   map
F

Figure

5: Proof and reduction rules for  and .
e(
e(

Figure

Proof and reduction rules for m and n.
From the algebraic semantics point of view, F is a least prexed point of F
wrt. the inclusion preorder of propositions: it is both itself a prexed point
of F (by the I-rule) and a lower bound of the set of all prexed points of F
(by the E-rule). (Recall that R is said to be a prexed point of F , if F (R)
is less than R.) F , dually, is a greatest postxed point of F . 3 Since a least
prexed [postxed] point of a monotonic function is also its least
xed point, F and F are also least and greatest xed points of F .
In a similar fashion, mF can be thought of as a least robustly prexed point
of F : it is both itself a robustly prexed point of F and a lower bound of all
robustly prexed points of F . Here, R is considered to be a robustly prexed
point of F , if not only is F (R) less than R, but F (Y ) is less than R for all
Y 's less than R. But mF is also a least (ordinary) prexed point of a function
sending any R to a supremum of the
set of all F (Y )'s such that Y is less than R. F e (which is always positive)
appears to be a least monotonic majorant of F wrt. the pointwise \lifting" of
the inclusion preorder of propositions to a preorder of proposition-functions.
If F is monotonic, then F and F e are equivalent (pointwise). The dualization
is obvious: nF is a greatest robustly postxed point of F and a greatest
(ordinary) postxed point of a function F a [F a (R)  8 2 ((Y )(R!Y )!F (Y ))]
sending any R to an inmum of the set of all F (Y )'s such that Y is greater
than R.
Under the programming interpretation, F is a data type, with wrap F a data
constructor and cata F an iterator, and F is a codata type, with ana F a
coiterator and open F a codata destructor, in the most standard sense. mF ,
with mapwrap and iter, and nF , with coit and mapopen, are Mendler-style
versions of these things. This is best explained on an example.
The type of standard natural numbers Nat, with zero and succ the constant
zero and the successor function and natcata the iterator, is normally axiomatized
as follows:
These typing and reduction rules are essentially nothing else than those for
3 Note here that, in a preorder (also in a Heyting algebra), it may turn out that
all monotonic functions have least [greatest] prexed [postxed] points; hence allowing
and  to apply to any positive F should not lead to inconsistencies (the
encodability of ,  in terms of 8 2 , 9 2 demonstrates that this is the case indeed).
conventional basic induction with N as the underlying proposition-function.
Indeed, making the following denitions ensures the required typing and reduction
properties:
Nat  (N)
zero  wrap N (inl(hi))
succ(c)  wrap N (inr(c))
This suggests a similar specialization of Mendler-style basic induction for N
by the following denitions:
Nat  m(N)
mapzero(d)  mapwrap(inl(hi); d)
d)  mapwrap(inr(c); d)
The type Nat of Mendler-style natural numbers, with mapzero, mapsucc and
natiter the Mendler-style constant zero, successor function, and iterator, obeys
the following typing and reduction rules.
Here, it may be helpful to think of Q as some chosen type of representations
for naturals and d as a method for converting representations of this type to
naturals. A natural, hence, is constructed from nothing or a representation
(for its predecessor), together with a method for converting representations to
naturals. Using Nat as Q, the standard constructors of naturals are denable
as follows:
zero  mapzero(())
succ(c)  mapsucc(c; ())
natcata and natiter are iterators. Iteration is a very simple form of total re-
cursion: the result of an iteration on a given natural is only dependent of the
result on the predecessor. If the \straightforward" denition of a function follows
some more complex form of recursion, then denitions by iteration can
get clumsy. The factorial of a given natural, for instance, depends not only
on the factorial of its predecessor, but also on the predecessor itself. An iterative
denition of the factorial has to dene both the factorial and the identity
function \in parallel" and then project the factorial component out.

zero


zero

Exactly the same trick of \tupling" is also needed to program the Fibonacci
function: the Fibonacci of a given natural number depends not only on the
Fibonacci of its predecessor, but also on the Fibonacci of its pre-predecessor.
An iterative denition of Fibonacci has to dene both Fibonacci and the \one-
step-behind Fibonacci" \in parallel".
bo(c)  fst(natcata(c;

zero;

case@ snd(
bo(c)  fst(natiter(c; (-)

zero;

case@ snd(-(
These examples show how other forms of recursion can be captured by iteration
using \tupling". Such modelling is not without drawbacks, however.
First, it is more transparent to dene a function using its \native" form of re-
cursion. Second, the intensional behavior of iterative denitions is not always
satisfactory. It is well known, for instance, that the predecessor function can
be programmed using iteration, but the programs take linear time to compute
(and only work as desirable on numerals, i.e., closed natural number terms).
pred(c)  cata N (c; (
pred(c)  iter(c; (
The more complex forms of induction considered in the following sections
remedy these problems by oering more advanced forms of recursion.
Basic [co]induction vs. 2nd-order quantiers
Both ,  and m, n can be encoded in terms of 8 2 , 9 2 in a proof- and reduction-
preserving manner.
Proposition 1 The following is a proof- and reduction-preserving encoding
of ,  in terms of 8
F (c)  (()  map
cata
F
ana
F
open
F (c)  map
F (fst(c)  snd(c); ()hfst(c); i)
This encoding is a proof theory recapitulation of the Knaster{Tarski xed
point theorem [33] stating that an inmum [supremum] of the set of all prexed
[postxed] points of a monotonic function is its least [greatest] prexed
[postxed] point. In its general form, the encoding seems to be a piece of folk-
lore. For the special case of \polynomial" proposition-functions (such as N),
essentially the same encoding was rst given by Bohm and Berarducci [1] and
Leivant [14]. For naturals, our encoding specializes to the following:
Nat
zero
natcata
(In Bohm and Berarducci's encoding, Nat
zero
c  e z  e s .)
Proposition 2 The following is a proof- and reduction-preserving encoding
of m, n in terms of 8
iter
coit
mapopen
This encoding builds on the following robust analog of the Knaster-Tarski
xed point theorem: an inmum [supremum] of the set of all robustly prexed
[postxed] points of any function (monotonic or not) is its least [greatest]
robustly prexed [postxed] point.
Corollary 3 NI 2 () (and also its any fragment, including NI) extended
with operators ;  or m; n is strongly normalizing and con
uent.
Mendler-style vs. conventional [co]induction
It is also possible to encode ,  in terms of m, n and vice versa. For the
encoding in the latter direction, 8 2 , 9 2 have to be available.
Proposition 4 The following is a proof- and reduction-preserving encoding
of ,  in terms of m, n:
F (c)  mapwrap(c; ())
cata
ana
F (e(
open
F
(c)  mapopen(c; ())
Proposition 5 The following is a proof- and reduction-preserving encoding
of m, n in terms of ,  in the presence of 9 2 ,
iter
F a (R)  8 2 ((Y )(R!Y )!F (Y
coit
mapopen d)  open F a(c)  (d)
The encoding of m, n in terms of ,  is a proof-theoretic version of the
observation that a least [greatest] prexed [postxed] point of F e [F a ] is a
least [greatest] robustly prexed [postxed] point of F .
Enhanced [co]induction
The logical constants from the two upper front nodes of the cube capture the
enhanced (in other words, \primitive-[co]recursive") forms of conventional-
and Mendler-style [co]inductive denition.  q and  q are operators of enhanced
induction and coinduction; m q and n q are their Mendler-style counterparts.
Their proof and reduction rules are given in Figures 7 and 8. Adding  q ,  q
to a proof system presupposes the presence of ^, _; there is no corresponding
restriction governing the addition of m q , n q .
q I
e(
para F (wrap q

para F (fst(); e);
e(
(R _  q
open q
open q

Figure

7: Proof and reduction rules for  q and  q .
From the algebraic semantics point-of-view,  q F is a least \recursive" prexed
point of a given (necessarily monotonic) F , i.e., a least element of the set of
all R's such that F (R ^  q F ) is less than R (note the recurrent occurrence of
q F here!).  q F is a greatest \recursive" postxed point of F .
is a least \recursive" robustly prexed point of a given F , ie., a least
element of the set of all R's such that F (Y ) is less than R for all Y 's less
than not only R but also m q F (note again the circularity!). n q F , dually, is a
greatest \recursive" robustly postxed point of F .
For programming,  q F is a \recursive" data type, with wrap q
F a \recursive"
data constructor and para F a primitive recursor, and  q F is a \recursive"
codata type, with apo F a primitive corecursor and open q
F a \recursive" codata
e(
rec(mapwrap q (c; d; i); e)   e(c; ()rec(d(); e); ()i())
e(
mapopen q (c; d;
mapopen q (cor(c; e); d; i)   e(c; ()d(cor(; e)); ()i())

Figure

8: Proof and reduction rules for m q and n q .
destructor. m q F , with mapwrap q and rec, and n q F , with cor and mapopen q , are
their Mendler-style equivalents.
Returning to our running example of naturals, specializing enhanced induction
for N yields the type Nat q of \recursive" natural numbers, with zero q , succ q
and natpara the \recursive" constant zero, \recursive" successor function and
primitive recursor.
Nat q   q (N)
zero q  wrap q
succ q (c)  wrap q
The typing and reduction rules for Nat q are the following:
Note that a non-zero \recursive" natural is constructed from a pair of naturals.
In the reduction rule, the rst of them is used as the argument for the recurrent
applications of the function being dened, while the second one is used directly.
In principle, the two naturals can be unrelated, but the normal usage of the
construction is that the second natural is equal to the rst (the predecessor),
so the standard successor function is recovered by duplicating its argument.
zero  zero q
succ(c)  succ q (hc; ci)
The type Nat q of \recursive" Mendler-style naturals is dened as follows:
Nat
mapzero q (d; i)  mapwrap q (inl(hi); d; i)
Nat q obeys the following typing and reduction rules:
mapzero q (d;
e z
natrec(mapzero q (d; i); e z
A non-zero \recursive" Mendler-style natural is constructed from a representation
(for the predecessor), a method for converting representations to naturals
and another function from representations to naturals. In the normal usage of
the construction, the second method is also a conversion method. Choosing
Nat q as the type of representations, the standard constructors are obtained
as follows:
zero  mapzero q ((); ())
succ(c)  mapsucc q (c; (); ())
On \recursive" naturals constructed using the standard constructors, natpara
and natrec capture standard primitive recursion. The factorial function, for
instance, can be programmed as follows:
A degenerate application of primitive recursion, which only uses the \direct-
access" predecessors of non-zero naturals, gives a fast (constant time) program
for the predecessor function:
pred(c)  natpara(c; inl(hi); (
pred(c)  natrec(c; (-; )inl(hi); (
Enhanced vs. basic [co]induction
Both ,  and m, n can be encoded in terms of  q ,  q and m q , n q . The converse is
also true, but only if the retractive recursive denition operator  is available.
Proposition 6 The following is a proof- and reduction-preserving encoding
of ,  in terms of  q ,
F
(c)  wrap q
F
F
cata
F
F
ana
F
F
open
F (c)  map
F (open q
Proposition 7 The following is a proof- and reduction-preserving encoding
of m, n in terms of m q ,
d)  mapwrap q (c; d; d)
iter
coit
mapopen d)  mapopen q (c; d; d)
Proposition 8 The following is a proof- and reduction-preserving encoding
of  q ,  q in terms of ,  in the presence of :
q
F q (R)  F (R ^  q
F (c)  i(wrap F q
F q
para
F
cata F q
q
F q (R)  F (R _  q
apo
F
open q
F q
(open F q (o(c)); ()i())
Proposition 9 The following is a proof- and reduction-preserving encoding
of m q , n q in terms of m, n in the presence of :
F q (R)  (R!m q
mapwrap q
rec
F q (R)  (n q
cor
In the last two encodings, we would really like to dene  q
cannot (because of
the circularity). Resorting to  is a way to overcome this obstacle. From the
result in [32], it follows that using  is a necessity, one cannot possibly do
without it.
The rst of these encodings is implicit in [25] and [15]. It also appears in [7].
The second seems to be new.
(and also its any fragment, including NI) extended
with operators  q ;  q or m q ; n q is strongly normalizing and con
uent.
5 Course-of-value [co]induction
The logical constants from the two lower rear nodes of the cube capture the
course-of-value forms of conventional- and Mendler-style [co]inductive deni-
tion.  ? and  ? are operators of course-of-value induction and coinduction; m ?
and n ? are their Mendler-style counterparts. Their proof and reduction rules
are given in Figures 9 and 10. Adding  ? ,  ? to a proof system presupposes
the presence of ^, , _,  ; there is no corresponding restriction governing the
addition of m ?
(R 4 F )(P )
F
e(
cvcata F
cvcata F (wrap ?

cvcata F (fst(open 4F (
snd(open 4F (
(R
e(
open ?
open ?
F (cvana F (c; e))
F
()cata 5F (; (
)wrap 5F (case@

Figure

9: Proof and reduction rules for  ? and  ? .
e(
e(
mapopen ? (c; d;
mapopen ? (cvcoit(c; e); d;

Figure

10: Proof and reduction rules for m ? and n ? .
From the algebraic semantics point-of-view,  ? F is a least course-of-value prexed
point of a given (necessarily monotonic) F , i.e., a least element of the
set of all R's such that F ((Z)R ^ F (Z)) is less than R.  ? F is a greatest
course-of-value postxed point of F .
is a least course-of-value robustly prexed point of a given F , i.e., a least
element of the set of all R's such that F (Y ) is less than R for all Y 's less than
not only R but also F (Y dually, is a greatest course-of-value robustly
postxed point of F .
For programming,  ? F is a course-of-value data type, with wrap ?
F a course-
of-value data constructor and cvcata F a course-of-value iterator, and  ? F is a
course-of-value codata type, with cvana F a course-of-value iterator and open ?
F
a course-of-value codata destructor. m ? F , with mapwrap ? and cviter, and n ? F ,
with cvcoit and mapopen ? , are their Mendler-style equivalents.
Specializing course-of-value induction for N yields the type Nat ? of \course-of-
value" natural numbers, with zero ? , succ ? and natcviter the \course-of-value"
versions of constant zero, successor function and iterator respectively.
Nat ?   ? (N)
zero ?  wrap ?
The specialized typing and reduction rules for these constants are the following


Similarly to the \recursive" case, non-zero \course-of-value" naturals are not
constructed from a single preceding natural. The argument of the \course-of-
value" successor function is a colist-like structure of naturals. The coiteration
in the reduction rule applies the function being dened recurrently to every
element of the colist. In principle, again, the naturals in the colist can be
unrelated. The normal usage, however, is that the tail of the colist is the ancestral
of its head (the predecessor of the natural being constructed). (By the
ancestral of a natural, we mean the colist of all lesser naturals in the descending
order.) The standard successor function for naturals is therefore easily
recovered from the \course-of-value" successor function by rst coiteratively
applying the predecessor function to its argument.
zero  zero ?
)h
pred(
The predecessor function, however, does not admit a very straightforward definition
(this is a problem that vanishes in the case of course-of-value primitive
recursion). But it is denable in terms of the ancestral function, which itself
is denable by course-of-value iteration in the same way as the predecessor
function is denable by simple iteration.
pred(c)
(pred ? (c); ()fst(open()))
pred ? (c)  cvcata N (c; (

The specialization of course-of-value Mendler-style induction for N yields the
Nat ? of \course-of-value" Mendler-style naturals.
Nat
mapzero ? (d;
The derived typing and reduction rules for the above-dened constants are
the following:
e z
A non-zero \course-of-value" Mendler-style natural is constructed from three
components. The rst two are the same as in the case of simple Mendler-
style naturals: a representation for a natural (the predecessor) and a method
to convert representations to naturals. The additional third component gives
a method for converting a representation (for some natural) into nothing or
another representation (normally for the predecessor of this natural). So, using
Nat ? as the type of representations, we obtain the standard constructors of
naturals as follows:
zero  mapzero ? ((); pred)
succ(c)  mapsucc ? (c; (); pred)
To dene the predecessor function, we again need also the ancestral function.
pred(c)
(pred ? (c); ()fst(open()))
pred ? (c)  cviter(c; (

On \course-of-value" naturals constructed using the standard constructors,
natcvcata and natcviter capture standard course-of-value iteration. The Fibonacci
function, for instance, can be programmed using natcvcata as follows.
bo(c)  natcvcata(c; zero; (
)case@ snd(open(
Using natcviter, the denition of the Fibonacci function becomes even more
straightforward, as, instead of having to manipulate an intermediate colist of
values that Fibonacci returns, we can \roll back" on inputs to it.
bo(c)  natcviter(c; (-; )zero; (
Course-of-value vs. basic [co]induction
Encoding ,  and m, n in terms of  ? ,  ? and m ? , n ? is very similar to
encoding these constants in terms of  q ,  q and m q , n q . Also encoding in the
opposite direction is analogous and, in fact, even simpler (as  in not needed).
Proposition 11 The following is a proof- and reduction-preserving encoding
of ,  in terms of  ? ,
F
(c)  wrap ?
F
cata
)case@
()fst(open 4F i
ana
F

F
open
F (c)  map
Proposition 12 The following is a proof- and reduction-preserving encoding
of m, n in terms of m ?
iter
coit
mapopen
Proposition 13 The following is a proof- and reduction-preserving encoding
of  ? ,  ? in terms of , :
F  wrap F ?(c)
cvcata
F (c; e)  cata F ?(c; e)
cvana
F
F  open F ?(c)
Proposition 14 The following is a proof- and reduction-preserving encoding
of m ? , n ? in terms of m, n:
mapwrap ?] (c; d;
cviter
cvcoit
mapopen ?] (c; d;
Corollary 15 NI 2 () (and also its any fragment, including NI) extended
with operators  strongly normalizing and con
uent.
6 Related work
The rst author to extend an intuitionistic n.d. system with (basic conventional-
style) inductively dened predicates uniformly by axiomatization was Martin-
Lof, with his \theory of iterated inductive denitions" [21].
Bohm and Berarducci [1] and Leivant [14] were the rst authors to describe
how to encode \polynomial" (basic conventional-style) inductive types in 2nd-
order simply typed lambda calculus (Girard and Reynold's system F; the
n.d. proof system for the !,8 2 -fragment of 2nd-order intuitionistic propositional
logic). This method is often referred to as the impredicative encoding
of inductive types (keeping in mind only basic conventional-style induction).
Mendler [19] described the extension by axiomatization of 2nd-order simply
typed lambda calculus with enhanced inductive and coinductive types of his
style. Mendler [20] discussed a similar system with basic Mendler-style inductive
and coinductive types. Extensions of the n.d. proof systems for 2nd-order
intuitionistic predicate logic with constructors of (basic) conventional- and
Mendler-style inductive predicates were described in Leivant's [15], a paper on
extracting programs in (extensions of) 2st-order simply typed lambda calculus
from proofs in (extensions of) the n.d. proof system for 2nd-order intuitionistic
predicate logic. Parigot's work [24,25] on realizability-based \programming
with proofs" bears connection to both Leivant's and Mendler's works.
Greiner [10] and Howard [13, chapter 3] considered programming in an extension
of 1st-order simply typed lambda calculus with axiomatized constructors
of conventional-style (co)inductive types with (co)iteration and data
destruction (codata construction). Both had their motivation in Hagino's
category-theoretic work cited below and studied thus not barely -reduction,
but even -conversion, driven by denite semantic considerations. Howard
implemented his system in a programming language Lemon. Geuvers [7] carried
out a comparative study of basic vs. enhanced, conventional- vs. Mendler-
style inductive and coinductive types in extensions of 2nd-order simply typed
lambda calculus.
In the spirit of Leivant, Paulin-Mohring [26] extracted programs in Girard's F !
from proofs in Coquand and Huet's CC (calculus of constructions). The milestone
papers on inductive type families in extensions of CC and Luo's ECC
(extended calculus of constructions, a combination of CC and Martin-Lof's
type theory) are Pfenning and Paulin-Mohring [28], Coquand and Paulin-Mohring
[4] and Ore [23]. Paulin-Mohring [27] formulated the calculus of inductive
constructions, which extends CC with inductive type families with
primitive recursion by axiomatization. The Coq proof development system
developed at INRIA-Rocqencourt and ENS-Lyon is an implementation of this
last system.
In category theory, (basic conventional-style) inductive and coinductive types
are modelled by initial algebras and terminal coalgebras for covariant functors.
Hagino [11] designed a typed functional language CPL based on distributive
categories with initial algebras and terminal coalgebras for strong covariant
functors. The implemented Charity language by Cockett et al. [3] is a similar
programming language.
The \program calculation" community is rooted in the Bird-Meertens formalism
or Squiggol [2], which, originally, was an equational theory of programming
with the parametric data type of lists. Malcolm [16] made the community
aware of Hagino's work, and studied program calculation based on
bi-Cartesian closed categories with initial algebras and terminal coalgebras
for !-cocontinuous resp. !-continuous covariant functors. Meertens [18] was
the rst author to give a treatment of primitive-recursion in this setting. Some
classic references in the area are Fokkinga's [6] and Sheard and Fegaras' [29].
7 Conclusion and Future Work
In this paper, we studied least and greatest xed point operators that intuitionistic
n.d. systems can be extended with. We described eight pairs of
such operators whose eliminations and introductions behave as recursors and
corecursors of meaningful kinds.
We intend to continue this research with a study of the perspectives of the utility
of intuitionistic n.d. systems with least and greatest xed point operators
in program construction from specications; this concerns both specication
methodology and computer assistance in synthesis. We have also started to
study the relating categorical deduction systems (typed combinatory logics a
la Curien), their utility in \program calculation" and the relevant categorical
theory [38,36,39,40]. We also intend to nd out the details of the apparent
close relationship of enhanced course-of-value Mendler-style (co)recursion to
Gimenez' new formulation of guarded (co)recursion [9] (for systems with sub-
and supertyping and quantication with upper and lower bounds; radically
dierent from the older, very syntactical formulation of [8]).

Acknowledgements

We are thankful to our anonymous referees for a number of helpful comments
and suggestions, especially in regards to matters of presentation. The proof
gures and diagrams appearing in the paper were typeset using the proof.sty
by Makoto Tatsuta and the XYpic generic
by Kristoer C. Rose, respectively.



--R


An introduction to the theory of lists
Yellow Series Report 92/480/18
Inductively de
A survey of the project AUTOMATH
Law and order in algorithmics
Inductive and coinductive types with iteration and recursion



A categorical programming language
A framework for de
Fixed points and extensionality in typed functional programming languages
Reasoning about functional programs and complexity classes associated with type disciplines
Contracting proofs to programs
Data structures and program transformation
Extensions of system F by iteration and primitive recursion on monotone inductive types

Recursive types and type constraints in second-order lambda- calculus
Inductive types and type constraints in the second-order lambda- calculus


The extended calculus of constructions (ECC) with inductive types
a second order type theory
Recursive programming with proofs
-Mohring, Extracting F!
-Mohring, Inductive de
-Mohring, Inductively de
A fold for all seasons
A natural extension of natural deduction
Generalized rules for quanti

A lattice-theoretical xpoint theorem and its applications
Positive recursive type assignment
Natural deduction for intuitionistic least and greatest

A cube of proof systems for the intuitionistic predicate
Primitive (co)recursion and course-of-value (co)iteration

Coding recursion
--TR
An introduction to the theory of lists
Extracting MYAMPERSANDohgr;''s programs from proofs in the calculus of constructions
Inductively defined types
Programming in Martin-LoMYAMPERSANDuml;f''s type theory: an introduction
Data structures and program transformation
Inductively defined types in the calculus of constructions
Recursive programming with proofs
A framework for defining logics
The extended calculus of constructions (ECC) with inductive types
A fold for all seasons
Fixed points and extensionality in typed functional programming languages
Type fixpoints
Programming with Proofs
Positive Recursive Type Assignment
Inductive Definitions in the system Coq - Rules and Properties
Structural Recursive Definitions in Type Theory
Codifying Guarded Definitions with Recursive Schemes
Mendler-style inductive types, categorically
Programming with Inductive and Co-Inductive Types
A categorical programming language

--CTR
Gilles Barthe , Tarmo Uustalu, CPS translating inductive and coinductive types, ACM SIGPLAN Notices, v.37 n.3, p.131-142, March 2002
G. Barthe , M. J. Frade , E. Gimnez , L. Pinto , T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science, v.14 n.1, p.97-141, February 2004
coding styles;least and greatest fixed points;coinductive types;schemes of total corecursion;typed lambda calculi;natural deduction