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









    





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



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









    





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]])] = 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.



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)









    





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.



In [13]:

    
termSet.map(_.typ).size









    Out[13]:





res12: Int = 1451



In [14]:

    
chF.map(_._5)









    





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



In [15]:

    
res13.cancel



In [ ]: