notebook.community

Edit and run

Generating with successive refinements

The goal is to keep generating distributions from just Type, Zero, One and Star till we timeout





InΒ [1]:



    


import $cp.bin.`provingground-core-jvm-09effc3.fat.jar`



    


















    
Out[1]:








import $cp.$                                           

















InΒ [2]:



    


import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}



    


















    
Out[2]:








import provingground._ , interface._, HoTT._, learning._ 


















InΒ [19]:



    


val terms = FiniteDistribution.unif[Term](Type, Unit, Zero, Star)
val typs = FiniteDistribution[Typ[Term]](Type -> 0.8, Unit -> 0.05, Zero -> 0.15)
val ts = TermState(terms, typs)



    


















    
Out[19]:








terms: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(𝒰 , 0.25),
    Weighted(Unit, 0.25),
    Weighted(Zero, 0.25),
    Weighted(Star, 0.25)
  )
)
typs: FiniteDistribution[Typ[Term]] = FiniteDistribution(
  Vector(Weighted(𝒰 , 0.8), Weighted(Unit, 0.05), Weighted(Zero, 0.15))
)
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.25),
      Weighted(Unit, 0.25),
      Weighted(Zero, 0.25),
      Weighted(Star, 0.25)
    )
  ),
  FiniteDistribution(
    Vector(Weighted(𝒰 , 0.8), Weighted(Unit, 0.05), Weighted(Zero, 0.15))
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)

















InΒ [20]:



    


import monix.execution.Scheduler.Implicits.global
def lp(n: Int) = LocalProver(ts).sharpen(math.pow(2, n))



    


















    
Out[20]:








import monix.execution.Scheduler.Implicits.global

defined function lp

















InΒ [21]:



    


def ns(n: Int) = lp(n).nextState.map{ns => n -> ns}



    


















    
Out[21]:








defined function ns

















InΒ [22]:



    


val bt = Utils.bestTask((1 to 30).map(ns))



    


















    
Out[22]:








bt: monix.eval.Task[Option[(Int, TermState)]] = FlatMap(
  FlatMap(
    Map(
      Async(<function2>, false, true, true),
      ammonite.$sess.cmd20$Helper$$Lambda$3316/1857030182@487cdc04,
      0
    ),
    <function1>
  ),
  provingground.Utils$$$Lambda$2797/1331520012@313b87a8
)

















InΒ [23]:



    


val bf = bt.runToFuture



    


















    























InΒ [24]:



    


val A = "A" :: Type
val tsT = bt.map(_.get._2)



    


















    
Out[24]:








A: Typ[Term] = A
tsT: monix.eval.Task[TermState] = Map(
  FlatMap(
    FlatMap(
      Map(
        Async(<function2>, false, true, true),
        ammonite.$sess.cmd20$Helper$$Lambda$3316/1857030182@487cdc04,
        0
      ),
      <function1>
    ),
    provingground.Utils$$$Lambda$2797/1331520012@313b87a8
  ),
  ammonite.$sess.cmd23$Helper$$Lambda$3327/584491755@78827119,
  0
)

















InΒ [25]:



    


val typT = tsT.map(_.typs)



    


















    
Out[25]:








typT: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Map(
  FlatMap(
    FlatMap(
      Map(
        Async(<function2>, false, true, true),
        ammonite.$sess.cmd20$Helper$$Lambda$3316/1857030182@487cdc04,
        0
      ),
      <function1>
    ),
    provingground.Utils$$$Lambda$2797/1331520012@313b87a8
  ),
  scala.Function1$$Lambda$275/1928301845@cf5ea27,
  1
)

















InΒ [26]:



    


val tpEntF = typT.map(_.entropyVec).runToFuture



    


















    























InΒ [27]:



    


val B = "B" :: Type
val MP = A ~>: (B ~>: (A ->: (A ->: B) ->: B))



    


















    
Out[27]:








B: Typ[Term] = B
MP: GenFuncTyp[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A β†’ ((A β†’ B) β†’ B)) } }

















InΒ [28]:



    


typT.map(_(MP)).runToFuture



    


















    























InΒ [29]:



    


val idTyp = A ~>: (A ->: A)
typT.map(_(idTyp)).runToFuture

Conclusions

  • Repeated running of tasks is okay.
  • However, we see single shot generation is pretty weak.




InΒ [30]:



    


def lp1(n: Int) = LocalProver(TermState(FiniteDistribution.unif(A, B), FiniteDistribution.unif(A, B))).sharpen(math.pow(2, n))



    


















    
Out[30]:








defined function lp1

















InΒ [31]:



    


def ns1(n: Int) = lp1(n).nextState.map{ns => n -> ns}



    


















    
Out[31]:








defined function ns1

















InΒ [41]:



    


val bT1 = Utils.bestTask((1 to 30).map(ns1))



    


















    
Out[41]:








bT1: monix.eval.Task[Option[(Int, TermState)]] = FlatMap(
  FlatMap(
    Map(
      Async(<function2>, false, true, true),
      ammonite.$sess.cmd30$Helper$$Lambda$3446/1142216442@2a9f3987,
      0
    ),
    <function1>
  ),
  provingground.Utils$$$Lambda$2797/1331520012@786eee75
)

















InΒ [42]:



    


val bF1 = bT1.runToFuture



    


















    























InΒ [43]:



    


val mp1T = bT1.map(_.get._2.typs(A ->: (A ->: B) ->: B))



    


















    
Out[43]:








mp1T: monix.eval.Task[Double] = Map(
  FlatMap(
    FlatMap(
      Map(
        Async(<function2>, false, true, true),
        ammonite.$sess.cmd30$Helper$$Lambda$3446/1142216442@2a9f3987,
        0
      ),
      <function1>
    ),
    provingground.Utils$$$Lambda$2797/1331520012@786eee75
  ),
  ammonite.$sess.cmd42$Helper$$Lambda$3457/424448485@f71aa6e,
  0
)

















InΒ [44]:



    


val mp1F = mp1T.runToFuture



    


















    























InΒ [45]:



    


val typs1T = bT1.map(_.get._2.typs)



    


















    
Out[45]:








typs1T: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Map(
  FlatMap(
    FlatMap(
      Map(
        Async(<function2>, false, true, true),
        ammonite.$sess.cmd30$Helper$$Lambda$3446/1142216442@2a9f3987,
        0
      ),
      <function1>
    ),
    provingground.Utils$$$Lambda$2797/1331520012@786eee75
  ),
  ammonite.$sess.cmd44$Helper$$Lambda$3464/1416231077@4a8a7522,
  0
)

















InΒ [46]:



    


typs1T.map(_(A ->: B)).runToFuture

Conclusion 2

When we had variables $A$ and $B$ this did discover Modus Ponens (though it took a long time to run as it ran through 12 steps).

Content source: siddhartha-gadgil/ProvingGround

Similar notebooks:

notebook.community | gallery | about