Liberal goal chomping¶

We run a variant of the most basic strategic prover - a goal chomper that keeps trying a succession of goals.
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.

The goals and proving.¶

To generate the goals, we start with just Type.
To prove them, we include also Zero, One and Star

import $cp.bin.`provingground-core-jvm-8f190786f9.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))

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
)

import monix.execution.Scheduler.Implicits.global
val lp = LocalProver(ts).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.0,
...
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
  ),
  1.0E-5,
  12 minutes,
  1.01,
  1.0,
  10000,
  10,
  1.0,
  1.0,
  None,
  false,
...

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 StrategicProvers._

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

import almond.display._

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

update(())

val chT = unknownsT.flatMap(typs => liberalChomper(lp, typs)).memoize

chT: monix.eval.Task[(Vector[Successes], Vector[Typ[Term]], Set[EquationNode], Vector[Typ[Term]])] = Async(<function2>, false, true, true)

val chF = chT.runToFuture

chF: monix.execution.CancelableFuture[(Vector[Successes], Vector[Typ[Term]], Set[EquationNode], 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.01970769689870014))
          )
        )
      ),
      Vector(
        (
          ((𝒰  → 𝒰 ) → 𝒰 ),
          0.5,
          FiniteDistribution(
            Vector(
              Weighted((@a : (𝒰  → 𝒰 )) ↦ @a(@a(Zero)), 0.003035898473921898),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ Zero, 0.004434521334908531),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ Unit, 0.004434521334908531),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ @a(Zero), 0.0030950013985154468),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ @a(@a(Unit)), 0.003035898473921898),
              Weighted((@a : (𝒰  → 𝒰 )) ↦ @a(Unit), 0.0030950013985154468)
            )
          )
        )
...

Interim conclusions¶

This is working smoothly, at least for purposes of testing.
One should have some concurrency, otherwise we wait for failures to timeout.

val succHandle = Markdown(successes.reverse.mkString("## Successes\n\n * ", "\n * ", "\n"))

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

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

update(())

val ft = failures.lastOption

ft: Option[Typ[Term]] = Some((𝒰  → ∏(@b : 𝒰 ){ @b×@b }))

Conclusions¶

Chomped to the end in a few hours
Eight failures, all can be addressed by sharper backward reasoning.
More immediate change is to repeat this with memoization/.

Liberal goal chomping¶

The goals and proving.¶

Goal chomping status¶

Interim conclusions¶

Successes¶

Failures¶

Conclusions¶