. Strings and n-tpls
There are several models of strings.
Suppose we have a set of symbols(T say) then the strings are
generated by starting with an empty string ("") and a putting symbols
(in T) onto it using a concatenation operation (!).
concatenation::function=`combines to strings into one by juxtaposing them".
! ::infix= concatenation.
Example:
(def)|- "abc" ! "xyz" = "abcxyz",
Some axioms:
|- (empty): for x:strings, "" ! x = x ! "" =x.
|- (associativity): For x,y,z:strings, x !(y!z)=(x!y)!z.
And so on...
.See http://www/dick/maths/math_62_Strings.html
.See http://www/dick/maths/math_61_String_Theories.html
.See http://www/dick/maths/logic_6_Numbers..Strings.html
We can also, if we want, treat a strings as $n_tples of
characters and define concatenation in terms of this model.
We define operations of union(|), intersection (&), complementation
(~), concatenation(), and iteration (#) on sets of strings:
For A,B: sets of strings,
A B ::={c || c=a!b and a in A and b in B},
#A ::=least{ X || X=({""} | A X) }.
For string s, s::={s} (in context demanding a set of strings, only)
Given a string s with n symbols in it then
|- |s|=n,
|- head(s)=s(1)=`the first symbol in s`,
|- tail(s)=`all sybols except the first in s`,
|- if|s|>=1 then s=head(s)!tail(s) ,
|- last(s)=s(|s|).
. Functions mapping strings into strings
These are neatly defined in terms of the set of functions
{ (head), (tail), (!), (last), ...}
using XBNF. For example
reverse("") ::="",
reverse::string~"" -> string=reverse(tail) ! (head).
. n_tples
Given a set of objects S then %S is the set of functions
1..n->S for some n:0,1,2,3,...
The concatentaion operation is defined on them.
|- %(%S)=`two dimensional arrays of S's`
|- #(%S)=%(S).
|- %(%S)<>%(S).
. LISTS
|- lists(S)=S| %S | %%S | %%%S | ....
In other words the set of objects defined as containing S and
all n-tuples of objects in S or lists(S).
. LISP
In LISP every thing is defined in terms of
|- PAIR::=Net{ car,cdr:List }
where
|- List::= Atom | NIL | $ $PAIR.