Enumerating all formulae of any first-order language

Question

I'm formalizing the metatheory of first-order logic with Coq. I want to enumerate all expressions of any first-order language.

The syntax of terms and formulae are:

Section SYNTAX.

Definition ivar : Set := nat.

Let arity : Set := nat.

#[projections(primitive)]
Record language : Type :=
  { function_symbols : Set
  ; constant_symbols : Set
  ; relation_symbols : Set
  ; function_arity_table : function_symbols -> arity
  ; relation_arity_table : relation_symbols -> arity
  }.

Context {L : language}.

Inductive trm : Set :=
  | Var_trm (x : ivar) : trm
  | Fun_trm (f : L.(function_symbols)) (ts : trms (L.(function_arity_table) f)) : trm
  | Con_trm (c : L.(constant_symbols)) : trm
with trms : arity -> Set :=
  | O_trms : trms O
  | S_trms (n : arity) (t : trm) (ts : trms n) : trms (S n).

Inductive frm : Set :=
  | Rel_frm (r : L.(relation_symbols)) (ts : trms (L.(relation_arity_table) r)) : frm
  | Eqn_frm (t1 : trm) (t2 : trm) : frm
  | Neg_frm (p1 : frm) : frm
  | Imp_frm (p1 : frm) (p2 : frm) : frm
  | All_frm (y : ivar) (p1 : frm) : frm.

Variable enum_function_symbols : nat -> L.(function_symbols).

Variable enum_constant_symbols : nat -> L.(constant_symbols).

Definition enum_trm : nat -> trm. Admitted.

Definition enum_trms {n : arity} : nat -> trms n. Admitted.

Variable enum_relation_symbols : nat -> L.(relation_symbols).

Definition enum_frm : nat -> frm. Admitted.

End SYNTAX.

How can I define enum_trm, enum_trms, and enum_frm which must be surjective? Any idea?

Answer 1

If you don't care about injectivity, you can use a Godel-numbering-like encoding, i.e. $$ \mathtt{enum\_trm}(n) = \begin{cases}t &\text{if } n \text{ is } 2^\left<\text{index of constructor of }t\right> * 3^\left<\text{encoding of the first argument of constructor of }t\right> * 5^\left<\text{second}\ldots\right> * 7^\left<\text{third}\ldots\right> * \ldots\\ \mathtt{Var\_trm}\ \ 0 & \text{otherwise} \end{cases} $$ And this will be provably surjective as far as your Variable things (for function symbols and so on) are surjective.

Answer 2

First of all, let us define the depth of expressions:

Fixpoint trm_depth (t : trm) : nat :=
  match t with
  | Var_trm x => 0
  | Fun_trm f ts => 1 + trms_depth ts
  | Con_trm c => 1
  end
with trms_depth {n : arity} (ts : trms n) : nat :=
  match ts with
  | O_trms => 0
  | S_trms _ t ts => 1 + max (trm_depth t) (trms_depth ts)
  end.

And we'll use the Cantor pairing function cp : nat -> (nat * nat):

Fixpoint cp (n : nat) {struct n} : nat * nat :=
  match n with
  | O => (0, 0)
  | S n' =>
    match cp n' with
    | (O, y) => (S y, 0)
    | (S x, y) => (x, S y)
    end
  end.

Note that cp is bijective because: $$ \mathtt{cp} \left( n \right) = \left( x , y \right) \iff n = \left( \sum_{i = 0}^{x + y} i \right) + y . $$

Now, we generate a trm t with the seed such that the depth of t is less than or equal to a given natural number rk — i.e., gen_trm seed rk = t holds for some seed if trm_depth t <= rk:

Fixpoint gen_trm (seed : nat) (rk : nat) {struct rk} : trm :=
  match rk with
  | O => Var_trm seed
  | S rk' =>
    let seed1 := fst (cp seed) in
    let seed' := snd (cp seed) in
    let seed2 := fst (cp seed') in
    let seed3 := snd (cp seed') in
    match seed1 with
    | 0 => Con_trm (enum_constant_symbols seed')
    | 1 => Fun_trm (enum_function_symbols seed2) (gen_trms seed3 rk')
    | S (S i) => Var_trm i
    end
  end
with gen_trms {n : arity} (seed : nat) (rk : nat) {struct rk} : trms n :=
  match n with
  | O => O_trms
  | S n' =>
    match rk with
    | O => nat_rec _ (O_trms) (fun x => fun acc => S_trms _ (Var_trm seed) acc) (S n')
    | S rk' =>
      let seed1 := fst (cp seed) in
      let seed2 := snd (cp seed) in
      S_trms _ (gen_trm seed1 rk') (gen_trms seed2 rk')
    end
  end.

Finally, we take:

Definition enum_trm (seed : nat) : trm :=
  let rk := fst (cp seed) in
  let seed' := snd (cp seed) in
  gen_trm seed' rk.

Definition enum_trms {n : arity} (seed : nat) : trms n :=
  let rk := fst (cp seed) in
  let seed' := snd (cp seed) in
  gen_trms seed' rk.

On the other hand, we can prove gen_trm_spec and gen_trms_spec by induction on t and ts and then destruct rk:

Hypothesis enum_function_symbols_onto
  : forall f : L.(function_symbols), { n : nat | enum_function_symbols n = f }.

Hypothesis enum_constant_symbols_onto
  : forall c : L.(constant_symbols), { n : nat | enum_constant_symbols n = c }.

Lemma gen_trm_spec (t : trm) (rk : nat)
  (RANK_LE : trm_depth t <= rk)
  : { seed : nat | gen_trm seed rk = t }
with gen_trms_spec (n : arity) (ts : trms n) (rk : nat)
  (RANK_LE : trms_depth ts <= rk)
  : { seed : nat | gen_trms seed rk = ts }.

Then, for given a trm t, applying gen_trm_spec with rk := trm_depth t and t := t, we can derive { seed : nat | enum_trm seed = t }:

Theorem trm_is_enumerable (t : trm)
  : { seed : nat | enum_trm seed = t }.

Theorem trms_is_enumerable (n : arity) (ts : trms n)
  : { seed : nat | enum_trms seed = ts }.

Therefore, we can conclude enum_trm and enum_trms are surjective.