NN.Optimisers.Definition

Definitions

record DOptimiser : (inputTy -> AddCont) -> Type -> Type

  Dependent stateful optimiser, modelled as a dependent lens
  Dependent version of section 8.1.3 of https://arxiv.org/abs/2403.13001
  Because we use dependent Para, optimiser can depend on the input

Totality: total
Visibility: public export
Constructor:

MkDOptimiser : ((x : inputTy) -> (Const ((paramCont x) .Shp) >< Const stateTy) =%> UC (paramCont x)) -> DOptimiser paramCont stateTy

Projection:

.opt : DOptimiser paramCont stateTy -> (x : inputTy) -> (Const ((paramCont x) .Shp) >< Const stateTy) =%> UC (paramCont x)

  Notably this produces an ordinary dependent lens, not an additive one

.opt : DOptimiser paramCont stateTy -> (x : inputTy) -> (Const ((paramCont x) .Shp) >< Const stateTy) =%> UC (paramCont x)

  Notably this produces an ordinary dependent lens, not an additive one

Totality: total
Visibility: public export

opt : DOptimiser paramCont stateTy -> (x : inputTy) -> (Const ((paramCont x) .Shp) >< Const stateTy) =%> UC (paramCont x)

  Notably this produces an ordinary dependent lens, not an additive one

Totality: total
Visibility: public export

record Optimiser : AddCont -> Type -> Type

Totality: total
Visibility: public export
Constructor:

MkOptimiser : (Const (paramCont .Shp) >< Const stateTy) =%> UC paramCont -> IO stateTy -> Optimiser paramCont stateTy

Projections:

.initState : Optimiser paramCont stateTy -> IO stateTy

  Initialising the state; parameters are initialised by the model

.opt : Optimiser paramCont stateTy -> (Const (paramCont .Shp) >< Const stateTy) =%> UC paramCont

Totality: total
Visibility: public export

opt : Optimiser paramCont stateTy -> (Const (paramCont .Shp) >< Const stateTy) =%> UC paramCont

Totality: total
Visibility: public export

.initState : Optimiser paramCont stateTy -> IO stateTy

  Initialising the state; parameters are initialised by the model

Totality: total
Visibility: public export

initState : Optimiser paramCont stateTy -> IO stateTy

  Initialising the state; parameters are initialised by the model

Totality: total
Visibility: public export

.fwd : Optimiser p s -> (p .Shp, s) -> p .Shp

  An optimiser is a lens: forward reads the parameter, backward updates (parameter, state)

Totality: total
Visibility: public export

.bwd : (opt : Optimiser pCont stateTy) -> (ps : (pCont .Shp, stateTy)) -> pCont .PosSet (opt .fwd ps) -> (pCont .Shp, stateTy)

Totality: total
Visibility: public export

composeParallel : Optimiser pCont s -> Optimiser qCont t -> Optimiser (pCont >*< qCont) (s, t)

  From 8.1.3. "Can we compose optimisers?" of https://arxiv.org/abs/2403.13001
  Not used yet

Totality: total
Visibility: public export