Generating and merging with equations.

Here we test generating final states with equations, including after merging equations from different local provers.

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]:
import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._
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]:
M: Typ[Term] = M
eqM: Func[Term, Func[Term, Typ[Term]]] = eqM
mul: Func[Term, Func[Term, Term]] = mul
m: Term = m
n: Term = n
sym: FuncLike[Term, FuncLike[Term, Func[Term, Term]]] = sym
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]:
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(M, 0.16666666666666666),
      Weighted(eqM, 0.16666666666666666),
      Weighted(m, 0.16666666666666666),
      Weighted(sym, 0.16666666666666666),
      Weighted(n, 0.16666666666666666),
      Weighted(mul, 0.16666666666666666)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted((M → (M → M)), 0.2),
      Weighted(∏(m : M){ ∏(n : M){ (eqM(m)(n) → eqM(n)(m)) } }, 0.2),
      Weighted(M, 0.2),
      Weighted((M → (M → 𝒰 )), 0.2),
      Weighted(𝒰 , 0.2)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
In [4]:
val lp = LocalProver(ts, decay = 0.95).noIsles
Out[4]:
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(M, 0.16666666666666666),
        Weighted(eqM, 0.16666666666666666),
        Weighted(m, 0.16666666666666666),
        Weighted(sym, 0.16666666666666666),
        Weighted(n, 0.16666666666666666),
        Weighted(mul, 0.16666666666666666)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted((M → (M → M)), 0.2),
        Weighted(∏(m : M){ ∏(n : M){ (eqM(m)(n) → eqM(n)(m)) } }, 0.2),
        Weighted(M, 0.2),
        Weighted((M → (M → 𝒰 )), 0.2),
        Weighted(𝒰 , 0.2)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.0,
    0.0,
    0.05,
    0.05,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
...
In [5]:
val nsT = lp.nextState.memoize
val evT = lp.expressionEval.memoize
Out[5]:
nsT: monix.eval.Task[TermState] = Async(<function2>, false, true, true)
evT: monix.eval.Task[ExpressionEval] = Async(<function2>, false, true, true)
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]:
terms1T: monix.eval.Task[FiniteDistribution[Term]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd7$Helper$$Lambda$3040/1707851184@4755d740,
  0
)
terms2T: monix.eval.Task[FiniteDistribution[Term]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd7$Helper$$Lambda$3041/453147566@49957982,
  0
)
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]:
suppDiffT: monix.eval.Task[(Set[Term], Set[Term])] = FlatMap(
  Map(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd7$Helper$$Lambda$3040/1707851184@4755d740,
    0
  ),
  ammonite.$sess.cmd10$Helper$$Lambda$3125/752953176@303b22e7
)
In [12]:
suppDiffT.runToFuture

First check

The same terms are generated using equations as those in the final distribution. Also (at least with decay) we get the result fairly quickly.

The next step will be to combine with equations from a more focussed generator and check supports.

In [13]:
val ts1 = TermState(FiniteDistribution.unif(mul, m, n), FiniteDistribution.unif(M, Type, mul.typ))
Out[13]:
ts1: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(mul, 0.3333333333333333),
      Weighted(m, 0.3333333333333333),
      Weighted(n, 0.3333333333333333)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.3333333333333333),
      Weighted(𝒰 , 0.3333333333333333),
      Weighted((M → (M → M)), 0.3333333333333333)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
In [17]:
val lp1 = LocalProver(ts1).noIsles.sharpen(10)
Out[17]:
lp1: LocalProverStep = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(mul, 0.3333333333333333),
        Weighted(m, 0.3333333333333333),
        Weighted(n, 0.3333333333333333)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.3333333333333333),
        Weighted(𝒰 , 0.3333333333333333),
        Weighted((M → (M → M)), 0.3333333333333333)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.0,
    0.0,
    0.05,
    0.05,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
...
In [18]:
val terms3T = lp1.nextState.map(_.terms).memoize
Out[18]:
terms3T: monix.eval.Task[FiniteDistribution[Term]] = Async(
  <function2>,
  false,
  true,
  true
)
In [19]:
terms3T.runToFuture
In [23]:
val diff3T = for {
    t3 <- terms3T
    t1 <- terms1T
} yield t3.pmf.find(wt => t1(wt.elem) == 0)
Out[23]:
diff3T: monix.eval.Task[Option[Weighted[Term]]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd22$Helper$$Lambda$3200/829051717@7247f343
)
In [24]:
val diff3F = diff3T.runToFuture
In [26]:
val eqs3T = lp1.equations.memoize
Out[26]:
eqs3T: monix.eval.Task[Set[Equation]] = Async(<function2>, false, true, true)
In [27]:
eqs3T.runToFuture
In [29]:
val eqs1T = lp.equations.memoize
Out[29]:
eqs1T: monix.eval.Task[Set[Equation]] = Async(<function2>, false, true, true)
In [30]:
val eqs1F = eqs1T.runToFuture
In [32]:
val eqsT = (for {
    eq1 <- eqs1T
    eq3 <- eqs3T
} yield Equation.merge(eq1, eq3)).memoize
Out[32]:
eqsT: monix.eval.Task[Set[Equation]] = Async(<function2>, false, true, true)
In [33]:
eqsT.runToFuture
In [36]:
val evMergeT = eqsT.map(eqs => ExpressionEval.fromInitEqs(ts, eqs, lp.tg, decayS = 0.95)).memoize
Out[36]:
evMergeT: monix.eval.Task[ExpressionEval] = Async(
  <function2>,
  false,
  true,
  true
)
In [37]:
val termsMergeT = evMergeT.map(_.finalTerms).memoize
Out[37]:
termsMergeT: monix.eval.Task[FiniteDistribution[Term]] = Async(
  <function2>,
  false,
  true,
  true
)
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]:
diffMergeT: monix.eval.Task[Option[Weighted[Term]]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd38$Helper$$Lambda$3311/1463157090@1b3afb28
)
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]:
diffMerge3T: monix.eval.Task[Option[Weighted[Term]]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd40$Helper$$Lambda$3324/2061589917@36d6df15
)
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]:
diff3MergeT: monix.eval.Task[Option[Weighted[Term]]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd42$Helper$$Lambda$3337/1829852448@7732ad90
)
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]:
diff1MergeT: monix.eval.Task[Option[Weighted[Term]]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd44$Helper$$Lambda$3350/314613443@70c67797
)
In [46]:
val dM1F = diff1MergeT.runToFuture

Conclusions

  • The combining of equations was successful, with both sets of terms generated.
  • The time to run (at least with decay) was reasonable.