[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / notn_3_Conveniences
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Oct 25 10:16:52 PDT 2010

# CONVENIENCES

## Summary

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

(Close Table)

## 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 "&...",

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. TBD 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:

5. all_possible_data::=good_data | erroneous_data | other_data

So is that of a compiler:

6. compile::=compile_good_program | check_bad_program | reject_non_program

Thus given that

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

then we can quote the following

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

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

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

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

When a term has several alternative meaning and they overlap then the first one defined takes priority??

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 :

12. 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:

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

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

The following syntax is a natural alternative:

15. "the" Base "with" Bindings

(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

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.