Variables, Modus Ponens

The primary goal is to test exporting an expression evaluator with respect to variables, in particular to obtain Modus ponens. A secondary goal is to test having empty initial term distribution

In [1]:
import $cp.bin.`provingground-core-jvm-13d7adec62.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 MPAB = A ->: (A ->: B) ->: B
val MP = A ~>: (B ~>: MPAB)
Out[3]:
A: Typ[Term] = A
B: Typ[Term] = B
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 [4]:
val lp = LocalProver(TermState(FiniteDistribution(), FiniteDistribution.unif(A, B))).sharpen(2)
Out[4]:
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    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
  ),
  5.0E-5,
  12 minutes,
  1.01,
  1.0,
  10000,
  10,
  1.0,
  1.0
)
In [5]:
import monix.execution.Scheduler.Implicits.global
val nsT = lp.nextState
val nsF = nsT.runToFuture

import monix.execution.Scheduler.Implicits.global

nsT: monix.eval.Task[TermState] = Async(<function2>, false, true, true)
nsF: monix.execution.CancelableFuture[TermState] = Success(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted((@a : A) ā†¦ (@a : (B ā†’ A)) ā†¦ @a, 5.240528464411918E-4),
        Weighted((@a : A) ā†¦ (@a : (A ā†’ A)) ā†¦ @a, 5.240528464411918E-4),
        Weighted(
          ((`@a_1 , @a_2) : (A ā†’ B)ƗA) ā†¦ (`@a_1 , @a_2),
          3.679356357927782E-4
        ),
        Weighted(
          ((`@a_1 , @a_2) : (B ā†’ B)ƗA) ā†¦ (`@a_1 , @a_2),
          3.679356357927782E-4
        ),
        Weighted(
          ((`@a_1 , @a_2) : (B ā†’ A)ƗA) ā†¦ (`@a_1 , @a_2),
          3.679356357927782E-4
        ),
        Weighted(
          ((`@a_1 , @a_2) : (A ā†’ A)ƗA) ā†¦ (`@a_1 , @a_2),
          3.679356357927782E-4
        ),
        Weighted((@a : B) ā†¦ (@a : (A ā†’ A)) ā†¦ @a, 5.24052846441192E-4),
        Weighted((@a : B) ā†¦ (@a : (B ā†’ A)) ā†¦ @a, 5.24052846441192E-4),
        Weighted((@a : B) ā†¦ (@a : B) ā†¦ @a, 0.02319914182230953),
        Weighted((@a : B) ā†¦ (@b : B) ā†¦ @a, 0.009524557356703807),
        Weighted((@a : (B ā†’ B)) ā†¦ (@a : B) ā†¦ @a, 9.946073128244794E-4),
        Weighted((@a : B) ā†¦ (@a : (A ā†’ B)) ā†¦ @a, 3.6683699250883445E-4),
        Weighted((@a : B) ā†¦ (@a : (B ā†’ B)) ā†¦ @a, 3.6683699250883445E-4),
        Weighted((@a : (A ā†’ B)) ā†¦ (@a : B) ā†¦ @a, 9.946073128244794E-4),
        Weighted((@a : (A ā†’ (B ā†’ B))) ā†¦ @a, 6.30746804216191E-4),
        Weighted((@a : (A ā†’ (A ā†’ B))) ā†¦ @a, 6.30746804216191E-4),
        Weighted((@a : (B ā†’ (A ā†’ B))) ā†¦ @a, 6.30746804216191E-4),
        Weighted((@a : (B ā†’ (B ā†’ B))) ā†¦ @a, 6.30746804216191E-4),
        Weighted((@a : (A ā†’ (A ā†’ A))) ā†¦ @a, 6.30746804216191E-4),
        Weighted((@a : (A ā†’ (B ā†’ A))) ā†¦ @a, 6.30746804216191E-4),
        Weighted((@a : (B ā†’ (A ā†’ A))) ā†¦ @a, 6.30746804216191E-4),
        Weighted((@a : (B ā†’ (B ā†’ A))) ā†¦ @a, 6.30746804216191E-4),
        Weighted((@a : (A ā†’ A)) ā†¦ (@a : B) ā†¦ @a, 9.946073128244794E-4),
...
In [6]:
val mpABpF = nsT.map(_.typs(MPAB)).runToFuture

mpABpF: monix.execution.CancelableFuture[Double] = Success(7.529314129678205E-5)

Interim conclusion

The secondary test was passed, but the variable weight is based on distribution in terms (at least in the current version). So we continue testing with a local prover with terms.

In [7]:
val lp0 = LocalProver(TermState(FiniteDistribution.unif(A, B), FiniteDistribution.unif(A, B))).sharpen(2)
Out[7]:
lp0: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    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
  ),
  5.0E-5,
  12 minutes,
  1.01,
  1.0,
  10000,
  10,
  1.0,
  1.0
)
In [8]:
val expEvT = lp0.expressionEval
Out[8]:
expEvT: monix.eval.Task[ExpressionEval] = Async(<function2>, false, true, true)
In [9]:
val outerExpEvT = expEvT.map{ev => ExpressionEval.export(ev, Vector(A, B))}
Out[9]:
outerExpEvT: monix.eval.Task[ExpressionEval] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd8$Helper$$Lambda$2956/2131709603@3eefc81d,
  0
)
In [10]:
val outTypsT = outerExpEvT.map(_.finalTyps)
val outTypsEF = outTypsT.map(_.entropyVec).runToFuture

outTypsT: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Map(
  Async(<function2>, false, true, true),
  scala.Function1$$Lambda$645/1406680501@15bc1612,
  1
)
outTypsEF: monix.execution.CancelableFuture[Vector[Weighted[Typ[Term]]]] = Success(
  Vector(
    Weighted((š’°  ā†’ āˆ(B : š’° ){ B }), 6.489213340290813),
    Weighted((š’°  ā†’ āˆ(B : š’° ){ (B ā†’ B) }), 10.005540662633953),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ B) } }, 10.175326468300284),
    Weighted((š’°  ā†’ āˆ(B : š’° ){ ((B ā†’ B) ā†’ B) }), 11.203247861423154),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ ((A ā†’ B) ā†’ B) } }, 11.20480622357255),
    Weighted((š’°  ā†’ āˆ(B : š’° ){ (((B ā†’ B) ā†’ B) ā†’ B) }), 11.21119910791957),
    Weighted(
      āˆ(A : š’° ){ āˆ(B : š’° ){ (((A ā†’ B) ā†’ B) ā†’ B) } },
      11.211205523337371
    ),
    Weighted((š’°  ā†’ āˆ(B : š’° ){ ((BƗB ā†’ B) ā†’ B) }), 11.211244776916596),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ ((AƗB ā†’ B) ā†’ B) } }, 11.2112455186309),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ ((BƗA ā†’ B) ā†’ B) } }, 11.211258240609004),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ ((AƗA ā†’ B) ā†’ B) } }, 11.211258240609004),
    Weighted(
      āˆ(A : š’° ){ āˆ(B : š’° ){ (((A ā†’ A) ā†’ B) ā†’ B) } },
      11.211258240609004
    ),
    Weighted(
      āˆ(A : š’° ){ āˆ(B : š’° ){ (((B ā†’ A) ā†’ B) ā†’ B) } },
      11.211258240609004
    ),
    Weighted((š’°  ā†’ āˆ(B : š’° ){ (BƗB ā†’ B) }), 11.214115785449748),
    Weighted((š’°  ā†’ āˆ(B : š’° ){ ((B ā†’ B)ƗB ā†’ B) }), 11.214279119987127),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ ((A ā†’ B)ƗB ā†’ B) } }, 11.214280706685622),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ ((A ā†’ A)ƗB ā†’ B) } }, 11.214293803115382),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ ((B ā†’ A)ƗB ā†’ B) } }, 11.214293803115382),
    Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ (AƗB ā†’ B) } }, 11.214293803115382),
    Weighted((š’°  ā†’ āˆ(B : š’° ){ ((B ā†’ (B ā†’ B)) ā†’ B) }), 11.216804871163022),
    Weighted(
      āˆ(A : š’° ){ āˆ(B : š’° ){ ((B ā†’ (A ā†’ B)) ā†’ B) } },
      11.216848465001458
    ),
    Weighted(
      āˆ(A : š’° ){ āˆ(B : š’° ){ ((A ā†’ (B ā†’ B)) ā†’ B) } },
      11.216861299795132
    ),
...
In [11]:
val mpWtF = outTypsT.map(_(MP)).runToFuture

mpWtF: monix.execution.CancelableFuture[Double] = Success(2.9485760403456388E-5)

Conclusions

  • We do get Modus Ponens - testing both generation and export.
  • Further (assuming everything is correct), while we need variables to discover modus ponens, once discovered it has reasonable weight.

As a coda, we compare the generated final types with the ones generated by equations.

In [12]:
val gExpEvT = lp.expressionEval.map(_.generateTyps)
Out[12]:
gExpEvT: monix.eval.Task[ExpressionEval] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd11$Helper$$Lambda$3208/818383182@7142bd2a,
  0
)
In [16]:
val mpABgenF = gExpEvT.map(_.finalTyps.safeNormalized(MPAB)).runToFuture

mpABgenF: monix.execution.CancelableFuture[Double] = Success(5.373624304933932E-4)
In [17]:
val eF = nsT.map(_.typs.entropyVec).runToFuture
val egF = gExpEvT.map(_.finalTyps.safeNormalized.entropyVec).runToFuture

eF: monix.execution.CancelableFuture[Vector[Weighted[Typ[Term]]]] = Success(
  Vector(
    Weighted(A, 1.2479275134435854),
    Weighted(B, 1.2479275134435854),
    Weighted((B ā†’ B), 5.790231427845975),
    Weighted((A ā†’ B), 5.790231427845975),
    Weighted((B ā†’ A), 5.790231427845975),
    Weighted((A ā†’ A), 5.790231427845975),
    Weighted(BƗA, 6.837227203385614),
    Weighted(AƗA, 6.837227203385614),
    Weighted(AƗB, 6.837227203385614),
    Weighted(BƗB, 6.837227203385614),
    Weighted(((A ā†’ A) ā†’ B), 9.915104777452932),
    Weighted(((B ā†’ A) ā†’ B), 9.915104777452932),
    Weighted(((A ā†’ B) ā†’ B), 9.915104777452932),
    Weighted(((B ā†’ B) ā†’ B), 9.915104777452932),
    Weighted(((B ā†’ B) ā†’ A), 9.915104777452932),
    Weighted(((A ā†’ B) ā†’ A), 9.915104777452932),
    Weighted(((B ā†’ A) ā†’ A), 9.915104777452932),
    Weighted(((A ā†’ A) ā†’ A), 9.915104777452932),
    Weighted((B ā†’ (B ā†’ A)), 10.112159522733336),
    Weighted((B ā†’ (A ā†’ A)), 10.112159522733336),
    Weighted((A ā†’ (A ā†’ A)), 10.112159522733336),
    Weighted((A ā†’ (B ā†’ A)), 10.112159522733336),
    Weighted((B ā†’ (B ā†’ B)), 10.112159522733336),
    Weighted((B ā†’ (A ā†’ B)), 10.112159522733336),
    Weighted((A ā†’ (B ā†’ B)), 10.112159522733336),
    Weighted((A ā†’ (A ā†’ B)), 10.112159522733336),
    Weighted((B ā†’ A)ƗB, 10.449934694589674),
    Weighted((A ā†’ A)ƗB, 10.449934694589674),
    Weighted((B ā†’ B)ƗA, 10.449934694589674),
    Weighted((A ā†’ B)ƗA, 10.449934694589674),
    Weighted((A ā†’ B)ƗB, 10.449934694589674),
    Weighted((B ā†’ B)ƗB, 10.449934694589674),
    Weighted((B ā†’ A)ƗA, 10.449934694589674),
    Weighted((A ā†’ A)ƗA, 10.449934694589674),
    Weighted((BƗB ā†’ B), 10.470319934780035),
    Weighted((AƗB ā†’ B), 10.470319934780035),
    Weighted((BƗA ā†’ B), 10.470319934780035),
...
egF: monix.execution.CancelableFuture[Vector[Weighted[Typ[Term]]]] = Success(
  Vector(
    Weighted(A, 3.2339300375523696),
    Weighted(B, 3.2339300375523696),
    Weighted((B ā†’ B), 7.024857460643389),
    Weighted((A ā†’ B), 7.024857460643389),
    Weighted((B ā†’ A), 7.024857460643389),
    Weighted((A ā†’ A), 7.024857460643389),
    Weighted(((A ā†’ B) ā†’ B), 7.068324710233895),
    Weighted(((B ā†’ B) ā†’ B), 7.068324710233895),
    Weighted(((B ā†’ A) ā†’ B), 7.068324710233895),
    Weighted(((A ā†’ A) ā†’ B), 7.068324710233895),
    Weighted(((A ā†’ B) ā†’ A), 7.068324710233895),
    Weighted(((B ā†’ B) ā†’ A), 7.068324710233895),
    Weighted(((A ā†’ A) ā†’ A), 7.068324710233895),
    Weighted(((B ā†’ A) ā†’ A), 7.068324710233895),
    Weighted((((B ā†’ A) ā†’ B) ā†’ B), 7.06841774975812),
    Weighted((((A ā†’ A) ā†’ B) ā†’ B), 7.06841774975812),
    Weighted((((A ā†’ B) ā†’ B) ā†’ B), 7.06841774975812),
    Weighted((((B ā†’ B) ā†’ B) ā†’ B), 7.06841774975812),
    Weighted((((B ā†’ A) ā†’ A) ā†’ B), 7.06841774975812),
    Weighted((((A ā†’ A) ā†’ A) ā†’ B), 7.06841774975812),
    Weighted((((A ā†’ B) ā†’ A) ā†’ B), 7.06841774975812),
    Weighted((((B ā†’ B) ā†’ A) ā†’ B), 7.06841774975812),
    Weighted((((B ā†’ A) ā†’ B) ā†’ A), 7.06841774975812),
    Weighted((((A ā†’ A) ā†’ B) ā†’ A), 7.06841774975812),
    Weighted((((A ā†’ B) ā†’ B) ā†’ A), 7.06841774975812),
    Weighted((((B ā†’ B) ā†’ B) ā†’ A), 7.06841774975812),
    Weighted((((B ā†’ B) ā†’ A) ā†’ A), 7.06841774975812),
    Weighted((((A ā†’ B) ā†’ A) ā†’ A), 7.06841774975812),
    Weighted((((A ā†’ A) ā†’ A) ā†’ A), 7.06841774975812),
    Weighted((((B ā†’ A) ā†’ A) ā†’ A), 7.06841774975812),
    Weighted(((AƗB ā†’ A) ā†’ B), 7.068421108580578),
    Weighted(((BƗA ā†’ A) ā†’ B), 7.068421108580578),
    Weighted(((AƗA ā†’ A) ā†’ B), 7.068421108580578),
    Weighted(((BƗB ā†’ A) ā†’ B), 7.068421108580578),
    Weighted(((BƗB ā†’ B) ā†’ B), 7.068421108580578),
    Weighted(((BƗA ā†’ B) ā†’ B), 7.068421108580578),
    Weighted(((AƗA ā†’ B) ā†’ B), 7.068421108580578),
...

Additional conclusion

There seems to be better distribution if we generate from equations (though we have to be careful to normalize)