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. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def +(other: String): String
    Implicit
    This member is added by an implicit conversion from TheoremFeedback toany2stringadd[TheoremFeedback] performed by method any2stringadd in scala.Predef.
    Definition Classes
    any2stringadd
  4. def ->[B](y: B): (TheoremFeedback, B)
    Implicit
    This member is added by an implicit conversion from TheoremFeedback toArrowAssoc[TheoremFeedback] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @inline()
  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. lazy val byProof: FiniteDistribution[Typ[Term]]

    distribution of theorems (inhabited types) weighted by proofs.

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

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

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

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

  10. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
  11. def ensuring(cond: (TheoremFeedback) => Boolean, msg: => Any): TheoremFeedback
    Implicit
    This member is added by an implicit conversion from TheoremFeedback toEnsuring[TheoremFeedback] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  12. def ensuring(cond: (TheoremFeedback) => Boolean): TheoremFeedback
    Implicit
    This member is added by an implicit conversion from TheoremFeedback toEnsuring[TheoremFeedback] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  13. def ensuring(cond: Boolean, msg: => Any): TheoremFeedback
    Implicit
    This member is added by an implicit conversion from TheoremFeedback toEnsuring[TheoremFeedback] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  14. def ensuring(cond: Boolean): TheoremFeedback
    Implicit
    This member is added by an implicit conversion from TheoremFeedback toEnsuring[TheoremFeedback] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  15. 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
  16. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. val fd: FiniteDistribution[Term]
  18. def feedbackFunction(x: Typ[Term]): Double

    term-type map feedback as function of type

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

    term-type map feedback map ie feedbackVec as a map

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

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

    feedback as function of distribution on types

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

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

  23. def formatted(fmtstr: String): String
    Implicit
    This member is added by an implicit conversion from TheoremFeedback toStringFormat[TheoremFeedback] performed by method StringFormat in scala.Predef.
    Definition Classes
    StringFormat
    Annotations
    @inline()
  24. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  25. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  26. lazy val lfd: FiniteDistribution[Term]

    terms mapped to lambdas with resepect to the variables

  27. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  28. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  29. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  30. lazy val pfd: FiniteDistribution[Typ[Term]]

    types mapped to pis with respect to the variables.

  31. def productElementNames: Iterator[String]
    Definition Classes
    Product
  32. val scale: Double
  33. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  34. val tfd: FiniteDistribution[Typ[Term]]
  35. def thmFeedbackFunction(x: Term): Double

    feedback based on total weight of theorems

  36. val thmScale: Double
  37. lazy val thmSet: Set[Typ[Term]]

    set of theorems

  38. lazy val thmShift: Double

    amount to shift to ensure theorems have a minimum total weight

  39. val thmTarget: Double
  40. lazy val thmTotal: Double

    total weight of theorems

  41. val vars: Vector[Term]
  42. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  43. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  44. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated
  2. def [B](y: B): (TheoremFeedback, B)
    Implicit
    This member is added by an implicit conversion from TheoremFeedback toArrowAssoc[TheoremFeedback] 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.

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from AnyRef

Inherited from Any

Inherited by implicit conversion any2stringadd fromTheoremFeedback to any2stringadd[TheoremFeedback]

Inherited by implicit conversion StringFormat fromTheoremFeedback to StringFormat[TheoremFeedback]

Inherited by implicit conversion Ensuring fromTheoremFeedback to Ensuring[TheoremFeedback]

Inherited by implicit conversion ArrowAssoc fromTheoremFeedback to ArrowAssoc[TheoremFeedback]

Ungrouped