Removing an explicit endmarker

An LR parser can read a fresh marker to make end-of-input observable. This file packages the language-level step which removes that implementation device: quotient by the singleton marker, then pull the result back along the injective Option.some embedding.

def endmarked {T : Type} (L : Language T) : Language (Option T)

Append a fresh none endmarker after embedding every original terminal with some.

Equations

• endmarked L = {v : List (Option T) | ∃ w ∈ L, v = List.map some w ++ [none]}

def endmarkedShape {T : Type} : Language (Option T)

The regular shape language consisting of any number of embedded terminals followed by exactly one endmarker.

Equations

• endmarkedShape = endmarked ⊤

theorem endmarkedShape_eq {T : Type} : endmarkedShape = (Language.map some) ⊤ * {[none]}

theorem endmarkedShape_isRegular {T : Type} : endmarkedShape.IsRegular

Properly endmarked words form a regular language.

theorem is_DCF_endmarked_of_marked_machine {T : Type} [Fintype T] (L : Language T) (K : Language (Option T)) (hK : is_DCF K) (hcorrect : ∀ (w : List T), List.map some w ++ [none] ∈ K ↔ w ∈ L) : is_DCF (endmarked L)

It suffices for a DPDA implementation to be correct on properly marked inputs. Intersecting its language with the regular marker-shape language removes any behavior it may have on malformed encodings.

theorem endmarked_rightQuotient_marker {T : Type} (L : Language T) : endmarked L / {[none]} = (Language.map some) L

Removing the final marker from an endmarked language leaves exactly the letterwise some image of the original language.

theorem is_DCF_of_is_DCF_endmarked {T : Type} [Fintype T] (L : Language T) (hL : is_DCF (endmarked L)) : is_DCF L

If the explicitly endmarked language is deterministic context-free, then so is the original language.