Starting with just types, we will seek top unknowns as goals.
In [1]:
import $cp.bin.`provingground-core-jvm-a6ae52a.fat.jar`
Out[1]:
import $cp.$
In [2]:
import provingground._ , interface._, HoTT._, learning._
Out[2]:
import provingground._ , interface._, HoTT._, learning._
In [3]:
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
In [4]:
val terms = FiniteDistribution.unif[Term](Type, Unit, Zero, Star)
val typs = FiniteDistribution.unif[Typ[Term]](Type, Unit, Zero)
val ts = TermState(terms, typs)
Out[4]:
terms: FiniteDistribution[Term] = FiniteDistribution(
Vector(
Weighted(𝒰 , 0.25),
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25)
)
)
typs: FiniteDistribution[Typ[Term]] = FiniteDistribution(
Vector(
Weighted(𝒰 , 0.3333333333333333),
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333)
)
)
ts: TermState = TermState(
FiniteDistribution(
Vector(
Weighted(𝒰 , 0.25),
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(𝒰 , 0.3333333333333333),
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
)
In [5]:
import monix.execution.Scheduler.Implicits.global
val lp = LocalProver(ts).sharpen(10)
val thmsT = lp.theoremsByStatement
val thmsF = thmsT.runToFuture
import monix.execution.Scheduler.Implicits.global
lp: LocalProver = LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(𝒰 , 0.25),
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25)
)
),
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,
...
thmsT: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Map(
FlatMap(
Map(
Async(<function2>, false, true, true),
provingground.learning.LocalProver$$Lambda$2760/368487092@670c538f,
0
),
provingground.learning.LocalProver$$Lambda$2761/1658847093@473b622e
),
provingground.learning.LocalProverStep$$Lambda$2762/303319596@364600a4,
0
)
thmsF: monix.execution.CancelableFuture[FiniteDistribution[Typ[Term]]] = Success(
FiniteDistribution(
Vector(
Weighted((Zero → (𝒰 → Unit)), 3.0497390746605195E-4),
Weighted((Zero → (Zero → Unit)), 4.356770106657885E-4),
Weighted((Zero → (Unit → Unit)), 4.356770106657885E-4),
Weighted((𝒰 → (Zero → Unit)), 2.688606639440138E-4),
Weighted((𝒰 → (𝒰 → Unit)), 1.8820246476080962E-4),
Weighted((𝒰 → (Unit → Unit)), 2.688606639440138E-4),
Weighted(∏(@a : 𝒰 ){ (@a → Unit) }, 3.4567799649944635E-4),
Weighted((Unit → (Unit → Unit)), 4.3567701066578866E-4),
Weighted((Unit → (Zero → Unit)), 4.3567701066578866E-4),
Weighted((Unit → (𝒰 → Unit)), 3.04973907466052E-4),
Weighted(𝒰 , 0.41378006453846056),
Weighted(Unit×𝒰 , 0.006307547629305582),
Weighted((𝒰 → Unit), 0.009476178164047663),
Weighted((Zero → Unit), 0.015196691774522063),
Weighted((𝒰 ×Zero → Unit), 1.6475595324836717E-4),
Weighted(((Zero → Unit) → Unit), 3.873991333137281E-4),
Weighted(((𝒰 → Unit) → Unit), 2.886934634346448E-4),
Weighted((∑(@a : { @a } → Unit), 2.1182908274790062E-4),
Weighted((Unit×Zero → Unit), 2.0476811332297058E-4),
Weighted((Unit×Unit → Unit), 2.0476811332297058E-4),
Weighted((Zero×𝒰 → Unit), 2.0476811332297058E-4),
Weighted((Zero×Unit → Unit), 2.0476811332297058E-4),
Weighted((𝒰 ×𝒰 → Unit), 1.6475595324836717E-4),
Weighted(((Zero → Zero) → Unit), 3.873991333137281E-4),
Weighted(((𝒰 → Zero) → Unit), 2.886934634346448E-4),
Weighted((Unit → Unit), 0.01650481911361812),
Weighted((Unit×𝒰 → Unit), 2.0476811332297058E-4),
Weighted(((Unit → Unit) → Unit), 3.873991333137281E-4),
Weighted(((Unit → Zero) → Unit), 3.873991333137281E-4),
Weighted((Zero×Zero → Unit), 2.0476811332297058E-4),
Weighted(((Zero → 𝒰 ) → Unit), 3.873991333137281E-4),
Weighted(((𝒰 → 𝒰 ) → Unit), 2.474515400868384E-4),
Weighted(((Unit → 𝒰 ) → Unit), 2.905493499852961E-4),
Weighted((𝒰 ×Unit → Unit), 1.6475595324836717E-4),
Weighted((∏(@a : 𝒰 ){ @a } → Unit), 3.7117731013025767E-4),
Weighted(∑(@a : { @a }, 0.005079885089552229),
...
In [10]:
val unknownsT = lp.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 },
(Unit → (Unit → Zero)),
(Zero → ∏(@a : 𝒰 ){ @a }),
(Unit → ∏(@a : 𝒰 ){ @a }),
(𝒰 → ∏(@b : 𝒰 ){ @b }),
∏(@a : 𝒰 ){ (Zero → @a) },
∏(@a : 𝒰 ){ (Unit → @a) },
(Unit → (𝒰 → Zero)),
∏(@a : (Unit → 𝒰 )){ @a(Star) },
(𝒰 → (Unit → Zero)),
∏(@a : 𝒰 ){ @a×@a },
∑(@a : { (@a → @a) },
∏(@a : 𝒰 ){ (𝒰 → @a) },
(Unit → Unit×Zero),
(Zero → Unit×Zero),
(Unit → Zero×𝒰 ),
(Zero → Zero×𝒰 ),
(Unit → Unit×𝒰 ),
(Zero → Unit×𝒰 ),
(Zero → Zero×Zero),
(Unit → Zero×Zero),
(Zero → Zero×Unit),
(Unit → Zero×Unit),
(Unit → Unit×Unit),
(Zero → Unit×Unit),
(Zero → ∑(@a : { @a }),
(Unit → ∑(@a : { @a }),
(Zero×Unit → Zero),
(Zero×𝒰 → Zero),
(Unit×Zero → Zero),
(Zero×Zero → Zero),
(𝒰 → ∑(@b : { @b }),
∏(@a : 𝒰 ){ @a×𝒰 },
∏(@a : 𝒰 ){ @a×Zero },
∏(@a : 𝒰 ){ @a×Unit },
∏(@a : 𝒰 ){ Zero×@a },
∏(@a : 𝒰 ){ Unit×@a },
...
In [12]:
def seekGoals(typ: Typ[Term]) = lp.addGoals(typ -> 0.5, negate(typ) -> 0.5).successes
Out[12]:
defined function seekGoals
In [13]:
def topGoals(n: Int) = (0 until n).map{j => unknownsT.flatMap(v => seekGoals(v(j)))}
Out[13]:
defined function topGoals
In [14]:
val top20 = topGoals(20)
top20.map(_.runToFuture)
top20: collection.immutable.IndexedSeq[monix.eval.Task[Vector[(Typ[Term], Double, FiniteDistribution[Term])]]] = Vector(
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@2d492f74
),
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@7e3c63c4
),
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@120460a6
),
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@7ffc7409
),
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@27a2b914
),
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@3a9dcc67
),
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@bad8ac2
),
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@17edfb82
),
FlatMap(
Async(<function2>, false, true, true),
ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@25359a72
),
FlatMap(
...
res13_1: collection.immutable.IndexedSeq[monix.execution.CancelableFuture[Vector[(Typ[Term], Double, FiniteDistribution[Term])]]] = Vector(
Success(
Vector(
(
∑(@a : { (@a → Zero) },
0.5,
FiniteDistribution(
Vector(
Weighted((Zero , rec_{ Zero ; Zero }), 0.009912434376452174),
Weighted((Zero , (@a : Zero) ↦ @a), 0.009912434376452174)
)
)
)
)
),
Success(
Vector(
(
((Unit → (Unit → Zero)) → Zero),
0.5,
FiniteDistribution(
Vector(
Weighted(
(@a : (Unit → (Unit → Zero))) ↦ @a(Star)(Star),
0.0191661641766036
)
)
)
)
)
),
Success(
Vector(
(
(Zero → ∏(@a : 𝒰 ){ @a }),
0.5,
FiniteDistribution(
Vector(Weighted(rec_{ Zero ; ∏(@a : 𝒰 ){ @a } }, 0.02524248658291313))
)
)
)
),
Success(
Vector(
(
((Unit → ∏(@a : 𝒰 ){ @a }) → Zero),
0.5,
FiniteDistribution(
Vector(
Weighted(
(@a : (Unit → ∏(@a : 𝒰 ){ @a })) ↦ @a(Star)(Zero),
0.0191661641766036
)
)
)
)
)
),
Success(
Vector(
(
((𝒰 → ∏(@b : 𝒰 ){ @b }) → Zero),
0.5,
FiniteDistribution(
Vector(
Weighted(
(@a : (𝒰 → ∏(@b : 𝒰 ){ @b })) ↦ @a(Unit)(Zero),
0.0095830820883018
),
Weighted(
(@a : (𝒰 → ∏(@b : 𝒰 ){ @b })) ↦ @a(Zero)(Zero),
0.0095830820883018
)
)
)
)
)
),
Success(
Vector(
(
∏(@a : 𝒰 ){ (Zero → @a) },
0.5,
FiniteDistribution(
Vector(Weighted((@a : 𝒰 ) ↦ rec_{ Zero ; @a }, 0.02216424605959186))
)
)
)
),
Success(
Vector(
(
∑(@a : { ((Unit → @a) → Zero) },
0.5,
FiniteDistribution(
Vector(
Weighted(
(Zero , (@a : (Unit → Zero)) ↦ @a(Star)),
0.01982316937709552
)
)
)
)
)
),
Success(
Vector(
(
((Unit → (𝒰 → Zero)) → Zero),
0.5,
FiniteDistribution(
Vector(
Weighted(
(@a : (Unit → (𝒰 → Zero))) ↦ @a(Star)(Zero),
0.0095830820883018
),
Weighted(
(@a : (Unit → (𝒰 → Zero))) ↦ @a(Star)(Unit),
0.0095830820883018
)
)
)
)
)
),
Success(
Vector(
(
∑(@a : { (@a(Star) → Zero) },
0.5,
FiniteDistribution(
Vector(
Weighted(
((@a : Unit) ↦ Zero , rec_{ Zero ; Zero }),
0.004946099629479799
),
Weighted(
((@a : Unit) ↦ Zero , (@a : Zero) ↦ @a),
0.004946099629479799
),
Weighted(
(rec_{ Unit ; 𝒰 }(Zero) , (@a : Zero) ↦ @a),
0.004946099629479799
),
Weighted(
(rec_{ Unit ; 𝒰 }(Zero) , rec_{ Zero ; Zero }),
0.004946099629479799
)
)
)
)
)
),
Success(
Vector(
(
((𝒰 → (Unit → Zero)) → Zero),
0.5,
FiniteDistribution(
Vector(
Weighted(
(@a : (𝒰 → (Unit → Zero))) ↦ @a(Unit)(Star),
0.0095830820883018
),
Weighted(
(@a : (𝒰 → (Unit → Zero))) ↦ @a(Zero)(Star),
0.0095830820883018
)
)
)
)
)
),
Success(
Vector(
(
∑(@a : { (@a → Zero) + (@a → Zero) },
0.5,
FiniteDistribution(
Vector(
Weighted(
(Zero , FirstIncl(PlusTyp((Zero) → (Zero),(Zero) → (Zero)),rec(Zero)(Zero))),
0.005120352121428702
),
Weighted(
(Zero , ScndIncl(PlusTyp((Zero) → (Zero),(Zero) → (Zero)),rec(Zero)(Zero))),
0.005120352121428702
),
Weighted(
(Zero , ScndIncl(PlusTyp((Zero) → (Zero),(Zero) → (Zero)),(`@a : Zero) ↦ (`@a))),
0.004791232567119057
),
Weighted(
(Zero , FirstIncl(PlusTyp((Zero) → (Zero),(Zero) → (Zero)),(`@a : Zero) ↦ (`@a))),
0.004791232567119057
)
)
)
)
)
),
Success(
Vector(
(
∑(@a : { (@a → @a) },
0.5,
FiniteDistribution(
Vector(
Weighted((Unit , rec_{ Unit ; Unit }(Star)), 0.004946499273937881),
Weighted((Zero , (@a : Zero) ↦ @a), 0.004946499273937881),
Weighted((Zero , rec_{ Zero ; Zero }), 0.004946499273937881),
Weighted((Unit , (@a : Unit) ↦ @a), 0.0031241048045923467),
Weighted((Unit , (@a : Unit) ↦ Star), 0.0018223944693455355)
)
)
)
)
),
Success(
Vector(
(
∑(@a : { ((𝒰 → @a) → Zero) },
0.5,
FiniteDistribution(
Vector(
Weighted((Zero , (@a : (𝒰 → Zero)) ↦ @a(Unit)), 0.00991158468854776),
Weighted((Zero , (@a : (𝒰 → Zero)) ↦ @a(Zero)), 0.00991158468854776)
)
)
)
)
),
Success(Vector()),
Success(
Vector(
(
(Zero → Unit×Zero),
0.5,
FiniteDistribution(
Vector(
Weighted(rec_{ Zero ; Unit×Zero }, 0.017091576549434707),
Weighted((@a : Zero) ↦ (Star , @a), 0.0104964584462948)
)
)
)
)
),
Success(Vector()),
Success(
Vector(
(
(Zero → Zero×𝒰 ),
0.5,
FiniteDistribution(
Vector(
Weighted((@a : Zero) ↦ (@a , Zero), 0.005238463685229454),
Weighted(rec_{ Zero ; Zero×𝒰 }, 0.01709191390737606),
Weighted((@a : Zero) ↦ (@a , Unit), 0.005238463685229454)
)
)
)
)
),
Success(
Vector(
(
(Unit → Unit×𝒰 ),
0.5,
FiniteDistribution(
Vector(
Weighted((@a : Unit) ↦ (@a , Zero), 0.003189116089034762),
Weighted(rec_{ Unit ; Unit×𝒰 }((Star , Zero)), 0.004755330860038047),
Weighted((@a : Unit) ↦ (@a , Unit), 0.003189116089034762),
Weighted(rec_{ Unit ; Unit×𝒰 }((Star , Unit)), 0.004755330860038047),
Weighted((@a : Unit) ↦ (Star , Unit), 0.001860317718603611),
Weighted((@a : Unit) ↦ (Star , Zero), 0.001860317718603611)
)
)
)
)
),
Success(
Vector(
(
(Zero → Unit×𝒰 ),
0.5,
FiniteDistribution(
Vector(
Weighted((@a : Zero) ↦ (Star , Zero), 0.005238463685229454),
Weighted((@a : Zero) ↦ (Star , Unit), 0.005238463685229454),
Weighted(rec_{ Zero ; Unit×𝒰 }, 0.01709191390737606)
)
)
)
)
),
Success(
Vector(
(
(Zero → Zero×Zero),
0.5,
FiniteDistribution(
Vector(
Weighted(rec_{ Zero ; Zero×Zero }, 0.017091576549434714),
Weighted((@a : Zero) ↦ (@a , @a), 0.010496458446294802)
)
)
)
)
)
)
While a very modest task, this has been a success in both workflow and results.
Content source: siddhartha-gadgil/ProvingGround
Similar notebooks: