[Prev][Next][Index]
Re: A miscellany
David,
Interesting suggestions. I've missed well-foundedness myself more than
once. I don't think you described the proof obligation for a claim of
well-foundedness?
I guess I need to think more about your item 3. Right off the bat, it
doesn't grab me.
I suspect that what you lose with the A-interpretation is the ability to
implement any specification whose data types aren't fully specified (i.e.,
admit non-isomorphic models), but I'm not real sure of this. If so, the
reason the problems with compositionality disappear is that there are no
implementations to compose.
Regarding separate implementations and compositionality: I don't see any
sensible way to use a module if the client and the implementation do not
agree on the representations of the data types they share. So, in your
example, the client that wants to use both Abstraction1 and Abstraction2 in
a module to implement some other specification must have some way of
ensuring that it is using the same representation as Abstraction1 and the
same representation as Abstraction2. Then the proof that Abstraction1 and
Abstraction2 agree is quite trivial. What have I missed?
I agree that generics are also a good reason for using the E-interpretation.
Jim H.
PS John and Steve are both on vacation right now, so don't expect immediate
responses. I haven't responded to the list at large, because I'd like to
make sure we understand each other about item 3 before involving the larger
group in the debate (if there turns out to be one).