What Connectives Preserve Finiteness?

In order to bridge the gap between finite unambiguity and unambiguity, we can try to restrict to grammars that have finitely many parse trees. We’d expect this to address the concern semantically, as that fixes the problem when the parses are interpreted in $𝐒𝐞𝐭$ .

We can define when a grammar is finite, and then try to prove that finiteness is preserved on some sane operations on grammars. For instance, $&$ , $\oplus$ , and $\to$ each preserve finiteness. I haven’t proven this myself (which would be a useful exercise), but the following is substantiated in any topos with a natural numbers object [johnstone-2002].

1 Finite Cardinal Arithmetic in a Topos finite-cardinal-arithmetic-topos

In a topos with a natural numbers object $(𝑁, 𝑧, 𝑠)$ , you can define finite cardinals as objects that arise as the pullback along a morphism $𝑝 : ⊤ \to 𝑁$ of the generic finite cardinal. Write $[𝑝]$ for the cardinal corresponding to $𝑝$ .

The above characterization is a little obtuse and does warrant some more explanation. One way to make it more concrete is that $[𝑧] = ⊥$ and $[𝑠 \circ 𝑛] = ⊤ \oplus [𝑛]$ , and that finite cardinals warrant a nice induction principle. If $𝑃$ is a property expressible in the internal language such that $⊥$ satisfies $𝑃$ , and that whenever $𝐴$ satisfies $𝑃$ then $⊤ \oplus 𝐴$ satisfies $𝑃$ ; then every finite cardinal satisfies $𝑃$ . That is, $𝑃$ forms a $(𝑧, 𝑠)$ -closed subobject of $𝑁$ and thus $𝑃$ is all of $𝑁$ .

My working mental model is in a presheaf topos, where the natural numbers object can be defined explicitly as $Δ (ℕ)$ .

Definition 1.1. Constant Presheaf constant-presheaf

The constant presheaf of a set $𝑋$ on a category $𝐶$ is a functor $Δ (𝑋) : 𝐶^{𝑜 𝑝} \to 𝐒𝐞𝐭$ such that

Δ (𝑋) 𝑐 ≔ 𝑋

I often call this the discrete presheaf for $𝑋$ , but I don’t know if that’s standard.

The finite cardinals with respect to $Δ (ℕ)$ can be characterized then as,

[0] ≔ ⊥

[𝗌𝗎𝖼 (𝑛)] ≔ ⊤ \oplus [𝑛]

These obey nice algebraic properties.

[𝑛 𝑚] ≅ [𝑛] \times [𝑚]

[𝑛 + 𝑚] ≅ [𝑛] \oplus [𝑚]

[𝑛^{𝑚}] ≅ [𝑚] \to [𝑛]

The case of $\otimes$ is more problematic. Semantically, for all $𝑤 : String$ we may bound the size of the set of parse trees

| (𝐴 \otimes 𝐵) 𝑤 | \leq Σ_{𝑤_{1} ++ 𝑤_{2} = 𝑤} | 𝐴 𝑤_{1} | | 𝐵 𝑤_{2} |

Precisely knowing this bound isn’t too important, but certainly it exists. We could capture this behavior by just adding an axiom that if $𝐴$ and $𝐵$ are each finite, then $𝐴 \otimes 𝐵$ is finite. Although, I’d rather not add an axiom.

We could directly try to prove that $\otimes$ preserves finiteness. The statement would follow from showing that $\otimes$ preserves monomorphisms. That is, if $𝑓 : 𝐴 ↪ 𝐶$ and $𝑔 : 𝐵 ↪ 𝐷$ , it suffices to show that $𝑓 \otimes 𝑔 : 𝐴 \otimes 𝐵 \to 𝐶 \otimes 𝐷$ is a monomorphism. This would imply finiteness, because you may then apply this for $𝐶$ and $𝐷$ as $𝖥𝗂𝗇$ . However, you would also need to show that $𝖥𝗂𝗇 \otimes 𝖥𝗂𝗇$ is finite, which isn’t immediately clear.