New Memoized Liberal goal chomping

  • We run a variant of the most basic strategic prover - a goal chomper that keeps trying a succession of goals.
  • The change from the first version are:
    • terms are remembered,
    • terms are looked up but with a map,
    • we do not evaluate equations to build the lookup table
    • negation is improved
  • Termination is when all goals are finished; with failures recorded.
  • Proving is only by generation, with the generation including backward reasoning rules.
In [1]:
import $cp.bin.`provingground-core-jvm-eb6940f0d5.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 terms = FiniteDistribution.unif[Term](Unit, Zero, Star)
val typs = FiniteDistribution.unif[Typ[Term]](Type, Unit, Zero)
val ts = TermState(terms, typs)
val ts0 = TermState(FiniteDistribution(), FiniteDistribution.unif(Type))
val tg = TermGenParams(solverW = 0.05)
Out[2]:
terms: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(Unit, 0.3333333333333333),
    Weighted(Zero, 0.3333333333333333),
    Weighted(Star, 0.3333333333333333)
  )
)
typs: FiniteDistribution[Typ[Term]] = FiniteDistribution(
  Vector(
    Weighted(š’° , 0.3333333333333333),
    Weighted(Unit, 0.3333333333333333),
    Weighted(Zero, 0.3333333333333333)
  )
)
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(Unit, 0.3333333333333333),
      Weighted(Zero, 0.3333333333333333),
      Weighted(Star, 0.3333333333333333)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(š’° , 0.3333333333333333),
      Weighted(Unit, 0.3333333333333333),
      Weighted(Zero, 0.3333333333333333)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
ts0: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(š’° , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
tg: TermGenParams = TermGenParams(
  0.1,
  0.1,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.05,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
In [3]:
import monix.execution.Scheduler.Implicits.global
val lp = LocalProver(ts, tg).sharpen(10)
val lp0 = LocalProver(ts0).sharpen(10)
Out[3]:
import monix.execution.Scheduler.Implicits.global

lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(Unit, 0.3333333333333333),
        Weighted(Zero, 0.3333333333333333),
        Weighted(Star, 0.3333333333333333)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(š’° , 0.3333333333333333),
        Weighted(Unit, 0.3333333333333333),
        Weighted(Zero, 0.3333333333333333)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.1,
    0.1,
    0.05,
    0.05,
    0.05,
    0.0,
    0.0,
    0.0,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.05,
...
lp0: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(š’° , 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.1,
    0.1,
    0.05,
    0.05,
    0.05,
    0.0,
    0.0,
    0.0,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
      <function1>
    )
  ),
  1.0E-5,
  12 minutes,
  1.01,
  1.0,
  10000,
...
In [4]:
val unknownsT = lp0.unknownStatements.map(_.entropyVec.map(_.elem)).memoize
val unF = unknownsT.runToFuture
In [5]:
import StrategicProvers._
import almond.display._
val chompView = Markdown("## Results from Goal chomping\n")

Goal chomping status

  • current goal : Some((@a : š’° _0 ) ~> ((((@a) , (@a))) ā†’ (@a)))
  • negated current goal: Some(āˆ‘((@a : š’° _0) ā†¦ (((((@a) , (@a))) , ((@a) ā†’ (Zero))))))
  • successes : 212
  • failures : 1
  • terms : 5005
  • equation-nodes: 2981176
  • last success : Some(Vector((āˆ‘((@a : š’° _0) ā†¦ ((@a) ā†’ (Zero))),0.5,[((Zero) , (rec(Zero)(Zero))) : 0.01127994556862484, ((Zero) , ((@a : Zero) ā†¦ (@a))) : 0.00974783102948558])))

    ### Failures

  • (((@a : š’° _0 ) ~> ((š’° _0) ā†’ (@a))) ā†’ (š’° _0)) ā†’ (š’° _0)

Out[5]:
import StrategicProvers._

import almond.display._
In [6]:
update = (_) => {
    chompView.withContent(md).update()  
}
update(())
In [7]:
val chT = unknownsT.flatMap(typs => liberalChomper(lp, typs, accumTerms = Set())).memoize
val chF = chT.runToFuture

Interim conclusions

  • We went past te first failure with the naive goal chomper without any problem.
  • We should check negate, in particular include proofs that it really is negation.
  • We should also add memo to the goal chomper that halts.
In [10]:
failures.headOption
failures.headOption.map(negate)
Out[10]:
res9_0: Option[Typ[Term]] = Some(((āˆ(@a : š’° ){ (š’°  ā†’ @a) } ā†’ š’° ) ā†’ š’° ))
res9_1: Option[Typ[Term]] = Some((āˆ(@a : š’° ){ (š’°  ā†’ @a) } ā†’ š’° )Ɨ(š’°  ā†’ Zero))
In [11]:
failures.headOption.map(_.toString)
Out[11]:
res10: Option[String] = Some(
  (((`@a : š’° _0 ) ~> ((š’° _0) ā†’ (`@a))) ā†’ (š’° _0)) ā†’ (š’° _0)
)
In [12]:
unF.map(_.size)

Conclusions (for chomping)

  • Of the 213 goals all but one was successfully chomped.
  • This was done in around an hour with a 12 minute timeout per goal and no parallelism.
  • The one missed case is puzzling since a constant function works for this.
  • The obvious improvement for runtime is to add terms generated while generating the problems to the lookup solver.
  • This kernel will be kept alive for further examination of equations etc.
In [13]:
termSet.map(_.typ).size
Out[13]:
res12: Int = 1451
In [14]:
chF.map(_._5)
In [15]:
res13.cancel
In [ ]: