Writing efficient decision procedures

Using Coq
1

I wrote a proof that entailment is decidable in singleton logic (one antecedent, one succedent). Here is my development:

Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Strings.String.

(** Singleton logic: only one assumption, only one conclusion *)
Inductive SingProp: Set :=
(** Atomic variable *)
| Var: string -> SingProp
(** Disjunction *)
| plus_: SingProp -> SingProp -> SingProp
(** Conjunction *)
| with_: SingProp -> SingProp -> SingProp.
Scheme Equality for SingProp.

Notation "A + B" := (plus_ A B) (at level 50, left associativity).
Notation "A & B" := (with_ A B) (at level 50, left associativity).

Reserved Notation "A |> B" (at level 60, no associativity).
Inductive entails: relation SingProp :=
| id s: Var s |> Var s

| plus_l A B C: A |> C -> B |> C -> A + B |> C
| plus_r1 A B C: A |> B -> A |> B + C
| plus_r2 A B C: A |> C -> A |> B + C

| with_l1 A B C: A |> C -> A & B |> C
| with_l2 A B C: B |> C -> A & B |> C
| with_r A B C: A |> B -> A |> C -> A |> B & C
where "A |> B" := (entails A B).

Lemma dec_entails A B: {A |> B} + {~ A |> B}.
Proof.
Admitted.

dec_entails has a simple informal proof, proceeding by induction on the sum of the sizes of the hypothesis and conclusion. When both are of the form Var _ (corresponding to a combined size of zero), entailment is decidable as there is only one inference rule that mentions atomic variables. Otherwise, we check if any other inference rule applies. All inference rules have antecedents that are strictly smaller than their conclusions, so we can decide the antecedents using the induction hypothesis.

I’ve implemented this by enumerating every possible antecedent and showing that it is decidable. So one case of the proof looks like:

  (* case _ & _ |> _ + _ *)
  - show_decidable (H (s1, s3 + s4)).
    show_decidable (H (s2, s3 + s4)).
    show_decidable (H (s1 & s2, s3)).
    show_decidable (H (s1 & s2, s4)).

The resulting decision procedure is positively enormous! I’m not sure how to get an exact number, but when I write Print dec_entails I get a four-thousand-line definition, with lots of ... hiding even more code. Checking the proof takes about one second, and printing it takes several. I haven’t tried writing an unverified version, but I suspect it would be under fifty lines of code.

So my question is: how do you a) write efficient decision procedures, and b) assess the efficiency of an existing decision procedure?

2

I am very happy you are considering this logic: it is my favorite one!

I am not at all an expert in such decision procedures in Coq, but I do not find so surprising that you get long Coq code: it contains the complete certification of your decision procedure. I am not sure it has bad impact on efficiency.
I think one possibility to have a shorter code is to separate into a Boolean function:

Definition entailsb (A B : SingProp) : bool.

and a proof of correctness:

Lemma entails_reflect A B : reflect (A |> B) (entailsb A B).

The following very naive function (I hope it is correct) which basically tries to apply any possible rule (slight optimization based on reversibility of plus_l and with_r):

Definition entailsb_naive (A B : SingProp) : bool.
Proof.
induction A.
- induction B.
  * exact (string_beq s s0).
  * exact (orb IHB1 IHB2).
  * exact (andb IHB1 IHB2).
- exact (andb IHA1 IHA2).
- induction B.
  * exact (orb IHA1 IHA2).
  * exact (orb (orb IHA1 IHA2) (orb IHB1 IHB2)).
  * exact (andb IHB1 IHB2).
Defined.

Print entailsb_naive.

gives 11 lines of code.

If you want to consider efficiency and look at less naive approaches, independently of Coq, there are different ways to go to a more efficient decision procedure for this logic: rely on the left/right symmetry of rules, rely on reversibility of some rules, rely on the focusing property, etc.

2 Likes
3

Second thought: it is probably more comfortable in practice to define entailsb directly as a fixpoint:

Fixpoint entailsb A : SingProp -> bool :=
match A with
| Var s1 => fix loc_entailsb B :=
            match B with
            | Var s2 => string_beq s1 s2
            | B1 + B2 => loc_entailsb B1 || loc_entailsb B2
            | B1 & B2 => loc_entailsb B1 && loc_entailsb B2
            end
| A1 + A2 => fun B => entailsb A1 B && entailsb A2 B
| A1 & A2 => fix loc_entailsb2 B :=
             match B with
             | Var s2 => entailsb A1 B || entailsb A2 B
             | B1 + B2 => entailsb A1 B || entailsb A2 B
                          || loc_entailsb2 B1 || loc_entailsb2 B2
             | B1 & B2 => loc_entailsb2 B1 && loc_entailsb2 B2
             end
end.

BTW I have proved this one correct (around 100 lines of Coq).

1 Like
4

I have to say I find it absolutely charming. It’s so simple to define, but it’s still a good vehicle for discussing basic metatheoretic properties.

1 Like