Summary

Name Sample
Substitutions	( x^2+x/(1+x) where x=(exp(y+sin(z)) )
Partial Descriptions	data::=good_data|...
Enumerated types .Item direction::={east, west, north, south}.
Inequality	Two notations: x!=y(C), x<>y (Pascal)

Substitutions

Substitutions create local or private dfinitions that have no meaning outside of the formula or documentation that they are defined.

Example of Substitution

1. (a*x^2+b*x+c where x=3) = for x:=3( a*x^2+b*x+c ) = (9a + 3b +c).

   Both forms bind values to abbreviations in a small area of text only.

   Syntax of Substitution

2. substitution::="(" expression "where" tight_binding #{","tight_binding} ")" | "for" tight_binding #(","tight_binding) "(" expression ")"

   Semantics of Substitution

   Both forms bind values to abreviations for the range of a single expression. Notice that in a tight binding it is not permitted to use the variable as part of the expression that represents its value. This implies that the variable can be replaced by the original without change of meaning. A formula like
3. (a*x^2+b*x+c where x=3) or for x=3( a*x^2+b*x+c )

   becomes

4. (9a + 3b +c)

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

Partial Descriptions, Ellipsis, and Enthymemes

When writing documentation it is usually easier to develop definitions piece meal rather than with all options, constraints, and complications at the same time. The tool for keeping this under control is the Ellipsis symbol ("..."). For example one technique is to start with a broad concept and then add more and more constraints. Thus if a term, t is defined as
1. t::= A & B & C

   then we can quote as facts.

2. |- t::=A &...
3. |- t::=B &...

   It is convenient to allow these to be valid input into a documentation system:

4. restriction::=described_term "::=" intersection "&...",

5. A described term is always the name of a set of possibilities and so can have many descriptions. It must satisfy them all. If t::=S&... then t represents the largest subset S that is a subset of all other descriptions. A term with a definition can be quoted as a description. If declared, then a term that is described as a set of type S must be declared as type @S. Chapter 5 provides the semantics of definitions in general.

   It is best to start from a specific, easily understood subset of the problem and progress to more general forms[Botting 84b]. The development of error handling is an ubiquitous example:

6. all_possible_data::=good_data | erroneous_data | other_data

   So is that of a compiler:

7. compile::=compile_good_program | check_bad_program | reject_non_program

   Thus given that

8. t::=A | B | C,

   then we can quote the following

9. |- t::=A |...,
10. |- t::=B |... .

    Again it should be possible to input a series of additional alternatives into a documentation processor, and have them, checked, appended, etc.

11. additional_alternative::=described_term "::=" selection "|..."

    Formally a set of additional alternatives are combined into a single definition where the term is defined as the union of the separate alternatives.

    It is incorrect to use more than one ellipsis on the same term.

12. description::=additional_alternative | restriction

    These notations are conveniences. Formally they do not exist. They become a set of definitions that are created by either the intersection or union of all the descriptions.

    An incomplete argument is called an enthymeme[Aristotle?]. In MATHS it is an argument with any contiguous set of steps replace by the ellipsis (...) symbol (see Chapter 5). Similarly the ellipsis can be used inside any set of documentation to hide a piece of irrelevant documentation from the reader/user. Online the three dots could react to being selected by expanding to show the details.

    A third form of incompleteness occurs when part of a sequence is left out. Similar - but much more informal - is the use of the ellipsis "..." in mathematical expressions :

13. n*(n+1)/2 = 1+2+3+...+n

    as in the design of bin.p above. These can only be verified if they are accompanied with a formal expression that makes clear what is meantSubstitutions

    Finally, if the class of a structured object is given (C) and a tight enough condition(P) specified, then missing attributes can be predicted that make the object fit the class. Formally, suppose that C is a class with structure N and P a boolean expression containing variable of N then:

14. the C(P) ::= the{ $(N) : C || P} = the $ N and $(N) in C and P.

    Similarly if C has identifers k and data d (C : @N(k)->(d)) then

15. the C(k1=>a1, k2=>a2, ...) ::= the C(k1=a1 and k2=a2 and ...).

    The following syntax is a natural alternative:

16. "the" Base "with" Bindings

17. (the B with L) ::= the{ x:set B || L }

. . . . . . . . . ( end of section Partial Descriptions, Ellipsis, and Enthymemes) <<Contents | End>>

Enumerated types

A definition like

 		direction::={east,north, west, south).

implies

 		direction::Sets.

 		east::direction.

 		north::direction.

 		west::direction.

 		south::direction.

 		|- direction = {east,north, west, south).

In general a defition of a new type as a set of new variables, implicitly declares the variables.

. . . . . . . . . ( end of section Enumerated types) <<Contents | End>>

Inequality

The operator "=" indicates identity or equality. There are two traditional symbols for inequality: "!=" and "<>". Both are (now) leagle in MATHS.

. . . . . . . . . ( end of section CONVENIENCES) <<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, and give them a name. 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.

Notes on the Underlying Logic of MATHS

For a complete listing of pages by topic see [ home.html ]