# Define a length function over $A^{*} \leftarrow{N}$ such that $length(l)$ outputs the length of $l$

Consider the following definitions

LIST:

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

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

NAT:

$$\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?

• The idea is that $\operatorname{length}(\mathrm{nil}) = 0$ whereas $\operatorname{length}(a\ell) = s(\operatorname{length}(\ell))$. – Yuval Filmus 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)$$