I am studying Goguen's paper Types as theories [1].Based on Goguen's paper, are the following true?Subsort inheritance provides a classification of values, every value of the sub-sort is a value of the super-sort.Module import inheritance provides classification of models, each model of the class of models of the importing module contains a model of the imported module.Below are two example coded in CafeOBJ (any other algebraic specification language would do).Assumptions the module is the software realization of a theoryloose semanticsnormal protecting mode for importthe term type is synonym for sortthe < symbol indicates subsortmod* SUBSORT { [  Group < Elt ]-- Signature in terms of super typeop e : -> Elt op _._ : Elt Elt -> Elt -- equations in terms of subtypevars A B C : Group eq A . e = A . eq e . A = A . eq A . (B . C) = ((A . B) . C) . }mod* MONOID {-- The TRIV theory represented by the CafeOBJ -- built in module TRIV which has Elt as its principal sortprotecting(TRIV)op e : -> Elt op _._ : Elt Elt -> Elt vars A B C : Elt eq A . e = A . eq e . A = A . eq A . (B . C) = ((A . B) . C) .}Regards,Pat[1]Goguen, J. (1991). Types as Theories. Topology and Category in ComputerScience. G. M. Reed, A. W. Roscoe and R. F. Wachter, Oxford UniversityPress: 357-390.http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.2241
Types as theories
semantics;denotational semantics