trait FixedProofs extends GenerateTyps
fixes the weights of proofs, to try to flow with types making worse matches
Linear Supertypes
Type Hierarchy
Ordering
- Alphabetic
- By Inheritance
Inherited
- FixedProofs
- GenerateTyps
- ExpressionEquationSolver
- AnyRef
- Any
Implicitly
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
Visibility
- Public
- Protected
Type Members
- case class FixedExpressionProbs(p: Map[Expression, Double]) extends Product with Serializable
- Definition Classes
- ExpressionEquationSolver
Abstract Value Members
- abstract val coeffsAsVars: Boolean
- Definition Classes
- ExpressionEquationSolver
- abstract val coeffval: (Coeff[_]) => Option[Double]
- Definition Classes
- ExpressionEquationSolver
- abstract val decay: Double
- Definition Classes
- ExpressionEquationSolver
- abstract val equations: Set[Equation]
- Definition Classes
- ExpressionEquationSolver
- abstract val exponent: Double
- Definition Classes
- ExpressionEquationSolver
- abstract val init: Map[Expression, Double]
- Definition Classes
- ExpressionEquationSolver
- abstract val maxRatio: Double
- Definition Classes
- ExpressionEquationSolver
- abstract val maxTime: Option[Long]
- Definition Classes
- ExpressionEquationSolver
- abstract val previousMap: Option[Map[Expression, Double]]
- Definition Classes
- ExpressionEquationSolver
- abstract val proofWeights: Map[Typ[Term], Double]
- abstract val resolution: Double
- Definition Classes
- ExpressionEquationSolver
- abstract val scale: Double
- Definition Classes
- ExpressionEquationSolver
- abstract val smoothing: Option[Double]
- Definition Classes
- ExpressionEquationSolver
- abstract val varWeight: Double
- Definition Classes
- ExpressionEquationSolver
Concrete Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- Implicit
- This member is added by an implicit conversion from FixedProofs toany2stringadd[FixedProofs] performed by method any2stringadd in scala.Predef.
- Definition Classes
- any2stringadd
- def ->[B](y: B): (FixedProofs, B)
- Implicit
- This member is added by an implicit conversion from FixedProofs toArrowAssoc[FixedProofs] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @inline()
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- lazy val Final: FixedExpressionProbs
- Definition Classes
- ExpressionEquationSolver
- def adverseIterant(hW: Double = 1, klW: Double = 1, p: Map[Expression, Double] = finalDist): Iterant[Task, Map[Expression, Double]]
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- lazy val atoms: Set[Expression]
the atomic expressions in the equations
the atomic expressions in the equations
- Definition Classes
- ExpressionEquationSolver
- def avgInit(that: ExpressionEquationSolver): ExpressionEquationSolver
new expression-equation-solver with initial distribution averaged with the current one
new expression-equation-solver with initial distribution averaged with the current one
- that
the other initial distribution
- returns
averaged expression eval
- Definition Classes
- ExpressionEquationSolver
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
- lazy val coefficients: Vector[Coeff[_]]
- Definition Classes
- ExpressionEquationSolver
- implicit lazy val dim: JetDim
- Definition Classes
- ExpressionEquationSolver
- def ensuring(cond: (FixedProofs) => Boolean, msg: => Any): FixedProofs
- Implicit
- This member is added by an implicit conversion from FixedProofs toEnsuring[FixedProofs] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: (FixedProofs) => Boolean): FixedProofs
- Implicit
- This member is added by an implicit conversion from FixedProofs toEnsuring[FixedProofs] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean, msg: => Any): FixedProofs
- Implicit
- This member is added by an implicit conversion from FixedProofs toEnsuring[FixedProofs] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean): FixedProofs
- Implicit
- This member is added by an implicit conversion from FixedProofs toEnsuring[FixedProofs] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def entropy(hW: Double = 1, klW: Double = 1): Expression
Expression for composite entropy.
Expression for composite entropy.
- Definition Classes
- ExpressionEquationSolver
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- lazy val eqnExpressions: Vector[Expression]
Expressions for equations.
Expressions for equations.
- Definition Classes
- ExpressionEquationSolver
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- def expressionGroup(exp: Expression): Option[Set[Expression]]
- Definition Classes
- ExpressionEquationSolver
- lazy val finalDist: Map[Expression, Double]
The final distributions, obtained from the initial one by finding an almost solution.
The final distributions, obtained from the initial one by finding an almost solution.
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTermEntropy: Expression
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTermMap: Map[Term, Expression]
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTermSet: Set[Term]
Terms in the final (i.e.
Terms in the final (i.e. evolved) distribution * May have extra terms that evaluate to zero
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTermSetSum: Sum
- Definition Classes
- ExpressionEquationSolver
- def finalTermState(vars: Vector[Term] = Vector(), inds: FiniteDistribution[ExstInducDefn] = FD.empty[induction.ExstInducDefn], goals: FiniteDistribution[Typ[Term]] = FD.empty, context: Context = Context.Empty): TermState
final term state
final term state
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTerms: FiniteDistribution[Term]
final distribution on terms
final distribution on terms
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTypEntropy: Expression
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTypMap: Map[Term, Expression]
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTypSet: Set[Typ[Term]]
Typs in the final (i.e.
Typs in the final (i.e. evolved) distribution May have extra types that evaluate to zero
- Definition Classes
- ExpressionEquationSolver
- lazy val finalTyps: FiniteDistribution[Typ[Term]]
- Definition Classes
- GenerateTyps → ExpressionEquationSolver
- lazy val finalVarGroups: Map[(RandomVar[_], Vector[_]), Set[Expression]]
- Definition Classes
- ExpressionEquationSolver
- def fixTypes: ExpressionEquationSolver
undoing generation of types by freezing them
undoing generation of types by freezing them
- Definition Classes
- ExpressionEquationSolver
- def flattenedEntropy(pow: Double, hW: Double = 1, klW: Double = 1): Expression
- Definition Classes
- ExpressionEquationSolver
- def flattenedKLExp(pow: Double): Expression
- Definition Classes
- ExpressionEquationSolver
- def flattenedOptimumTask(pow: Double, hW: Double = 1, klW: Double = 1, cutoff: Double, p: Map[Expression, Double] = finalDist, maxRatio: Double = 1.01): Task[Map[Expression, Double]]
- Definition Classes
- ExpressionEquationSolver
- def formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from FixedProofs toStringFormat[FixedProofs] performed by method StringFormat in scala.Predef.
- Definition Classes
- StringFormat
- Annotations
- @inline()
- lazy val funcTotal: Expression
- Definition Classes
- ExpressionEquationSolver
- lazy val genTerms: Map[Term, Expression]
Terms of the generating distribution
Terms of the generating distribution
- Definition Classes
- ExpressionEquationSolver
- def generateTyps: ExpressionEquationSolver
copy with types generated from equations
copy with types generated from equations
- Definition Classes
- GenerateTyps → ExpressionEquationSolver
- def generatorIterant(hW: Double = 1, klW: Double = 1, cutoff: Double, p: Map[Expression, Double] = finalDist): Iterant[Task, FiniteDistribution[Term]]
- Definition Classes
- ExpressionEquationSolver
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def gradShift(p: Map[Expression, Double], t: Vector[Double], eps: Double = scale): Map[Expression, Double]
Shift downwards by the gradient, mapped by sigmoids.
Shift downwards by the gradient, mapped by sigmoids.
- Definition Classes
- ExpressionEquationSolver
- lazy val hExp: Expression
Expression for entropy of the generating distribution
Expression for entropy of the generating distribution
- Definition Classes
- ExpressionEquationSolver
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def indepEquations(variable: Term): Set[Equation]
equations not depending on a variable, to be used with boats
equations not depending on a variable, to be used with boats
- Definition Classes
- ExpressionEquationSolver
- lazy val indexEquationSolver: IndexEquationSolver
the solver that does the actual solving
the solver that does the actual solving
- returns
indexed-equation-solver with the correct parameters
- Definition Classes
- ExpressionEquationSolver
- lazy val initTerms: Vector[Term]
Terms in the initial distributions, used to calculate total weights of functions etc
Terms in the initial distributions, used to calculate total weights of functions etc
- Definition Classes
- ExpressionEquationSolver
- lazy val initTermsSum: Sum
- Definition Classes
- ExpressionEquationSolver
- lazy val initVarGroups: Map[(RandomVar[_], Vector[_]), Set[Expression]]
- Definition Classes
- ExpressionEquationSolver
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def isleVar(el: Elem[_]): Boolean
identifying an isle variable by having an initial value, but one that is not part of the initial distribution
identifying an isle variable by having an initial value, but one that is not part of the initial distribution
- el
the element to decide
- returns
whether the element is an isle-var
- Definition Classes
- ExpressionEquationSolver
- def iterant(hW: Double = 1, klW: Double = 1, p: Map[Expression, Double] = finalDist): Iterant[Task, Map[Expression, Double]]
- Definition Classes
- ExpressionEquationSolver
- def iterator(hW: Double = 1, klW: Double = 1, p: Map[Expression, Double] = finalDist): Iterator[Map[Expression, Double]]
- Definition Classes
- ExpressionEquationSolver
- implicit lazy val jetField: Field[Jet[Double]]
- Definition Classes
- ExpressionEquationSolver
- lazy val keys: Vector[Expression]
- Definition Classes
- ExpressionEquationSolver
- lazy val klExp: Expression
Expression for Kullback-Liebler divergence of proofs from statements of theorems.
Expression for Kullback-Liebler divergence of proofs from statements of theorems.
- Definition Classes
- ExpressionEquationSolver
- def lambdaExportEquations(variable: Term): Set[Equation]
- Definition Classes
- ExpressionEquationSolver
- def modify(initNew: Map[Expression, Double] = self.init, finalTypsNew: => FiniteDistribution[Typ[Term]] = self.finalTyps, equationsNew: Set[Equation] = self.equations, coeffvalNew: (Coeff[_]) => Option[Double] = self.coeffval, varWeightNew: Double, coeffsAsVarsNew: Boolean = self.coeffsAsVars, maxRatioNew: Double = self.maxRatio, resolutionNew: Double = self.resolution, scaleNew: Double = self.scale, smoothNew: Option[Double] = self.smoothing, exponentNew: Double = self.exponent, decayNew: Double = self.decay, maxTimeNew: Option[Long] = self.maxTime): ExpressionEquationSolver
modified copy
modified copy
- Definition Classes
- GenerateTyps → ExpressionEquationSolver
- val mvs: VectorSpace[Map[Expression, Double], Double]
- Definition Classes
- ExpressionEquationSolver
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def normalizedMap(p: Map[Expression, Double]): Map[Expression, Double]
- Definition Classes
- ExpressionEquationSolver
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def optimum(hW: Double = 1, klW: Double = 1, cutoff: Double, p: Map[Expression, Double] = finalDist, maxRatio: Double = 1.01): Map[Expression, Double]
Optimal value, more precisely stable under gradient flow.
Optimal value, more precisely stable under gradient flow.
- hW
entropy weight
- klW
Kullback-Liebler weight
- p
Initial distribution
- Definition Classes
- ExpressionEquationSolver
- def optimumTask(hW: Double = 1, klW: Double = 1, cutoff: Double, p: Map[Expression, Double] = finalDist, maxRatio: Double = 1.01): Task[Map[Expression, Double]]
- Definition Classes
- ExpressionEquationSolver
- def piExportEquations(variable: Term): Set[Equation]
- Definition Classes
- ExpressionEquationSolver
- def piTermExportEquations(variable: Term): Set[Equation]
- Definition Classes
- ExpressionEquationSolver
- def proofExpression(typ: Typ[Term]): Expression
- Definition Classes
- FixedProofs → ExpressionEquationSolver
- def relVariable(x: Term): ExpressionEquationSolver
- Definition Classes
- ExpressionEquationSolver
- def resolveOpt(exp: Expression): Option[Expression]
- Definition Classes
- ExpressionEquationSolver
- def rhs(exp: Expression): Expression
- Definition Classes
- ExpressionEquationSolver
- def setProofWeights(pm: Map[Typ[Term], Double]): ExpressionEquationSolver
- Definition Classes
- GenerateTyps
- def stableGradShift(p: Map[Expression, Double], t: Vector[Double], eps: Double = scale): Map[Expression, Double]
- Definition Classes
- ExpressionEquationSolver
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- lazy val thmProbsByStatement: Map[Typ[Term], Double]
- Definition Classes
- ExpressionEquationSolver
- lazy val thmSet: Set[Typ[Term]]
- Definition Classes
- ExpressionEquationSolver
- lazy val thmsByProof: Map[Typ[Term], Expression]
- Definition Classes
- ExpressionEquationSolver
- lazy val thmsByStatement: Map[Typ[Term], Expression]
- Definition Classes
- GenerateTyps → ExpressionEquationSolver
- def toString(): String
- Definition Classes
- AnyRef → Any
- lazy val typFamilyTotal: Expression
- Definition Classes
- ExpressionEquationSolver
- def unitJet(p: Map[Expression, Double], exp: Expression): Jet[Double]
- Definition Classes
- ExpressionEquationSolver
- lazy val unknownsExp: Option[Expression]
- Definition Classes
- ExpressionEquationSolver
- lazy val unknownsValue: Option[Double]
- Definition Classes
- ExpressionEquationSolver
- lazy val valueVars: Vector[Expression]
Vector of all variables.
Vector of all variables. This is frozen so that their indices can be used.
- Definition Classes
- ExpressionEquationSolver
- lazy val variableIndex: Map[Expression, Int]
- Definition Classes
- ExpressionEquationSolver
- lazy val vars: Vector[Expression]
- Definition Classes
- ExpressionEquationSolver
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
- def →[B](y: B): (FixedProofs, B)
- Implicit
- This member is added by an implicit conversion from FixedProofs toArrowAssoc[FixedProofs] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @deprecated
- Deprecated
(Since version 2.13.0) Use
->instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.