0
$\begingroup$

Let $\Sigma$ denote an alphabet and $[ \Sigma ]$ set of lists.

I've encountered the following function:

$f([])=[]$ (empty list)

$f([x])=[x]$, for $x \in \Sigma$

$f(x:L)=f(L)$, for $x \in \Sigma$ and $L \in [ \Sigma ]$

The function is supposed to return a tail for nonempty list. That is:

$f([x_1,x_2,...,x_n])=[x_n]$

How would you understand the ":" operator in the definition?

Inductive proof should be possible for showing that such a "tail function" is indeed working.

$\endgroup$
1
  • 1
    $\begingroup$ Also posted at mathoverflow and math within a few hours. Please do not post the same question on multiple sites. Each community should have an honest shot at answering without wasting anybody's time. If you don't get a satisfying answer after a week or so, you may flag to request migration. $\endgroup$
    – John L.
    Apr 23, 2022 at 21:59

1 Answer 1

2
$\begingroup$

I think it's a template match, meaning if you have some list $L = [x_1, x_2, \dots, x_n]$, then $L = x:L'$ where $L' = [x_2, x_3, \dots, x_n]$.

So you can imagine what that definition is saying is that $f(x:L)$ is equivalent to operating on the rest of the list, i.e. $L$ in this case, hence $f(L)$.

Induction follows pretty easily because once you've shown for a list of length $n$, to show $n+1$, you just use the function definition, which peels off the first element, and you immediately have a list of $n$, which is true by the inductive hypothesis.

Note that there are also notations such as

  • $L:y$ : $y$ is the last element
  • $x:L:y$ : $x$ is the head, $y$ is the tail
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.