[Prev][Next][Index][Thread]

Re: data types and initiality

	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