Packages

c

provingground.learning

TheoremFeedback

case class TheoremFeedback(fd: FiniteDistribution[Term], tfd: FiniteDistribution[Typ[Term]], vars: Vector[Term] = Vector(), scale: Double = 1.0, thmScale: Double = 0.3, thmTarget: Double = 0.2) extends Product with Serializable

feedback based on the term-type map as well as ensuring total weight of theorems is not small; various steps are explicit for exploration and debugging

Linear Supertypes
Serializable, Product, Equals, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TheoremFeedback
  2. Serializable
  3. Product
  4. Equals
  5. AnyRef
  6. 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

Instance Constructors

  1. new TheoremFeedback(fd: FiniteDistribution[Term], tfd: FiniteDistribution[Typ[Term]], vars: Vector[Term] = Vector(), scale: Double = 1.0, thmScale: Double = 0.3, thmTarget: Double = 0.2)

Value Members

  1. lazy val byProof: FiniteDistribution[Typ[Term]]

    distribution of theorems (inhabited types) weighted by proofs.

  2. lazy val byStatement: FiniteDistribution[Typ[Term]]

    distribution of theorems (inhabited types) weighted as in the type distribution and normalized.

  3. lazy val byStatementUnscaled: FiniteDistribution[Typ[Term]]

    distribution of theorems (inhabited types) weighted as in the type distribution, not normalized.

  4. lazy val entropyPairs: Vector[(Typ[Term], (Double, Double))]

    for each theorem, the pair of entropies with respect to the distribution

    for each theorem, the pair of entropies with respect to the distribution

    • as statement weight
    • as proof weight
  5. val fd: FiniteDistribution[Term]
  6. def feedbackFunction(x: Typ[Term]): Double

    term-type map feedback as function of type

  7. lazy val feedbackMap: Map[Typ[Term], Double]

    term-type map feedback map ie feedbackVec as a map

  8. def feedbackTermDist(fd: FiniteDistribution[Term], typfd: FiniteDistribution[Typ[Term]]): Double

    feedback based on distributions on terms and on types, by backward propagation from feedbackTypDist and thmFeedbackFunction

  9. def feedbackTypDist(fd: FiniteDistribution[Typ[Term]]): Double

    feedback as function of distribution on types

  10. lazy val feedbackVec: Vector[(Typ[Term], Double)]

    term-type map feedback vector with entries pairs (typ, p)

  11. lazy val lfd: FiniteDistribution[Term]

    terms mapped to lambdas with resepect to the variables

  12. lazy val pfd: FiniteDistribution[Typ[Term]]

    types mapped to pis with respect to the variables.

  13. def productElementNames: Iterator[String]
    Definition Classes
    Product
  14. val scale: Double
  15. val tfd: FiniteDistribution[Typ[Term]]
  16. def thmFeedbackFunction(x: Term): Double

    feedback based on total weight of theorems

  17. val thmScale: Double
  18. lazy val thmSet: Set[Typ[Term]]

    set of theorems

  19. lazy val thmShift: Double

    amount to shift to ensure theorems have a minimum total weight

  20. val thmTarget: Double
  21. lazy val thmTotal: Double

    total weight of theorems

  22. val vars: Vector[Term]