object ProverTasks
- Alphabetic
- By Inheritance
- ProverTasks
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- def branchedGatherTask[X, Y](tsk: Task[X], results: (Int) => (X) => Task[Y], combine: (Y, Y) => Y, spawn: (Int) => (X) => Task[Vector[Task[X]]], depth: Int = 0): Task[Y]
bread-first accumulation of results; a typical example is interesting proofs, with X finite-distributions of terms.
bread-first accumulation of results; a typical example is interesting proofs, with X finite-distributions of terms. each element of
Xcan spawn a vector of elements in which we also search. Everything is wrapped in tasks.- tsk
the initial element for the search
- results
the result, depending on an element of
X- also the depth, but this is used mainly for tracking.- spawn
new vectors in
Xspawned by an element inX, depeneding on the depth.- depth
the depth of the current recursive step.
- def breadthFirstTask[X, Y](tv: Task[Vector[Task[X]]], p: (X) => Option[Y], spawn: (Int) => (X) => Task[Vector[Task[X]]], depth: Int = 0): Task[Option[Y]]
bread-first search for an element in
Xsatisying a predicate-mapp; each element ofXcan spawn a vector of elements in which we also search.bread-first search for an element in
Xsatisying a predicate-mapp; each element ofXcan spawn a vector of elements in which we also search. Everything is wrapped in tasks.- tv
the initial vector in which we search
- p
the predicate to be satisfied + map; actually an optional map.
- spawn
new vectors in
Xspawned by an element inX, depeneding on the depth.- depth
the depth of the current recursive step.
- def h[A](fd: FiniteDistribution[A]): Double
- def h0(p: Double, q: Double): Double
An entropy measure for parsimonious generation of terms inhabiting types.
- def hExp(p: Double, q: Double, scale: Double): Double
Exponent of an entropy measure for parsimonious generation of terms inhabiting types; low values correspond to important terms, with the
scaleincreasing sensitivity. - def inTaskVecTask[X, Y](tv: Task[Vector[Task[X]]], p: (X) => Option[Y]): Task[Option[Y]]
Looks for an element satisfying a predicate in a vector of tasks.
Looks for an element satisfying a predicate in a vector of tasks.
- tv
task giving a vector of tasks giving elements of X.
- p
an optional map, ie predicate+map
- returns
task giving optional element satisying the predicate.
- def kl[A](p: FiniteDistribution[A], q: FiniteDistribution[A]): Double
- def minOn[A](fd: FiniteDistribution[A], minValue: Double, supp: Set[A]): FiniteDistribution[A]
- def newNeighbours[A](fd: FiniteDistribution[A], pert: Vector[A], epsilon: Double): Vector[FiniteDistribution[A]]
- def pfMatch(ev: (FiniteDistribution[Term]) => Task[FiniteDistribution[Term]], typs: Task[FiniteDistribution[Typ[Term]]], wt: Double = 1.0)(gen: FiniteDistribution[Term]): Task[Double]
- def pfMatchDiff(ev: (FiniteDistribution[Term]) => Task[FiniteDistribution[Term]], typs: Task[FiniteDistribution[Typ[Term]]], cutoff: Double, wt: Double = 1.0)(gen0: FiniteDistribution[Term], gen1: FiniteDistribution[Term]): Task[Double]
- def prsmEntMemoTask(termsTask: Task[FiniteDistribution[Term]], typsTask: Task[FiniteDistribution[Typ[Term]]], scale: Double, vars: Vector[Term] = Vector()): Task[(Vector[(Term, Double)], Set[Term], Set[Typ[Term]])]
task to find proofs that are useful based on parsimony, i.e., reducing relative entropy of the final result with a cost for the increase in entropy of the initial distribution.
task to find proofs that are useful based on parsimony, i.e., reducing relative entropy of the final result with a cost for the increase in entropy of the initial distribution. Also return terms and types
- termsTask
task for evolution of terms.
- typsTask
task for evolution of types.
- returns
task for proofs with, and sorted by, parsimonious entropies.
- def prsmEntTask(termsTask: Task[FiniteDistribution[Term]], typsTask: Task[FiniteDistribution[Typ[Term]]], scale: Double, vars: Vector[Term] = Vector()): Task[Vector[(Term, Double)]]
task to find proofs that are useful based on parsimony, i.e., reducing relative entropy of the final result with a cost for the increase in entropy of the initial distribution.
task to find proofs that are useful based on parsimony, i.e., reducing relative entropy of the final result with a cost for the increase in entropy of the initial distribution.
- termsTask
task for evolution of terms.
- typsTask
task for evolution of types.
- returns
task for proofs with, and sorted by, parsimonious entropies.
- def quasiGradFlowTask[A](base: A, neighMap: (A) => Vector[A], derTask: (A, A) => Task[Double], halt: (A, A) => Boolean)(implicit ls: VectorSpace[A, Double]): Task[A]
- def quasiGradShift[A](base: A, neighbours: Vector[A], derTask: (A, A) => Task[Double])(implicit ls: VectorSpace[A, Double]): Task[A]
- def selfNeighbours[A](fd: FiniteDistribution[A], epsilon: Double): Vector[FiniteDistribution[A]]
- def stabHalt(x: FiniteDistribution[Term], y: FiniteDistribution[Term], level: Double): Boolean