Convergence of nullability in the derivative of parser combinators

δ.md

Interpreting δ as the least fixed point of the nullability equations, ascending from ⊥ = false.

Given S → ϵ ∪ S,

The zeroth iteration is ⊥:

δ⁰(S) = ⊥ = false

The first is computed:

δ¹(S)
	= δ(ϵ ∪ S)
	= δ(ϵ) or δ⁰(S)
	= true or false
	= true

It has now converged, as shown by the second:

δ²(S)
	= δ(ϵ ∪ S)
	= δ(ϵ) or δ¹(S)
	= true or true
	= true

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

---

Given S → ϵ ∘ S, and again ascending from ⊥ = false,

The zeroth iteration is ⊥:

δ⁰(S) = ⊥ = false

The first is computed:

δ¹(S)
	= δ(ϵ ∘ S)
	= δ(ϵ) and δ⁰(S)
	= true and false
	= false

It has already converged with ⊥.

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

---

Given S → ϵ ∪ S ∪ S,

The zeroth iteration is ⊥:

δ⁰(S) = ⊥ = false

The first is computed:

δ¹(S)
	= δ(ϵ ∪ S ∪ S)
	= δ(ϵ) or δ⁰(S) or δ⁰(S)
	= true or false or false
	= true

It has now converged, as shown by the second:

δ²(S)
	= δ(ϵ ∪ S ∪ S)
	= δ(ϵ) or δ¹(S) or δ¹(S)
	= true or true or true
	= true

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

---

In order for δ not to stabilize, it would have to return true when δⁿ⁻¹ = false, and false when δⁿ⁻¹ = true. But then we couldn’t apply lfp at all, since it would be flip-flopping (and therefore not monotone) and would fail to terminate.

∴ If δ is monotone, it stabilizes in one iteration.

On second thought:

1. Isn’t that descending from ⊥ = true instead of ascending from ⊥ = false?
2. I’m not sure I follow why an acyclic grammar requires multiple passes.

To the second point, I have been (mis?)understanding δⁿ(L) as computing a pass through the entire grammar; it looks like your use of it implies that it’s actually computing a pass for L alone. If so, that’d be the flaw in my reasoning right there, I think.