Packages

trait ExpressionEquationSolver extends AnyRef

Solve equations based on expressions (approximately), and compute various related quantities The actual solving is done after translating the equations to ones based on indices, for the sake of efficiency. Other methods let one construct new expression-equation-solvers, including by export.

Self Type
ExpressionEquationSolver
Linear Supertypes
AnyRef, Any
Known Subclasses
FixedProofs, GenerateTyps
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ExpressionEquationSolver
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. case class FixedExpressionProbs(p: Map[Expression, Double]) extends Product with Serializable

Abstract Value Members

  1. abstract val coeffsAsVars: Boolean
  2. abstract val coeffval: (Coeff[_]) => Option[Double]
  3. abstract val decay: Double
  4. abstract val equations: Set[Equation]
  5. abstract val exponent: Double
  6. abstract val finalTyps: FiniteDistribution[Typ[Term]]
  7. abstract val init: Map[Expression, Double]
  8. abstract val maxRatio: Double
  9. abstract val maxTime: Option[Long]
  10. abstract val previousMap: Option[Map[Expression, Double]]
  11. abstract val resolution: Double
  12. abstract val scale: Double
  13. abstract val smoothing: Option[Double]
  14. abstract val varWeight: Double

Concrete Value Members

  1. lazy val Final: FixedExpressionProbs
  2. lazy val atoms: Set[Expression]

    the atomic expressions in the equations

  3. 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

  4. lazy val coefficients: Vector[Coeff[_]]
  5. implicit lazy val dim: JetDim
  6. def entropy(hW: Double = 1, klW: Double = 1): Expression

    Expression for composite entropy.

  7. lazy val eqnExpressions: Vector[Expression]

    Expressions for equations.

  8. def expressionGroup(exp: Expression): Option[Set[Expression]]
  9. lazy val finalDist: Map[Expression, Double]

    The final distributions, obtained from the initial one by finding an almost solution.

  10. lazy val finalTermEntropy: Expression
  11. lazy val finalTermMap: Map[Term, Expression]
  12. 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

  13. lazy val finalTermSetSum: Sum
  14. 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

  15. lazy val finalTerms: FiniteDistribution[Term]

    final distribution on terms

  16. lazy val finalTypEntropy: Expression
  17. lazy val finalTypMap: Map[Term, Expression]
  18. 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

  19. lazy val finalVarGroups: Map[(RandomVar[_], Vector[_]), Set[Expression]]
  20. def fixTypes: ExpressionEquationSolver

    undoing generation of types by freezing them

  21. def flattenedEntropy(pow: Double, hW: Double = 1, klW: Double = 1): Expression
  22. def flattenedKLExp(pow: Double): Expression
  23. 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]]
  24. lazy val funcTotal: Expression
  25. lazy val genTerms: Map[Term, Expression]

    Terms of the generating distribution

  26. def generateTyps: ExpressionEquationSolver

    copy with types generated from equations

  27. def generatorIterant(hW: Double = 1, klW: Double = 1, cutoff: Double, p: Map[Expression, Double] = finalDist): Iterant[Task, FiniteDistribution[Term]]
  28. def gradShift(p: Map[Expression, Double], t: Vector[Double], eps: Double = scale): Map[Expression, Double]

    Shift downwards by the gradient, mapped by sigmoids.

  29. lazy val hExp: Expression

    Expression for entropy of the generating distribution

  30. def indepEquations(variable: Term): Set[Equation]

    equations not depending on a variable, to be used with boats

  31. 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

  32. lazy val initTerms: Vector[Term]

    Terms in the initial distributions, used to calculate total weights of functions etc

  33. lazy val initTermsSum: Sum
  34. lazy val initVarGroups: Map[(RandomVar[_], Vector[_]), Set[Expression]]
  35. 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

  36. def iterant(hW: Double = 1, klW: Double = 1, p: Map[Expression, Double] = finalDist): Iterant[Task, Map[Expression, Double]]
  37. def iterator(hW: Double = 1, klW: Double = 1, p: Map[Expression, Double] = finalDist): Iterator[Map[Expression, Double]]
  38. implicit lazy val jetField: Field[Jet[Double]]
  39. lazy val keys: Vector[Expression]
  40. lazy val klExp: Expression

    Expression for Kullback-Liebler divergence of proofs from statements of theorems.

  41. def lambdaExportEquations(variable: Term): Set[Equation]
  42. 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 = self.varWeight, 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

  43. val mvs: VectorSpace[Map[Expression, Double], Double]
  44. def normalizedMap(p: Map[Expression, Double]): Map[Expression, Double]
  45. 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

  46. def optimumTask(hW: Double = 1, klW: Double = 1, cutoff: Double, p: Map[Expression, Double] = finalDist, maxRatio: Double = 1.01): Task[Map[Expression, Double]]
  47. def piExportEquations(variable: Term): Set[Equation]
  48. def piTermExportEquations(variable: Term): Set[Equation]
  49. def proofExpression(typ: Typ[Term]): Expression
  50. def relVariable(x: Term): ExpressionEquationSolver
  51. def resolveOpt(exp: Expression): Option[Expression]
  52. def rhs(exp: Expression): Expression
  53. def stableGradShift(p: Map[Expression, Double], t: Vector[Double], eps: Double = scale): Map[Expression, Double]
  54. lazy val thmProbsByStatement: Map[Typ[Term], Double]
  55. lazy val thmSet: Set[Typ[Term]]
  56. lazy val thmsByProof: Map[Typ[Term], Expression]
  57. lazy val thmsByStatement: Map[Typ[Term], Expression]
  58. lazy val typFamilyTotal: Expression
  59. def unitJet(p: Map[Expression, Double], exp: Expression): Jet[Double]
  60. lazy val unknownsExp: Option[Expression]
  61. lazy val unknownsValue: Option[Double]
  62. lazy val valueVars: Vector[Expression]

    Vector of all variables.

    Vector of all variables. This is frozen so that their indices can be used.

  63. lazy val variableIndex: Map[Expression, Int]
  64. lazy val vars: Vector[Expression]