4
$\begingroup$

I'm trying to define a first-order relational structure in Coq.

I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough.

I also have a way to insist that a pre-first-order-relational-structure is actually a relational structure.

These things can be stitched together with a sig type, but this does not make idiomatic use of Coq features. What's a better way to do it?

See Appendix B for a brief history of this question.


The approach that I've taken so far is to define a pre first-order structure as a thing that takes a type of symbols S and then wraps a type U denoting the universe/domain/carrier.

Every symbol has an arity, which is None if the symbol is not defined in this particular structure.

Also, every list of items taken from U is potentially inside the interpretation of any relation symbol (i.e. symbols don't a priori respect arity).

This approach keeps the type signature of a PreFOS simple.

Defining IsFOS, which takes a PreFOS and insists that it actually does respect arity is not that difficult.

Appendix A: Original Implementation

Require Import List.

(* A pre-[Relational First-order Structure] 

S is the set of all symbols, a symbol may or may not be defined
in a given relational structure.

 *)
Record PreFOS (S : Type) (U : Type) : Type :=
  { arity : S -> option nat
  ; interpretation : S -> (list U) -> Prop
  }.

(*
IsFOSImpl defines what it means to be a relational first-order structure.

If a symbol is undefined, it must be false everywhere.

If a symbol is defined, but called with the wrong number of arguments,
it must also return false.
 *)
Definition IsFOS (S : Type) (U : Type) (M : PreFOS S U) : Prop :=
  (
    (* Undefined symbols always interpret to false. *)
    (forall s : S,
        arity S U M s = None ->
        (forall args : list U, interpretation S U M s args -> False))
  ) /\
    (
      (* Defined symbols interpret to false outside their arity. *)
      (forall s : S,
          (exists n : nat, arity S U M s = Some n ->
                           (forall args : list U,
                               length args <> n ->
                               (interpretation S U M s args -> False))))
    ).

Appendix B: History of Question

This question was originally about how to take an existing type X and produce a type referring to the Xs that satisfy P. This is a sig type as pointed out by Andrej Bauer in the comments.

However, the original question was ambiguous how do you make a type constrained by a predicate could be referring to sig types. It is also a description of a first-order relational structure is.

Andrej's answer very thoroughly addresses everything that's non-idiomatic with Appendix A. I think this has a lot of value, especially for novice Coq users like me.

I'm retroactively changing this question to make the answer on topic.

$\endgroup$
6
  • 1
    $\begingroup$ Can you explain why you want some symbols to be undefined, please? It seems far saner to just insist that every symbol be interpreted. Also, PreFos does not ensure that the arity and the interpretation fit together (because you are using list instead of a tuple of the given arity). It looks like the whole thing would benefit from more dependent types and less first-order-logic thinking. $\endgroup$ Feb 19 at 22:32
  • $\begingroup$ @AndrejBauer For this question, the main thing I was trying to do was figure out how to express ($X$s satisfying $P$) as a type in Coq, since doing that is currently beyond my ability. In retrospect, picking a relational first-order structure was not really a great example for my question. I could have just used nat and asked how to express a natural number greater than zero. I don't want to change the example now because your answer is great. $\endgroup$ Feb 19 at 23:28
  • $\begingroup$ @AndrejBauer I also noticed that you changed the title of my question to match the example rather than the construction ($X$s satisfying $P$) (that I don't know the name of). How should I express that? The construction (building a definition of FOS out of PreFOS and IsFOS) was intended to be more important than the specific example, which is just a translation of the first-order logic concept as it's normally presented written in very naive Coq. $\endgroup$ Feb 19 at 23:33
  • 1
    $\begingroup$ Are you looking for the sig type, written as { x : A | p x }? Sorry, I did read your question as it being about how to define relational structures, which is why I changed the title. Feel free to change it back, but before that, also please look at the sig type to see if that answers your question. $\endgroup$ Feb 20 at 8:08
  • 1
    $\begingroup$ @AndrejBauer, yes. The sig type tag is exactly what I am looking for. Thank you. Your answer is extremely helpful though (although a lot of it is beyond my level of understanding). I'm going to edit my question with an update explaining what the question originally was and what it is now. $\endgroup$ Feb 20 at 19:29

1 Answer 1

5
$\begingroup$

Supplemental: It looks like I misunderstood the point of the question and the OP might have simply been looking for the sig type, usually written as {x : A | P A}. Apologies for showing below some irrelevant code.

Here is the idomatic approach to defining relational signatures and relational structures. It uses dependent types the way they're supposed to be used.

(* A relational signature is given by a type of relational symbols, and for each
   symbol an arity. While it is customary to think of the arity as a number, it
   is more principled to think of it as a set of indices (indexing the
   arguments).

   Thus, instead of saying that S has arity 2, we say that S har arity bool (or any other
   two-element type).
*)

Record RelationalSignature : Type :=
  { symbols :> Type
  ; arity : symbols -> Type
  }.

Arguments arity {_} _.

(* A relational structure is given by a carrier type U and an interpetation function
   which, for each relational symbol S of arity n, gives a predicate on U^n.

   Notice how taking arities to be types allows us to write just "arity S -> carrier".
*)

Record RelationalStructure (Sig : RelationalSignature) : Type :=
  { carrier :> Type
  ; interpretation : forall S : Sig, (arity S -> carrier) -> Prop
  }.

(* Example: a signature with a binary symbol Cow and a unary symbol Rabbit. *)

(* The type of symbols. *)
Inductive MySymbols : Type := Cow | Rabbit.

(* The arity of a unary symbol. *)
Inductive Unary : Type := the_arg.

(* The arity of a binary symbol. *)
Inductive Binary : Type := arg1 | arg2.

Definition MySignature :=
  {| symbols := MySymbols
   ; arity := fun S => match S with
                         | Cow => Binary
                         | Rabbit => Unary
                       end
  |}.

(* An example of a relational structure on natural numbers in which we interpret
   Cow as "less than or equal" and Rabbit as "not zero". *)

Definition MyStructure : RelationalStructure MySignature :=
  {| carrier := nat
   ; interpretation :=
       fun (S : MySignature) =>
         match S with
           | Cow => (fun xs => xs arg1 <= xs arg2)
           | Rabbit => fun xs => xs the_arg <> 0
         end
  |}.

You do not need any predicates explaining that the signature or the relational structure is valid. It is all taken care of by the dependent types.

$\endgroup$
1
  • $\begingroup$ Thank you. This answer is very helpful, so I changed the question so it's unambiguously about how do I define a relation first-order structure idiomatically. I included a history of the question itself in an appendix at the end. $\endgroup$ Feb 20 at 19:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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