From: Jeremy Gibbons <Jeremy.Gibbons@comlab.ox.ac.uk>
To: categories@mta.ca
Subject: Re: coinduction
Date: Mon, 30 Oct 2000 15:55:25 GMT [thread overview]
Message-ID: <200010301555.PAA02925@loire.comlab> (raw)
In-Reply-To: <003301c03a95$49f73610$448a0dd8@main> (al.r@VILCIUS.com)
> can anyone explain coinduction?
> in what sense it dual to induction?
We've heard some very erudite answers to these questions. I
don't know the questioner's background, but here is a
different answer, in case it helps.
In the algebraic approach to functional programming, an
initial datatype of a functor F is a datatype T and an
operation in : F T -> T for which the equation in h
h . in = f . F h
has a unique solution for given f. We write "fold_F f" for
that unique solution, so
h = fold_F f <=> h . in = f . F h
This is an inductive definition of fold, and the above
equivalence (the "universal property for fold") encapsulates
proof by structural induction.
(For example, when F X = 1+X, then T is N, the naturals. The
injection in : 1+N->N is the coproduct morphism [0,1+].
Folds on naturals are functions of the form
fold_{1+} [z,s] 0 = z
fold_{1+} [z,s] (1+n) = s (fold_{1+} [z,s] n)
To prove that a predicate p holds for every natural n is
equivalent to proving that the function p : N -> Bool is
equal to the function alwaystrue : N -> Bool that always
returns true. Now alwaystrue is a fold,
alwaystrue = fold_{1+} [true,step]
where step true = true
Therefore, to prove that p holds for every natural, we can
use the universal property:
predicate p holds of every natural
<=>
p = alwaystrue
<=>
p = fold_{1+} [true,step]
<=>
p . [0,1+] = [true,step] . id+p
<=>
p(0) = true and p(1+n) = step(p(n))
<=>
p(0) = true and (p(1+n) = true when p(n) = true)
which is the usual principle of mathematical induction.)
Dually, a final datatype of a functor F is a datatype T and
an operation out : T -> F T for which the equation in h
out . h = F h . f
has a unique solution for given f. We write "unfold_F f" for
that unique solution, so
h = unfold_F f <=> out . h = F h . f
This is a coinductive definition of unfold, and the above
equivalence (the "universal property for unfold")
encapsulates proof by structural coinduction.
> how is it used to prove theorems?
Exactly the same way. For example, the datatype Stream A of
streams of A's is the final datatype of the functor taking X
to A x X. An example of an unfold for this type is the
function iterate, for which
iterate f x = [ x, f x, f (f x), f (f (f x)), ... ]
defined by
iterate f = unfold_{A x} <id,f>
One might expect that
iterate f . f = Stream f . iterate f
and the proof of this fact is a straightforward application
of the universal property of unfold (that is, a proof by
coinduction).
Jeremy
--
Jeremy.Gibbons@comlab.ox.ac.uk
Oxford University Computing Laboratory, TEL: +44 1865 283508
Wolfson Building, Parks Road, FAX: +44 1865 273839
Oxford OX1 3QD, UK.
URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html
next prev parent reply other threads:[~2000-10-30 15:55 UTC|newest]
Thread overview: 10+ messages / expand[flat|nested] mbox.gz Atom feed top
2000-10-20 12:57 coinduction Al Vilcius
2000-10-20 15:35 ` coinduction Hendrik Tews
2000-10-20 22:01 ` coinduction Jesse F. Hughes
2000-10-21 1:19 ` coinduction Charles Wells
2000-10-26 23:49 ` coinduction Dusko Pavlovic
2000-10-30 15:55 ` Jeremy Gibbons [this message]
2000-10-27 20:40 coinduction Jesse F. Hughes
2000-10-30 3:38 ` coinduction Dusko Pavlovic
2000-10-28 19:39 coinduction Mamuka Jibladze
2000-10-30 23:09 coinduction Jesse F. Hughes
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=200010301555.PAA02925@loire.comlab \
--to=jeremy.gibbons@comlab.ox.ac.uk \
--cc=categories@mta.ca \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).