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.