.Open Theories of Strings

Here are some alternate THEORIES of Strings.

.Open The Regular Calculus of John Horton Conway.

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.

	len::#T>-0..,
	(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('!').
	!::infix(#T).
	(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.
.See http://www/dick/maths/math_33_Monoids.html
	|-(JHC3): MONOID ( #T, (!), "").

Extend the monoid  ( #T, (!), "") from strings in #T to a monoid on sets of strings(@#T):
	1::@#T::={""}= `the set of the empty string`.
	For A,B:@#T, A B::={a!b || a in A and b in B}.
	|-(JHC4): MONOID(@#T, ( ), 1).

 For A :@#T,#A is the smallest set X:@#T that satisfies this equation `X = X A | 1`:
	For A :@#T, #A = the smallest {X : @#T || X = X A | 1 }.

. Regular Expressions
	|-(JHC5): SEMI_RING (@#T,( ),(|),(#),1,0)

. Particular Cases
 Regular Sets
.Hole

. Axiomatic model of Sets of Strings
|-For A,B,C,X :@#T, AXIOMS_OF_SETS_OF_STRINGS.
AXIOMS_OF_SETS_OF_STRINGS.::=Net{
	For A,B,C,X :@#T.
	0,1::@#T.
	(S1): A|(B|C)=(A|B)|C,
	(S2): A|B=B|A,
	(S3): A|A=A,
	(S4): A|0=A,

	(S5): A (B C)=(A B) C,
	(S6): 1 A =A 1=A,
	(S7): 0 A =A 0=0,
	(S8): if A B=A then (B=1 or A=0),
	(S9): if A B=B then (A=1 or B=0),

	(S10): A X | 1 = X iff X=#A.

.Hole
}=::AXIOMS_OF_SETS_OF_STRINGS.
}=::JHC.
.Close The Regular Calculus of J H Conway.

. Alonzo Church's Logic

CHURCH::=Net{
.Source Mendelsohn
	string_algebra::=$ Net{
	  (sa0): Set:Sets.
	  (sa1): MONOID(op=>(!), u=>1).
	  (sa2): For all a,b,c:Set ( a=b iff a!c=b!c).
	  (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.
       string_algebra.
       prime::={p:Set || for all x,y:Set(if x!y=p then x=1 or y=1)}~{1}.

      (sa4): for all a<>1, some x,y: Set, p,q:prime(a=p!x and a=y!q).
    (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.
  
	(sa6): For all a:Set~{1},  a=hd(a)!tl(a)=ft(a)!bk(t).
       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{
Manna & Waldinger define strings as those objects generated by prefixing characters to the empty string. 

empty::strings,
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
.See http://www/dick/maths/math_5_Object_Theory.html#GENESYS

nonempty::=strings~{empty}.
  (MW2):for all u:char,x:strings (u?x<>empty).
 (MW3): for all u,v:char,x,y:strings, if u?x=v?y then u=v and x=y.
 (MW4): for all u (u?empty=u).
  |-(MW5): not empty in char.

extend (?) to define empty?x.
	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...

INDUCTION::=Net{
  P::@strings.
  (basis): empty in P.
  (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
   suffix::@(strings, non_empty) ={(x, u?x) || u:char,x:string},
   |- (MW6):  for all y:non_empty, some x:strings(x suffix y).
   . Proof of MW6
		INDUCTION{P=>{y || y=empty or some x:strings(x suffix y)}).

   |-(MW7): suffix in strings (1)-(|char|) non_empty.

   head,tail :: strings^strings,
	(MW8):tail(empty)=empty,
	(MW9):head(empty)=empty,
	(MW10):for x:non_empty, head(x)=the[u:char]for some y(x=u?y)),
	(MW11):for x:non_empty, tail(x)=the suffix(x),
	|-(MW12): for x, x=head(x)?tail(x),
	|-(MW13): for u:char (head(u)=u and tail(u)=empty),
	|-(MW14): map X(X/tail)=generate,
	|-(MW15): for n:Nat0, x:n.th_generation(|x|=|char|^n)
	|-(MW16): {empty}/do(tail)=strings

TAIL_INDUCTION::=Net{
    P::@strings,
    (basis):	empty in P, 
    (step):	For all x:non_empty (if tail(x) in P then x in P)
}=::TAIL_INDUCTION.
|-(Tail_induction)For all TAIL_INDUCTION, P=strings.

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


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

RECURSIVE_DEFINITION::=Net{
  defined:: strings->strings,
  if_empty:: strings,
  if_non_empty:: (char><strings><strings)->strings,
   (rd1):  defined(empty)=if_empty,
   (rd2):  for all u:char,x:string (defined(u!x)=if_non_empty(u,x,defined(x))).
}=::RECURSIVE_DEFINTION.

|-(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(
	defined=>      reversed,
	if_empty=>     empty,
	if_nonempty=>  map[u,x,d](d!u),
).
  |-  reverse::strings->strings,
  |- reverse(empty)=empty,
  |- for u,x, (reverse(u!x)=reverse(x)!u).
  |- for all x,y (reverse(x!y)=reverse(x)!reverse(y)).

AT_END::=Net{
          at_end::strings><strings->@`x is at end of y`.
          (ae1):for x:strings(x at_end empty iff x = empty).
          (ae2): for x,y:strings, if y <>empty then x at_end y iff x=y or x at_end tail(y).
          |-(ae3): x at_end y iff for some z(x!z=y).
}=::AT_END.

SUBSTRING::=Net{
          substr::strings><strings->@.
          (ss1):for x,y, x substr y iff for some z1,z2:strings(z1!x!z2=y).
          |-(ss2): POSET(strings, substr, strict=>proper_substr,  inverse=>supstr,strict_inverse=>proper_supstr).
          |-(ss3): {empty}=min(strings).
          |-(ss4):{empty}=least(strings).
          |-(ss5): for u,x (x proper_substr u!x, x!u).
}=::SUBSTRING.

COMPLETE_INDUCTION::=Net{
   |-(ci1): for P:@strings,  if  P inv (proper_substr)  then P=strings.
          |-(ci2): {strings}=inv(proper_substr).
          |-(ci3): for all x:nonempty~char, some u,v,y, (x=u!y!v).
}=::COMPLETE_INDUCTION.

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

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

}=::MW.


.Open Positional Notation

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

base::Nat,
digits::FiniteSets, 
(pn1): |digits|=base, 
c::digits---0..base-1::=code.
(pn2): c("0")=0.

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

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

STRINGS(char=>digits, nonempty=>proto_numbers).
.See #STRINGS
leading_zeroes::={x:proto_numbers || head(x)=0 and tail(x)<>empty}.

numbers::=protonumbers~leading_zeroes.

Extend c from digits to numbers by
        c::numbers->Nat0
where
        for all u:digits, x:numbers, (c(x!u)=(base*c(x))+c(u)).
then
        |-(pn3) c in numbers---Nat0.

Further `c` can be extended to protonumbers by noting that
	(pn4): for all z:leading_zeroes, one n:numbers ( z in  #"0" {n})
hence
	proper::leadingzeroes->numbers, for all z, for one l:Nat0, z="0"^l!proper(z),
and
	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:
	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.

.Open Project 2

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

  Use your package to:
	1. Calculate and print 2^((2^n)-1),  +(1..n), and *(1..n) for n= 1 to 100.

	2. Calculate (do(n<>1;(2n'=n|2n'=3n+1);n!);n=1) for n= 1 to 100.
.Close Project 2
.Close Positional Notation
.Open Partly Baked Idea
Here is a strange sequence of ideas that might become part of
the MATHS approach to strings.
ALTERNATIVE_SETS_OF_STRINGS::=following,
.Net
 Assuming a definitions of string and operators on sets of strings.
    For n:Nat0, S:@string, S^n ::= `Defined above`.
    For n, S, n S ::= S^n.
.As_is 		4 "abc" = "abcabcabcabc".
.As_is 		2 {"a","bc"} = {"aa","abc","bca","bcbc"}.
    For N:@Nat0, S, N S ::= |[n:N](n S).
.As_is 		1..2 {"a","bc"} = {"a", "bc", "aa","abc","bca","bcbc"}.
()|- Nat0 A = {""} | Nat0 A.
()|- # = Nat0. -- given fixed point definition of "#".
    # ::= Nat0, any number including none.
    N ::= Nat, one or more of.
    O ::= {0,1}, --optional.

(Problem): Is this ambiguous....

.Close.Net ALTERNATIVE_SETS_OF_STRINGS.
.Close Partly Baked Idea
.Close Theories of Strings