.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 & 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, 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) For example, the input-output of the Pascal language is described by: PascalIO::=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)) }=::PascalIO. on::@(files,files)=rel a,b(for some c:#S(a!c=b). For a:records, b:files. b:!a=(b'=(b!a)). --See $STANDARD_ASSIGNMENTS b!:a=((b!a)=b'). --See$STANDARD_ASSIGNMENTS 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 img, '|', or 'post' operator. Is 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. $TBA. }=::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, |, {}, , {()}, #) . Tagged Sequences and Parsing TAGGED_SEQUENCES::=Net{ This is a Partly-Baked-Idea. Better then Half-baked. Alternative - para_grammar tagged_sequence::= "(" (tag":"|) item #((tag":"|)item) ")", tag::=symbolic_identifier, item::=See regular expressions (a:#0 b:#1 a:#0 b:#1) ={ a b a b||a:#0, b:#1}==>#0#1#0#1 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 ...) means |{(... a .... a ...)|| a:A&B}. Further tags keep their binding across intersections (... a:A...)&(...a:B...) means |{(...a...)&(...b...)||a:A&B}, and even in tuples: ((...a:A...) , (...a:B...) ) means |{((...a...) , (...a...) )||a:A&B}. However, these bindings do not reach past '|' or '#' or beyond a single definition. 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. Perhaps, if B and C are @#char, the tags in A::syntax=(b:B c:C), imply A::semantics=Net{ b:B.semantics, c:C.semantics}. }=::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::=Net{ For a:#records, A:@records, a /& A:: #records a /& A ::= .( 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). }. Filtering::=Projection. 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), and bag(a)=bag(b)+bag(c), and |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(b,c)do( ( u?:b | u?:c ); a:!u)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)) -- .See [Ginsburg66] 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)))} ) -- .See [Dillonetal86] }=::Interleaving. }=::Other_operations. . Expressions on a set of elements For e:syntax, regular(e) ::syntax=Regular(REGULAR(element=>e)) REGULAR::=Net{ element::Finite_sets. Regular::@#element, SERIAL(Regular, sequence, vertical_bar), sequence::@#element. SERIAL(sequence, regular_item, ()), regular_item::@#element, regular_item::=(hash|)( element |"(" regular ")" ). }=::REGULAR. For A:Alphabet, event_expressions(A) ::=$Event_expressions(EVENT(A)). EVENT(A) ::=Net{ Event_expressions::@#A, SERIAL(Event_expressions, $shuffle, "|"). shuffle::@#A, SERIAL(shuffle,$sequenceE, "<*>"), sequenceE::@#A, SERIAL(sequenceE, \$phase, ()), phase::=("#"|)( 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. . See Also STANDARD_ASSIGNMENTS::=http://www/dick//maths/math_11_STANDARD.html#ASSIGNMENTS.