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)

inductive Cslib.Circuits.FullOp (k : ℕ) (Carrier : Sort u_1) : Sort (max 1 u_1)

An operation with labels for all constants and operations of arity k.

• fn {k : ℕ} {Carrier : Sort u_1} : ((Fin k → Carrier) → Carrier) → FullOp k Carrier
• con {k : ℕ} {Carrier : Sort u_1} : Carrier → FullOp k Carrier

def Cslib.Circuits.fullSignature (k : ℕ) (Carrier : Type v) : Signature

The signature for FullOp.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Circuits.fullInterpretation {k : ℕ} {Carrier : Type u_1} : Interpretation (fullSignature k Carrier) Carrier

The natural interpretation for FullOp, where we evaluate each constant and function to itself.

Equations

• Cslib.Circuits.fullInterpretation (Cslib.Circuits.FullOp.fn f) tuple_2 = f tuple_2
• Cslib.Circuits.fullInterpretation (Cslib.Circuits.FullOp.con c) tuple_2 = c