.Open Strings

Uses LANGUAGES.
Uses MATHS_COMMON.
Uses GRAMMARS.

T::Types.

MATHS_STRINGS::=Net{
	S::@T, 
	#S::@#T=`strings/sequences/lists/files of S's`.
	#S=|{1..n->S || n:Nat0 },
	for all a:S, n:Nat0, a^n=[i:1..n]a in #S,
	len::#S->Nat0 = [a]|a|,
	|- for all a:#S, len(a)=|a| in Nat0, |a|=|dom(a)|=`The number of elements in a`.
	|- for all a:#S, R:@(S,S), R(a)=for all i:1..|a|-1(a[i] R a[i+1]).
	|- for all a:#S, f:S->X, f(a)=f o a in #X.
	|- for all a:#S, o:(S><S)->S & serial,
	 o(a)=1st(a) o o(rest(a))=`a1 o a2 o a3...`.
	|- for all a:#S,b:S, b./a={i:1..|a| || a(i)=b}=`The positions of bs in a`.
	For all a:#S, bag(a) ::=[b:|a]|b./a|::=`The bag of elements in a`.
	|- for all a:#S, |(a)=img(a)=`The set of elements in a`.
	For all a:#S, I:@(1..|a|), a[I]::=(+(min(I)-1);I;a,  a[I]::=`Subarray of elements in a`.
	|- for all a:#S, i:1..|a|, i a[..i]=(1..i);a.
	|- for all a:#S, i,j:1..|a|, a[i..]=(+(i-1));a.
	(!): :#S><#S+>#S=`Concatenation of (1st) and (2nd)`,
	SERIAL(!),
	So |- !(a,b,c)=a!b!c.
	for all a,b:#S, a!b in S^(1..|a|+|b|).
	for all a,b:#S, a!b=(if 1..|a| then a else (-|a|);b).
	|- len in (#S,!,{()})->(Nat0,+,0).
	GENESYS (basis=>S|{()}, generator=>map A:@#S({s!a || s:S, a:A}, free).
	rest::#S->#S.
	for all a:#S( a=() or a<>() and a=1st(a)!rest(b)  )
	prefix::#S->@#S,
	For all s:#S, prefix(s) ::={u:#S || for some v:#S (u ! v = s)}
	(?) is a special operation that can only operates when one operand is a single element.  
	It used for stripping of a single item from the ends of the string:
	For all s:#S, a:S, a?s::=a!s.
	For all s,t,u:#S, if s?t=u then len(s)=1 and s!t=u.
 If there was a up-side-down query in ASCII then it would be used for the reverse operator.

}=::STRINGS.


STREAMS::=Net{
	records::Sets,
	EOF::Things~records
	STRINGS(char=>records,strings=>files,head=>first,tail=>rest)

	Pascal::=Net{
	        buffer::(files->records)=map [f](if(len(f)>0,first(f), EOF)
	        get::(@(files,files))=rel [f1,f2](f2=rest(f1))
	        put::(records->@(files,files))=map[ r](rel f1,f2(f2=f1!r))
	}=::Pascal.
	on::@(files,files)=rel a,b(for some c:#S(a!c=b)

	b:!a=(b'=(b!a))		--See STANDARD
	b!:a=((b!a)=b')		--See STANDARD

 For a:records, b:files,
	a?:b::=((a?b')=b)   -- a is a single character by '?'
	a'?:b==>/a!:b  --- /b!:a = (b=(b'!a')) in (1)-(many)
	for A:@#records, A?:b::=for some a:A(b=a!b')
	Note that a?:b and {a}?:b are different.
	b:?a::=(b=(b'!a) and len(a)=1)	-- useful for deques and stacks.
Streams can be output into unordered sets by using the '|' or 'post' relation, while its inverse '/|' extracts a sequence from a set that fits what the input requires.  '|' and '/|' give random access to data.  This imples a powerful query language.

}=::STREAMS.

. Languages

 For T:Types.
 For A in finite(T), Languages(A) ::=@#A,
	@#A =`sets of finite sequences of elements of A`

 For X,Y,Z:@#A,
	MONOID( Languages(A), op=>[X,Y]{x!y||x:X, y:Y}, u=>{""}, free(A))
	(X Y) ::={x!y || x:X, y:Y}
	(X Y Z) ::=(X (Y Z))

expression(#@A) ::=$ $GRAMMAR,tagged.para_regular_expression

#:@#A->@#A, for all X:@#A, #X={()}.do(map Y:@#A((Y X)))=free(X)

RegularAlgebra(@#A, |, {}, , {()}, #)


.Roadworks_ahead
??{
TAGGED_SEQUENCES::=Net{	This is a Partly-Baked-Idea. 
 		Alternative - para_grammar

	tagged_sequence::= "(" (tag":"|) item #((tag":"|)item) ")",
	tag::=symbolic_identifier,
	item::=`See regular expressions`
Tags are variables bound to sets of strings that appear in expressions defining other sets of strings. Parts of a sequence with the same tags represent equal strings. An expression like
	(... a:A ... a:B ...) ::=|{(... a .... a ...)|| a:A&B}
Further tags keep their binding across intersections
	(... a:A...)&(...a:B...) ::=|{(...a...)&(...b...)||a:A&B},
and even
	((...a:A...) , (...a:B...) ) ::=|{((...a...) , (...a...) )||a:A&B}.
However, there bindings do not reach past '|' or '#' or a single definition.
.Example.
	a:#0 b:#1 a:#0 b:#1 ={ a b a b||a:#0, b:#1}==>#0#1#0#1

Tags can also be interpreted as defining maps, so for example if
	A::=#(b:B c:C),
then we might expect b:#(B C)->#B, c:#(B C)->#C.

}=::TAGGED_SEQUENCES.
}?

}=::MATHS_STRINGS.

. Categorical result

A system is 'categorical' if its model is determined up to isomophism.
This means that the axioms determine - upto the particular notation - a standard normal form.  All systems described by either Church's or Manna's  axioms (CHURCH and MW) are isomorphic to (#X,'!',"") defined above (MATHS_STRINGS)
          some X with X---chars.

. Typographical theory
WIDTH::=Net{
In general the typographical width of a string is not the same as its length because characters can vary in width:
width::chars->Real.
width::strings->Real.
 width in (monoid)(strings,!,())->(Real,+,0)
}=::WIDTH.

. Filters and Decorators
Other_operarations::=Net{
  These are developed 30 to 40 years after the original work on strings.
Useful for expressing information hiding in CSP and constrained expressions.

Projection::=Filtering::=Net{
 For a:#records, A:@records,
	a /& A:: #records= if a="" then "" else
		if |a|>=1 and a[1] in A then a!(rest(a)/& A)
		else (rest(a)/& A).
|-	(_/& A) in (monoid) (#records,!,"")->(#A,!,""),
	|- 	(a!b) /& A = (a/&A)!(b/&A), ""/&A="".

|- 	(_/&(A&B)) = (_/&A);(_/&B).
	|- 	a/&(A&B) = (a/&A)/&B=a.(_/&A);(_/&B).
}

decorators::=Net{
Used for expresing semantics of processes with multiple streams of Input and output.
 For a,b,x:#T,  a//x//b::##T=map [i](a x[i] b)
    "i:"//"101001"//"?"->("i:1?", "i:0?", "i:1?", "i:0?", "i:0?", "i:1?")

 For all a,b,x:#T, a//x//b=(a!_)o(_!b)o(x)

 For *:infix(T), a,b:T, x:#T, a/*/x/*/b::#T=map [i:dom(x)](a * x[i] * b)
      a/*/x/*/b=(a *_)o(_* b)o(x)

}

Interleaving::=Net{
Used for expressing semantics of processes with multiple streams of Input and output being combined in an undetermined manner. Appears in CSP and also in theory of constrained expressions. Similar to the JSD concept of a rough merge.
Special case of free merge in process algebra.
	<+>:: #T><#T->@#T.
	for b,c:#T, b<+>c = {a:#T|| b=c=a=()
		 or 1st(a)=1st(b) and rest(a) in rest(b)<+>c 
		 or 1st(a)=1st(c) and rest(a) in rest(c)<+>b}.
	|- for b,c, b<+>c = c<+>b.

	|- for b,c, a:b<+>c, len(a)=len(b)+len(c),
		bag(a)=bag(b)+bad(c),
		|a=|b | |c.

	|- for b,c, a:b<+>c, i,j:|\b,k,l:|\a,
		if  b[i]=a[k] and b[j]=a[l] and i<j then k<l.

	(x,y)+>(b,c)do( ( u?:b | u?:c ); a:!x)a+>z iff z in x<+>y.

	For a1,a2:#T, a1 phase a2::= for some b,c ( a1 and a2 in b<+>c).

	|- do phase = @(#T,#T).

	for f:#T->X,
	 if for b,c:#T, a1,a2:b<+>c(f(a1)=f(a2))
	 then for p:(1)-(1), f o p = f.

	for a:#T, card{(b,c) ||a in b<+>c}=2^(len(a)).

	Hence <+>{(1,2,3),(2,3,4),(1,3,4)}, and so on...

	For A:B:@#T, A<+>B::= |{a<+>b || a:A, b:B}.

	for A,B:Regular(T) (A<+>B in Regular(T))  --[Ginsburg 66]

	For A:@#T, <*>A ::="".do(_<+>A)

	|- For a,b:T ( <*>{a!b}={x:#{a,b}||Card(/x(a))=Card(/x(b))
		 and for #{a,b} u,v where u!v=x (Card(/u(a))>=Card(/u(b)))} )

 			--[Dillon et all 86]

}=::Interleaving.

}=::Other_operations.


. Expressions on a set of elements

 For e:syntax, regular(e) ::syntax=Regular(REGULAR(element=>e))
REGULAR::=Net{ 
	SERIAL(Regular, sequence, vertical_bar),
	SERIAL(sequence, regular_item, ()),
	regular_item::=(hash|)( element |"(" regular ")" ).

}=::REGULAR.

 For A:Alphabet, event_expressions(A) ::=Event_expressions(EVENT(A)).
EVENT(A) ::=Net{
	SERIAL(Event_expressions, shuffle, vertical_bar),
	SERIAL(shuffle, sequence, "<*>"),
	SERIAL(sequence, vertical_bar),
	SERIAL(sequence, phase, ()),
	phase::=(hash|)( A |"(" Event_expressions ")" ).
}=::EVENT.


Constrained_Expressions::= Net{
Regular expressions with constraints on various subalphabets. --[Dillon et all 86]
A::Alphabet.
Events==>A,
Subsets::@@A,
 For all S:Subsets, \kappa(S) ::=event_expressions(S)

\eta::regular(A).

constrained_prefixes::={ u:prefix(\eta) ||
			for all S:Subsets( u/&S in \kappa(S))
			},

language::=constrained_prefixes /& Events.

}=::Constrained_Expressions.

. Substitution

SUBSTITUTION::=Net{
	Use STRINGS.
	For a,b:strings,
		(a|+>b) ::=rel [x,y:strings](for some w,z:strings(x=w!a!z and y=w!b!z).

	substitutions::={(a|+>b)||a,b:strings}.
       
	For a:strings, (a|-.) ::=rel [x,y](x=y and not a substr x).

Example. P::=do(1|+>0);(1|-.) then P converts all 1's into 0's

 Production systems- set of substitutions ...
}=::SUBSTITUTION.

.Close Strings
. Alternatives
.See http://www/dick/maths/math_61_String_Theories.html#ALTERNATIVE_SETS_OF_STRINGS.