finite

Tag. finite

finite

Notes (5)

Definition. A Grammar of Finite Cardinals finite-cardinal-grammar

Define a grammar for each finite cardinal $𝑛 : ℕ$ .

[0] ≔ ⊥

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

Then define the grammar of all finite cardinals as

𝖥𝗂𝗇 ≔ ⨁_{𝑛 : ℕ} [𝑛]

Definition. Finite Unambiguity finite-unambiguity

Define a grammar $𝐴$ to be finitely unambiguous if $𝐴 & 𝐴 ≅ 𝐴$ .

There is likely a better name for this.

Finite Unambiguity is Not Equivalent to Unambiguity finite-unambiguity-not-unambiguity

For a while I believed finite unambiguity to be equivalent to the other definitions of unambiguity.

Definition 0.1. Finite Unambiguity finite-unambiguity

Define a grammar $𝐴$ to be finitely unambiguous if $𝐴 & 𝐴 ≅ 𝐴$ .

There is likely a better name for this.

Definition 0.2. Unambiguity as Subterminality unambiguity-as-subterminality

A grammar $𝐴$ is unambiguous if the unique map into the terminal object is a monomorphism. That is, $𝐴$ is a subobject of $⊤$ .

Definition 0.3. Unambiguity as Unique Map into Codomain unambiguity-as-unique-map

A grammar $𝐴$ is unambiguous if for all grammars $𝐵$ and maps $𝑒, 𝑒' : 𝐴 ⊢ 𝐵$ we have $𝑒 = 𝑒'$ .

In a category with terminal objects, this is equivalent to unambiguity defined via subterminality.

Definition 0.3.1. Unambiguity as Subterminality unambiguity-as-subterminality

A grammar $𝐴$ is unambiguous if the unique map into the terminal object is a monomorphism. That is, $𝐴$ is a subobject of $⊤$ .

We may use an analogy from the category of sets, however I had missed the infinite case when translating this idea to grammars.

It is true that if a grammar is unambiguous, then it is finitely unambiguous. However, the converse does not hold unless the grammar has finitely many parse trees for each string. This finiteness condition is a semantic one. If this proof of unambiguity were to be internalized, then it could maybe be captured through the lens of some grammar of finite cardinals.

Let $𝐴 ≔ ⨁_{𝑛 : ℕ} ⊤$ . $𝐴$ is finitely unambiguous but not unambiguous. The isomorphism between $𝐴$ and $𝐴 & 𝐴$ amounts to building a bijection between $ℕ$ and $ℕ \times ℕ$ , which is straightforward.

What Connectives Preserve Finiteness? finiteness-preserving-connectives

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].

0.4 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 0.4.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.

Internal Finiteness internally-finite-grammar

Define a grammar $𝐴$ to be finite (or perhaps subfinite) if it is a subobject of grammar of finite cardinals.

𝐴 ↪ 𝖥𝗂𝗇

Where $𝖥𝗂𝗇$ is defined as follows.

Definition 0.5. A Grammar of Finite Cardinals finite-cardinal-grammar

Define a grammar for each finite cardinal $𝑛 : ℕ$ .

[0] ≔ ⊥

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

Then define the grammar of all finite cardinals as

𝖥𝗂𝗇 ≔ ⨁_{𝑛 : ℕ} [𝑛]