HMM adapters as NNModuleSpecs

The HMM spec model (NN/Spec/Models/Hmm.lean) uses discrete observations (Fin nObservations).

For composition and demos, it is sometimes convenient to accept a tensor of scores/probabilities over the observation alphabet and decode each timestep via argmax. The wrappers in this file provide that bridge and package the resulting behavior as NNModuleSpecs.

def Spec.tensorToDiscreteObs {α : Type} [Context α] {nObservations : ℕ} [Inhabited (Fin nObservations)] (h_nobs : nObservations > 0) (obs_tensor : Tensor α (Shape.dim nObservations Shape.scalar)) : Fin nObservations

Decode a single observation vector into a discrete symbol by taking argmax.

@[irreducible]

def Spec.tensorToDiscreteObs.find_argmax {α : Type} [Context α] {nObservations : ℕ} (obs_tensor : Tensor α (Shape.dim nObservations Shape.scalar)) (i : ℕ) (max_val : α) (max_idx : Fin nObservations) : Fin nObservations

def Spec.tensorSeqToDiscreteSeq {α : Type} [Context α] {seqLen nObservations : ℕ} [Inhabited (Fin nObservations)] (h_nobs : nObservations > 0) (obs_seq_tensor : Tensor α (Shape.dim seqLen (Shape.dim nObservations Shape.scalar))) : ObservationSeq nObservations

Convert a tensor of per-symbol scores/probabilities into a discrete observation sequence by decoding each timestep with argmax.

@[irreducible]

def Spec.tensorSeqToDiscreteSeq.convert_seq {α : Type} [Context α] {seqLen nObservations : ℕ} [Inhabited (Fin nObservations)] (h_nobs : nObservations > 0) (obs_seq_tensor : Tensor α (Shape.dim seqLen (Shape.dim nObservations Shape.scalar))) (t : ℕ) (acc : List (Fin nObservations)) : List (Fin nObservations)

def Spec.HMMModuleSpec {α : Type} [Context α] {nStates nObservations : ℕ} [Inhabited (Fin nObservations)] (h_nobs : nObservations > 0) (m : HMMSpec α nStates nObservations) : ModSpec.NNModuleSpec α (Shape.dim nObservations Shape.scalar) (Shape.dim nStates Shape.scalar)

A one-step HMM module: map an observation distribution to a filtered state distribution.

def Spec.hmmForwardPassSpec {α : Type} [Context α] {nStates nObservations : ℕ} [Inhabited (Fin nObservations)] (m : HMMSpec α nStates nObservations) (observations : ObservationSeq nObservations) : List (Tensor α (Shape.dim nStates Shape.scalar))

Forward messages α_t for each timestep (scaled).

def Spec.HMMSeqModuleSpec {α : Type} [Context α] {seqLen nStates nObservations : ℕ} [Inhabited (Fin nObservations)] (h_nobs : nObservations > 0) (m : HMMSpec α nStates nObservations) : ModSpec.NNModuleSpec α (Shape.dim seqLen (Shape.dim nObservations Shape.scalar)) (Shape.dim seqLen (Shape.dim nStates Shape.scalar))

Sequence module: compute forward messages α_t for each timestep.

def Spec.HMMSeqLikelihoodModuleSpec {α : Type} [Context α] {seqLen nStates nObservations : ℕ} [Inhabited (Fin nObservations)] (h_nobs : nObservations > 0) (m : HMMSpec α nStates nObservations) : ModSpec.NNModuleSpec α (Shape.dim seqLen (Shape.dim nObservations Shape.scalar)) (Shape.dim seqLen Shape.scalar)

Sequence module: compute prefix likelihoods p(o₀:t) for each timestep t.

def Spec.HMMSeqStateProbModuleSpec {α : Type} [Context α] {seqLen nStates nObservations : ℕ} [Inhabited (Fin nObservations)] (h_nobs : nObservations > 0) (m : HMMSpec α nStates nObservations) : ModSpec.NNModuleSpec α (Shape.dim seqLen (Shape.dim nObservations Shape.scalar)) (Shape.dim seqLen (Shape.dim nStates Shape.scalar))

Sequence module: normalized state probabilities at each timestep.

def Spec.HMMSeqIndependentModuleSpec {α : Type} [Context α] {seqLen nStates nObservations : ℕ} [Inhabited (Fin nObservations)] (h_nobs : nObservations > 0) (m : HMMSpec α nStates nObservations) : ModSpec.NNModuleSpec α (Shape.dim seqLen (Shape.dim nObservations Shape.scalar)) (Shape.dim seqLen (Shape.dim nStates Shape.scalar))

Sequence module: apply the one-step update independently at each timestep.