Pop At Index Zero Property

remaining elements after [ x, xs ] is popped at index 0 and visited stack is ys = reverse of (result of dumping xs to ys)

When the index is 0, we can pop the first element in the list. At this point, the list may have more elements remaining. Also, there is the "visited" list which contains the elements visited so far, in reverse. So the question is, we do with the remaining elements and the "visited" list?

The right side of the equality looks complicated, so let's break it down. As in math, the innermost operation is performed first, which is the "reverse and insert" operation. So we reverse the remaining list "xs" and insert it to the beginning of the "visited" list "ys." Then, the outer operation says we reverse the whole thing.

This makes more sense with some examples.

Examples

remaining elements after [ 5, [ ] ] is popped at index 0 and visited stack is [ 10, [ 15, [ ] ] ] = reverse of (result of dumping [ ] to [ 10, [ 15, [ ] ] ])

remaining elements after [ "Cherry", [ "Durian", [ "Eggplant", [ ] ] ] ] is popped at index 0 and visited stack is [ "Banana", [ "Apple", [ ] ] ] = reverse of (result of dumping [ "Durian", [ "Eggplant", [ ] ] ] to [ "Banana", [ "Apple", [ ] ] ])

Details

It helps to start with the original list. It's a bit tricky to visualize, but the original list for the first example is

[15, [10, [5, []]]]

And the index that we want to pop is 2.

Then, after 2 induction steps, 15 and 10 are removed from the list and added to the "visited" list in reverse. And index 2 is changed to 1 then 0. Now, we reached 5, which is the element we want to pop. So at this point, the element list is empty, so there is nothing to "reverse and insert." Then we are left with

[10,[15, []]]

And when we reverse this, the result is

[15, [10, []]]

We had to reverse the "visited" list because elements were inserted in reverse during the inductive step, and we need to undo the reverse insertions.

Now let's look at the second example. The original list is

["Apple", ["Banana", ["Cherry", ["Durian", ["Eggplant", []]]]]]

And we want to pop at index 2, which is "Cherry"

Then, after 2 induction steps, the elements list becomes

["Cherry", ["Durian", ["Eggplant", []]]]

and the "visited" list is

["Banana", ["Apple", []]]

Then, we remove "Cherry" and reverse the rest of the list. The result is:

["Eggplant", ["Durian", []]]

We then insert this to the beginning of the "visited" list. The result is:

["Eggplant", ["Durian", ["Banana", ["Apple", []]]]]

Notice that this list is the reverse of what we want. This happened because the induction step adds elements to the "visited" list in reverse, and we also reversed the remaining elements before inserting them to the beginning of the "visited" list. Thus, the only remaining step is to reverse the entire list.

Comments

Please log in to add comments