Theories of Strings

Here are some alternate THEORIES of Strings.

The Regular Calculus of John Horton Conway.

JHC::=
Net{
1. len::#T>-0..,
2. (JHC1): For all s:#T, i:1..len(s), s[i] in T. Notice that when len(s) =0 then we have the empty (or null) string exhibitted here between two quotes: "".
  Given two strings we can concatenate them('!').
3. !::infix(#T).
4. (JHC2): For s,t in #T, len(s!t)=len(s)+len(t) and if i<=len(s) then (s!t)[i] = s[i] and if i>len(s) then (s!t)[i]=t[i-len(s)].
  We can show that concatenation forms a monoid with the null or empty string is the unit. [ math_33_Monoids.html ]
5. |- (JHC3): MONOID ( #T, (!), "").
  Extend the monoid ( #T, (!), "") from strings in #T to a monoid on sets of strings(@#T):
6. 1::@#T::={""}= the set of the empty string.
7. For A,B:@#T, A B::={a!b || a in A and b in B}.
8. |- (JHC4): MONOID(@#T, ( ), 1).
9. For A :@#T,#A is the smallest set X:@#T that satisfies this equation X = X A | 1:
10. For A :@#T, #A = the smallest {X : @#T || X = X A | 1 }.
  
  Regular Expressions
11. |- (JHC5): SEMI_RING (@#T,( ),(|),(#),1,0)
  
  Particular Cases
12. Regular Sets [click here if you can fill this hole]
  
  Axiomatic model of Sets of Strings
13. |-For A,B,C,X :@#T, AXIOMS_OF_SETS_OF_STRINGS.
14. AXIOMS_OF_SETS_OF_STRINGS.::=
  Net{
  1. For A,B,C,X :@#T. 0,1::@#T.
  2. (S1): A|(B|C)=(A|B)|C,
  3. (S2): A|B=B|A,
  4. (S3): A|A=A,
  5. (S4): A|0=A,
  6. (S5): A (B C)=(A B) C,
  7. (S6): 1 A =A 1=A,
  8. (S7): 0 A =A 0=0,
  9. (S8): if A B=A then (B=1 or A=0),
  10. (S9): if A B=B then (A=1 or B=0),
  11. (S10): A X | 1 = X iff X=#A.
    [click here if you can fill this hole]
  }=::AXIOMS_OF_SETS_OF_STRINGS.
}=::JHC.

. . . . . . . . . ( end of section The Regular Calculus of J H Conway.) <<Contents | End>>

Alonzo Church's Logic

CHURCH::=
Net{
1. string_algebra::=$
  Net{
  1. (sa0): Set:Sets.
  2. (sa1): MONOID(op=>(!), u=>1).
  3. (sa2): For all a,b,c:Set ( a=b iff a!c=b!c).
  4. (sa3): For all a,b,c,d:Set if a!b=c!d then for some x:Set(a!x=c or c!x=a).
  }=::string_algebra.
2. string_algebra.
3. prime::={p:Set || for all x,y:Set(if x!y=p then x=1 or y=1)}~{1}.
4. (sa4): for all a<>1, some x,y: Set, p,q:prime(a=p!x and a=y!q).
5. (def, sa4)|- (sa5): for all a<>1, one x,y: Set, p,q:prime(a=p!x and a=y!q). For all a:Set~{1}, hd(a),bk(a) ::prime. For all a:Set~{1}, tl(a),ft(a) ::Set.
6. (sa6): For all a:Set~{1}, a=hd(a)!tl(a)=ft(a)!bk(t).
7. a sub_string b::= for some x,y:Set(x!a!y=b).
  (sa7): len::(monoid)string_algebra(set, (!), 1)->(Nat, +, 0).
}=::CHURCH.
Manna and Waldinger
MW::=
Net{
1. empty::strings,
2. char::@strings, (?) ::char><strings->strings=prefix character onto string.
  .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 ]
3. nonempty::=strings~{empty}.
4. (MW2): for all u:char,x:strings (u?x<>empty).
5. (MW3): for all u,v:char,x,y:strings, if u?x=v?y then u=v and x=y.
6. (MW4): for all u (u?empty=u).
7. |- (MW5): not empty in char.
  extend (?) to define empty?x.
8. For all x:strings, empty?x::=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...
9. INDUCTION::=
  Net{
  1. P::@strings.
  2. (basis): empty in P.
  3. (step): For u,x (if x in P then u?x in P).
  }=::INDUCTION.
  (Induction): For all INDUCTION, P=strings. This has important implications that are not normally noted. For example it means that all strings have a finite length - they result from a finite number of prefix operations. Also it makes sure that the set of strings is a connected acyclic graph. In turn this allows us to apply Structural Induction in language theory and data directed design.
  
  Head and Tail Operations
10. suffix::@(strings, non_empty) ={(x, u?x) || u:char,x:string},
11. |- (MW6): for all y:non_empty, some x:strings(x suffix y).
12. . Proof of MW6
13. INDUCTION{P=>{y || y=empty or some x:strings(x suffix y)}).
14. |- (MW7): suffix in strings (1)-(|char|) non_empty.
  head,tail :: strings^strings,
15. (MW8): tail(empty)=empty,
16. (MW9): head(empty)=empty,
17. (MW10): for x:non_empty, head(x)=the[u:char]for some y(x=u?y)),
18. (MW11): for x:non_empty, tail(x)=the suffix(x),
19. |- (MW12): for x, x=head(x)?tail(x),
20. |- (MW13): for u:char (head(u)=u and tail(u)=empty),
21. |- (MW14): map X(X/tail)=generate,
22. |- (MW15): for n:Nat0, x:n.th_generation(|x|=|char|^n)
23. |- (MW16): {empty}/do(tail)=strings
24. TAIL_INDUCTION::=
  Net{
  1. P::@strings,
  2. (basis): empty in P,
  3. (step): For all x:non_empty (if tail(x) in P then x in P)
  }=::TAIL_INDUCTION.
25. |-(Tail_induction)For all TAIL_INDUCTION, P=strings.
  
  Concatenation
  .Note CONCATENATION is defined by making (!) the extension of (?) from (char><strings) to (strings><strings).
26. CONCATENTATION::=
  Net{
  1. !::(strings~char)><strings->strings concatenation of two strings
    (conc1): for y (empty!y=y)
    (conc2): for u,x,y((u?x)!y=u?(x!y)).
  }=::CONCATENTATION.
27. |- (conc3): (!) in (strings><strings->strings) | (char><strings->strings).
28. ! is automatically generalized to operate on sets of strings
29. (STANDARD)|- (conc4): for X,Y:@strings, X!Y={x!y||x:X, y:Y}.
30. |- (conc5): monoid(strings, ! , empty).
31. |- (conc6): for x (x!empty=x).
32. |- (conc7): ! in associative(strings).
33. |- (conc8): for x,y, if x!y=x then y=empty.
34. |- (conc9): for x,y, if x in nonempty then head(x!y)=head(x) and tail(x!y)=tail(x)!y).
35. |- (conc10): for x,y:strings,u,v:char, if x!u=y!u then x=y and u=v.
36. |- (conc11): strings>=={{empty}, char, char ! strings ! char}.
37. |- (conc12): for x, (x=empty or x in char or for some u,v,y (x=u!y!v)).
38. |- (conc13): for x,y, if x ! y = empty then x=y=empty.
39. RECURSIVE_DEFINITION::=
  Net{
  1. defined::strings->strings,
  2. if_empty::strings,
  3. if_non_empty::(char><strings><strings)->strings,
  4. (rd1): defined(empty)=if_empty,
  5. (rd2): for all u:char,x:string (defined(u!x)=if_non_empty(u,x,defined(x))).
  }=::RECURSIVE_DEFINTION.
40. |- (RD1): $ Net{if_empty:strings, if_non_empty:char><strings><strings->strings)} in id($ RECURSIVE_DEFINITION).
  |-(RD2): for all if_empty:strings, all if_non_empty::char><strings><strings->strings, one defined::strings->strings (constraints(RECURSIVE_DEFINITION))
  
  Example of Recursive Definition
  RECURSIVE_DEFINITION(
41. defined=> reversed,
42. if_empty=> empty,
43. if_nonempty=> map[u,x,d](d!u), ).
44. |- reverse::strings->strings,
45. |-reverse(empty)=empty,
46. |-for u,x, (reverse(u!x)=reverse(x)!u).
47. |-for all x,y (reverse(x!y)=reverse(x)!reverse(y)).
48. AT_END::=
  Net{
  1. at_end::strings><strings->@x is at end of y.
  2. (ae1): for x:strings(x at_end empty iff x = empty).
  3. (ae2): for x,y:strings, if y <>empty then x at_end y iff x=y or x at_end tail(y).
  4. |- (ae3): x at_end y iff for some z(x!z=y).
  }=::AT_END.
49. SUBSTRING::=
  Net{
  1. substr::strings><strings->@.
  2. (ss1): for x,y, x substr y iff for some z1,z2:strings(z1!x!z2=y).
  3. |- (ss2): POSET(strings, substr, strict=>proper_substr, inverse=>supstr,strict_inverse=>proper_supstr).
  4. |- (ss3): {empty}=min(strings).
  5. |- (ss4): {empty}=least(strings).
  6. |- (ss5): for u,x (x proper_substr u!x, x!u).
  }=::SUBSTRING.
50. COMPLETE_INDUCTION::=
  Net{
  1. |- (ci1): for P:@strings, if P inv (proper_substr) then P=strings.
  2. |- (ci2): {strings}=inv(proper_substr).
  3. |- (ci3): for all x:nonempty~char, some u,v,y, (x=u!y!v).
  }=::COMPLETE_INDUCTION.
  Palindromes
51. palin::=palindromes::#T={x || x=reverse(x)}.
52. |- (pal): palin={y!reverse(y) || y:strings} | {y!u!reverse(y) || for some u,y}.
  
  Length
53. length::strings->Nat0, len=length. For s:strings, |s|=len(s).
54. (l0): For s:strings, |s|=generation(s).
55. |- (l1): for u:char,x:strings, (length(u!x)=1+length(x)).
56. |- (l2): for u:char, (|u|=1).
57. |- (l3): length in (monoid)(strings,!,empty)->(Nat0,+,0).
}=::MW.
Positional Notation
1. POSITIONAL_NOTATION::=
  Net{
  1. base::Nat,
  2. digits::FiniteSets,
    (pn1): |digits|=base,
  3. c::digits---0..base-1::=code.
    (pn2): c("0")=0.
  4. Convention. In all western notations - c("0")=0, c("1")=1.
    
    Note
    In ASCII, EBCDIC and many other character codes there is a map
  5. ord::characters---0..|characters|,
  6. For x:char, c(x)=ord(x)-ord("0").
    STRINGS(char=>digits, nonempty=>proto_numbers). [ #STRINGS ]
  7. leading_zeroes::={x:proto_numbers || head(x)=0 and tail(x)<>empty}.
  8. numbers::=protonumbers~leading_zeroes.
    Extend c from digits to numbers by
  9. c::numbers->Nat0 where
  10. for all u:digits, x:numbers, (c(x!u)=(base*c(x))+c(u)). then
  11. |-(pn3) c in numbers---Nat0.
    Further c can be extended to protonumbers by noting that
  12. (pn4): for all z:leading_zeroes, one n:numbers ( z in #"0" {n}) hence
  13. proper::leadingzeroes->numbers, for all z, for one l:Nat0, z="0"^l!proper(z), and
  14. For all z, c(z)::=c(proper(z)).
  }=::POSITIONAL_NOTATION.
  Exercise 1
  What do we call POSITIONAL_NOTATION when digits={"0","1"}, base=2.
  
  Exercise 2
  Examine the POSITIONAL_NOTATION generated by digits ={"0"} - called Unary.
  
  Exercise 3
  Examine the POSITIONAL_NOTATION where you assume that the base can be negative:
2. Int::= -|digits| rather than base:Nat. (Hint: Knuth Volume 2)
  
  Exercise 4
  Using POSITIONAL_NOTATION define plus:numbers><numbers->numbers where c(x plus y)=c(x)+c(y).
  
  Project 1
  Using POSITIONAL_NOTATION define all the normal arithmetic operators (add, subtract, multiply, modulus, divide,...) on numbers.
  
  Project 2
  1. Use your package to:
  2. 1. Calculate and print 2^((2^n)-1), +(1..n), and *(1..n) for n= 1 to 100.
  3. 2. Calculate (do(n<>1;(2n'=n|2n'=3n+1);n!);n=1) for n= 1 to 100.
  . . . . . . . . . ( end of section Project 2) <<Contents | End>>
. . . . . . . . . ( end of section Positional Notation) <<Contents | End>>
Partly Baked Idea
1. ALTERNATIVE_SETS_OF_STRINGS::=following,
  Net
  1. Assuming a definitions of string and operators on sets of strings.
  2. For n:Nat0, S:@string, S^n::= Defined above.
  3. For n, S, n S::= S^n.
```
 		4 "abc" = "abcabcabcabc".
```
```
 		2 {"a","bc"} = {"aa","abc","bca","bcbc"}.
```
  4. For N:@Nat0, S, N S::= |[n:N](n S).
```
 		1..2 {"a","bc"} = {"a", "bc", "aa","abc","bca","bcbc"}.
```
  5. (above)|-Nat0 A = {""} | Nat0 A.
  6. (above)|-# = Nat0. -- given fixed point definition of "#".
  7. #::= Nat0, any number including none.
  8. N::= Nat, one or more of.
  9. O::= {0,1}, --optional.
    
    (Problem): Is this ambiguous....
  (End of Net ALTERNATIVE_SETS_OF_STRINGS.)
. . . . . . . . . ( end of section Partly Baked Idea) <<Contents | End>>

. . . . . . . . . ( end of section Theories of Strings) <<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

STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

Glossary

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

given::reason="I've been told that...", used to describe a problem.

given::variable="I'll be given a value or object like this...", used to describe a problem.

goal::theorem="The result I'm trying to prove right now".

goal::variable="The value or object I'm trying to find or construct".

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.

hyp::reason="I assumed this in my last Let/Case/Po/...".

QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.

QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.

RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.