Library nullable

Load grammar.

Computing Nullable

The goal in this file is to define a function that computes the Nullable predicate.

Require Import List.
Require Import Arith.

Inductive definition of nullable symbols

The first step is to show that Nullable can be characterized inductively as follows.

Inductive Nullable_sym (g:grammar) : sym -> Prop :=
  | Nullable_In : forall nt exp, In (nt ,exp ) g ->
      (forall x, In x exp -> Nullable_sym g x ) ->
      Nullable_sym g (NT nt).

Theorem Nullable_sym_spec : forall g s, Nullable_sym g s <-> Nullable g (s ::nil).
Proof.
Admitted.

Computation step

We first define a function nullable_step that takes a set of non-terminals assumed to be nullable, and attempts to enrich it with new symbols based on the productions of the grammar.

Require Import MSets.
Module NatSet := MSetList.Make(Nat).

NatSet allows to work on sets of natural numbers (represented as strictly increasing lists). Coq's standard equality eq won't hold between sets containing the same elements but built in different ways. Set equality is available as NatSet.equal, but you should be able to complete this file without using it.

Now define all_NT_In_dec e l which determines if all items in e are non-terminals that belong to l.

Lemma all_NT_In_dec : forall (e :list sym ) (l:NatSet.t),
  { forall x , In x e -> exists y , x = NT y /\ NatSet.In y l } +
  { ~ forall x, In x e -> exists y, x = NT y /\ NatSet.In y l }.
Proof.
Admitted.

Fixpoint nullable_step (g :grammar) (s :NatSet.t ) : NatSet.t :=
  match g with
  | nil => s
  | (n,e)::g =>
      if all_NT_In_dec e s then NatSet.add n (nullable_step g s) else nullable_step g s
  end.

You will need to prove (at least) the correctness and completeness of nullable_step. Formulating these two lemmas requires some care; the most immediate formulation won't allow a direct proof by induction.

Iterated computation

Iterate nullable_step some number of times, starting with NatSet.empty. A possible bonus: improve the function to stop when a fixed point is reached.

Fixpoint nullables g k : NatSet.t :=
  match k with
   | O => NatSet.empty
   | S k => nullable_step g (nullables g k)
  end.

Definition nullable_sym g s f :=
  match s with
    | T _ => False
    | NT n => NatSet.In n (nullables g f)
  end.

Correctness of nullable_sym.

Lemma nullable_Nullable : forall g f s, nullable_sym g s f -> Nullable_sym g s.
Proof.
Admitted.

Complteness of nullable_sym.

Lemma Nullable_nullable : forall g s, Nullable_sym g s -> exists f, nullable_sym g s f.
Proof.
Admitted.