Here are some alternate THEORIES of Strings.
Given two strings we can concatenate them('!').
We can show that concatenation forms a monoid with the null or empty string is the unit.
[ math_33_Monoids.html ]
Extend the monoid ( #T, (!), "") from strings in #T to a monoid on sets of strings(@#T):
. . . . . . . . . ( end of section The Regular Calculus of J H Conway.) <<Contents | End>>
Source: Mendelsohn
(sa7): len::(monoid)string_algebra(set, (!), 1)->(Nat, +, 0).
.Note MW define the infix(string) concatenation in terms of the simpler operation of prefixing a character to a string. MATHS defines (?) as an operator which is a special case of (!) - when one or other operand is a single character.
(MW1): GENESYS(strings) and generate=[X]{c?x||c:char,x:X}and basis={empty} and loop_free
[ GENESYS in math_5_Object_Theory ]
extend (?) to define empty?x.
The above properties of '?' are vital to establish inductive arguments and recursive defintions. If the prefix operator can't be used to disect a composite object in a unique way then it becomes difficult to define more complicated ideas like interleaving and hence concurrency...
|-(RD2): for all if_empty:strings, all if_non_empty:char><strings><strings->strings, one defined::strings->strings (constraints(RECURSIVE_DEFINITION))
[click here if you can fill this hole]
STRINGS(char=>digits, nonempty=>proto_numbers). [ #STRINGS ]
Extend c from digits to numbers by
Further c can be extended to protonumbers by noting that
What is the largest number that this POSITIONAL_NOTATION describes? Implement a similar unlimitted length arithmetic in your favorite programming system.
. . . . . . . . . ( end of section Project 2) <<Contents | End>>
. . . . . . . . . ( end of section Positional Notation) <<Contents | End>>
4 "abc" = "abcabcabcabc".
2 {"a","bc"} = {"aa","abc","bca","bcbc"}.
1..2 {"a","bc"} = {"a", "bc", "aa","abc","bca","bcbc"}.
(Problem): Is this ambiguous....
. . . . . . . . . ( end of section Partly Baked Idea) <<Contents | End>>
. . . . . . . . . ( end of section Theories of Strings) <<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