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)