[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng Dept] / [R J Botting] / [ MATHS ] / math_62_Strings
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Nov 16 14:36:05 PST 2009

Contents

    Strings

      Uses LANGUAGES. Uses MATHS_COMMON. Uses GRAMMARS.

    1. T::Types.

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


      }=::STRINGS.

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

        For example, the input-output of the Pascal language is described by:

      4. PascalIO::=
        Net{
        1. buffer::(files->records)=map [f](if(len(f)>0,first(f), EOF)
        2. get::(@(files,files))=rel [f1,f2](f2=rest(f1))
        3. put::(records->@(files,files))=map[ r](rel f1,f2(f2=f1!r))

        }=::PascalIO.
      5. on::@(files,files)=rel a,b(for some c:#S(a!c=b).

      6. For a:records, b:files.

      7. b:!a=(b'=(b!a)). --See STANDARD_ASSIGNMENTS
      8. b!:a=((b!a)=b'). --See STANDARD_ASSIGNMENTS

        a?:b::=((a?b')=b), -- a is a single character by '?'

      9. a'?:b==>/a!:b,


      10. (above)|-/b!:a = (b=(b'!a')) in (1)-(many)

      11. For A:@#records, A?:b::=for some a:A(b=a!b')

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

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

    7. For X,Y,Z:@#A,
    8. 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))

    9. 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 ??{

    10. TAGGED_SEQUENCES::=
      Net{
        This is a Partly-Baked-Idea.
      1. Alternative - para_grammar

      2. tagged_sequence::= "(" (tag":"|) item #((tag":"|)item) ")",
      3. tag::=symbolic_identifier,
      4. 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.
      5. 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

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

  1. some X with X---chars.

    Typographical theory

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

    }=::WIDTH.

    Filters and Decorators

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

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


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

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

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

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


        }

    4. 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.
      1. <+>::#T><#T->@#T.
      2. for b,c:#T, b<+>c = {a:#T|| b=c=a=()
      3. or 1st(a)=1st(b) and rest(a) in rest(b)<+>c
      4. or 1st(a)=1st(c) and rest(a) in rest(c)<+>b}.
      5. |-for b,c, b<+>c = c<+>b.


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


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

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

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


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

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

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

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

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

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

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


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

      24. --[Dillon et all 86]


      }=::Interleaving.


    }=::Other_operations.

    Expressions on a set of elements

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


    }=::REGULAR.

  6. For A:Alphabet, event_expressions(A)::=Event_expressions(EVENT(A)).
  7. EVENT(A)::=
    Net{
    1. SERIAL(Event_expressions, shuffle, vertical_bar),
    2. SERIAL(shuffle, sequence, "<*>"),
    3. SERIAL(sequence, vertical_bar),
    4. SERIAL(sequence, phase, ()),
    5. phase::=(hash|)( A |"(" Event_expressions ")" ).

    }=::EVENT.

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

    4. η::regular(A).

    5. constrained_prefixes::={ u:prefix(η) ||
    6. for all S:Subsets( u/&S in κ(S))
    7. },

    8. language::=constrained_prefixes /& Events.


    }=::Constrained_Expressions.

    Substitution

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

    3. substitutions::={(a|+>b)||a,b:strings}.

    4. For a:strings, (a|-.) ::=rel [x,y](x=y and not a substr x).

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

    6. Production systems- set of substitutions ...

    }=::SUBSTITUTION.

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

Alternatives

[ ALTERNATIVE_SETS_OF_STRINGS. in math_61_String_Theories ]

See Also
  • STANDARD_ASSIGNMENTS::= See http://cse.csusb.edu/dick//maths/math_11_STANDARD.html#ASSIGNMENTS.

    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

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

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

    End