Vocabularies (Signatures)

Following Immerman's "Descriptive Complexity", a vocabulary (also called a signature) is a tuple of relation symbols with arities, plus constant symbols. We represent this finitely: numRels relation symbols with arities given by relArity, and numConsts constant symbols.

structure Complexity.DescriptiveComplexity.Vocabulary : Type

A vocabulary (signature) consisting of finitely many relation symbols with specified arities and finitely many constant symbols.

• numRels : Nat

  Number of relation symbols

• relArity : Fin self.numRels → Nat

  Arity of each relation symbol

• numConsts : Nat

  Number of constant symbols

def Complexity.DescriptiveComplexity.Vocabulary.IsRelational (V : Vocabulary) : Prop

A vocabulary is relational if it has no constant symbols.

Equations

• V.IsRelational = (V.numConsts = 0)

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Vocabulary.empty : Vocabulary

The empty vocabulary with no relation or constant symbols.

Equations

• Complexity.DescriptiveComplexity.Vocabulary.empty = { numRels := 0, relArity := Fin.elim0, numConsts := 0 }

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Vocabulary.ofRel (arity : Nat) : Vocabulary

Construct a vocabulary with a single relation of given arity and no constants.

Equations

• Complexity.DescriptiveComplexity.Vocabulary.ofRel arity = { numRels := 1, relArity := fun (x : Fin 1) => arity, numConsts := 0 }

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Vocabulary.graph : Vocabulary

The vocabulary of directed graphs: one binary relation E.

Equations

• Complexity.DescriptiveComplexity.Vocabulary.graph = Complexity.DescriptiveComplexity.Vocabulary.ofRel 2

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Vocabulary.graphST : Vocabulary

The vocabulary of directed graphs with distinguished source and target: one binary relation E and two constants s, t.

Equations

• Complexity.DescriptiveComplexity.Vocabulary.graphST = { numRels := 1, relArity := fun (x : Fin 1) => 2, numConsts := 2 }

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Vocabulary.stringBuiltinOrder : Vocabulary

The vocabulary for binary strings with built-in ordering (Proviso 1.14): one unary relation S (the "1-bit" predicate). The linear order ≤ and successor are built-in numeric predicates, not part of the vocabulary.

Equations

• Complexity.DescriptiveComplexity.Vocabulary.stringBuiltinOrder = Complexity.DescriptiveComplexity.Vocabulary.ofRel 1

theorem Complexity.DescriptiveComplexity.Vocabulary.graph_isRelational : graph.IsRelational

theorem Complexity.DescriptiveComplexity.Vocabulary.stringBuiltinOrder_isRelational : stringBuiltinOrder.IsRelational