Net
X::=Net{ a:A, b:B, W(a,b...)}.
Y::=Net{ parts of Y, S:=$ X, more parts of Y}.
Then it is as if the definition of Y had been written:
Y::=Net{ parts of Y, S:={ a:A, b:B || W(a,b...) }, more parts of Y}.
However, if the definition of X changes, then so does the definition of Y. There is no need for the definition of X to be in the same physical document if there is a ".See" directive:
.See X_s_URL#Xor if there is link in the form of a remote_definition:
X::=X_s_URL#X.
X::=Net{ a:A, b:B, W(a,b...)}
Z::=Net{ parts of Y, X, more parts of Y}.
Then it is as if the definition of Z had been written:
Z::=Net{ parts of Y, a:A, b:B, W(a,b...), more parts of Y}.
However, if the definition of X changes, then so does the definition of Z. The "X" in Z acts like a kind of "hot-linked macro". As above a ".See" directive permits the use of terms defined in other documents. A copy of the definition of X can also be imported or inherited in two ways:
W1::=Net{ parts of Y, definition(X), more parts of Y}.
W2::=following
.Net
parts of Y
X::=X_s_URL#X
more parts of Y
.Close.Net
Then it is as if the definition of W had been written:
W::=Net{ parts of Y, X:=Net{a:A, b:B, W(a,b...)}, more parts of Y}.
When name of a piece of documentation is used in another piece of documentation then some of the declarations and definitions of the referenced documentation become part of the document that makes the reference. Other definitions and declarations may be redefined or redeclared and so be hidden. This follows the Rule of the Most Visible Meaning - symbols in an expression always refer to the most visible definition or declaration of the symbols that fits their particular context in the expression.
When included documentation is inserted and includes a document that has already been included then this inclusion has no effect. Circular re-usage also has no effect.
The key logical problem is that re-used documentation is quoted "out of context". This is similar to questions of dynamic and static scoping in programming language semantics. The formal semantics implies that identifers that appear in a piece of document but not defined in it can gain a meaning from the document in which they are re-used. This is close to dynamic scoping -- each re-use of a document may create a different binding for identifiers that are free in the re-used document. Therefore it wise to design documents for re-use that have no free variables: all variable should be bound as parameters or to terms. So, for example, given
WORSE::=Net{ a+b=c }.
BETTER::=Net{ Set:Sets, a,b,c:Set, a+b=c}.then WORSE has three free variables that can take on new meanings, but BETTER only has Sets free and this is defined in the MATHS's STANDARD package.
Further, a re-used piece of documentation looses its original context.
If a piece of documentation
makes use of an assumption that is stated in its definition's environment,
then it can not be validly used in another document unless that document
recreates the context in which the original was defined. It is wise then
to design special pieces of documentation (Nets) that state their
assumptions explicitly. On the other hand: to insist that every re-usable
piece of documentation explicitly states its contextual assumptions seems
to be a heavy burden for the producer of the documentation. For example:
suppose
Let
The declared variables in piece of documentation are effectively parameters for that documentation. One interesting question is what happens when a piece of documentation is re-used in a context where a parameter (declared variable) is bound to a fixed meaning. For example: M below has three variables { "Nat0", "0", "+" }
We don't expect to see the symbols "0" and "+" used like this, perhaps. But, this is equivalent to the basic definition that results by taking the generic monoid
and substituting:
Thus we have the following rule:
x::Sfor some set S and also appears as a constant in D2, then the declaration is converted into an axiom x in S in D2.
So in any context where natural number exist, re-using or citing M above, effectively the following formulae:
Finally note that since these are all true in a context that define Nat0 as the natural numbers with 0, we would like assert M as a theorem:
A documentation system would help the users to disclose and hide the content quickly and easily. Either an 'out liner' or a hypertext model is an appropriate implementation. The system needs to also record the use of a given piece of documentation, and ensure that when the used documentation is changed then the all references to it are automatically kept in step - or (at least) protected from losing the linkage. When feasible a documentation system will make visible to a viewer the dependencies between documents buy placing two directives near the start of the document:
This ideal is difficult to reconcile with the freewheeling nature of the World-Wide Web. What happens if you refer to a document that someone else has written, and owns. How can they know? Can they be forced to maintain their end of the link? What happens if they need to revise their document -- formal documents evolve by a dialectical process of proposal, refutation, and improvement? I don't think there is any real solution to this problem. Clearly it means that it is best to link to documents that appear stable: well argued, reasonable, and based on stable assumptions. Clearly it means that it is necessary to regularly review links. Finally it is very wise to tell the author that you need the link and for authors to maintain a subscriber list who can be notified when changes are about to happen.
Perhaps some form of deprecation process should be introduced. In standard deprecated features are likely not to be supported in a future version.
For example suppose
X::=Net{ a:A, b:B, W(a,b...)},
V::=Net{ parts of Y, X(a=>x, b=>c), more parts of Y},
then it is as if the definition of V had been written:
Net{ parts of Y, x:A, x:B, W(x,y...), more parts of Y}.If
V1::=Net{ parts of Y, X with P, more parts of Y},
then it as if V1 was written
Net{ parts of Y, a:A, b:B, W(a,b...). P. more parts of Y}.
First to add a constraint w to a document named N right 'N and w'. This is a simple reuse notation described earlier.
To add a set of features (including both declarations and wffs) use: "with".
This is again a simple abbreviation.
(with):
N with v:S
N with{ D }
N with following
.Net
D
.Close.Net
If a set S is defined as $ N then
A common example:
.Dangerous_Bend
However there is a danger in combining a pair of systems like this. You may end up describing a class that can not exists - a triangle with four sides. Therefore it is important that whenever you reuse a mathematical system you always create an example that satisfies all the rules you have gathered together. For example the Natural numbers {0,1,2,3,...} satisfy the three axioms r1, r2, r3 above.
This may also help your readers understand what you are getting at.
Name::=following,
.Net
documentation
.Close.Netor a name or term defined to equal one of these nets. It is reused by by using the name plus some simple changes
Name(changes)The changes include applying substitutions, quantifications, and projections to the documentation (left to right).
Variables and terms can be changed when referring to some documentation:
documentation(old=>new, ... )The above names the result of replacing all free occurrences of old in the documentation by new. New can be a constant, expression, or a variable.
Terms can also be bound and so hidden:
documentation(for some list_of_hidden_terms)
documentation.(list_of_variables_to_be_kept)
documentation with element
If a document is basic (it has no definitions or theorems) then it is possible to remove axioms from it
basic_documentation without (list_of_axioms)However this is deprecated because it indicates that there is a simpler network of assumptions that could have been studied first.
These (possibly modified) pieces of documentation can be combined as if they were propositions - MATHS defines the resulting documentation, it does not entail any logical calculus of documentation yet (unlike Z). The result of editing and combining can be used as a macro in any other piece of documentation. These structures can be used any where the name of a local piece of documentation can be used.
The usage of terms needs be documented (automatically) in both the reference and also in the referred to documentation.
In the example above, Z is equivalent to Y and X.
. . . . . . . . . ( end of section Summary) <<Contents | End>>
PROPOSITION(elementary_proposition=>elementary_document, proposition=>document_description). [ logic_10_PC_LPC#PC] .
A remote definition is a useful way to define a term by quote the definition of the same (or other) term in another documentation:
ABC2::= Net{a:A, b:B(a), c:=C(a,b), P(a,b,c)}, where C:A>< |B >->T.
ABC2 = Net{a:A, b:B(a), c:T, c=C(a,b), P(a,b,c)}.
ABC2(a=>x, b=>y, c=>z) = Net{x:A, y:B(x), z:=C(x,y), P(x,y,z)}.
If x in A, and y and a and y+a in B(x) then
ABC2(a=>x, b=>y+a, c=>z) = ABC2(b=>y+a, a=>x, c=>z)
= Net{x:A, z:=C(x,y+a), P(x,y+a,z)}.
ABC2(a=>x, c=>b)(for some b) = Net{x:A, for some b:B(x)(b=C(x,b) and P(x,b,b))}.
ABC2(a=>1,b=>2)(c=>z) = Net{z:=C(1,2), P(1,2,C(1,2))}.
ABC2(a=>1,b=>2)(c=>z).z = z::=C(1,2). P(1,2,C(1,2))
ABC2(a=>2, b=>3, c=>1) = Net{2 in A, 3 in B(2), 1 in T, 1=C(2,3), P(1,2,3)}.
ABC3 = Net{x:A, y:B(x), (L): P(x,y)}.
ABC3 without L = Net{x:A, y:B(x) }.
A modification can be any sequence of operations:
R::=Net{ a:X, b:Y, W1(a,b)}, S::=Net{c:Y, d:Z, W2(c,d)}Formula Expansion
(R(b=>u) and S(c=>u)).(a,d) a::X, d::Z, for some u:Y ( W1(a,u) and W2(u,d) )
. . . . . . . . . ( end of section Syntax) <<Contents | End>>
variables(Z) = variables(Y) | variables(X),
declarations(Z) = declarations(Y) | { (v,T1):declarations(X) || for no T2 ((v,T2):declarations(Y))},
definitions(Z) = definitions(Y) | { (t,T,e1):definitions(X) || for no e2 ((t,T,e2):definitions(Y))},
assertions(Z) = assertions(Y) | hide(variables(Y) & variables(X)) o substitute({ (t,T,e1):definitions(X)
| for some e2 ((t,T,e2):definitions(Y))})( assertions(X)),where
Note that multiple (or even circular) re-use generates only one copy of definitions, assertions, etc..
When a general expression is substituted then some more complex things occur. So if a predefined term replaces a parameter it can not be redeclared. Instead the declaration becomes a constraint added to the term:
In other words when a globally defined expression replaces a term then the effect is to replace declarations by assertions. Further if these are already true they can be omitted. For example consider:
Thus we can claim a theorem:
. . . . . . . . . ( end of section Semantics) <<Contents | End>>
. . . . . . . . . ( end of section Formal description of Reuse) <<Contents | End>>
The simplest operation is to just add more elementary pieces of documentation to what already exists. This done by the 'and' operator.
Boolean operations ({ not, and, or, if.then., iff...}) are used to combine pieces of documentation.
ABC2::=following.
.Net
a::A,
b::B(a),
c::=C(a,b),
P(a,b,c)
.Close.Netthen
Formula Expansion
not ABC2 a::A,
b::B(a),
c::=C(a,b),
not P(a,b,c)
When two pieces of documentation are combined, common variables and terms must have compatible declarations or definitions. The formal definition of the result of a boolean operation between two named is:
The result will not be valid if X and Y give two different definitions to a term in a single context, or two different declarations to a variable. Sometimes one piece of documentation declares a variable that is defined as a term in the other piece. This is OK, as long as the type of the definition is that of the declaration.
AB::=Net{ a:A, b:B}, XY::=Net{ x:A, y:B}.
Formula Expansion
AX and XY a,x:A, b,y:B
AB and Net{x:X} a:A, x:X, b:B(a), c:=C(a,b), P(a,b,c)
ABC2 or a=b a:A, b:B(a), c:=C(a,b), P(a,b,c) or a=b
if ABC2 then a=c a:A, b:B(a), c:=C(a,b), if P(a,b,c) then a=c
. . . . . . . . . ( end of section Modifying named documentation) <<Contents | End>>
Name "::=" cross_reference.Later the name can be used or modified and inserted.
ABC2::=following.
.Net
a::A,
b::B(a),
c::=C(a,b),
P(a,b,c)
.Close.Netthen
Net{a:A. ALEPH:=ABC2(x,y,z). aleph:=$ ALEPH(x=a). }becomes
Net{ a:A.
aleph::=$ Net{ y:B(a), z:=C(a,y), P(a,y,z) }.
}
Another variation is to import a copy of the definition of a named piece of documentation into another piece of documentation:
.As_is Use Nor
With Ninserts the original
N::=Net{... x:X. ...}.Thus the effect is like 'with' in Ada: Terms defined in N's documentation can only be referred to by qualifying by the name N by their name:
N.x.
ABC2::=following.
.Net
a::A,
b::B(a),
c::=C(a,b),
P(a,b,c)
.Close.Netthen
Net{ a:X. Use ABC2. Y(ABC2.a, a)}becomes
Net{
a::X.
ABC2::=Net{ a:A, b:B(a), c:=C(a,b), P(a,b,c) }.
Y(ABC2.a, a)
}
SERIAL
.Net
This defines a generalized pre/post/infix expression.
b::=basis::@#char, -- a parameter
f::=function_symbols::@#char.
e::=expression::= b | p "." f | f p | b #(f b),
p::=parameter_pack::= b | left b #(separator b) right.
.Close.Net
For all x,y,z:@#char,SERIAL(x,y,z) ::=SERIAL(b=>x, f=>y, e=>z, for some p).
Hence
SERIAL(b=>primary,f=>(times|divide),e=>term,for some p),
SERIAL(b=>expression,f=>(plus|minus),e=>primary,for some p).
Or even
term:=SERIAL(b=>primary,f=>(times|divide), for some p).e
primary::=SERIAL(b=>expression,f=>(plus|minus),for some p).e
"For" declare_arguments "," model_expression "::=" "Net{" documentation "}"An example,
@{N ||for (Q1 v1, Q2 v2, Q3 v3,...,Q[n] v[n])}::= {X:@$ N|| for Q1 d1, Q2 d2, ..., Q[n] d[n] ( constraint(s)) }.
Notice that X:@$ N, so X satisfies the constraints of N.
(for Q1 v1, Q2 v2, Q3 v3,...,Q[n] v[n](N)) ::= for Q1 d1, Q2 d2, ..., Q[n] d[n] ( constraint(s)).
Notice that this is meaningless whenever there are no constraints defined in N.
A useful abbreviation is to use the name of the documentation rather than listing all the remaining variables.
(for Q1 v1, Q2 v2,...Q[p] v[p], Q[q] N) ::= for Q1 d1, Q2 d2, ..., Q[p] d[p], Q[q] d[p+1],..., Q[q] d[n](N).
There follows a summary, for more details see: [ math_14_Dynamics,html ]
A dynamic proposition in a piece of documentation means that the '$' operator forms a set of pairs or binary relation rather than a set of single states. For example, if
X::=Net{ a:A, W1(a) },
Y::=Net{ a:A, W2(a, a')}then
$ X={a:A || W1(a) }and has type @A but
$ Y=rel[a,a':A](W2(a,a') )and has type @(A,A).
If 'D2' is a piece of documentation with one or more dynamic variables in it then
$ D2=rel[ declarations(D2), primed(declarations(D2)] (constraint(D2) and static variable do not change)
The declarations(D2) are list of the declarations of D2.The primed(declarations(D2) are declarations of D2 with a prime added to each variable. So (unlike Z) the primed variables are implicitly in the same state space as the unprimed variables.
Consider a piece of documentation D1 with no dynamic propositions in it and documentation
D2 ::=Net{D1, W(x1',x2',x3',...,x1,x2,x3,...)}
where x1,... in variables(D1).Thus
assertions(D2)=assertions(D1)|{`W(x1',...,x1, ...)`}
Let z=(z1,z2,...)=variables(D)~{x1,x2,x3,...} then in D2
(1) A duplicate set of `x`s are implicitly added to D1's variables.
variables(D2) =variables(D) | {x1,...} | {x1',...} | {z1',...}
(2) The relation is constrained by the requirement that static variables do not change.
constraint(D2) = constraint(D1) and z1'=z1 and z2'=z2 and ...
The Z idiom of defining the state space separately is also used in MATHS. Here is an example from recreational mathematics:
. . . . . . . . . ( end of section Re-use & Inheritance) <<Contents | End>>
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 ]
For a more rigorous description of the standard notations see