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.