[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / notn_16_Classification
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Aug 14 19:34:44 PDT 2012

Contents


    Classifications and Ontologies

      Domains have large numbers of terms indicating objects of different sets and types. This are typically organized in several hierarchies. It is useful to have a simple way of expressing such hierarchies.

      Sets

        Enumerations and Finite sets of constants

        It would be nice to have a notation that introduces a set of values for a variable. This is allowed in Pascal, C, C++, and Ada. Currently a declaration like
         	traffic_light:{Red, Amber, Green}.
        would not automatically define the terms Red, Amber, etc. However
         	traffic_lights::={Red, Amber, Green}.
        is short hand for
           	traffic_lights::Sets,
           	Red::traffic_lights,
           	Amber::traffic_lights,
           	Green::traffic_lights,
           	|- traffic_lights={Red, Amber, Green}.

        [ Enumerating Finite Sets in logic_30_Sets ]

        Notice that no order is implied between the elements listed above. In programming, an enumeration is an linearly ordered set and in MATHS the notation is

         	enum(intuitive, sensing)
        [ math_77_Enumerations.html ]

        Subsets

        The simplest classification system for a set of objects is created by using the Subsets. In the MATHS notation the set of all subsets is indicated by the curly "@" sign. This is reminiscient of the curly P used by mathematicians:
      1. (set)|-For Set S, @S = { A. A==>S }.
          For example to make B and C be special kinds of A we write:
        1. A:Sets,
        2. B::@A,
        3. C::@A.

          The above imply the following:

        4. (above)|- (E1): B ==> A.
        5. (above)|- (E2): C ==> A.
        6. (E1)|-for all b:B, b in A.
        7. (E2)|-for all c:C, c in A.

          They do not assume that every A is either a B or C however. Some A's may be neither.

           	<-------------------------A----------------->
           	<----------B--->
           	                         <----C------------->

        You need to be careful of the meaning of words indicating subsets in English and other natural languages. For example in the set of People we often distinguish Tall and Short people:
        Net

        1. People::Sets,
        2. Tall::@People,
        3. Short::@People.

        (End of Net)

        What we should not assume is that everybody is either Tall or Short. We have people who are neither. So we do not add the assumption
      2. People = Tall | Short.

        Niether can we assume

      3. Tall = People ~ Short.
      4. Short = People ~ Tall.

        What we do have, in this case, is

      5. Short ==> People~Tall,
      6. Tall ==> People~Short.
         	<--Short--><------------People~Short------------------->
         	<-------People~Tall-----------------><------Tall------->

        This is a common pattern [Leech74] when we have an underlying ordering governed by an attribute -- in the above case height.

        There is another trap when you are trying to compare items in different sets... for example consider a large chihuahua vs small saint bernard.

        BNF -- unions that cover a set

        Bachus Naur Form allows one to define one set as the union of other sets:
        1. A::= B | C.

          This implies the following deductions:

        2. (above)|-for all a:A, a in B or a in B.
        3. (above)|-for all b:B, b in A.
        4. (above)|-for all c:C, c in A.

          However, it is possible for an item in A to be in both B and C.

           	<-------------------------A----------------->
           	<----------B--------->
           	                <-------------C------------->

          In jargon: A is covered by B and C. See set_families.


        Partitions -- nonoverlapping classification

        The statement
      7. A >== {B, C},

        says the same thing as

      8. A = B | C and B & C = {}.

        A partition implies

      9. B = A ~ C and C=A~B.

        In other words that every A is a either a B or a C, and no A is both a B and C.

         	<-------------------------A----------------->
         	<----------B---->
         	                 <------------C------------->

        In the UML this is a disjoint and complete specialization.

        For more on the theory of partitions and their relationship to mappings and equivalence relations see set_families.

        Combinations of subsets Leads to complex ontologies

        Notice that if B==>A then A>=={B, A~B}.

        If we have a set A with two subsets B==>A and C==>A then we can partition A as follows

      10. A>== {
        1. B&C,
        2. B~C,
        3. C~B,
        4. ~B~C
        }.

        Similarly with three subsets(B,C,D) we have a partition with 8 sets: {

        1. B&C&D,
        2. B~C&D,
        3. C~B&D,
        4. D~B~C,
        5. B&C~D,
        6. B~C~D,
        7. C~B~D,
        8. ~B~C~D
        }.

        A Venn Diagram is a handy way to render these structures [ ../samples/nerd-venn-diagram.html ] (humorous example) plus [ http://cartesianproduct.wordpress.com/2012/08/12/venn-diagrams-for-11-sets/ ] (nice layouts for many variables)

        More, these partitions give rise to an easy to use logic -- term logic. For example, Leech [Leech74] presents the idea (from anthropology) that terms in natural language can be given meaning in terms of components:

         	man	+HUMAN+ADULT+MALE
         	woman	+HUMAN+ADULT-MALE
         	boy	+HUMAN-ADULT+MALE
         	girl	+HUMAN-ADULT-MALE

        Using the approach described above we would define
        Net

        1. Being::Sets
        2. Human::@Being,
        3. Adult::@Being,
        4. Male::@Being.
        5. Female::=Being~Male.

        6. Man::=Human&Adult&Male.
        7. Woman::=Human&Adult~Male.
        8. Boy::=Human~Adult&Male.
        9. Girl::=Human~Adult~Male.

        10. Child::=Human~Adult.

          Sample theorem

        11. (above)|- (CBG): Child = Boy | Girl.

          Proof of CBG


          Let
          1. Boy | Girl
          2. (Boy, Girl)|-
          3. = (Human~Adult&Male)|(Human~Adult~Male)
          4. (Female)|-
          5. = (Human~Adult&Male)|(Human~Adult&Female)
          6. (extract common factor)|-
          7. = (Human~Adult)&(Male|Female)
          8. (Male, Female, union of complements)|-
          9. = Human~Adult&Being
          10. (Commutative and associative)|-
          11. = Being&Human~Adult
          12. (Human, Being, subset)|-
          13. = Human~Adult
          14. (Child)|-
          15. = Child.

          (Close Let )

          Informal rules used in proof

          The following a theorems derived in the theory of sets
          (extract common factor): (A&B)|(A&C) = A&(B|C).
          (union of complements): Male|Female = Being.
          (Commutative and associative): We can reorder factors as we wish and insert parentheses if we wish.
          (subset): If A==>B then A&B=A.

        (End of Net)

      . . . . . . . . . ( end of section Sets) <<Contents | End>>

      Nets

        Abbreviations

        The following are introduced to allow the simple and natural expression of simple ideas like a person is either male or female but not both:
         		Person::=Net{..... Either male or female. .... }.

      1. For A, B:word,
      2. either A or B::=Net{ A, B:@. A iff not B },
      3. Either A or B::=either A or B.

      4. For A, B:word, L:#("," word), (either A L, or B) ::=Net{ A, L, B:@. One(A L, B) }, (Either A L, or B) ::=(either A L, or B).

      . . . . . . . . . ( end of section Nets) <<Contents | End>>

      Polymorphism

        MATHS permits the same identifier to have different meanings in different contexts. A context is determined by the type of thing that fits in that context.

        A consequence of allowing multiple polymorphic symbols in documentation is that all functions in MATHS should be seen as "multimethods" [PuppydogRacoon99]. In the classic problem of "Feeding the Animals" for example, we have two types: Animal and Food. Animals are classified as Wolves and Cows. Foods are classified as Meat and Grass. All Animals eat Food and get energy from it, but Wolves only eat Meat and Cows only eat Grass. A language with multimethods or another form of automaic down casting will invalidate the idea of Cows eating Meat and Wolves eating Grass.


        1. FTA::=following
          Net
            Feeding the Animals.
          1. Animal::Sets.
          2. Food::Sets.
          3. |-Animal>== {Wolf, Cow}.
          4. |-Food>== {Meat, Grass}.
          5. |-Number>== {int, float}.
          6. energy::Animal->Number.
          7. energy::Wolf->float.
          8. energy::Cow->int.
          9. energy::Food->Number.
          10. energy::Grass->int.
          11. energy::Meat->float.
          12. eat::Animal><Food->Animal.
          13. For all cow:Cows, grass:Grass, eat(cow,grass)::= the Cow(energy=>energy(cow)+energy(grass)).
          14. For all wolf:Wolf, meat:Meat, eat(wolf,meat)::=the Wolf(energy=>energy(wolf)+energy(meat)).

            It is now valid to have Cows eat Grass and Wolves eat meat and reason with the consequences but nothing can be deduced about eat(wolf,grass) and eat(cow,meat).

            Further because Animal and Food are declared separately as Sets they are implictly not in the same type. This means that eat(grass, wolf) is illegitimate in this Net.

            However, if this net was instanciated with two sets (Animal, Food) in the same hierarchy then an expression like eats(grass, cow) is definable and may even provoke thought about the meaning intended for eat. Indeed, eats(wolf, cow) starts to look meaningful and ominous.


          (End of Net)


        Duck Typing

        MATHS does allow something like the kind of polymorphism found in Python where a collection of Nets of declare the same attributes, then they define same types of object. This is because in MATHS types are universal sets. Thus [ notn_14_Docn_Semantics.html ] the type of a Net is the type of the Net with no axioms, constraints, etc. So, many objects, though they are in different sets, will be of the same type.

        However if two nets have different variables then they will belong in different types.

        In particular, if one net ABC say defines a:A, b:B, c:C then its objects are of a different type to the net AB that only defines a:A and b:B. We would say that ABC extends AB. We could even define ABC as AB with {c:C} as an explicit extension.

      . . . . . . . . . ( end of section Polymorphism) <<Contents | End>>

      See Also

    1. set::= See http://www.csci.csusb.edu/dick/maths/logic_30_Sets.html.
    2. set_families::= See http://www.csci.csusb.edu/dick/maths/logic_31_Families_of_Sets.html.
    3. set_theory::= See http://www.csci.csusb.edu/dick/maths/logic_32_Set_Theory.html.
    4. enumerations::= See http://www.csci.csusb.edu/dick/maths/math_77_Enumerations.html.

    5. ontology::= See http://www.csci.csusb.edu/dick/samples/index.html#Ontologies.
    6. an_Ontology_for_English::= See http://www.csci.csusb.edu/dick/maths/logic_8_Natural_Language.html.

    . . . . . . . . . ( end of section Classifications and Ontologies) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End