A view of an entity A as a theory T consists of a mapping from the types of T to the types of A and a mapping from the operations of T to the operations of A that preserves arity (the list of argument types), value type (if any), and operation attributes such as assoc, comm, and id: (if any) such that the translation of every axiom in T is satisfied by A.

view NATD :: POSET =>  NATURAL is
   types (ELT =>  NATURAL)
   ops   (< =  =>  DIVIDES)
end NATD

Contents    Page-10    Prev    Next    Page+10    Index