Rob Kremer

Z Specification of CLASSIC

This page is ongoing work on specifying CLASSIC in Z. The work is based on the paper The version of the Z notation used here is the ZSL language developed by Xiaoping Jia at dePaul University. The ZSL language is used in conjunction with the ZTC (Z Type Checker), version 2.0, also from Xiaoping Jia. One of the nice things about ZTC is that it will take this page (either saved as HTML source or as pure text) as input. Since the type checker only interprets lines beginning with a tab character, it is easy to write a combination HTML and ZSL file.

Contents

        specification

Definition 1: Possible Worlds/Interpretation

The universal type for classic is called THING. We want to say nothing about THING at all, but ZTC seems to need to say something, so we will comply by giving everying a name (not very elegant). 
        [NAMES]

        --- THING -------------------------------------
        | name: NAMES
        |---------------------------
        | name in NAMES
        -----------------------------------------------

The Realms

There are two subtypes of THING called the CLASSIC_REALM and the HOST_REALM. 
        --- CLASSIC_REALM -----------------------------
        | THING
        |---------------------------
        | THING
        -----------------------------------------------

        --- HOST_REALM -----------------------------
        | THING
        |---------------------------
        | THING
        -----------------------------------------------
CLASSIC_REALM and HOST_REALM disjointly divide THING. 
        forall x:THING @ ((x in CLASSIC_REALM ) \/ (x in HOST_REALM ))
                /\ (x in CLASSIC_REALM ) => not (x in HOST_REALM)

Concepts, Roles, and Attributes

There are three kinds of objects withing the CLASSIC_REALM: Concepts, Roles, and Attributes. 
        | AtomicConcept : P CLASSIC_REALM;
        | AtomicRole    : P (CLASSIC_REALM & THING);
        | AtomicAttr    : P (CLASSIC_REALM --> THING);

Constructors

Non-atomic CLASSIC descriptions are formed by using the combinators intersection, role and attribute value restriction, minimum and maximum restriction, and equality restriction. Intersection has three flavours: one for each of concept, role, and attribute. Restriction has two flavours for role and attribute. Roles are multi-valued and concepts may be described by the arity of roles, so we get the minumum and maximum restriction combinators applying to roles only. Attributes are like roles by are single-valued (min- max-restrictions would make no sense!); the equality combinator applies only to attributes to keep the algorithms tractable. 
        | % The different flavours of interstection...
        | Intersect_C : AtomicConcept & AtomicConcept --> AtomicConcept;
        | Intersect_R : AtomicRole & AtomicRole --> AtomicRole;
        | Intersect_A : AtomicAttr & AtomicAttr --> AtomicAttr;
        |
        | % Role and attribute value restriction...
        | Restrict_R  : AtomicRole & AtomicConcept --> AtomicConcept;   
        | Restrict_A  : AtomicAttr & AtomicConcept --> AtomicConcept;
        |
        | % Minimum and Maximum number restriction...
        | MinRestrict : N & AtomicRole --> AtomicConcept;
        | MaxRestrict : N & AtomicRole --> AtomicConcept;
        |
        | % Equality Restriction
        | EqRestrict  : seq AtomicAttr & seq AtomicAttr --> AtomicConcept;

Extensional Interpretation

The denotational semantics of CLASSIC descriptors is based on extensions in a possible world. It seems there are actually three interpretation functions needed, one for each of the three atomic types (if the interpretation function is going to be well-typed without any mathematical tricks). I've called these Interp_C, Interp_R, Interp_A. (see note 1)

Atomic Extensions: The interpretation of an atomic concept is everything it subsumes. The interpretation of an atomic role is some relation between objects in the CLASSIC_REALM and objects in the universe. Since attributes are just single-valued roles, their interpretations are functions instead of relations.

Intersections: The extension of an intersection is just the set intersection of the extensions of the operands.

Value Restrictions: The extension of a value restriction is all those objects that have the specified role filled with an object in the extension of the specified concept.

Number Restriction: The extension of a number restriction is all those CLASSIC objects with at least (most) the specified number of fillers for the specified role. 

        exists y: AtomicConcept @ y=y

        | Interp_C: AtomicConcept --> P CLASSIC_REALM;
        | Interp_R: AtomicRole --> P (CLASSIC_REALM  &  THING);
%       | Interp_A: AtomicAttr --> P (CLASSIC_REALM +-> THING);
        | Interp_A: AtomicAttr --> P (CLASSIC_REALM  &  THING);
        | CLASSIC_THING : CLASSIC_REALM;
        |------------------------
        | Interp_C(CLASSIC_THING) = CLASSIC_REALM;
        |
        | % Intersections...
        | forall c,d: AtomicConcept @
        |       Interp_C(Intersect_C(c,d)) = Interp_C(c) && Interp_C(d);
        | forall r,s: AtomicRole @
        |       Interp_R(Intersect_R(r,s)) = Interp_R(r) && Interp_R(s);
        | forall a,b: AtomicAttr @
        |       Interp_A(Intersect_A(a,b)) = Interp_A(a) && Interp_A(b);
        |
        | % Role and attribute value restriction...
        | forall r: AtomicRole @ forall c: AtomicConcept @
        |       Interp_C(Restrict_R(r,c)) = {d:CLASSIC_REALM | forall x:THING @
        |               (d -> x) in Interp_R(r) => x in Interp_C(c)};
        | forall a: AtomicAttr @ forall c: AtomicConcept @
        |       Interp_C(Restrict_A(a,c)) = {d:CLASSIC_REALM | forall x:THING @
        |               (d -> x) in Interp_A(a) => x in Interp_C(c)};
        |
        | % Minimum number restriction, Maximum number restriction...
        | forall n: N @ forall r: AtomicRole @
        |       Interp_C(MinRestrict(n,r))= {d:CLASSIC_REALM | 
        |               #{x:THING | (d -> x) in Interp_R(r)} < n+1};
        | forall n: N @ forall r: AtomicRole @
        |       Interp_C(MaxRestrict(n,r))= {d:CLASSIC_REALM | 
        |               #{x:THING | (d -> x) in Interp_R(r)} > n-1};
        |
        | % Equality restriction
        | forall sa, sb: seq AtomicAttr @ 
        |       Interp_C(EqRestrict(sa,sb)) = {d:CLASSIC_REALM |
        |            #sa=1 /\ #sb=1 /\
        |              (exists x: THING @
        |                (d -> x) in Interp_A(head sa) /\ 
        |                (d -> x) in Interp_A(head sb))
        |         \/ #sa>1 /\ #sb=1 /\
        |              (exists c:CLASSIC_REALM @ exists x: THING @
        |                (d -> c) in Interp_A(head sa) /\
        |                c        in Interp_C(EqRestrict(tail sa,sb)) /\ 
        |                (d -> x) in Interp_A(head sb))
        |         \/ #sa=1 /\ #sb>1 /\
        |              (exists c:CLASSIC_REALM @ exists x: THING @
        |                (d -> x) in Interp_A(head sa) /\
        |                (d -> c) in Interp_A(head sb) /\
        |                c        in Interp_C(EqRestrict(sa,tail sb))) 
        |         \/ #sa>1 /\ #sb>1 /\
        |              (exists c,e:CLASSIC_REALM @ exists x: THING @
        |                (d -> c) in Interp_A(head sa) /\
        |                c        in Interp_C(EqRestrict(tail sa,tail sb)) /\ 
        |                (d -> e) in Interp_A(head sb) /\
        |                e        in Interp_C(EqRestrict(tail sa,tail sb))) 
        |         }

Definition 2: Description Graphs

This section describes description graphs. The definition is recursive, so we must first describe DescrGraph as a given set, then redefine it when we have all the pieces in place. 
        [DescrGraph] %forward declaration to be overridden
A bit of housekeeping: we need the maximum number of fillers for a role to be either a natrual number or infinity. 
        MAX_SPEC ::= infinity | const << N >>
A R_Edge is a tuple, , describing a role, role is its name, min and max restrict the arity of the role, and the restriction graph is (recursively) a description graph which restricts the fillers of the role. 
        --- R_Edge -------------------------------------
        | role : NAMES;
        | min_ : N;
        | max_ : MAX_SPEC;
        | restrictionGraph : DescrGraph;
        |---------------------
        | 1=1
        ------------------------------------------------
A Node is a set of concept names (the atoms of the node) together with a bag of R_Edges (the roles of the node). 
        --- Node --------------------------------------
        | concepts : P THING; %??
        | r_edges : bag R_Edge
        |---------------------
        | 1=1
        ------------------------------------------------
An A_Edge is an attribute edge and is a binary role, so it has exactly two nodes... 
        --- A_Edge ----------------------------------------
        | node1, node2 : Node;
        | attr : NAMES;
        |---------------------
        | 1=1
        ------------------------------------------------
Finally, a description graph may be defined. A description graph has a set of nodes, a bag of A_Edges, and a distinguished node r in the set of nodes. 
        --- DescrGraph ---------------------------------
        | nodes : P Node;
        | edges : bag A_Edge;
        | r: Node;
        |---------------------
        | r in nodes;
        ------------------------------------------------

Definition 3: Interpretation of Description Graphs

        end specification
Note 1: the third line (INTERP_A) of the declaration part of this axiom is commented out and replaced with a simimlar declaration using a relation instead of a function. This is necessary since I can't find a way to say a maplet is in a function. The type system insists that maplets are relations and not functions (they sould be both).
Rob Kremer
kremer@cpsc.ucalgary.ca