In [1]:
import $cp.bin.`provingground-core-jvm-0b2e2155ea.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
Out[1]:
In [2]:
val M = "M" :: Type
val eqM = "eqM" :: M ->: M ->: Type
val mul = "mul" :: M ->: M ->: M
val m = "m" :: M
val n = "n" :: M
val sym = "sym" :: m ~>: (n ~>: (eqM(m)(n) ->: eqM(n)(m)))
Out[2]:
In [3]:
val ts = TermState(FiniteDistribution.unif(M, eqM, mul, m, n, sym), FiniteDistribution.unif(M, Type, eqM.typ, mul.typ, sym.typ))
Out[3]:
In [4]:
val lp = LocalProver(ts, decay = 0.95).noIsles
Out[4]:
In [5]:
val nsT = lp.nextState.memoize
val evT = lp.expressionEval.memoize
Out[5]:
In [6]:
import monix.execution.Scheduler.Implicits.global
val nsF = nsT.runToFuture
In [7]:
evT.map(_.decay).runToFuture
In [8]:
val terms1T = nsT.map(_.terms)
val terms2T = evT.map(_.finalTerms)
Out[8]:
In [9]:
terms1T.map(_.entropyVec).runToFuture
In [10]:
terms2T.map(_.entropyVec).runToFuture
In [11]:
val suppDiffT =
for {
t1 <- terms1T
t2 <- terms2T
} yield (t1.support -- t2.support, t2.support -- t1.support)
Out[11]:
In [12]:
suppDiffT.runToFuture
In [13]:
val ts1 = TermState(FiniteDistribution.unif(mul, m, n), FiniteDistribution.unif(M, Type, mul.typ))
Out[13]:
In [17]:
val lp1 = LocalProver(ts1).noIsles.sharpen(10)
Out[17]:
In [18]:
val terms3T = lp1.nextState.map(_.terms).memoize
Out[18]:
In [19]:
terms3T.runToFuture
In [23]:
val diff3T = for {
t3 <- terms3T
t1 <- terms1T
} yield t3.pmf.find(wt => t1(wt.elem) == 0)
Out[23]:
In [24]:
val diff3F = diff3T.runToFuture
In [26]:
val eqs3T = lp1.equations.memoize
Out[26]:
In [27]:
eqs3T.runToFuture
In [29]:
val eqs1T = lp.equations.memoize
Out[29]:
In [30]:
val eqs1F = eqs1T.runToFuture
In [32]:
val eqsT = (for {
eq1 <- eqs1T
eq3 <- eqs3T
} yield Equation.merge(eq1, eq3)).memoize
Out[32]:
In [33]:
eqsT.runToFuture
In [36]:
val evMergeT = eqsT.map(eqs => ExpressionEval.fromInitEqs(ts, eqs, lp.tg, decayS = 0.95)).memoize
Out[36]:
In [37]:
val termsMergeT = evMergeT.map(_.finalTerms).memoize
Out[37]:
In [38]:
val tmF = termsMergeT.runToFuture
In [39]:
val diffMergeT = for {
tM <- termsMergeT
t1 <- terms1T
} yield tM.pmf.find(wt => t1(wt.elem) == 0)
Out[39]:
In [40]:
val dF = diffMergeT.runToFuture
In [41]:
val diffMerge3T = for {
tM <- termsMergeT
t3 <- terms3T
} yield tM.pmf.find(wt => t3(wt.elem) == 0)
Out[41]:
In [42]:
val d3F = diffMerge3T.runToFuture
In [43]:
val diff3MergeT = for {
tM <- termsMergeT
t3 <- terms3T
} yield t3.pmf.find(wt => tM(wt.elem) == 0)
Out[43]:
In [44]:
val dM3F = diff3MergeT.runToFuture
In [45]:
val diff1MergeT = for {
tM <- termsMergeT
t1 <- terms1T
} yield t1.pmf.find(wt => tM(wt.elem) == 0)
Out[45]:
In [46]:
val dM1F = diff1MergeT.runToFuture