[Prev][Next][Index][Thread]
Re: data types and initiality
Date: Thu, 10 Nov 88 17:18:40 MST
To: meyer@theory.LCS.MIT.EDU
Cc: types@theory.LCS.MIT.EDU
Date: Thu, 10 Nov 88 16:49:12 EST
From: meyer@theory.lcs.mit.edu
I understand wanting to interpret equality as obs-cong, but then it
seems to me the implementation might BE a homomorphic image of the
initial algebra rather than vice-versa.
For example, suppose we have two sorts called INT and BOOL,the
signature
TRUE, FALSE:BOOL
ZERO:NAT
SUC:NAT-->NAT
EQPARITY:NAT x NAT-->BOOL
with specifying equations
EQPARITY(x, SUC(SUC(x))) = TRUE
EQPARITY(x, SUC(x)) = FALSE.
Now assume the only observables are TRUE and FALSE. Then the initial
algebra has NAT = the natural numbers under succcessor. But an
``implementation'' which is obs-cong to this initial algebra has
NAT={TRUE, FALSE}, SUC=complement, and EQPARITY = equivalence.
Note by the way, that the implementation can interpret ZERO to be TRUE
or FALSE; there is no final algebra in this case. So the obs-cong
approach is not EXACTLY asking for final algebras--close though.
Regards, A.
Isn't it the case that the two implementations are isomorphic, and BOTH
are final?
By the way, either I'm confused, or the equations above aren't the
whole story, since EQPARITY in the implementation relates every pair of
NATS, but the equations don't yield TRUE or FALSE for terms like
EQPARITY(ZERO, SUC(SUC(SUC(ZERO)))). I think the intended algebraic
theory can be specified by these equations:
EQPARITY(x, x) = TRUE
EQPARITY(x, SUC(x)) = FALSE
EQPARITY(x, SUC(SUC(y)) = EQPARITY(x, y)
EQPARITY(x, y) = EQPARITY(y, x)
Cheers,
--Joe