Interfaces

Difficulty: moderate — 4 definitions, 1 abbreviations, 0 lemmas, 1 theorems.

definition abbreviation theorem

legend

An interface is a list of ports. Each port can carry its own type of value — unlike Component.Impl, where every port carries the same Wire type. A Component.Impl is just the special case where every port happens to carry the same type as every other port.

Ports have no direction: an interface by itself doesn’t say which ports are “in” and which are “out”. That distinction only shows up once something actually uses two interfaces together, one for what goes in and one for what comes out — not here.

This file only describes the ports themselves. It says nothing about time, or about what happens over time; that’s left for other files to add later, on top of this one.

Interface

An interface: card ports, each with its own carried type, inhabited and size-measured.

structure Interface where
  /-- The number of ports. -/
  card : Nat
  /-- The type carried by each port. -/
  Port : Fin card → Type
  /-- Every port is inhabited: there's always some value it could carry. -/
  nonempty : ∀ i, Nonempty (Port i)
  /-- Every port's type has a canonical real-valued measure. -/
  size : ∀ i, Norm (Port i)

Outer dependencies: (none)

Mathlib dependencies: Norm

Lean core dependencies: Eq, Fin, HEq, Nat, Nonempty

Used by: Interface.Value, Interface.homogeneous, Interface.tensor, Interface.unit, Layer, LayeredArchitecture, NetworkArchitecture, NetworkBoundary, instNonemptyValue, instNormValue

Interface.Value

A value carried on every port of an interface at once, at a single instant.

abbrev Interface.Value (I : Interface) := (i : Fin I.card) → I.Port i

Outer dependencies: Interface

Lean core dependencies: Fin

Used by: Layer, instNonemptyValue, instNormValue

instNormValue

The measure of an interface value is the sum of the measures of its ports’ values.

noncomputable instance (I : Interface) : Norm I.Value where
  norm v := ∑ i, @Norm.norm _ (I.size i) (v i)

Outer dependencies: Interface, Interface.Value

Mathlib dependencies: Finset.sum, Finset.univ, Norm, Real

Lean core dependencies: Fin

Used by: Layer

Interface.unit

The empty interface: no ports at all. Combining it with any other interface (via Interface.tensor below) leaves that other interface unchanged.

def Interface.unit : Interface where
  card := 0
  Port := fun i => i.elim0
  nonempty := fun i => i.elim0
  size := fun i => i.elim0

Outer dependencies: Interface

Mathlib dependencies: Norm

Lean core dependencies: Fin, Fin.elim0, Nat, Nonempty

Used by: (none)

Interface.tensor

Concatenate two interfaces: the first’s ports followed by the second’s.

def Interface.tensor (I J : Interface) : Interface where
  card := I.card + J.card
  Port k := if h : (k : Nat) < I.card then I.Port ⟨k, h⟩ else J.Port ⟨(k : Nat) - I.card, by omega⟩
  nonempty k := by
    show Nonempty (if h : (k : Nat) < I.card then I.Port ⟨k, h⟩
      else J.Port ⟨(k : Nat) - I.card, by omega⟩)
    split
    · exact I.nonempty _
    · exact J.nonempty _
  size k := by
    show Norm (if h : (k : Nat) < I.card then I.Port ⟨k, h⟩
      else J.Port ⟨(k : Nat) - I.card, by omega⟩)
    split
    · exact I.size _
    · exact J.size _

Outer dependencies: Interface

Mathlib dependencies: Norm

Used by: (none)

Interface.homogeneous

The homogeneous case recovers today’s Component.Impl: every port carries the same type.

def Interface.homogeneous (Wire : Type) [Nonempty Wire] [Norm Wire] (n : Nat) : Interface where
  card := n
  Port _ := Wire
  nonempty _ := ‹Nonempty Wire›
  size _ := ‹Norm Wire›

Outer dependencies: Interface

Mathlib dependencies: Norm

Lean core dependencies: Fin, Nat, Nonempty

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.

definitionabbreviationtheoremdeclared elsewheredependencyproof dependency

legend