For any string $𝑤$, we can define a representable grammar $\lceil 𝑤\rceil$ which matches exactly the string $𝑤$ and nothing else. The parse trees for a representable grammar are proofs that the string is exactly equal to $𝑤$:

Define a grammar for each finite cardinal $𝑛:\mathbb{N}$.

Then define the grammar of all finite cardinals as

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

There is likely a better name for this.

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

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

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

Finite unambiguity does not serve as an adequate definition of unambiguity that is equivalent to unambiguity as subterminality and unambiguity as a unique map. However, the definition attempted via finite unambiguity can be refined to something that is equivalent to these.

A grammar $𝐴$ is unambiguous if $\mathrm{\Delta }:𝐴⊢𝐴\&𝐴$ is an isomorphism. Equivalently, $𝐴$ is unambiguous if ${𝜋}_1:𝐴\&𝐴⊢𝐴$ and ${𝜋}_2:𝐴\&𝐴⊢𝐴$ are equal.

For a grammar $𝐴$, the Kleene star ${𝐴}^{\ast }$ is defined as a least-fixed point,

For a grammar $𝐴$, the Kleene star ${𝐴}^{\ast }$ is isomorphic to an indexed coproduct.

That is, we may view the parses of ${𝐴}^{\ast }$ like a linear list comprising parses of $𝐴$ concatenated together. Further, for each of these lists we may know the precise length.

When viewing Dependent Lambek Calculus as a model of Kleene algebra, this is precisely the statement that star continuity holds.

The first set of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with ones of the grammars

The followlast set of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with ones of the grammars

The nullability ($\text{𝖭𝗎𝗅𝗅}(\cdot )$) of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with one of the grammars

The tensor of grammars,

is simply typed, so $𝐵$ cannot see what $𝐴$ matched.

Just as we have the generalization from the pair type $𝐴\times 𝐵$ to the dependent pair ${\mathrm{\Sigma }}_{𝑎:𝐴}𝐵𝑎$, we can define a dependent tensor operation. It is a $\mathrm{\Sigma }$-like generalization over the ordinary tensor, in which the second grammar depends on a parse tree of the first.

Write $\text{𝖳𝗋𝖾𝖾}(𝐴)={\sum }_{𝑤}𝐴(𝑤)$ for the type of parse trees of $𝐴$, each paired with the string it parses.

For a grammar $𝐴$ and a family of grammars $𝐵:\text{𝖳𝗋𝖾𝖾}(𝐴)\to \text{𝐆𝐫}$, the dependent tensor is:

We may also write it as $(𝑎\in 𝐴)\otimes 𝐵(𝑎)$.

When $𝐵$ is a constant family, the dependent tensor reduces to the ordinary tensor $𝐴\otimes 𝐵$.

Dependence runs left to right here, which fits left-to-right parsing. The other handedness, in which the first grammar depends on a parse of the second, is also definable.

Write $𝑢⊏𝑣$ when $𝑢$ is a proper suffix of $𝑣$, that is, $𝑣=𝑥\text{++}𝑢$ with $𝑥\ne 𝜀$. The later of a grammar $𝐴$ is

A parse of $▷𝐴$ over $𝑣$ is a parse of $𝐴$ over every proper suffix of $𝑣$. In particular $(▷𝐴)𝜀$ is a singleton.

This is later on families for strings under the proper-suffix order. That order is well-founded because it strictly decreases length, so it is a thin direct category. There is at most one map $𝑢\to 𝑣$, so the product over maps from the strict past has one factor per proper suffix. Guarded recursion is modelled by presheaves on $𝜔$, the topos of trees, and more generally by sheaves over a well-founded base [1]. Here the later acts on families, which is what grammars are, and there is no clock.

Later is the right adjoint of the proper-suffix derivative. Let $\text{𝖭𝖤𝖲}={⨁}_{𝑥\ne 𝜀}\lceil 𝑥\rceil$ be the grammar of non-empty strings. Then the derivative $({𝜕}_{\text{𝖭𝖤𝖲}}𝐵)𝑢\cong {\sum }_{𝑥\ne 𝜀}𝐵(𝑥\text{++}𝑢)$ has the right adjoint

so ${𝜕}_{\text{𝖭𝖤𝖲}}-⊣▷$. Splitting $\text{𝖭𝖤𝖲}$ into its summands gives the form of $▷$ that the calculus can define:

The component at $𝑤$ says: if the string begins with $𝑤$, then the rest parses as $𝐴$.

The restriction to non-empty $𝑤$ is what makes this a later. At $𝑤=𝜀$ the component is $\sqrt[\lceil 𝜀\rceil ]{𝐴}\cong 𝐴$. Including it would give a projection $▷𝐴⊢𝐴$, and Löb would then prove every grammar. For the same reason the later is a product over suffixes. A sum such as ${⨁}_{𝑐}\lceil 𝑐\rceil ⊸𝐴$ is empty at $𝜀$, and at $𝐴=\perp$ it is $\perp$. The identity step $\perp ⊢\perp$ would then give Löb a proof of $\top ⊢\perp$.

In the Agda this is ▷ in Grammar/Later/Base.agda, which is defined as the indexed conjunction of √l-string. The mirror image ▷r, over proper prefixes, is defined in the same way. See also the bilateral later and the later along an arbitrary well-founded order.

For every grammar $𝐴$ and every term $𝜑:▷𝐴⊢𝐴$, where $▷$ is the later on grammars, there is a unique global parse $\text{𝗅ö𝖻}𝜑:\top ⊢𝐴$ with

Here $\text{𝗇𝖾𝗑𝗍}𝑡:\top ⊢▷𝐴$ restricts a global parse $𝑡$ to every proper suffix.

The proof is recursion on the length of the string. At $𝑣$, the parses already built at the proper suffixes of $𝑣$ form an element of $(▷𝐴)𝑣$, and $𝜑$ turns it into a parse at $𝑣$. Uniqueness is Löb for families over the proper-suffix order. In the Agda, lob in Grammar/Later/Base.agda is this recursion, done by well-founded induction on length.

To prove an entailment $𝐵⊢𝐶$ this way, apply Löb to $𝐴=𝐵\Rightarrow 𝐶$. The hypothesis $▷(𝐵\Rightarrow 𝐶)$ is the induction hypothesis at every proper suffix. It becomes usable once a non-nullable grammar has been consumed. If $𝜀\&𝐵⊢\perp$, then

because a parse of $𝐵\otimes \top$ over $𝑣$ splits $𝑣=𝑥\text{++}𝑢$ with $𝑥$ non-empty, so $𝑢⊏𝑣$. This is ▷-app-NE in Grammar/Later/Properties.agda. Induction on a Kleene star is the standard use.

For presheaves, $\text{𝗇𝖾𝗑𝗍}:𝑃\to ▷𝑃$ restricts along the strict past, as in later on presheaves. A grammar is only a family over strings, so a map $\text{𝗇𝖾𝗑𝗍}:𝐴⊢▷𝐴$ into the later on grammars is extra data. It sends a parse over $𝑣$ to parses over every proper suffix of $𝑣$.

Let $\square 𝐴=𝐴\&▷𝐴$, so that $(\square 𝐴)𝑣\cong {\prod }_{𝑢⊑𝑣}𝐴𝑢$. This is the comonad $𝑈\circ \text{Cofree}$ for the suffix order, and presheaves are comonadic over families. The counit law forces the first component of a coalgebra $𝐴⊢\square 𝐴$ to be the identity. Hence:

• a presheaf on strings under the suffix order is the same as a grammar $𝐴$ with a map $\text{𝗇𝖾𝗑𝗍}:𝐴⊢▷𝐴$ that satisfies coassociativity. Restricting to $𝑢\prime$ and then to $𝑢⊏𝑢\prime$ must agree with restricting to $𝑢$ directly;
• for a proposition-valued grammar (a language), coassociativity is automatic, and $\text{𝗇𝖾𝗑𝗍}$ exists exactly when the language is closed under suffixes. For example, $\top$ has one, but $\lceil 𝑎\rceil$ does not, since $(▷\lceil 𝑎\rceil )𝑎\cong \lceil 𝑎\rceil 𝜀$ is empty.

Löb does not need $\text{𝗇𝖾𝗑𝗍}$ on $𝐴$. The fixed-point equation only restricts a global parse $\top ⊢𝐴$, and a global parse can always be restricted. In the Agda, the grammar-level IsCoalgebra record, with only the field next, is in Grammar/Later/Coalgebra.agda on the guarded branch.

On presheaves the strict downset of $𝑐\text{++}𝑡$ is represented by $𝑡$, because every proper suffix of $𝑐\text{++}𝑡$ is a suffix of $𝑡$. So predecessors simplify later to $(▷𝑃)(𝑐\text{++}𝑡)\cong 𝑃𝑡$. On grammars there is no such simplification, since the factors at different suffixes are unrelated.

For formal grammars $𝐴$ and $𝐵$, their tensor $𝐴\otimes 𝐵$ represents the concatenation of the languages they describe. A parse for $𝐴\otimes 𝐵$ at a string $𝑤$ consists of a splitting of $𝑤$ into a prefix $𝑢$ and suffix $𝑣$, along with a parse of $𝑢$ in $𝐴$ and a parse of $𝑣$ in $𝐵$.

Formally, it is defined as:

This operation is exactly the Day convolution of $𝐴$ and $𝐵$, where we view formal grammars as presheaves over the monoid of strings.

Fix a finitary algebraic theory $\mathrm{𝒯︀}$: sorts $𝑆$, a signature $𝜎$, equations, and a set $𝑉$ of generators. Write $𝑴$ for the free $\mathrm{𝒯︀}$-model on $𝑉$ and $|𝑴{|}_{𝑠}$ for its carrier at sort $𝑠$.

A $\mathrm{𝒯︀}$-type of sort $𝑠$ is a family $𝐴:|𝑴{|}_{𝑠}\to \text{𝖳𝗒𝗉𝖾}$.

For $\mathrm{𝒯︀}$-types $𝐴$ and $𝐵$ of sort $𝑠$ we have the additives, defined pointwise,

along with $\top$, $\perp$, and their indexed versions.

Each operation $𝑜:{𝑠}_0,\dots ,{𝑠}_{𝑛-1}\to 𝑠$ of $\mathrm{𝒯︀}$ gives a multiplicative, defined by Day convolution,

Each lifted operation also has closed structure: a residual in each of its arguments. Day algebras [1] give a more general convolutional definition.

When $\mathrm{𝒯︀}$ is the theory of monoids and $𝑉$ is an alphabet, $\mathrm{𝒯︀}$-types are formal grammars. Multiplication gives $\otimes$, the unit gives $𝜀$, and we recover Lambek${\begin{array}{}\end{array}}^{𝙳}$.