initial algebras

To: types@theory.LCS.MIT.EDU
Subject: initial algebras
From: tobias@dash2.lcs.mit.edu (Tobias Nipkow)
Date: Thu, 10 Nov 88 17:42:37 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: Thu, 10 Nov 88 17:33:32 EST
To: jcm%cs.stanford.edu@xx.lcs.mit.edu

I agree with your latest iff-chain although I don't understand what you mean
by "Perhaps this leads to the final algebra".

As to whether this is an accepted position: the trend seems to go into this
direction but not everybody seems to be convinced yet.

The most interesting question you raised is the one about what "observing"
means. Most work on observational equivalence of ADTs uses expressions over
the signature and avoids the issue of more powerful observers like programs.
For algebraic expressions it is not difficult to show that observational
congruence coincides with logical relations. In trying to extend this to
programs one is faced with the question: what kind of programs? Lambda
calculus, CSP or what? In my PhD I have used a particular class of
first-order applicative languages to investigate this. It turns out that
under certain assumptions on the language semantics (essentially enforcing
some abstract version of information hiding) these programs do not add any
observational power. However, this this fails to hold for nondeterministic
data types. In case you are interested I can give you some
references/details.

Tobias