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 last time is that terms are remembered and looked up but with a map.
• Termination is when all goals are finished; with failures recorded.
• Proving is only by generation, with the generation including backward reasoning rules.
• So far the goal chomper is untested; we test this.
• We also test updating displays etc.

import $cp.bin.`provingground-core-jvm-bcec456d48.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]]] = 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")

Goal chomping status

• current goal : Some(((@a : 𝒰 _0 ) ~> (((@a) → (𝒰 _0)) → (𝒰 _0))) → (𝒰 _0))
• successes : 146
• failures : 29
• terms : 35368
• equation-nodes: 3011386
• last success : Some(Vector((∑((@a : 𝒰 _0) ↦ ((@a) → (Zero))),0.5,[((Zero) , (rec(Zero)(Zero))) : 0.01127994556862484, ((Zero) , ((@a : Zero) ↦ (@a))) : 0.00974783102948558])))
• last failure : Some((𝒰 _0) → ((@b : 𝒰 _0 ) ~> (@b)))

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]])] = [running]

val failHandle = Markdown(failures.reverse.mkString("## Failures\n\n * ", "\n * ", "\n"))

Failures

• ∑((@a : 𝒰 _0) ↦ ((@a) → ((𝒰 _0) → (`@a))))
• (((𝒰 _0) → (𝒰 _0)) → (𝒰 _0)) → ((@a : 𝒰 _0 ) ~> (@a))
• (((@a : 𝒰 _0 ) ~> ((𝒰 _0) → (@a))) → (𝒰 _0)) → (𝒰 _0)
• ∑((@a : 𝒰 _0) ↦ ((@a) → (((𝒰 _0) , (𝒰 _0)))))
• ∑((@a : 𝒰 _0) ↦ ((@a : (𝒰 _0) → (𝒰 _0) ) ~> ((@a) (@a))))
• (𝒰 _0) → (∑((@b : 𝒰 _0) ↦ ((@b) → (`@b))))
• ∑((@a : 𝒰 _0) ↦ ((((𝒰 _0) , (@a))) → (𝒰 _0)))
• ∑((@a : 𝒰 _0) ↦ ((@a) → ((`@a) → (𝒰 _0))))
• ∑((@a : 𝒰 _0) ↦ ((𝒰 _0) → ((@a) → (𝒰 _0))))
• (𝒰 _0) → ((@b : 𝒰 _0 ) ~> (((@b) , (`@b))))
• (@a : 𝒰 _0 ) ~> ((@a : (𝒰 _0) → (𝒰 _0) ) ~> ((@a) (@a)))
• (𝒰 _0) → ((@b : 𝒰 _0 ) ~> (((𝒰 _0) , (@b))))
• (∑((@a : 𝒰 _0) ↦ (@a))) → ((@a : 𝒰 _0 ) ~> (@a))
• ∑((@a : 𝒰 _0) ↦ ((((@a) , (𝒰 _0))) → (𝒰 _0)))
• ∑((@a : 𝒰 _0) ↦ ((((@a) → (𝒰 _0)) , (𝒰 _0))))
• (@a : (𝒰 _0) → (𝒰 _0) ) ~> (∑((@a : 𝒰 _0) ↦ ((@a) (@a))))
• (𝒰 _0) → (∑((@b : 𝒰 _0) ↦ ((@b) → (𝒰 _0))))
• (𝒰 _0) → (((𝒰 _0) , ((@c : 𝒰 _0 ) ~> (@c))))
• (∑((@a : 𝒰 _0) ↦ ((@a) → (`@a)))) → (𝒰 _0)
• ∑((@a : 𝒰 _0) ↦ ((@a) → ((𝒰 _0) → (𝒰 _0))))
• (𝒰 _0) → ((@b : 𝒰 _0 ) ~> (((@b) , (𝒰 _0))))
• (𝒰 _0) → ((@b : 𝒰 _0 ) ~> ((𝒰 _0) → (@b)))
• (𝒰 _0) → ((((@b : 𝒰 _0 ) ~> (@b)) , (𝒰 _0)))
• (@a : (𝒰 _0) → (𝒰 _0) ) ~> ((@a : 𝒰 _0 ) ~> ((@a) (@a)))
• (((𝒰 _0) , (𝒰 _0))) → ((@a : 𝒰 _0 ) ~> (@a))
• (𝒰 _0) → ((𝒰 _0) → ((@c : 𝒰 _0 ) ~> (@c)))
• ((@a : 𝒰 _0 ) ~> ((𝒰 _0) → (@a))) → (𝒰 _0)
• ((𝒰 _0) → (𝒰 _0)) → ((@a : 𝒰 _0 ) ~> (@a))
• (𝒰 _0) → ((@b : 𝒰 _0 ) ~> (@b))

update = (_) => {
    chompView.withContent(md).update()  
    failHandle.withContent(failures.reverse.mkString("## Failures\n\n * ", "\n * ", "\n")).update()
}

update(())