🚀 go-pugleaf

In article <1ciumrINN9mk@iraul1.ira.uka.de> prechelt@i41s18.ira.uka.de  
(Lutz Prechelt) writes:
> [...]
> 4. How can I check whether one specification subsumes another,
>    i.e., the first datatype can emulate the second ?
> 
> [[ Again, this is difficult to formalize unless the signatures are
>    isomorphic. (E.g. of course you can emulate a stack with a linked
>    list -- but what exactly does ``emulate'' mean in general ?)
>    For isomorphic signatures the set of axioms of the subsuming 
>    specification implies the set of axioms of the subsumed  
specification.
> [...]
The ``emulation'' can be expressed by a homomorphism given as an attribute  
to the subsuming-relation between the two specifications.
The homomorphism (h) transforms the `concrete' representation (the linked  
list) to the abstract representation (the stack).
h is a map from a link and a state to a term (which describes an abstract  
stack), i.e.
  h: concrete link * concrete state -> abstract stack
The description of h determines `exactly' the ``emulation''.

Michael Mehlich