Set theory(computing) Help with Question

[london-G]

Hello,

There is a question which I don't really quite understand. Can someone explain the answer to me?

I get the first part: the declaration of the "function" however the rest of it I am quite confused. Variables do not need to be declared for this type of exercise.

Insert a sequence at a given location in another sequence.
For example, if the sequence <z,x,z> were to be inserted at location 2 of the sequence <x,y,z>,
the result would be the sequence <x,z,x,z,y,z>.
(Note that this operation is defined only for locations that are within the sequence, in above
example, locations 1, 2 and 3).

The answer is given below.

insert: seq X → NAT → seq X ⇸ seq   X       
n   <    #t  ⇒   
(i  <    n   ⇒   (insert s   n   t)  i   =   t   i   ∧   
n   ≤   i   <    n   ⇒   (insert s   n   t)  i   =   s(i –   n   +   1)  ∧   
i   ≥   n   +   #s  ⇒   (insert s   n   t)  i   =   t(i -   #s))    

[Hiroshe]

First off, this has nothing to do with set theory, or set's for that matter. A set contains one of each element, and order is not relavent. (Ie, the set of real numbers, or the set of dvd's you own).

Second off, I have no idea what's going on with that solution. It looks like a mix of several different systems.

[london-G]

Hiroshe, if you can't help then I guess there is no point in answering the question.

You can see that the symbols used above are actually part of set theory. Such as cardinality, relation, function...

Not trying to be rude here but what is the intent of you answer?

[Hiroshe]

Sure, your definatly using symbols from set theory. However, it doesn't seem that this problem concerns set theory. Primaraly because this problem seems to be revolved around ordered lists.

The solution you provided is written in a strange way to me. To me, it looks like an unusual mixture. Do you know what the system is called? If I know what it's written in, assisting with a solution would be much easier.

[TrustyTony]

Looks little like prolog, I see that first is out of bounds base case, others area the recursion cases.

Here is discussion how in Prolog you would define inserting, maybe it gives you some help. You would only need to check that length of beginning part is asked number, and start insert there. Basically length of X must be the given n for the base case and would need to add one more parameter for that (three parameters + result, arity raises to 4)

[rubberman]

Honestly, I have to agree with Hiroshe. If the result of the insert operation of z,x,z into the second position of x,y,z is to result in a set, then the results should be x,z,y - anything else is a list, not a set. Sets do NOT have duplicates.

[TrustyTony]

I think OP does not mean data but the rules as set. Data type is likely to be actually tuple or list like you said.

[Hiroshe]

Yup. OP is posting in computer science, and asking about sets. This really shouldn't have much to do with programming (other then applications, and reading syntax). So, I'm more concerned with the mathematical meaning of what he means, like tony said.

Just for fun (of learning for the readers, to help to understand what is going on here and to illistrate my opinion), let's define mathematics, sets, and where what the OP is asking seems to be located.

First, we need to define logic. Let's define it with some consistent and uncomplete system. Say, lambda-calculus or First-order logic. We pick some syntax, but note that semantics have not yet been assigned.

We can of course define some kind of deduction system, like say the Hilbert System, as long as it doesnt mess with the consistency of our system.

This is where prolog works (though, prolog defines numbers) I beleive.

Now, we our "matter" so to speak. That is sets. This is where sementics start to play a role. Sets make up everything else we do in mathematics and computer science. For example, sets are a generalization of ordered lists. They are also a generalization of numbers, algebra, arithmatic, etc... We can do this by defining an empty set, and then defining the operations on a set. We can think of sets as an unordered list of unique elements for convenience.

(ie, lets define the syntax/semantics "0" to be the empty set. Define the syntax/semantics "1" to be the set containing an empty set. etc.. Then we define addition with y-combinator if were using lambda-calculus, etc... and now we have defined natural numbers! Cool, eh?)

This is where mathematics branches off into thousands of feilds, and where we add applicatable semantics and convienient syntax.

What the OP posted seems to be using a mixture of ordered lists, algebra, set theory and first order logic (note that every branch of mathematics uses set theory and logic). But the semantics of the problem seem to indicate that it is really concerning ordered lists of numbers, so it has less to do with set theory itself. This is just an educated guess though, because the syntax of the answer seems strange - it looks like an inconsistent mix of algebra, FOL, lisp and prolog. It's likely that I just have never came across said syntax before.