User:Gilbert189/String arithmetic

Not sure what to call this other than arithmetic, even though it's nothing like arithmetic at all. Also, I'm pretty sure somebody else has made one of these before me.

ε ∅: empty string ("")
    - smaller and earlier than any string
    ∀ a
        a < "" ∧ a << ""
        ⇔ a ≠ ε

< = >: lexicographic ordered comparison ("apple" < "bee" > "banana" = "banana" > "ban")
    - Done by comparing each element in order and then comparing the size
    a p p l e
    b e e (∵ a < b)
    b a n a n a (∵ e > a)
    b a n a n a (∵ b = b ∧ a = a ∧ n = n)
    b a n (∵ b = b ∧ a = a ∧ n = n ∧ length of "banana" > length of "ban")
    - a > b ⇔ a is later than b, a succedes b
    - a < b ⇔ a is earlier than b, a precedes b
    - a ≺ b or a ≻ b may also be used as well

<< == >>: radix ordered comparison ("apple" >> "bee" << "car" == "car")
    - Done by comparing the size and then comparing each element in order
    a p p l e
        b e e (∵ length of "apple" > length of "bee")
        c a r (∵ b < c)
        c a r (∵ length of "car" > length of "car" ∧ c = c ∧ a = a ∧ r = r)
    - a >> b ⇔ a is greater than b, a is larger than b
    - a << b ⇔ a is less than b, a is smaller than b
    - There are cases where a > b ∧ a << b
    "a" > "bb"
    "a" << "bb"

|: contains, has substring ("stuff" | "ff")
    - right side must be smaller
    ∀ a ∀ b
        a | b
        ⇔ a >> b

.: concatenation ("hello" . "world" = "helloworld")
    - associative
    ("foo" . "bar") . "baz" = "foo" . ("bar" . "baz")
           "foobar" . "baz" = "foo" . "barbaz"
                "foobarbaz" = "foobarbaz"
    - non-commutative
    "foo" . "bar" ≠ "bar" . "foo"
         "foobar" ≠ "barfoo"
    - has an identity: ""
    "what" . "" = "what"
    "" . "what" = "what"
    - gives a later result compared to the left side
    ∀ a ∀ b
        a . b > a
        ⇔ b ≠ ""
    - gives a bigger result
    ∀ a ∀ b
        a . b > a ∧ a . b > b
        ⇔ a ≠ "" ∨ b ≠ ""

%: prefix, head (%"hello" = "h")
    - gives an earlier result
    ∀ a
        %a < a
    %"hello" = "h" < "hello"
    - gives a smaller result
    ∀ a
        %a << a
    %"hello" = "h" << "hello"
    - %"" is undefined (it's as bad as dividing by 0)

~: anti-prefix, tail (~"hello" = "ello")
    - gives a smaller result
    ∀ a
        %a << a
    ~"hello" = "ello" << "hello"
    - usually doesn't give an earlier result
    ~"hello" = "ello" < "hello"
    ~"president" = "resident" > "president"
    - ~"" is undefined (ditto)

!: reversal (!"hello" = "olleh")
    - if a string is earlier than the reversed string, the string is weakly ascending
    "hello" < !"hello" = "olleh"
    - if a string is later than the reversed string, the string is weakly descending
    "goodbye" > !"goodbye" = "eybdoog"
    - if a string equals the reversed string, the string is a palindrome
    "racecar" = !"racecar" = "racecar"
    - combining ! with % and ~ gives postfix (tip) and anti-postfix (body)
    %!"hello" = "o"
    ~!"hello" = "lleh"

-: elision ("hello" - "ll" = "heo")
    - gives a smaller result compared to the left side
    ∀ a
        a - b << a
    - elides the last match
    "banana" - "an" = "bana"
    - non-commutative
    "banana" - "na" ≠ "na" - "banana"
             "bana" ≠ "banana"
    - non-associative
    "abacaba" - ("ba" - "ac") ≠ ("abacaba" - "ba") - "ac"
             "abacaba" - "ba" ≠ "abaca" - "ac"
                      "abaca" ≠ "aba"
    - has an identity: "" (right side only)
    "hello" - "" = "hello"

--: global elision ("hello" -- "l" = "heo")
    - gives a smaller result compared to the left side
    ∀ a
        a -- b << a
    - ÷ may also be used to differentiate it with -
    "hello" ÷ "l = "heo"
    - non-commutative
    "banana" - "na" ≠ "na" - "banana"
             "bana" ≠ "banana"
    - non-associative
    "abacaba" -- ("ba" -- "ac") ≠ ("abacaba" -- "ba") -- "ac"
              "abacaba" -- "ba" ≠ "aca" -- "ac"
                          "aca" ≠ "a"
    - has an identity: "" (right side only)
    "hello" -- "" = "hello"

{ ... }: replacement ("pollo" {"ll"} "y" = "poyo")
    - usually gives a larger result compared to the left side
    ∀ a ∀ b ∀ c
        a {b} c > a
        ⇔ a | b ∧ c > b
    "card" {"d"} "t" = "cart" > "card"
    - only replaces the first match
    "banana" {"an"} "o" = "banoa"
    - if available, +a may be used as well
    "pollo" +"ll" "y" = "poyo"
    - non-commutative
    "hello" {"ll"} "y" ≠ "y" {"ll"} "hello"
                "heyo" ≠ "y"
    - {""} matches the last character boundary (functionally the same as .)
    "hello" {""} "world" = "helloworld"
    (implies that {a} is associative for some string a)
    - (needs proof) Is there another operator {a} other than {""} that is associative?

-{ ... }-: global replacement ("pollo" -{"l"}- "y" = "poyyo")
    - written as braces with a long stem (could be approximated like -{ this }- in text)
    - usually gives a larger result compared to the left side
    ∀ a ∀ b ∀ c
        a -{b}- c > a
        ⇔ a | b ∧ c > b
    "baba" -{"a"}- "o" = "bobo" > "baba"
    - if available, /a may be used as well
    "pollo" /"ll" "y" = "poyo"
    - non-commutative
    "hello" -{"l"}- "y" ≠ "y" -{"l"}- "hello"
                "heyyo" ≠ "y"
    - {""} matches all character boundaries
    "hello" -{""}- "!" = "h!e!l!l!o!w!o!r!l!d"
        - (superscript) < or > means "also check this character boundary"
        "hello" -{""}-< "!" = "!h!e!l!l!o!w!o!r!l!d"
        "hello" -{""}-> "!" = "h!e!l!l!o!w!o!r!l!d!"
        "hello" -{""}-<> "!" = "!h!e!l!l!o!w!o!r!l!d!"
        "hello" <-{""}-> "!" = "!h!e!l!l!o!w!o!r!l!d!"