.Open Re-use & Inheritance
. Basis
Because the MATHS notation includes the idea of naming a
piece of documentation
.See http://www/dick/maths/notn_15_Naming_Documentn.html
.See http://www/dick/maths/notn_13_Docn_Syntax.html
.See http://www/dick/maths/notn_14_Docn_Semantics.html
it is possible to use the name as a reference to that documentation
that implies its reuse in the current document. This page goes into
the details of a natural an powerful idea.
. Re-using Documentation
Named documentation is often used to construct elements, maps, sets etc..
.Net
Suppose
.As_is X::=Net{ a:A, b:B, W(a,b...)}.
.As_is Y::=Net{ parts of Y, S:=$ X, more parts of Y}.
Then it is as if the definition of Y had been written:
.As_is 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:
.As_is .See X_s_URL#X
or if there is link in the form of a $remote_definition:
.As_is X::=X_s_URL#X.
.Close.Net
The name of a piece of documentation can appear in other pieces of documentation referring to the original. This has an effect similar to that of 'inheritance' in object oriented programming languages - in essence the content of the named documentation replaces the name.
.Net
Suppose
.As_is X::=Net{ a:A, b:B, W(a,b...)}
.As_is Z::=Net{ parts of Y, X, more parts of Y}.
Then it is as if the definition of Z had been written:
.As_is 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:
.As_is W1::=Net{ parts of Y, definition(X), more parts of Y}.
.As_is W2::=following
.As_is .Net
.As_is parts of Y
.As_is X::=X_s_URL#X
.As_is more parts of Y
.As_is .Close.Net
Then it is as if the definition of W had been written:
.As_is W::=Net{ parts of Y, X:=Net{a:A, b:B, W(a,b...)}, more parts of Y}.
.Close.Net
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
.As_is WORSE::=Net{ a+b=c }.
.As_is 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
(1): For all a:A,b:B, if W(a,b) then W2(a).
X::=Net{ a:A, b:B, W(a,b). |- W2(a) }
Z::=Net{ parts of Y, X, more parts of Y}.
.Close.Let
Then Z's context consists of X's context plus the definition of X itself,
and so the reuse of X within Z is valid. Similarly a document that makes
use of an identifier that is declared in the environment rather than the
document (A,B above for example) must also be defined (or declared) in the
context in which the document is used. However in a context without a
formula that at least implies (1) above, it is not valid to re-use Z.
Notice that if a piece of documentation has no theorems or undeclared
identifiers then it can be reused in any context.
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", "+" }`
M::=Net { Nat0:Sets, 0:Nat0, +:serial(Nat0), for all s:Nat0( s+0 = 0+s = s ) }.
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
MONOID::=http://www/dick/maths/math_31_One_Associative_Op.html#MONOID
and substituting:
MONOID( Set=>Nat0, op=> +, unit=>0). [
.See Modified Re-Use
below]
Now, we know that the natural numbers with zero form a monoid under
addition, so, in any context where the natural numbers are available (the
standard one), we could re-use `M`:
|-(2): M.
But to assert `M` like this means (apparently) that the declaration of $M
are added to our document and redefine 0, + and Nat0!
Thus we have the following rule:
When a piece of documentation `D1` is
re-used in document `D2` and `x` is a variable declared in `D1` like this
.As_is x::S
for 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:
Nat0 in Sets.
0 in Nat0.
+ in serial(Nat0).
for all s:Nat0( s+0 = 0+s = s ).
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:
()|-(3): $M.
Meaning that the four formulae above are theorems.
. Proof of 3
By inspection.
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:
.Uses list of names
.Used_by list of names
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.
. Modified Re-Use
A name can be followed by operations that describe modifications to the
documentation to which it refers. These work as if they generated an
edited copy that is inserted in place of the modified name.
For example suppose
.As_is X::=Net{ a:A, b:B, W(a,b...)},
.As_is 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:
.As_is Net{ parts of Y, x:A, x:B, W(x,y...), more parts of Y}.
If
.As_is V1::=Net{ parts of Y, X with P, more parts of Y},
then it as if V1 was written
.As_is Net{ parts of Y, a:A, b:B, W(a,b...). P. more parts of Y}.
. Extension
Experience of object-oriented technology and methods
provides convincing evidence of the
need to take previous work and quickly extend it by adding new features
and/or constraints. MATHS has two predefined notations to do this.
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):
.As_is N with v:S
.As_is N with{ D }
.As_is N with following
.As_is .Net
.As_is D
.As_is .Close.Net
If a set S is defined as $ N then
S and w::= $ Net{ N. w . }.
S with {D}::=$ Net{ N. D. }.
A common example:
ALGEBRA::=Net{ Set:Sets }.
SEMIGROUP ::= ALGEBRA with op:associative(Set).
MONOID::= SEMIGROUP with u:neuter(op).
. Inheritance
Notice that a new formal system can easily be created that inherits
features from many different formal systems -- merely by asserting them:
RING::=following,
.Net
|- (r1): GROUP(Set, +, 0, -).
|- (r2): MONOID(Set, *, 1).
|- (r3): (*) distributes_over (+).
...
.Close.Net
The result is a system (a logic, an algebra, a model, ...) that
satisfies the properties of both its parent systems. MATHS includes
multiple inheritance... just like its less formal
parent "mathematics" did.
.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.
.Open Summary
. Documentation is Data
Documentation can be assigned names in definitions. The simplest document is a net of declarations, definitions, comments and assertions:
.As_is Name::=following,
.As_is .Net
.As_is documentation
.As_is .Close.Net
or a name or term defined to equal one of these nets. It is reused by by using the name plus some simple changes
.As_is 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:
.As_is 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:
.As_is documentation(for some list_of_hidden_terms)
Similarly it is possible to hide all variables and terms except a specified subset, by using a `projection`.
.As_is documentation.(list_of_variables_to_be_kept)
Parts can be added to a defined network as well:
.As_is documentation with element
Two or more pieces of documentation can also be combined using the Boolean
operations.
If a document is basic (it has no definitions or theorems) then it is
possible to remove axioms from it
.As_is 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.
. Example -- Piping two specifications
Suppose that `N1` is the name of some documentation describing a variable called `output`
and `N2` is the name of documentation that describes a variable `input` then
(N1 and N2 and output=input)(for some input, output),
specifies a process that connects N1 to N2 and hides the connection.
. Beyond Re-use
In MATHS combining documentation is merely a notational convenience. A
full calculus could be developed in the future. The basis will be an
equivalence relation or congruence on pieces of documentation. Two pieces
of documentation are semantically equivalent if they have the same
signature (variables and types) and for all values of the variables the
constraints are equal. Thus D1 and D2 are equivalent if they are of the
same type and define the same set of tuples:
For Documentation D1,D2, if signature(D1)=signature(D2) then D1 equivalent D2::= ($ D1 = $ D2) else D1 equivalent D2::=false.
In the example above, `Z` is equivalent to `Y and X`.
.Close Summary
.Open Formal description of Reuse
.See http://www/dick/maths/notn_15_Naming_Documentn.html
.See http://www/dick/maths/notn_13_Docn_Syntax.html
.See http://www/dick/maths/notn_14_Docn_Semantics.html
.Open Syntax
elementary_piece_formal_documentation::=... | cross_reference,
cross_reference::=(document_description | simple_reference) citation.
PROPOSITION(elementary_proposition=>elementary_document, proposition=>document_description).
.See http://www/dick/maths/logic_10_PC_LPC#PC.
elementary_document::=net | re_used_document.
simple_reference::= "With" Name,
directive::=(".Used_by" | ".See" |".Use" ) #Name EOLN.
citation::= ".See" URL EOLN.
A remote definition is a useful way to define a term by quote the
definition of the same (or other) term in another documentation:
remote_definition::= term_defined ":" ":" optional_type = URL.
URL::=`Uniform Resource Locator`,
A URL specifies a protocol, a host and further information identifying
a resource on the World Wide Web.
For s:Syntax, re_used(s) ::= s #( (substitution | quantification)| "." projection | deletion ).
reused_documentation::=re_used(name_of_documentation).
. Simple changes
substitution::="(" L( term "=>" expression ) ")". -- All substitutions in the list are done simultaneously.
quantification::="(" "for some" L(term ) ")".
projection::= "." P(term).
deletion::= "without" P(label).
. Examples of Substitution and Hiding
Note. Below '=' is short for 'equivalent'.
.As_is ABC2::= Net{a:A, b:B(a), c:=C(a,b), P(a,b,c)}, where C:A>< |B >->T.
.As_is ABC2 = Net{a:A, b:B(a), c:T, c=C(a,b), P(a,b,c)}.
.As_is ABC2(a=>x, b=>y, c=>z) = Net{x:A, y:B(x), z:=C(x,y), P(x,y,z)}.
.As_is If x in A, and y and a and y+a in B(x) then
.As_is ABC2(a=>x, b=>y+a, c=>z) = ABC2(b=>y+a, a=>x, c=>z)
.As_is = Net{x:A, z:=C(x,y+a), P(x,y+a,z)}.
.As_is 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))}.
.As_is ABC2(a=>1,b=>2)(c=>z) = Net{z:=C(1,2), P(1,2,C(1,2))}.
.As_is ABC2(a=>1,b=>2)(c=>z).z = z::=C(1,2). P(1,2,C(1,2))
. Example of unusual Substitution
.As_is 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)}.
. Example of deletion
.As_is ABC3 = Net{x:A, y:B(x), (L): P(x,y)}.
.As_is ABC3 without L = Net{x:A, y:B(x) }.
A modification can be any sequence of operations:
name_of_documentation operation operation ...
. Example
.As_is R::=Net{ a:X, b:Y, W1(a,b)}, S::=Net{c:Y, d:Z, W2(c,d)}
Formula Expansion
.As_is (R(b=>u) and S(c=>u)).(a,d) a::X, d::Z, for some u:Y ( W1(a,u) and W2(u,d) )
.Close Syntax
.Open Semantics
. Reuse
Let X,Y, and Z be valid sets of documentation. Let Z be made by putting one or more copies of X's name into Y as an elementary pieces of formal documentation,
.As_is variables(Z) = variables(Y) | variables(X),
.As_is declarations(Z) = declarations(Y) | { (v,T1):declarations(X) || for no T2 ((v,T2):declarations(Y))},
.As_is definitions(Z) = definitions(Y) | { (t,T,e1):definitions(X) || for no e2 ((t,T,e2):definitions(Y))},
.As_is assertions(Z) = assertions(Y) | hide(variables(Y) & variables(X)) o substitute({ (t,T,e1):definitions(X)
.As_is | for some e2 ((t,T,e2):definitions(Y))})( assertions(X)),
where
For V:@variables(X),a:assertion, hide(V)(a):assertion, hide({})(a)=(a),
For v:variable, V:@variables(X),a:assertion, hide({v}|V)(a)=for some v:types(v,X)(hide(V)(a)),
For D:@definitions(X), substitute(V)(a):assertion, substitute({})(a)=(a),
For d:definitions(X), D:@definitions(X),a:assertion, substitute({(t,T,e)}|V)(a)=for t:T=e(v,X)(substitute(D)(a))
Note that multiple (or even circular) re-use generates only one copy of definitions, assertions, etc..
. Modification
The normal modification is substituting a free variable for a defined term
or declared variable(parameter). This a straight forward, almost syntactic
operation.
AB::=Net{ a:A, b:B=f(a) }.
AB(x,y) = Net{ x:A, y:B=f(x)},
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:
AB(1,2) = Net{ 1 in A, 2 inB, 2=f(1)}.
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:
EX::=AB(A=>Nat, B=>Nat, f=>++).
=following,
.Net
a:Nat.
b:Nat= a+1.
.Close.Net
and so
EX(1,2) = Net{ 1 in Nat, 2 in Nat, 2=1+1 } = Net{true}.
Thus we can claim a theorem:
()|-EX(1,2).
.Close Semantics
.Close Formal description of Reuse
.Open Combining named documentation
Operations are shown as modifications to the names of pieces of documentation, but NOT on the named documents themselves. Referring to a piece of documentation with a modification does not change the original - the original is used as a basis for the new, inserted documentation.
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.
. With
The `with` operator is an abbreviation for combining a network with a
simple list of declarations and axioms P:
N with P::= N and Net{P}.
. Negation
The formal definition of the result of negating a name describes a structure:
For X : name of pieces of documentation, declarations(not X ) = declarations(X) and definitions( not X ) = definitions(X) and assertions(not X) = not constraint(X)
. Example of negation
If
.As_is ABC2::=following.
.As_is .Net
.As_is a::A,
.As_is b::B(a),
.As_is c::=C(a,b),
.As_is P(a,b,c)
.As_is .Close.Net
then
.As_is Formula Expansion
.As_is not ABC2 a::A,
.As_is b::B(a),
.As_is c::=C(a,b),
.As_is not P(a,b,c)
. Boolean combinations
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:
For X : name of piece of documentation, Y an elementary piece or another name, *:{and,or,iff,if__then__},
declarations(X * Y) = declarations(X) | declarations(Y) and definitions(X * Y) = definitions(X) | definitions(Y) and assertions(X * Y) ={ constraint(X) * constraint(Y)}.
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.
. Example of Boolean Operations
.As_is AB::=Net{ a:A, b:B}, XY::=Net{ x:A, y:B}.
.As_is Formula Expansion
.As_is AX and XY a,x:A, b,y:B
.As_is AB and Net{x:X} a:A, x:X, b:B(a), c:=C(a,b), P(a,b,c)
.As_is ABC2 or a=b a:A, b:B(a), c:=C(a,b), P(a,b,c) or a=b
.As_is if ABC2 then a=c a:A, b:B(a), c:=C(a,b), if P(a,b,c) then a=c
.Close Modifying named documentation
. Noting and defining
Section headings give a name to part of a document and also includes it as part of the document. A definition attaches a name to be bound to a piece of documentation but without the content being inserted in the document. To name a piece of documentation for future use,
.As_is Name "::=" cross_reference.
Later the name can be used or modified and inserted.
.Open Example
If
.As_is ABC2::=following.
.As_is .Net
.As_is a::A,
.As_is b::B(a),
.As_is c::=C(a,b),
.As_is P(a,b,c)
.As_is .Close.Net
then
.As_is Net{a:A. ALEPH:=ABC2(x,y,z). aleph:=$ ALEPH(x=a). }
becomes
.As_is Net{ a:A.
.As_is aleph::=$ Net{ y:B(a), z:=C(a,y), P(a,y,z) }.
.As_is }
.Close
Another variation is to import a copy of the definition of a named piece of documentation into another piece of documentation:
.As_is .As_is Use N
or
.As_is With N
inserts the original
.As_is 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:
.As_is N.x.
.Open Example of Use/With
If
.As_is ABC2::=following.
.As_is .Net
.As_is a::A,
.As_is b::B(a),
.As_is c::=C(a,b),
.As_is P(a,b,c)
.As_is .Close.Net
then
.As_is Net{ a:X. Use ABC2. Y(ABC2.a, a)}
becomes
.As_is Net{
.As_is a::X.
.As_is ABC2::=Net{ a:A, b:B(a), c:=C(a,b), P(a,b,c) }.
.As_is Y(ABC2.a, a)
.As_is }
.Close
. Parametric or Generic Documentation
In MATHS we create documentation with declared terms so that it can be used for similar purposes by substituting and/or hiding the them.
.Open Example of Generic Documentation
.As_is SERIAL
.As_is .Net
.As_is This defines a generalized pre/post/infix expression.
.As_is b::=basis::@#char, -- a parameter
.As_is f::=function_symbols::@#char.
.As_is e::=expression::= b | p "." f | f p | b #(f b),
.As_is p::=parameter_pack::= b | left b #(separator b) right.
.As_is .Close.Net
.As_is For all x,y,z:@#char,SERIAL(x,y,z) ::=SERIAL(b=>x, f=>y, e=>z, for some p).
Hence
.As_is SERIAL(b=>primary,f=>(times|divide),e=>term,for some p),
.As_is SERIAL(b=>expression,f=>(plus|minus),e=>primary,for some p).
Or even
.As_is term:=SERIAL(b=>primary,f=>(times|divide), for some p).e
.As_is primary::=SERIAL(b=>expression,f=>(plus|minus),for some p).e
.Close
. Formulae defined as documentation
MATHS lets the writer define an expression whose meaning is a piece of documentation, once certain substitutions are carried out:
.As_is "For" declare_arguments "," model_expression "::=" "Net{" documentation "}"
An example,
For A,B:variable, Either A or B::=Net{ A,B:@. A iff not B.},
For A,B,C:variable, Either A, B, or C::=Net{ A,B,C:@. if A then not B and not C else Either B or C.}.
. Quantified Documentation.
If N is the name of documentation s, n::= |declarations(s)| and d is a list of all declarations(s) in some order and Q a list of n quantifiers, and v is the list of variables in d (in the same order) and X is declared to be of type @N then
@{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.
For X:@$ D then (for Q1 v1, Q2 v2, ...(X)) ::= Q1 d1, Q2 d2,...($(N) in X).
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).
. Dynamics
A dynamic proposition is any proposition with a primed variable in it. The
primed variables are said to be dynamic variables, and the remainder
static. Such predicates a not completely specified until the types of the
variables are specified. A piece of documentation that declares the
variables and includes a dynamic predicate describes a change of state.
The space of states is defined by the declarations. Additional static
propositions state any invariants that are maintained. A prime is used
only in wffs, and not used in declarations because a primed variable is
implicitly declared as being the same type as the unprimed version.
There follows a summary, for more details see:
.See http://www/dick/maths/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
.As_is X::=Net{ a:A, W1(a) },
.As_is Y::=Net{ a:A, W2(a, a')}
then
.As_is $ X={a:A || W1(a) }
and has type @A
but
.As_is $ 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
.As_is D2 ::=Net{D1, W(x1',x2',x3',...,x1,x2,x3,...)}
.As_is where x1,... in variables(D1).
Thus
.As_is assertions(D2)=assertions(D1)|{`W(x1',...,x1, ...)`}
Let z=(z1,z2,...)=variables(D)~{x1,x2,x3,...} then in D2
.As_is (1) A duplicate set of `x`s are implicitly added to D1's variables.
.As_is variables(D2) =variables(D) | {x1,...} | {x1',...} | {z1',...}
.As_is (2) The relation is constrained by the requirement that static variables do not change.
.As_is 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:
HAILSTONE::=following.
.Net
State::=Net{ n: Nat },
Op1::=Net{ $State, 2*n'=3*n+1},
Op2::=Net{ $State, 2*n'=n},
End::=Net{ $State, n=1}.
Delta::= $Op1 or $Op2.
()|- pre($ $Delta) = pre ($ $Op1) | pre ($ $Op2) =$State.
()|- no pre($ $Op1) & pre ($ $Op2).
()|- State >== {pre($ Op1) , pre($ Op2)},
()|- $ $End.$ $Op1.$ $Op2=$ $End.
??{ Nat. do($ $Delta) = $ $End. }??
Loop::=Net{State, n'=n}.
??{ For all n0, if $ Net{State, n=n0}==>$ Net{State, n=n0}. do($ Op1 | $ Op2) then n0 in {1,2}. }??
.Close.Net
. Theory
There is a suitable theory of the MATHS re_use in
.See [Wirsing90].
.Close Re-use & Inheritance