Signatures and interpretations

A Signature specifies operation symbols with finite arities. The set of symbols may be infinite, and their arities need not have a uniform bound. An Interpretation assigns each symbol an operation on a carrier type. Programs and circuits keep the signature separate from its interpretation.

structure Cslib.Circuits.Signature : Type (v + 1)

A collection of operation symbols, each with a fixed finite arity.

• Op : Type v

  The operation symbols of the signature.

• Arity : self.Op → ℕ

  The number of arguments taken by each operation symbol.

@[reducible, inline]

abbrev Cslib.Circuits.Interpretation (σ : Signature) (Carrier : Type u_1) : Type (max u_1 u_2)

An interpretation assigns an operation on Carrier to every symbol in σ.

Equations

• Cslib.Circuits.Interpretation σ Carrier = ((op : σ.Op) → (Fin (σ.Arity op) → Carrier) → Carrier)