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%20Finite%20Sets 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 is

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

    	<--Short--><------------People~Short------------------->

    	<-------People~Tall-----------------><------Tall------->

   This is a common pattern when we have and 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 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.

. . . . . . . . . ( 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

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 = Net{radius:Positive Real, center:Point}.

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

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see