[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / math_61_String_Theories
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 2 14:30:55 PDT 2011

# Theories of Strings

Here are some alternate THEORIES of Strings.

## The Regular Calculus of John Horton Conway.

1. JHC::=
Net{
The set of all strings of symbols of type T is written (#T). All strings have a length and is the number of symbols in the string. Thus for s in #T we have len(s) in 0.. and when len(s) >0 then for all i in 1..len(s), s[i] in T.

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

1. CHURCH::=
Net{

Source: Mendelsohn

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

2. MW::=
Net{
Manna & Waldinger define strings as those objects generated by prefixing characters to the empty string.

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.

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.

15. head::strings^strings, picks the first character out of a string.
16. tail::strings^strings, picks all the characters except the first out of a string.
17. (MW8): tail(empty)=empty,
19. (MW10): for x:non_empty, head(x)=the[u:char]for some y(x=u?y)),
20. (MW11): for x:non_empty, tail(x)=the suffix(x),
21. |- (MW12): for x, x=head(x)?tail(x),
22. |- (MW13): for u:char (head(u)=u and tail(u)=empty),
23. |- (MW14): map X(X/tail)=generate,
24. |- (MW15): for n:Nat0, x:n.th_generation(|x|=|char|^n)
25. |- (MW16): {empty}/do(tail)=strings

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

27. |-(Tail_induction)For all TAIL_INDUCTION, P=strings.

## Concatenation

.Note CONCATENATION is defined by making (!) the extension of (?) from (char><strings) to (strings><strings).
28. 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.

29. |- (conc3): (!) in (strings><strings->strings) | (char><strings->strings).
30. ! is automatically generalized to operate on sets of strings
31. (STANDARD)|- (conc4): for X,Y:@strings, X!Y={x!y||x:X, y:Y}.
32. |- (conc5): monoid(strings, ! , empty).
33. |- (conc6): for x (x!empty=x).
34. |- (conc7): ! in associative(strings).
35. |- (conc8): for x,y, if x!y=x then y=empty.
36. |- (conc9): for x,y, if x in nonempty then head(x!y)=head(x) and tail(x!y)=tail(x)!y).
37. |- (conc10): for x,y:strings,u,v:char, if x!u=y!u then x=y and u=v.
38. |- (conc11): strings>=={{empty}, char, char ! strings ! char}.
39. |- (conc12): for x, (x=empty or x in char or for some u,v,y (x=u!y!v)).
40. |- (conc13): for x,y, if x ! y = empty then x=y=empty.

## Recurive definitions of functions.

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

42. |- (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(
43. defined=> reversed,
44. if_empty=> empty,
45. if_nonempty=> map[u,x,d](d!u), ).
46. |- reverse::strings->strings,
47. |-reverse(empty)=empty,
48. |-for u,x, (reverse(u!x)=reverse(x)!u).
49. |-for all x,y (reverse(x!y)=reverse(x)!reverse(y)).

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

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

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

53. palindromes::#T={x || x=reverse(x)}.
54. palin:=palindromes.
55. |- (pal): palin={y!reverse(y) || y:strings} | {y!u!reverse(y) || for some u,y}.

## Length

56. length::strings->Nat0, len=length. For s:strings, |s|=len(s).
57. (l0): For s:strings, |s|=generation(s).
58. |- (l1): for u:char,x:strings, (length(u!x)=1+length(x)).
59. |- (l2): for u:char, (|u|=1).
60. |- (l3): length in (monoid)(strings,!,empty)->(Nat0,+,0).

}=::MW.

## Exercise -- Front and back operations

Front and back are dual to head and tail. The back of a non-empty string is the last element in the string and the front is all the rest of the string except the back:
3. back::strings^strings.
4. front::strings^strings.
5. |-for x:strings~empty, length(back) = 1.
6. |-for x:strings~empty, front(x) ! last(x) = x.

[click here if you can fill this hole]

## Positional Notation

1. POSITIONAL_NOTATION::=
Net{
Representing numbers as strings of numbers. Use MW. Generalized from Manna et al as an application of strings.

1. base::Nat, Type DIGITS.
2. digits::Finite_sets(DIGITS),
(pn1): |digits|=base,
3. code::digits---0..base-1.
4. c::=code.
(pn2): c("0")=0.

5. Convention. In all western notations - c("0")=0, c("1")=1.

### Note

In ASCII, EBCDIC and many other character codes there is a map
6. ord::characters---0..|characters|,
7. For x:char, c(x)=ord(x)-ord("0").

STRINGS(char=>digits, nonempty=>proto_numbers). [ #STRINGS ]

Extend c from digits to numbers by

10. c::numbers->Nat0 where
11. for all u:digits, x:numbers, (c(x!u)=(base*c(x))+c(u)). then
12. |-(pn3) c in numbers---Nat0.

Further c can be extended to protonumbers by noting that

13. (pn4): for all z:leading_zeroes, one n:numbers ( z in #"0" {n}) hence
14. proper::leadingzeroes->numbers, for all z, for one l:Nat0, z="0"^l!proper(z), and
15. 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

What is the largest number that this POSITIONAL_NOTATION describes? Implement a similar unlimitted length arithmetic in your favorite programming system.

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

Here is a strange sequence of ideas that might become part of the MATHS approach to strings.
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>>

1. STANDARD::= See http://cse.csusb.edu/dick/maths/math_11_STANDARD.html, and [ intro_standard.html ] (introduction to the standard definitions).

# 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

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

# Glossary

3. 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).
4. given::reason="I've been told that...", used to describe a problem.
5. given::variable="I'll be given a value or object like this...", used to describe a problem.
6. goal::theorem="The result I'm trying to prove right now".
7. goal::variable="The value or object I'm trying to find or construct".
8. 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.
9. hyp::reason="I assumed this in my last Let/Case/Po/...".
10. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
11. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
12. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.