notebook.community

Edit and run

Refining till success or error; Modus Ponens

Here we illustrate running a sequence of tasks till either some criterion for success is met or we have an error (usually a timeout) or all tasks run with no success. Here we seek the statement of Modus Ponens, but with two types in the distribution.





In [1]:



    


import $cp.bin.`provingground-core-jvm-3d48753.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 [3]:



    


val A = "A" :: Type
val B = "B" :: Type
val MPAB = A ->: (A ->: B) ->: B



    


















    
Out[3]:








A: Typ[Term] = A
B: Typ[Term] = B
MPAB: FuncTyp[Term, Func[Func[Term, Term], Term]] = (A → ((A → B) → B))

















In [4]:



    


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



    


















    
Out[4]:








defined function lp

















In [5]:



    


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



    


















    
Out[5]:








defined function ns

















In [6]:



    


val bT = Utils.bestTask[(Int, TermState)]((1 to 30).map(ns), {case (_, s) => s.typs(MPAB) > 0} )



    


















    
Out[6]:








bT: monix.eval.Task[Option[(Int, TermState)]] = FlatMap(
  FlatMap(
    Map(
      Async(<function2>, false, true, true),
      ammonite.$sess.cmd4$Helper$$Lambda$2778/1910977826@51c7a9a1,
      0
    ),
    <function1>
  ),
  provingground.Utils$$$Lambda$2781/2106070045@69bca247
)

















In [7]:



    


import monix.execution.Scheduler.Implicits.global
val bF = bT.runToFuture



    


















    








import monix.execution.Scheduler.Implicits.global

bF: monix.execution.CancelableFuture[Option[(Int, TermState)]] = Success(
  Some(
    (
      1,
      TermState(
        FiniteDistribution(
          Vector(
            Weighted((@a : B) ↦ (@b : B) ↦ A, 5.282996737933199E-4),
            Weighted((@a : A) ↦ (@b : A) ↦ A, 5.282996737933199E-4),
            Weighted(A, 0.4128465718655667),
            Weighted(((@a_1 , @a_2) : B×A) ↦ B, 5.480350064350246E-4),
            Weighted((@a : B) ↦ (@b : B) ↦ @b, 6.468975597469228E-4),
            Weighted((@a : B) ↦ (@b : B) ↦ @a, 4.5282829182284584E-4),
            Weighted((@a : ((B → B) → B)) ↦ B, 9.133916773917078E-5),
            Weighted((@a : ((A → B) → B)) ↦ B, 9.133916773917078E-5),
            Weighted((@a : (B → B)) ↦ B, 9.394885824600418E-4),
            Weighted((@a : (A → B)) ↦ B, 9.394885824600418E-4),
            Weighted((@a : ((A → A) → B)) ↦ B, 9.133916773917078E-5),
            Weighted((@a : ((B → A) → B)) ↦ B, 9.133916773917078E-5),
            Weighted((@a : (A → (B → B))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (A → (A → B))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (B → (A → B))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (B → (B → B))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (A → (A → A))) ↦ B, 7.82907152050035E-5),
            Weighted((@a : (A → (B → A))) ↦ B, 7.82907152050035E-5),
            Weighted((@a : (B → (A → A))) ↦ B, 7.82907152050035E-5),
            Weighted((@a : (B → (B → A))) ↦ B, 7.82907152050035E-5),
            Weighted(((@a_1 , @a_2) : A×A) ↦ B, 5.480350064350246E-4),
            Weighted((@a : ((B → A) → A)) ↦ A, 9.133916773917078E-5),
            Weighted((@a : ((A → A) → A)) ↦ A, 9.133916773917078E-5),
            Weighted((@a : (A → A)) ↦ A, 9.394885824600418E-4),
            Weighted((@a : (B → A)) ↦ A, 9.394885824600418E-4),
            Weighted((@a : ((A → B) → A)) ↦ A, 9.133916773917078E-5),
            Weighted((@a : ((B → B) → A)) ↦ A, 9.133916773917078E-5),
            Weighted((@a : A) ↦ (@b : A) ↦ B, 5.282996737933199E-4),
            Weighted((@a : (A → (A → A))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (A → (B → A))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (B → (A → A))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (B → (B → A))) ↦ @a, 6.710632731857444E-5),
...

















In [8]:



    


bF.map(_.get._2.typs(MPAB))



    


















    








res7: monix.execution.CancelableFuture[Double] = Success(7.529314129678205E-5)

















In [9]:



    


val bT2 = Utils.bestTask[(Int, TermState)]((-5 to 25).map(ns), {case (_, s) => s.typs(MPAB) > 0} )



    


















    
Out[9]:








bT2: monix.eval.Task[Option[(Int, TermState)]] = FlatMap(
  FlatMap(
    Map(
      Async(<function2>, false, true, true),
      ammonite.$sess.cmd4$Helper$$Lambda$2778/1910977826@2981bfc0,
      0
    ),
    <function1>
  ),
  provingground.Utils$$$Lambda$2781/2106070045@658d4ed1
)

















In [10]:



    


val bF2 = bT2.runToFuture



    


















    








bF2: monix.execution.CancelableFuture[Option[(Int, TermState)]] = Success(
  Some(
    (
      1,
      TermState(
        FiniteDistribution(
          Vector(
            Weighted((@a : B) ↦ (@b : B) ↦ A, 5.282996737933199E-4),
            Weighted((@a : A) ↦ (@b : A) ↦ A, 5.282996737933199E-4),
            Weighted(A, 0.4128465718655667),
            Weighted(((@a_1 , @a_2) : B×A) ↦ B, 5.480350064350246E-4),
            Weighted((@a : B) ↦ (@b : B) ↦ @b, 6.468975597469228E-4),
            Weighted((@a : B) ↦ (@b : B) ↦ @a, 4.5282829182284584E-4),
            Weighted((@a : ((B → B) → B)) ↦ B, 9.133916773917078E-5),
            Weighted((@a : ((A → B) → B)) ↦ B, 9.133916773917078E-5),
            Weighted((@a : (B → B)) ↦ B, 9.394885824600418E-4),
            Weighted((@a : (A → B)) ↦ B, 9.394885824600418E-4),
            Weighted((@a : ((A → A) → B)) ↦ B, 9.133916773917078E-5),
            Weighted((@a : ((B → A) → B)) ↦ B, 9.133916773917078E-5),
            Weighted((@a : (A → (B → B))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (A → (A → B))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (B → (A → B))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (B → (B → B))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (A → (A → A))) ↦ B, 7.82907152050035E-5),
            Weighted((@a : (A → (B → A))) ↦ B, 7.82907152050035E-5),
            Weighted((@a : (B → (A → A))) ↦ B, 7.82907152050035E-5),
            Weighted((@a : (B → (B → A))) ↦ B, 7.82907152050035E-5),
            Weighted(((@a_1 , @a_2) : A×A) ↦ B, 5.480350064350246E-4),
            Weighted((@a : ((B → A) → A)) ↦ A, 9.133916773917078E-5),
            Weighted((@a : ((A → A) → A)) ↦ A, 9.133916773917078E-5),
            Weighted((@a : (A → A)) ↦ A, 9.394885824600418E-4),
            Weighted((@a : (B → A)) ↦ A, 9.394885824600418E-4),
            Weighted((@a : ((A → B) → A)) ↦ A, 9.133916773917078E-5),
            Weighted((@a : ((B → B) → A)) ↦ A, 9.133916773917078E-5),
            Weighted((@a : A) ↦ (@b : A) ↦ B, 5.282996737933199E-4),
            Weighted((@a : (A → (A → A))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (A → (B → A))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (B → (A → A))) ↦ @a, 6.710632731857444E-5),
            Weighted((@a : (B → (B → A))) ↦ @a, 6.710632731857444E-5),
...

Conclusions

  • Correctly ran until success, even when the success was not in the first step.
  • Huge speedup over running to the end
  • The desired form of Modus Ponens was found soon.

Content source: siddhartha-gadgil/ProvingGround

Similar notebooks:

notebook.community | gallery | about