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.
A -> B u B
B -> C u C
C -> x
Initially:
A is nullable
B is nullable
C is nullable
After first pass:
A is nullable
B is nullable
C is not nullable
After second pass:
A is nullable
B is not nullable
C is not nullable
After third pass:
A is not nullable
B is not nullable
C is not nullable