Induction, Co-induction, and Types in Slate

Massimo Dentico
Wed, 29 Mar 2000 21:28:26 +0200

Kyle Lahnakoski wrote:
> "Brian T. Rice" wrote:
> > I originally came up with this idea to deal with the oddities of
> > co-inductive types, such as streams of values or even the rational number
> > system. Both of these ideas don't admit to a numeration via the natural
> > number system, and in programming languages are naturally
> > lazily-implemented. However, a robust general method (using equational
> > expressions) exists for specifying these types beyond simple algorithms.
> > However, I'm still working out the mechanics of this type of framework in
> > Slate, and I invite your comments.
> To tell you the truth, I do not know what you are saying in this
> paragraph.  It sounds interesting, but I can not comment unless I know
> more.
> What is co-inductive?

>From "Interaction, Computability, and Church’s Thesis", P. Wegner:



4.1 The Inductive Modeling Paradigm

Induction determines a construction paradigm for definition, reasoning,
and modeling characterized by:

(1) An initiality condition that determines base elements of inductively
    generated sets
(2) An iteration condition that allows new elements to be constructed
    (derived) from initial elements
(3) A minimality condition that only elements so constructed are definable

inductive definition: initiality (base) condition, constructive iteration
  condition, minimality condition
construction paradigm: generate (construct) structures inductively from
  base elements


4.2 Coinduction and Greatest Fixed Points

Coinduction determines a deconstruction paradigm that deconstructs
composite structures into progres-sively more primitive ones. Coinduction
models processes of observation. Observation is a deconstruction
process that reveals progressively more structure about observed entities.
Processes of observation make no initiality assumptions and can continue
to reveal new knowledge about the observed objects indefi-nitely:
hidden information is progressively approximated by processes that do
not terminate. Coinduction can be derived from induction by relaxing
requirements of induction as follows:

(1) Eliminate the initiality condition (base case)
(2) Reverse the direction of iteration: construction -> deconstruction,
(3) Replace minimal by maximal fixed points

coinductive definition: deconstructive iteration condition, maximality
observation paradigm: observe already existing constructed elements.


Peter Wegner home page:

> [...]

Massimo Dentico