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.