Convergence of parseNull in the derivative of parser combinators

parseNull.md

Interpreting parseNull as the least fixed point of the parse null equations, ascending from ⊥ = {}

Given S → ϵ↓{x} ∪ S,

The zeroth iteration is ⊥:

parseNull⁰(S) = ⊥ = {}

The first is computed:

parseNull¹(S)
	= parseNull(ϵ↓{x} ∪ S)
	= parseNull(ϵ↓{x}) ∪ parseNull⁰(S)
	= {x} ∪ {}
	= {x}

It has now converged, as shown by the second:

parseNull²(S)
	= parseNull(ϵ↓{x} ∪ S)
	= parseNull(ϵ↓{x}) ∪ parseNull¹(S)
	= {x} ∪ {x}
	= {x}

∴ It seems like parseNull over a single alternation will always stabilize within a single iteration.

---

Given S → ϵ↓{x} ∘ S, and again ascending from ⊥ = false,

The zeroth iteration is ⊥:

parseNull⁰(S) = ⊥ = {}

The first is computed:

parseNull¹(S)
	= parseNull(ϵ↓{x} ∘ S)
	= parseNull(ϵ↓{x}) and parseNull⁰(S)
	= {x} ✕ {}
	= {}

It has already converged with ⊥.

∴ It seems like parseNull over a single concatenation will always stabilize within a single iteration.

---

Given S → ϵ↓{x} ∪ S ∪ S,

The zeroth iteration is ⊥:

parseNull⁰(S) = ⊥ = {}

The first is computed:

parseNull¹(S)
	= parseNull(ϵ↓{x} ∪ S ∪ S)
	= parseNull(ϵ↓{x}) ∪ parseNull⁰(S) ∪ parseNull⁰(S)
	= {x} ∪ {} ∪ {}
	= {x} ∪ {} ∪ {}
	= {x}

It has now converged, as shown by the second:

parseNull²(S)
	= parseNull(ϵ↓{x} ∪ S ∪ S)
	= parseNull(ϵ↓{x}) ∪ parseNull¹(S) ∪ parseNull¹(S)
	= {x} ∪ {x} ∪ {x}
	= {x}

∴ It seems like parseNull over two alternations will always stabilize within a single iteration.

---

In order for parseNull not to stabilize, it would have to return {x} when parseNullⁿ⁻¹ = {}, and {} when parseNullⁿ⁻¹ = {x}. But then we couldn’t apply lfp at all, since it would be flip-flopping and would fail to terminate.

This one I’m less sure of because it’s not just {x} vs. {}—there could be intermediate values.