Consider the following definitions


$\overline{nil} \ \ \ \ \ \frac{l}{a \ l}$ $a \in A$

$A^* = \mu \widehat{LIST}, \ A^{\infty} = v \widehat{LIST}$


$\overline{0} \ \ \ \ \ \frac{x}{s(x)}$

$ N = \mu \widehat{NAT}, \ N^{\infty} = v \widehat{NAT}$

Given those definitions I have to define a length function over $A^{*} \leftarrow{N}$ such that $length(l)$ outputs the length of $l$.

I have tried to do this problem using structural induction on a given $l$ but I don't seem to get any relevant result.

In general, how would you approach this kind of problem?

  • 1
    $\begingroup$ The idea is that $\operatorname{length}(\mathrm{nil}) = 0$ whereas $\operatorname{length}(a\ell) = s(\operatorname{length}(\ell))$. $\endgroup$ Oct 17 '18 at 4:05

Let F denote a “shape”, as your LIST and NAT shapes for example.

Declaring $I := μF$ is tantamount to saying that $I$ is recursively defined by some $α : F(I) ≅ I$ and moreover for any $β : F(K) → K$ there is a unique $f : I → K$ that respects the “F”-structure.

Since you define $A^* = μ(LIST)$, where the “LIST” structure on a set $X$ consists of a constant $c : X$ and a function $n : A × X → X$ --- c.f., your $nil, -·-$ --- we automatically obtain an operation $A^* → ℕ$ if we can endow $ℕ$ with a “LIST” structure; namely a constant such as zero $0 : ℕ$ and an operation on ℕ such as $A \times ℕ → ℕ : (a, n) ↦ s\, n$.

So by the μ-definition of lists, since we furnished ℕ with a LIST structure, we have that there is a unique function, call it $length$, that respects the LIST structure in that it takes the shape constants-to-constants and the shape functions-to-functions: $$ \mathsf{length}(nil) \;=\; 0 $$ $$ \mathsf{length}(a \cdot l) \;=\; s(\mathsf{length}\, l) $$

Alternatively, these properties also serve to “define length by structural induction on the shape of lists”.

Hope that helps a bit :-)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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