Induction, Co-induction, and Types in Slate

[Massimo Dentico]

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:

- http://www.cs.brown.edu/people/pw/papers/bcj1.pdf

======================================================================
[...]

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,
    observation
(3) Replace minimal by maximal fixed points

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

[...]
======================================================================

Peter Wegner home page:
- http://www.cs.brown.edu/people/pw/

> [...]

-- 
Massimo Dentico