3
$\begingroup$

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?

$\endgroup$

2 Answers 2

3
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ Why is this not injective? I thought the point of a Gödel encoding was to be injective $\endgroup$
    – Couchy
    Commented Jun 12 at 20:20
  • $\begingroup$ @Couchy How would you handle 2 * 3 * 5 and 2 * 3 * 5 * 7 where 1 (the power for 2) is the index for Var_trm? There simply aren't such "second" or "third" argument, so without special treatment, they can collide. Likewise for any other cases. $\endgroup$
    – Clare Jang
    Commented Jun 12 at 20:24
  • $\begingroup$ Gödel's encoding has a similar problem. What if the power/prime numbers/... go over the designated ranges? Like, if we treat 2^<a> * 3^<b> * ... as a string that represents abc... (where <a> is the encoding of a), what if 2^x, where x does not corresponds to any symbol? For example, IIRC, Gödel's original encoding does not have symbol corresponding to 2, so 2^2 is not really an encoding, or, if we take the approach in this answer, will collide with other "invalid" numbers. $\endgroup$
    – Clare Jang
    Commented Jun 12 at 20:39
  • $\begingroup$ Or maybe the confusion is the direction of the function? Here the enumeration function (from nat to term) is surjective if and only if the corresponding encoding function (from term to nat) is injective. In that sense, the given encoding is indeed injective. However, the enumeration function is, as I explained in the previous comments, surjective but not injective. $\endgroup$
    – Clare Jang
    Commented Jun 12 at 20:40
  • $\begingroup$ But how can I implement it constructively? If the metalanguage was ZFC, the enumeration function you suggested would be well-defined. But I'm working with Coq (without additional Axiom), the function is hard to be implemented directly. (Sorry for the late reply.) $\endgroup$ Commented Jun 13 at 14:11
3
$\begingroup$

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.

$\endgroup$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.