Packages

  • package root
    Definition Classes
    root
  • package provingground

    This is work towards automated theorem proving based on learning, using homotopy type theory (HoTT) as foundations and natural language processing.

    This is work towards automated theorem proving based on learning, using homotopy type theory (HoTT) as foundations and natural language processing.

    The implementation of homotopy type theory is split into:

    • the object HoTT with terms, types, functions and dependent functions, pairs etc
    • the package induction with general inductive types and recursion/induction on these.

    The learning package has the code for learning.

    Scala code, including the spire library, is integrated with homotopy type theory in the scalahott package

    We have implemented a functor based approach to translation in the translation package, used for nlp as well as serialization and parsing.

    The library package is contains basic structures implemented in HoTT.

    Definition Classes
    root
  • package learning
    Definition Classes
    provingground
  • object ExpressionEquationSolver

    Working with expressions built from initial and final values of random variables, including in islands, given equations satisfied by these

    Working with expressions built from initial and final values of random variables, including in islands, given equations satisfied by these

    Definition Classes
    learning
  • FixedProofs
  • GenerateTyps

trait GenerateTyps extends ExpressionEquationSolver

ExpressionEquationSolver where the type distribution is generated from the equations

Self Type
GenerateTyps
Linear Supertypes
Known Subclasses
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. GenerateTyps
  2. ExpressionEquationSolver
  3. AnyRef
  4. 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
    Definition Classes
    ExpressionEquationSolver

Abstract Value Members

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

Concrete 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 GenerateTyps toany2stringadd[GenerateTyps] performed by method any2stringadd in scala.Predef.
    Definition Classes
    any2stringadd
  4. def ->[B](y: B): (GenerateTyps, B)
    Implicit
    This member is added by an implicit conversion from GenerateTyps toArrowAssoc[GenerateTyps] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @inline()
  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. lazy val Final: FixedExpressionProbs
    Definition Classes
    ExpressionEquationSolver
  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. lazy val atoms: Set[Expression]

    the atomic expressions in the equations

    the atomic expressions in the equations

    Definition Classes
    ExpressionEquationSolver
  9. 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
  10. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
  11. lazy val coefficients: Vector[Coeff[_]]
    Definition Classes
    ExpressionEquationSolver
  12. implicit lazy val dim: JetDim
    Definition Classes
    ExpressionEquationSolver
  13. def ensuring(cond: (GenerateTyps) => Boolean, msg: => Any): GenerateTyps
    Implicit
    This member is added by an implicit conversion from GenerateTyps toEnsuring[GenerateTyps] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  14. def ensuring(cond: (GenerateTyps) => Boolean): GenerateTyps
    Implicit
    This member is added by an implicit conversion from GenerateTyps toEnsuring[GenerateTyps] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  15. def ensuring(cond: Boolean, msg: => Any): GenerateTyps
    Implicit
    This member is added by an implicit conversion from GenerateTyps toEnsuring[GenerateTyps] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  16. def ensuring(cond: Boolean): GenerateTyps
    Implicit
    This member is added by an implicit conversion from GenerateTyps toEnsuring[GenerateTyps] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  17. def entropy(hW: Double = 1, klW: Double = 1): Expression

    Expression for composite entropy.

    Expression for composite entropy.

    Definition Classes
    ExpressionEquationSolver
  18. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. lazy val eqnExpressions: Vector[Expression]

    Expressions for equations.

    Expressions for equations.

    Definition Classes
    ExpressionEquationSolver
  20. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  21. def expressionGroup(exp: Expression): Option[Set[Expression]]
    Definition Classes
    ExpressionEquationSolver
  22. 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
  23. lazy val finalTermEntropy: Expression
    Definition Classes
    ExpressionEquationSolver
  24. lazy val finalTermMap: Map[Term, Expression]
    Definition Classes
    ExpressionEquationSolver
  25. 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
  26. lazy val finalTermSetSum: Sum
    Definition Classes
    ExpressionEquationSolver
  27. 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
  28. lazy val finalTerms: FiniteDistribution[Term]

    final distribution on terms

    final distribution on terms

    Definition Classes
    ExpressionEquationSolver
  29. lazy val finalTypEntropy: Expression
    Definition Classes
    ExpressionEquationSolver
  30. lazy val finalTypMap: Map[Term, Expression]
    Definition Classes
    ExpressionEquationSolver
  31. 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
  32. lazy val finalTyps: FiniteDistribution[Typ[Term]]
  33. lazy val finalVarGroups: Map[(RandomVar[_], Vector[_]), Set[Expression]]
    Definition Classes
    ExpressionEquationSolver
  34. def fixTypes: ExpressionEquationSolver

    undoing generation of types by freezing them

    undoing generation of types by freezing them

    Definition Classes
    ExpressionEquationSolver
  35. def flattenedEntropy(pow: Double, hW: Double = 1, klW: Double = 1): Expression
    Definition Classes
    ExpressionEquationSolver
  36. def flattenedKLExp(pow: Double): Expression
    Definition Classes
    ExpressionEquationSolver
  37. 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
  38. def formatted(fmtstr: String): String
    Implicit
    This member is added by an implicit conversion from GenerateTyps toStringFormat[GenerateTyps] performed by method StringFormat in scala.Predef.
    Definition Classes
    StringFormat
    Annotations
    @inline()
  39. lazy val funcTotal: Expression
    Definition Classes
    ExpressionEquationSolver
  40. lazy val genTerms: Map[Term, Expression]

    Terms of the generating distribution

    Terms of the generating distribution

    Definition Classes
    ExpressionEquationSolver
  41. def generateTyps: ExpressionEquationSolver

    copy with types generated from equations

    copy with types generated from equations

    Definition Classes
    GenerateTypsExpressionEquationSolver
  42. def generatorIterant(hW: Double = 1, klW: Double = 1, cutoff: Double, p: Map[Expression, Double] = finalDist): Iterant[Task, FiniteDistribution[Term]]
    Definition Classes
    ExpressionEquationSolver
  43. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  44. 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
  45. lazy val hExp: Expression

    Expression for entropy of the generating distribution

    Expression for entropy of the generating distribution

    Definition Classes
    ExpressionEquationSolver
  46. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  47. 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
  48. 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
  49. 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
  50. lazy val initTermsSum: Sum
    Definition Classes
    ExpressionEquationSolver
  51. lazy val initVarGroups: Map[(RandomVar[_], Vector[_]), Set[Expression]]
    Definition Classes
    ExpressionEquationSolver
  52. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  53. 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
  54. def iterant(hW: Double = 1, klW: Double = 1, p: Map[Expression, Double] = finalDist): Iterant[Task, Map[Expression, Double]]
    Definition Classes
    ExpressionEquationSolver
  55. def iterator(hW: Double = 1, klW: Double = 1, p: Map[Expression, Double] = finalDist): Iterator[Map[Expression, Double]]
    Definition Classes
    ExpressionEquationSolver
  56. implicit lazy val jetField: Field[Jet[Double]]
    Definition Classes
    ExpressionEquationSolver
  57. lazy val keys: Vector[Expression]
    Definition Classes
    ExpressionEquationSolver
  58. 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
  59. def lambdaExportEquations(variable: Term): Set[Equation]
    Definition Classes
    ExpressionEquationSolver
  60. 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
    GenerateTypsExpressionEquationSolver
  61. val mvs: VectorSpace[Map[Expression, Double], Double]
    Definition Classes
    ExpressionEquationSolver
  62. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  63. def normalizedMap(p: Map[Expression, Double]): Map[Expression, Double]
    Definition Classes
    ExpressionEquationSolver
  64. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  65. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  66. 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
  67. 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
  68. def piExportEquations(variable: Term): Set[Equation]
    Definition Classes
    ExpressionEquationSolver
  69. def piTermExportEquations(variable: Term): Set[Equation]
    Definition Classes
    ExpressionEquationSolver
  70. def proofExpression(typ: Typ[Term]): Expression
    Definition Classes
    ExpressionEquationSolver
  71. def relVariable(x: Term): ExpressionEquationSolver
    Definition Classes
    ExpressionEquationSolver
  72. def resolveOpt(exp: Expression): Option[Expression]
    Definition Classes
    ExpressionEquationSolver
  73. def rhs(exp: Expression): Expression
    Definition Classes
    ExpressionEquationSolver
  74. def setProofWeights(pm: Map[Typ[Term], Double]): ExpressionEquationSolver
  75. def stableGradShift(p: Map[Expression, Double], t: Vector[Double], eps: Double = scale): Map[Expression, Double]
    Definition Classes
    ExpressionEquationSolver
  76. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  77. lazy val thmProbsByStatement: Map[Typ[Term], Double]
    Definition Classes
    ExpressionEquationSolver
  78. lazy val thmSet: Set[Typ[Term]]
    Definition Classes
    ExpressionEquationSolver
  79. lazy val thmsByProof: Map[Typ[Term], Expression]
    Definition Classes
    ExpressionEquationSolver
  80. lazy val thmsByStatement: Map[Typ[Term], Expression]
  81. def toString(): String
    Definition Classes
    AnyRef → Any
  82. lazy val typFamilyTotal: Expression
    Definition Classes
    ExpressionEquationSolver
  83. def unitJet(p: Map[Expression, Double], exp: Expression): Jet[Double]
    Definition Classes
    ExpressionEquationSolver
  84. lazy val unknownsExp: Option[Expression]
    Definition Classes
    ExpressionEquationSolver
  85. lazy val unknownsValue: Option[Double]
    Definition Classes
    ExpressionEquationSolver
  86. 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
  87. lazy val variableIndex: Map[Expression, Int]
    Definition Classes
    ExpressionEquationSolver
  88. lazy val vars: Vector[Expression]
    Definition Classes
    ExpressionEquationSolver
  89. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  90. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  91. 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): (GenerateTyps, B)
    Implicit
    This member is added by an implicit conversion from GenerateTyps toArrowAssoc[GenerateTyps] 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 AnyRef

Inherited from Any

Inherited by implicit conversion any2stringadd fromGenerateTyps to any2stringadd[GenerateTyps]

Inherited by implicit conversion StringFormat fromGenerateTyps to StringFormat[GenerateTyps]

Inherited by implicit conversion Ensuring fromGenerateTyps to Ensuring[GenerateTyps]

Inherited by implicit conversion ArrowAssoc fromGenerateTyps to ArrowAssoc[GenerateTyps]

Ungrouped