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.

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
    }
  )
}

import $cp.$                                              

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

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)

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>
  )
)

import monix.execution.Scheduler.Implicits.global
val lp = LocalProver(ts, tg).sharpen(10)
val lp0 = LocalProver(ts0).sharpen(10)

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,
...

val unknownsT = lp0.unknownStatements.map(_.entropyVec.map(_.elem)).memoize
val unF = unknownsT.runToFuture

unknownsT: monix.eval.Task[Vector[Typ[Term]]] = Async(
  <function2>,
  false,
  true,
  true
)
unF: monix.execution.CancelableFuture[Vector[Typ[Term]]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Vector(
    ∏(@a : 𝒰 ){ @a },
    ∑(@a : { @a },
    ((𝒰  → 𝒰 ) → 𝒰 ),
    (𝒰 ×𝒰  → 𝒰 ),
    (𝒰  → ∏(@b : 𝒰 ){ @b }),
    (∏(@a : 𝒰 ){ @a } → 𝒰 ),
    (𝒰  → 𝒰 ×𝒰 ),
    ∏(@a : 𝒰 ){ (𝒰  → @a) },
    (∑(@a : { @a } → 𝒰 ),
    ∑(@a : { (@a → 𝒰 ) },
    ∏(@a : 𝒰 ){ @a×𝒰  },
    (𝒰  → ∑(@b : { @b }),
    ∑(@a : { (𝒰  → @a) },
    ∏(@a : 𝒰 ){ 𝒰 ×@a },
    ∑(@a : { @a×𝒰  },
    ((𝒰 ×𝒰  → 𝒰 ) → 𝒰 ),
    ((𝒰  → 𝒰 )×𝒰  → 𝒰 ),
    ∑(@a : { (@a → @a) },
    ∏(@a : 𝒰 ){ @a×@a },
    ((𝒰  → (𝒰  → 𝒰 )) → 𝒰 ),
    ((∏(@a : 𝒰 ){ @a } → 𝒰 ) → 𝒰 ),
    ∑(@a : { 𝒰 ×@a },
    ((𝒰  → 𝒰 ) → 𝒰 ×𝒰 ),
    (𝒰 ×𝒰 ×𝒰  → 𝒰 ),
    (𝒰 ×(𝒰  → 𝒰 ) → 𝒰 ),
    (∏(@a : 𝒰 ){ @a }×𝒰  → 𝒰 ),
    ((∑(@a : { @a } → 𝒰 ) → 𝒰 ),
    ((𝒰  → ∏(@b : 𝒰 ){ @b }) → 𝒰 ),
    ((𝒰  → 𝒰 ) → ∏(@a : 𝒰 ){ @a }),
    ((𝒰  → 𝒰 ×𝒰 ) → 𝒰 ),
    ∑(@a : { @a×@a },
    ((((𝒰  → 𝒰 ) → 𝒰 ) → 𝒰 ) → 𝒰 ),
    (∑(@a : { (@a → 𝒰 ) } → 𝒰 ),
    (𝒰 ×∏(@b : 𝒰 ){ @b } → 𝒰 ),
    (𝒰  → (𝒰  → 𝒰 )×𝒰 ),
    (∏(@a : 𝒰 ){ (𝒰  → @a) } → 𝒰 ),
    (𝒰  → (𝒰  → ∏(@c : 𝒰 ){ @c })),
...

import StrategicProvers._
import almond.display._
val chompView = Markdown("## Results from Goal chomping\n")

import StrategicProvers._

import almond.display._

update = (_) => {
    chompView.withContent(md).update()  
}
update(())

val chT = unknownsT.flatMap(typs => liberalChomper(lp, typs, accumTerms = Set())).memoize
val chF = chT.runToFuture

chT: monix.eval.Task[(Vector[Successes], Vector[Typ[Term]], Set[EquationNode], Set[Term], Vector[Typ[Term]])] = Async(<function2>, false, true, true)
chF: monix.execution.CancelableFuture[(Vector[Successes], Vector[Typ[Term]], Set[EquationNode], Set[Term], Vector[Typ[Term]])] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  (
    Vector(
      Vector(
        (
          ∑(@a : { (@a → Zero) },
          0.5,
          FiniteDistribution(
            Vector(
              Weighted((Zero , rec_{ Zero ; Zero }), 0.01127994556862484),
              Weighted((Zero , (@a : Zero) ↦ @a), 0.00974783102948558)
            )
          )
        )
      ),
      Vector(
        (
          ∑(@a : { @a },
          0.5,
          FiniteDistribution(
            Vector(Weighted((Unit , Star), 0.021169694309528184))
          )
        )
      ),
      Vector(
        (
          ((𝒰  → 𝒰 ) → 𝒰 ),
          0.5,
          FiniteDistribution(
            Vector(
              Weighted((@a : (𝒰  → 𝒰 )) ↦ @a(@a(Zero)), 0.002578418972552347),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ Zero, 0.0033744467284184186),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ Unit, 0.005170232425794764),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ @a(Zero), 0.0045022382768380755),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ @a(@a(Unit)), 0.002578418972552347),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ @a(Unit), 0.0029259128097459935)
            )
          )
        )
...

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.

failures.headOption
failures.headOption.map(negate)

res9_0: Option[Typ[Term]] = Some(((∏(@a : 𝒰 ){ (𝒰  → @a) } → 𝒰 ) → 𝒰 ))
res9_1: Option[Typ[Term]] = Some((∏(@a : 𝒰 ){ (𝒰  → @a) } → 𝒰 )×(𝒰  → Zero))

failures.headOption.map(_.toString)

res10: Option[String] = Some(
  (((`@a : 𝒰 _0 ) ~> ((𝒰 _0) → (`@a))) → (𝒰 _0)) → (𝒰 _0)
)

unF.map(_.size)

res11: monix.execution.CancelableFuture[Int] = Success(213)

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.

termSet.map(_.typ).size

res12: Int = 1451

chF.map(_._5)

res13: monix.execution.CancelableFuture[Vector[Typ[Term]]] = [running]

res13.cancel

New Memoized Liberal goal chomping¶

Goal chomping status¶

Interim conclusions¶

Conclusions (for chomping)¶