[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / 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::=
          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 [socket symbol] if you can fill this hole]

          Axiomatic model of Sets of Strings

        13. |-For A,B,C,X :@#T, AXIOMS_OF_SETS_OF_STRINGS.
          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 [socket symbol] if you can fill this hole]



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

      Alonzo Church's Logic

    1. CHURCH::=

        Source: Mendelsohn

      1. string_algebra::=$
        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).

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


      Manna and Waldinger

    2. MW::=
        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::=
        1. P::@strings.
        2. (basis): empty in P.
        3. (step): For u,x (if x in P then u?x in P).


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

      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,
      18. (MW9): head(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::=
        1. P::@strings,
        2. (basis): empty in P,
        3. (step): For all x:non_empty (if tail(x) in P then x in P)


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


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


      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.

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


      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

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


      51. SUBSTRING::=
        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).



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



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


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


      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 [socket symbol] if you can fill this hole]

      Positional Notation

          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.


          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 ]

        8. leading_zeroes::={x:proto_numbers || head(x)=0 and tail(x)<>empty}.

        9. numbers::=protonumbers~leading_zeroes.

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


        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.

        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

        Here is a strange sequence of ideas that might become part of the MATHS approach to strings.
      1. ALTERNATIVE_SETS_OF_STRINGS::=following,
        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 section Partly Baked Idea) <<Contents | End>>

    . . . . . . . . . ( end of section Theories of Strings) <<Contents | End>>

    See Also

  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


  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.