[Prev][Next][Index][Thread]
initiality, etc.
Date: Thu, 10 Nov 88 14:25:46 PDT
To: meyer@theory.LCS.MIT.EDU
Remember that being initial means there is a homomorphism to every
other algebra (satisfying the equations), so if we collapse
the implementation by observational congruence, we should
get something that satisfies the equational specification,
and therefore a homomorphic image of the initial algebra...
I guess one conclusion might be that "satisfying a spec" should
be interpreted after collapsing modulo observational congruence.
This might imply a logical relation between implementation and
initial algebra, or maybe not, but this would easily be settled
by five minutes thought; either of us could probably figure out
the rest of the story off line on the way home.
The more we discuss this, the more I think that logical relations
and obs-cong are the important notions, and all the dogmatic
initial-final-loose algebraic interpretation arguments irrelevant.
We already knew that logical relations were important for abstract
data types and lambda calculus, so it shouldn't be too surprising
that the same holds in the algebraic framework.
I was trying to decide whether I should encourage a student
to look into this. I think the answer is yes, with the eventual
hope of re-working our second-order logical relations paper and
my follow-up on data abstraction (POPL 86, I think). In those
papers, impredicativity got in the way of making a simple point,
which I now think could be illustrated first using
multi-sorted algebra.
John