ch:mendler-recursion: ch:mendler-recursion

Let the result carrier be ${\mu }^{\mathsf{M}}{F}_B$ and define In the cons clause $\mathit{rec}:R\to {\mu }^{\mathsf{M}}{F}_B$ and $r:R$. Mendler beta therefore gives map-nil as the target nil and map-cons as target cons applied to $f(a)$ and the recursively mapped tail.

The attempted algebra is $$\varphi :\prod _{R:{\mathcal{U}}_i}(R\to ({\mu }^{\mathsf{M}}{F}_{\mathsf{T}}\to \mathbf{1}))\to (R\to \mathbf{1})\to ({\mu }^{\mathsf{M}}{F}_{\mathsf{T}}\to \mathbf{1})$$ with $\varphi (R,\mathit{rec},f):=f$. The extracted $f$ has domain $R$, while the expected result has domain ${\mu }^{\mathsf{M}}{F}_{\mathsf{T}}$; abstract $R$ cannot be converted to that fixed type. Replacing the clause by $\lambda x:{\mu }^{\mathsf{M}}{F}_{\mathsf{T}}.\star$ typechecks, but ignores $f$. Consequently it cannot expose the negative function needed for $\mathsf{out}(x)(x)$ and cannot recreate the self-application cycle.

Strengthen the claim to every $A$ and induct on $t:\mathsf{Term}(A)$. Variables and applications compute directly. In the lambda case the induction hypothesis at $\mathsf{Incr}(A)$ applies because $$\mathsf{lift}(\mathsf{id})(\mathsf{zeroV})=\mathsf{zeroV},\mathsf{lift}(\mathsf{id})(\mathsf{sucV}(a))=\mathsf{sucV}(a).$$ Thus $\mathsf{lift}(\mathsf{id})$ is pointwise the identity, so $$\mathsf{rename}(\mathsf{id},\mathsf{lam}(b))=\mathsf{lam}(\mathsf{rename}(\mathsf{id},b))=\mathsf{lam}(b).$$

First inspect $z:\mathsf{Incr}(A)$. At $\mathsf{zeroV}$ both $\mathsf{liftSub}({\eta }_A)(z)$ and ${\eta }_{\mathsf{Incr}(A)}(z)$ are $\mathsf{var}(\mathsf{zeroV})$. At $\mathsf{sucV}(a)$, $$\mathsf{liftSub}({\eta }_A)(\mathsf{sucV}(a))=\mathsf{rename}(\mathsf{sucV},\mathsf{var}(a))=\mathsf{var}(\mathsf{sucV}(a)).$$ Nested induction on $t$ now settles variables and applications by computation. In the lambda case use the displayed pointwise equality, the induction hypothesis at $\mathsf{Incr}(A)$, and congruence for $\mathsf{lam}$.

At arbitrary $R$, the recursive placeholder has type $\mathit{rec}:R\to \mathbb{N}$. In the nonempty layer, $f:R\to R$ and $r:R$, so $f(r):R$ and $\mathsf{suc}(\mathit{rec}(f(r))):\mathbb{N}$. An unrolled parent instead has type ${\mu }^{\mathsf{M}}{F}_{\mathsf{Foo}}$. It cannot be passed to $\mathit{rec}$ because the latter’s domain is the universally quantified $R$, not the fixed point. This is the exact abstract-domain barrier.

In ${\tau }_0=A\to {\tau }_1$ and ${\tau }_1=B\to {\tau }_0$, each traversal follows an arrow codomain, so the occurrence returning to ${\tau }_0$ is positive. The same argument starts at ${\tau }_1$; property $P$ passes. If the second constraint is changed to ${\tau }_1={\tau }_0\to B$, the traversal from ${\tau }_0$ to ${\tau }_1$ preserves polarity and the arrow domain reverses it on returning to ${\tau }_0$. Thus a type equal to ${\tau }_0$ contains a negative occurrence of ${\tau }_0$, and property $P$ fails.

For natural-number sum on lists, use result $\mathbb{N}$: $${\varphi }_{\mathrm{\Sigma }}(R,\mathit{rec},\mathsf{inl}\star )=0,{\varphi }_{\mathrm{\Sigma }}(R,\mathit{rec},\mathsf{inr}(n,r))=n+\mathit{rec}(r).$$ For append to a fixed second list $ys:{\mu }^{\mathsf{M}}{F}_A$, use that list type as the result: $${\varphi }_{ys}(R,\mathit{rec},\mathsf{inl}\star )=ys,{\varphi }_{ys}(R,\mathit{rec},\mathsf{inr}(a,r))={\mathsf{in}}_{F_A}^{\mathsf{M}}(\mathsf{inr}(a,\mathit{rec}(r))).$$ The beta rule gives the ordinary nil and cons equations. Only the first list is folded; the second is already the result value returned at nil, so no destructor for the first list is needed.

First prove, by cases on $z:\mathsf{Incr}(A)$, $$\mathsf{subst}(\mathsf{liftSub}(\tau ),\mathsf{liftSub}(\sigma )(z))=\mathsf{liftSub}(\lambda a.\mathsf{subst}(\tau ,\sigma (a)))(z).$$ The zero case is reflexivity. The successor case uses renaming–substitution fusion and $\mathsf{liftSub}(\tau )(\mathsf{sucV}(b))=\mathsf{rename}(\mathsf{sucV},\tau (b))$. Now strengthen the main claim over the variable type and induct on $t$. The variable case is the definition, and the application case uses both induction hypotheses. In the lambda case, the induction hypothesis at $\mathsf{Incr}(A)$ reduces the goal to the displayed lift equation; congruence for $\mathsf{lam}$ closes it.

For $F_{\mathsf{T}}(R)=R\to \mathbf{1}$, the attempted destructor algebra extracts $f:R\to \mathbf{1}$ where a result ${\mu }^{\mathsf{M}}{F}_{\mathsf{T}}\to \mathbf{1}$ is required; it fails because $R$ is abstract. By contrast, the nonempty $\mathsf{Foo}$ layer contains $f:R\to R$ and $r:R$, so $\mathit{rec}(f(r))$ is well typed for $\mathit{rec}:R\to \mathbb{N}$.

In the source example, put ${\mathsf{coo}}_0=\mathsf{coo}(\mathsf{id})$ and $g=\mathsf{coo}({\mathsf{coo}}_0)(\mathsf{noo})$. Then $\mathsf{foo}={\mathsf{coo}}_0(g)$. The histomorphism can unroll $g$, recover ${\mathsf{coo}}_0$, and form The catamorphism supplies only $R\to \mathbb{N}$; the histomorphism additionally supplies the unrolling observation that makes this larger self-containing argument available.