I am trying to formulate an inductive definition of string concatenation and am having a little trouble. What I've gotten so far is something like this:
(Basis) if y = empty string, then xy = x
(Step) We know a string can be build by adding one symbol at a time to the empty string, so string concatenation can take place if y = ab where a is a string and b is a single symbol (xa)b = xy
I'm having trouble with the concept, so if anyone could help me clean this up and gain a better understanding, it would really help. Thank you.
Before you can give a recursive definition of concatenation, you need an inductive definition of strings (inductive types and recursive functions go hand-in-hand).
So,
(1) the empty string is a string;
(2) if x is a string and a is a symbol, then xa is a string;
(3) all strings are built using rules (1) and (2)
This is basically correct. Given two strings x and y, the program analyzes y. If it is the empty string, the program returns x. If y = y'b, then y' is simpler than y and so the program should already know how to compute xy'. After doing that, it adds b to xy' using rule (2) and returns the result.(Basis) if y = empty string, then xy = x
(Step) We know a string can be build by adding one symbol at a time to the empty string, so string concatenation can take place if y = ab where a is a string and b is a single symbol (xa)b = xy
Instead of (xa)b = xy in the quote above I would write xy = (xa)b because the left-hand side is what has to be computed and the right-hand side is how to compute it.
Usually strings are defined so that new symbols are added on the left.
One common notion of a string is that a string is a finite sequence (a finite sequence is a function whose domain is a natural number).
For the empty string 0, let length(0) = 0
For a non-empty string f, let length(f) = max(dom(f))+1.
Then the concatenation of two strings f and g may be defined ['u' for binary union and 'E' for the existential quantifier]:
concat(f g) = f u {<x y> | En(<n y> in g & x = n+length(f)}
That definition is not couched inductively.
Then among key theorems is that the concatenation operation is associative.
But what is
xa
?
That is, what does the notation of 'x' followed by 'a' stand for? I would think it stands for some kind of concatenation. But you were definining 'string' in order to then define 'concatenation', so there can't be an appeal to concatenation in the definition of 'string' without circularity.
The OP should clarify the context (functional programming, free groups, etc.). He repeatedly refused to do this in response to Drexel's question.That is, what does the notation of 'x' followed by 'a' stand for? I would think it stands for some kind of concatenation. But you were definining 'string' in order to then define 'concatenation', so there can't be an appeal to concatenation in the definition of 'string' without circularity.
Recursive definitions are often used in functional programming, where they go together with inductive types. When defining a new type, we introduce new functional symbols, called constructors, of given types, and say that all terms of the newly defined inductive type are built from those constructors. E.g., when defining the type of natural numbers Nat, we introduce two constructors: 0 : Nat and s : Nat -> Nat. Similarly, when we are defining the type of strings String T for some other type T, we introduce two constructors: nil : String T and cons : String T -> T -> String T. So, after the type is defined, we already have functions to build strings one symbol at a time.