notebook.community

Edit and run

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.

Content source: siddhartha-gadgil/ProvingGround

Similar notebooks:

notebook.community | gallery | about