Abstract:Introducing the type transformation functions between subtypes and supertypes, the definition of order-sorted algebra is generalized. According to this definition, a type needn't be a subset of its supertype, and a record model may form an order-sorted algebra. The concept of forest-order signature is introduced for describing single inheritance relation between types. A new meaning of equation is given. It is proved that an equational theory has its initial model.