notebook.community

Edit and run

Variables and Modus Ponens using relative expression evaluation

Before a larger run, this is to test the use of variables in a LocalProver to export.





In [1]:



    


import $cp.bin.`provingground-core-jvm-dbd333bd25.fat.jar`



    


















    
Out[1]:








import $cp.$                                              

















In [2]:



    


import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}



    


















    
Out[2]:








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


















In [3]:



    


val A = "A" :: Type
val B = "B" :: Type
val ts = TermState(FiniteDistribution.unif(A, B), FiniteDistribution.unif(A, B), vars = Vector(A, B))



    


















    
Out[3]:








A: Typ[Term] = A
B: Typ[Term] = B
ts: TermState = TermState(
  FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
  FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
  Vector(A, B),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)

















In [4]:



    


val lp = LocalProver(ts, relativeEval = true).sharpen(10)



    


















    
Out[4]:








lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    Vector(A, B),
    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,
  true,
...

















In [5]:



    


import monix.execution.Scheduler.Implicits.global
val nsT = lp.nextState
val nsF = nsT.runToFuture



    


















    























In [6]:



    


val MPAB = A ->: (A ->: B) ->: B
val MP = A ~>: (B ~>: MPAB)



    


















    
Out[6]:








MPAB: FuncTyp[Term, Func[Func[Term, Term], Term]] = (A → ((A → B) → B))
MP: GenFuncTyp[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }

















In [7]:



    


val evT = lp.expressionEval
val evF = evT.runToFuture



    


















    























In [8]:



    


evT.map(_.finalTyps(MP)).runToFuture



    


















    























In [9]:



    


evT.map(_.finalTyps.entropyVec).runToFuture



    


















    























In [10]:



    


evT.map(_.finalTyps.entropy(MP)).runToFuture



    


















    























In [11]:



    


MP



    


















    
Out[11]:








res10: GenFuncTyp[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }

Conclusions

  • the sanity check has passed, where we do get the statement of Modus Ponens when we work with variables
  • in this case, product terms are a nuisance; we may want to avoid such coefficients in a convenient way.




In [12]:



    


val lp1 = LocalProver(ts, tg = TermGenParams(sigmaW = 0), relativeEval = true).sharpen(10)



    


















    
Out[12]:








lp1: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    Vector(A, B),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.1,
    0.1,
    0.05,
    0.05,
    0.0,
    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,
  true,
...

















In [14]:



    


val nsT1 = lp1.nextState
val nsF1 = nsT1.runToFuture



    


















    























In [24]:



    


val evT1 = lp1.expressionEval
evT1.map(_.finalTyps(MP)).runToFuture



    


















    























In [26]:



    


evT1.map(_.finalTyps.entropyVec).runToFuture



    


















    























In [25]:



    


evT1.map(_.finalTyps.entropy(MP)).runToFuture



    


















    























In [27]:



    


evT1.map(_.finalTerms.filter(_.typ == MP)).runToFuture

Conclusions round two

  • The generation of the modus ponens statement is a litte more robust if sigma-islands (hence products) are excluded.
  • We still do not get a proof of Modus Ponens if it is not targetted.

Content source: siddhartha-gadgil/ProvingGround

Similar notebooks:

notebook.community | gallery | about