.Open CONVENIENCES
. Summary
.Table
Name Sample
.Row
Substitutions
.Item
( x^2+x/(1+x) where x=(exp(y+sin(z)) )
.Row
Partial Descriptions
.Item
data::=good_data|...
.Row Enumerated types
.Item direction::={east, west, north, south}.
.Row Inequality
.Item Two notations: x!=y(C), x<>y (Pascal)
.Close.Table
.Open Substitutions
Substitutions create local or private dfinitions that have no meaning outside of the formula or documentation that they are defined.
. Example of Substitution
(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
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
(a*x^2+b*x+c where x=3)
or for x=3( a*x^2+b*x+c )
becomes
(9a + 3b +c)
.Close Substitutions
.Open 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
t::= A & B & C
then we can quote as facts.
|- t::=A &...
|- t::=B &...
It is convenient to allow these to be valid input into a documentation system:
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:
all_possible_data::=good_data | erroneous_data | other_data
So is that of a compiler:
compile::=compile_good_program | check_bad_program | reject_non_program
Thus given that
t::=A | B | C,
then we can quote the following
|- t::=A |...,
|- t::=B |... .
Again it should be possible to input a series of additional alternatives into a documentation processor, and have them, checked, appended, etc.
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.
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 :
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:
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
the C(k1=>a1, k2=>a2, ...) ::= the C(k1=a1 and k2=a2 and ...).
The following syntax is a natural alternative:
"the" Base "with" Bindings
(the B with L) ::= the{ x:set B || L }
.Close Partial Descriptions, Ellipsis, and Enthymemes
.Open Enumerated types
A definition like
.As_is direction::={east,north, west, south).
implies
.As_is direction::Sets.
.As_is east::direction.
.As_is north::direction.
.As_is west::direction.
.As_is south::direction.
.As_is |- direction = {east,north, west, south).
In general a defition of a new type as a set of new variables,
implicitly declares the variables.
.Close Enumerated types
. Inequality
The operator "=" indicates identity or equality. There are two traditional symbols
for inequality: "!=" and "<>". Both are (now) leagle in MATHS.
.Close CONVENIENCES