In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
Out[1]:
import $ivy.$
In [2]:
import provingground._ , interface._, HoTT._
import provingground.{FiniteDistribution => FD}
Out[2]:
import provingground._ , interface._, HoTT._
import provingground.{FiniteDistribution => FD}
In [3]:
val A = "A" :: Type
val B = "B" :: Type
val MP = A ~>: (B ~>: (A ->: (A ->: B) ->: B))
Out[3]:
A: Typ[Term] = SymbTyp(Name("A"), 0)
B: Typ[Term] = SymbTyp(Name("B"), 0)
MP: GenFuncTyp[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = PiDefn(
SymbTyp(A, 0),
PiDefn(
SymbTyp(B, 0),
FuncTyp(
SymbTyp(A, 0),
FuncTyp(FuncTyp(SymbTyp(A, 0), SymbTyp(B, 0)), SymbTyp(B, 0))
)
)
)
In [4]:
repl.pprinter.bind(translation.FansiShow.fansiPrint)
In [5]:
import learning._
val tg = TermGenParams()
val mfd = MonixFiniteDistributionEq(tg.nodeCoeffSeq)
val ts = TermState(FD.unif(Type), FD.unif(Type), goals = FD.unif(MP))
Out[5]:
import learning._
tg: TermGenParams = TermGenParams(0.1, 0.1, 0.1, 0.1, 0.1, 0.05, 0.05, 0.05, 0.3, 0.5, 0.5)
mfd: MonixFiniteDistributionEq[TermState, Term] = MonixFiniteDistributionEq(
Cons(
BaseCons(
BasePi(
provingground.learning.RandomVarFamily$$Lambda$3765/1938135699@5621c319,
FuncsWithDomain
),
0.55,
BaseCons(
BasePi(
provingground.learning.GeneratorNode$$Lambda$3768/328900033@1bd62afd,
FuncsWithDomain
),
0.1,
BaseCons(
BasePi(
provingground.learning.GeneratorNode$$Lambda$3768/328900033@7cb1b783,
FuncsWithDomain
),
0.1,
BaseCons(
BasePi(
provingground.learning.GeneratorNode$$Lambda$3768/328900033@50c609f4,
FuncsWithDomain
),
0.1,
BaseCons(
BasePi(
provingground.learning.TermGeneratorNodes$$Lambda$3759/319800441@838a04e,
FuncsWithDomain
),
0.1,
Target(FuncsWithDomain)
)
)
)
)
),
Cons(
BaseCons(
Map(
provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3771/1620514355@16c01a2,
Goals,
TargetTyps
),
0.5,
BaseCons(
Map(
provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3772/396853136@4062de80,
...
ts: TermState = TermState(
FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector(Weighted(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, 1.0))),
Empty
)
In [6]:
import TermRandomVars._
val tsk = mfd.varDist(ts)(Terms, 0.00001)
import monix.execution.Scheduler.Implicits.global
Out[6]:
import TermRandomVars._
tsk: monix.eval.Task[(FiniteDistribution[Term], Set[GeneratorVariables.EquationTerm])] = FlatMap(
Async(<function2>, true, true, true),
monix.eval.Task$$Lambda$3893/194816733@4ed79980
)
import monix.execution.Scheduler.Implicits.global
In [7]:
val (fd, eqts) = tsk.runSyncUnsafe()
Out[7]:
fd: FiniteDistribution[Term] = FiniteDistribution(
Vector(
Weighted((@a : (𝒰 → 𝒰 )) ↦ @a(@a), 2.5720562233697236E-4),
Weighted((_ : @a) ↦ 𝒰 , 3.3308015913189606E-4),
Weighted((@a : ∏(@a : 𝒰 ){ 𝒰 ×@a }) ↦ @a, 1.868265711348081E-5),
Weighted((@a : 𝒰 ) ↦ (@a , @a), 5.088938816774152E-5),
Weighted((((__1_1 , __1_2) , __2) : 𝒰 ×𝒰 ×(𝒰 → 𝒰 )) ↦ 𝒰 , 1.6162528038990986E-5),
Weighted((@a : 𝒰 ) ↦ (_ : (𝒰 → @a)) ↦ 𝒰 , 5.7080968568555135E-5),
Weighted((@a : 𝒰 ) ↦ (_ : (@a → @a)) ↦ 𝒰 , 3.4947531776666405E-5),
Weighted((_ : 𝒰 ) ↦ (_ : ∏(@b : 𝒰 ){ @b }) ↦ 𝒰 , 8.15442408122216E-5),
Weighted((_ : ∏(@a : 𝒰 ){ @a }) ↦ (_ : 𝒰 ) ↦ 𝒰 , 1.0972601302852661E-4),
Weighted(
(((@a_1_1 , @a_1_2) , @a_2) : (𝒰 → 𝒰 )×𝒰 ×𝒰 ) ↦ ((@a_1_1 , @a_1_2) , @a_2),
1.104989161849384E-5
),
Weighted(
((@a_1 , (@a_2_1 , @a_2_2)) : 𝒰 ×∑(@b : { @b }) ↦ (@a_1 , (@a_2_1 , @a_2_2)),
1.7806741960864288E-5
),
Weighted(((__1 , __2) : 𝒰 ×(𝒰 → 𝒰 )) ↦ 𝒰 , 1.2838746108731833E-4),
Weighted(((__1 , __2) : 𝒰 ×((𝒰 → 𝒰 ) → 𝒰 )) ↦ 𝒰 , 1.49785371268538E-5),
Weighted((_ : 𝒰 ) ↦ ((__1 , __2) : 𝒰 ×𝒰 ) ↦ 𝒰 , 7.434789406767466E-5),
Weighted(((__1 , __2) : 𝒰 ×𝒰 ) ↦ (_ : 𝒰 ) ↦ 𝒰 , 1.414581859196728E-4),
Weighted(((@a_1 , @a_2) : ∑(@a : { @a }) ↦ (@a_1 , @a_2), 2.706772538895482E-4),
Weighted((@a : 𝒰 ) ↦ ((__1 , __2) : ∑(@b : { @b }) ↦ @a, 1.9508193778690146E-5),
Weighted(((__1 , __2) : ∑(@a : { @a }) ↦ (@a : 𝒰 ) ↦ @a, 4.239700466872449E-5),
Weighted(((@a_1 , @a_2) : (𝒰 → 𝒰 )×(𝒰 → 𝒰 )) ↦ (@a_1 , @a_2), 1.088914968823132E-5),
Weighted((@a : ∏(@a : 𝒰 ){ @a×@a }) ↦ @a, 1.1438361498049473E-5),
Weighted((@a : ∏(@a : 𝒰 ){ @a }) ↦ @a, 5.24912194961889E-5),
Weighted(((__1 , __2) : 𝒰 ×𝒰 ) ↦ @a, 7.039458036969333E-5),
Weighted(
((@a_1 , (@a_2_1 , @a_2_2)) : ∑(@a : { @a×𝒰 }) ↦ (@a_1 , (@a_2_1 , @a_2_2)),
1.7806741960864288E-5
),
Weighted((_ : 𝒰 ) ↦ (@a : ∏(@b : 𝒰 ){ @b }) ↦ @a, 4.992504539523773E-5),
Weighted((@a : ∏(@a : 𝒰 ){ @a }) ↦ (_ : 𝒰 ) ↦ @a, 4.702543415508284E-5),
Weighted((_ : (𝒰 → 𝒰 )) ↦ @a, 1.8499153661335303E-4),
Weighted((_ : ∏(@b : 𝒰 ){ @b }) ↦ 𝒰 , 0.0012864813449930822),
Weighted(((__1 , (__2_1 , __2_2)) : 𝒰 ×𝒰 ×𝒰 ) ↦ 𝒰 , 6.786347213973834E-5),
Weighted(𝒰 , 0.6842153844698987),
Weighted((@a : 𝒰 ) ↦ ((__1 , __2) : 𝒰 ×@a) ↦ @a, 1.3655735645083106E-5),
Weighted(((__1 , (__2_1 , __2_2)) : ∑(@a : { 𝒰 ×@a }) ↦ 𝒰 , 2.9084345202745012E-5),
Weighted((_ : @a) ↦ @a, 1.4274863962795541E-4),
Weighted((_ : (𝒰 → 𝒰 )) ↦ (_ : (𝒰 → 𝒰 )) ↦ 𝒰 , 3.527359991948709E-5),
Weighted((@a : ∏(@a : 𝒰 ){ (@a → @a) }) ↦ @a, 4.1942359484037535E-5),
Weighted((@a : (∏(@a : 𝒰 ){ @a } → ∏(@a : 𝒰 ){ @a })) ↦ @a, 2.7907837998167127E-5),
Weighted((@a : (𝒰 → ∏(@b : 𝒰 ){ @b })) ↦ @a, 4.78123456776949E-5),
Weighted((@a : ∏(@a : 𝒰 ){ (𝒰 → @a) }) ↦ @a, 3.346864197438644E-5),
Weighted((@a : 𝒰 ) ↦ (_ : @a) ↦ (@a : @a) ↦ @a, 3.841128101966749E-5),
...
eqts: Set[GeneratorVariables.EquationTerm] = Set(
EquationTerm(
FinalVal(
InIsle(
Elem((@a : 𝒰 ) ↦ @a, Terms),
@a,
Island(AtCoord(FuncsWithDomain, 𝒰 :: HNil), ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
)
),
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
Product(
Coeff(
BaseThenCondition(
FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms),
Funcs,
Restrict(FuncOpt)
),
Funcs
),
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
FinalVal(
InIsle(
InIsle(
Elem(@a, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
),
@a,
Island(
AtCoord(FuncsWithDomain, 𝒰 :: HNil),
ConstRandVar(Terms),
AddVar(𝒰 , 0.3),
Lambda,
InIsle
)
)
)
)
)
)
)
),
EquationTerm(
FinalVal(
InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
...
In [8]:
fd.filter(_.typ == MP)
Out[8]:
res7: FiniteDistribution[Term] = FiniteDistribution(
Vector(
Weighted((@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), 0.027399963852253788)
)
)
In [9]:
val eqs = GeneratorVariables.Equation.group(eqts)
Out[9]:
eqs: Set[GeneratorVariables.Equation] = Set(
Equation(
FinalVal(
InIsle(
InIsle(
Elem(𝒰 , Terms),
@b,
Island(Terms, ConstRandVar(Terms), AddVar((𝒰 → 𝒰 ), 0.3), Lambda, InIsle)
),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((𝒰 → 𝒰 ), 0.3), Lambda, InIsle)
)
),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
Product(
Coeff(Init(Terms), Terms),
InitialVal(
InIsle(
InIsle(
Elem(𝒰 , Terms),
@b,
Island(Terms, ConstRandVar(Terms), AddVar((𝒰 → 𝒰 ), 0.3), Lambda, InIsle)
),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((𝒰 → 𝒰 ), 0.3), Lambda, InIsle)
)
)
)
)
)
),
Equation(
InitialVal(
InIsle(
InIsle(
Elem(@a, Terms),
(@a_1 , @a_2),
Island(Terms, ConstRandVar(Terms), AddVar(∑(@a : { @a }, 0.3), Lambda, InIsle)
),
@a,
Island(AtCoord(FuncsWithDomain, 𝒰 :: HNil), ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
)
),
Product(
Coeff(FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms), Terms),
Product(
...
In [10]:
import TermRandomVars._
Out[10]:
import TermRandomVars._
In [11]:
val mpProof = fd.support.find(_.typ == MP).get
Out[11]:
mpProof: Term = (@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a)
In [12]:
import GeneratorVariables._, Expression._
val pfVal = FinalVal(Elem(mpProof, Terms))
Out[12]:
import GeneratorVariables._
pfVal: FinalVal[Term] = FinalVal(
Elem((@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), Terms)
)
In [13]:
val mpEqs = eqs.find(_.lhs == pfVal)
Out[13]:
mpEqs: Option[Equation] = Some(
Equation(
FinalVal(Elem((@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), Terms)),
Sum(
Sum(
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
Product(
FinalVal(Elem(𝒰 , Typs)),
FinalVal(Elem((@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), Terms))
)
),
Product(
Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
Product(
FinalVal(Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, TargetTyps)),
FinalVal(
Elem(
(@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
)
)
)
)
),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
FinalVal(
InIsle(
Elem((@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
)
)
)
)
)
)
In [14]:
val mpEqTerms = Expression.sumTerms(mpEqs.get.rhs)
Out[14]:
mpEqTerms: Vector[Expression] = Vector(
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
Product(
FinalVal(Elem(𝒰 , Typs)),
FinalVal(Elem((@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), Terms))
)
),
Product(
Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
Product(
FinalVal(Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, TargetTyps)),
FinalVal(
Elem(
(@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
)
)
)
),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
FinalVal(
InIsle(
Elem((@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
)
)
)
)
In [15]:
mpEqTerms.size
Out[15]:
res14: Int = 3
In [16]:
val ats = eqs.map(_.rhs).flatMap(Expression.atoms)
Out[16]:
ats: Set[Expression] = Set(
InitialVal(
InIsle(
InIsle(
InIsle(
InIsle(
Elem(@b, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, 𝒰 :: HNil),
ConstRandVar(Terms),
AddVar(𝒰 , 0.3),
Lambda,
InIsle
)
),
@a,
Island(
AtCoord(TermsWithTyp, (@a → ((@a → @b) → @b)) :: HNil),
ConstRandVar(AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil)),
AddVar(@a, 0.3),
Lambda,
InIsle
)
),
@b,
Island(
AtCoord(TermsWithTyp, ∏(B : 𝒰 ){ (@a → ((@a → B) → B)) } :: HNil),
PiOutput(∏(B : 𝒰 ){ (@a → ((@a → B) → B)) }),
AddVar(𝒰 , 0.3),
Lambda,
InIsle
)
),
@a,
Island(
AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
AddVar(𝒰 , 0.3),
Lambda,
InIsle
)
)
),
FinalVal(
InIsle(
InIsle(
InIsle(
InIsle(
...
In [17]:
val coeffs = ats.collect{case coeff @ Coeff(_, _) => coeff}
Out[17]:
coeffs: Set[Coeff[Any]] = Set(
Coeff(
BaseThenCondition(ZipMapOpt(UnifApplnOpt, TypFamilies, Terms, Terms), Typs, Restrict(TypOpt)),
Typs
),
Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs),
Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
Funcs,
Restrict(FuncOpt)
),
Funcs
),
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, TypFamilies, Terms),
TypFamilies,
Restrict(TypFamilyOpt)
),
TypFamilies
),
Coeff(
FlatMap(Typs, provingground.learning.TermGeneratorNodes$$Lambda$3760/965851966@772ff1b1, Typs),
Typs
),
Coeff(Init(Goals), Goals),
Coeff(FlatMap(Typs, LambdaTypFamilyIsle, TypFamilies), TypFamilies),
Coeff(
Map(
provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3771/1620514355@16c01a2,
Goals,
TargetTyps
),
TargetTyps
),
Coeff(
BaseThenCondition(
FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms),
Funcs,
Restrict(FuncOpt)
),
Funcs
),
Coeff(FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms), Terms),
Coeff(FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms), Terms),
Coeff(Init(Terms), Terms),
Coeff(Init(TypFamilies), TypFamilies),
...
In [18]:
val cs = coeffs.toVector.map(c => c.get(tg.nodeCoeffSeq) -> c.rv)
Out[18]:
cs: Vector[(Option[Double], RandomVar[Any])] = Vector(
(Some(0.1), Typs),
(Some(0.1), Funcs),
(Some(0.05), Terms),
(Some(0.1), Funcs),
(Some(0.1), TypFamilies),
(Some(0.1), Typs),
(Some(1.0), Goals),
(Some(0.1), TypFamilies),
(Some(0.5), TargetTyps),
(Some(0.1), Funcs),
(Some(0.1), Terms),
(Some(0.1), Terms),
(Some(0.55), Terms),
(Some(0.55), TypFamilies),
(Some(0.1), Terms),
(Some(0.1), Typs),
(Some(0.1), Terms),
(Some(0.05), Typs),
(Some(0.1), Funcs),
(Some(0.05), Funcs),
(Some(0.55), Funcs),
(Some(0.5), TargetTyps),
(Some(0.1), TypFamilies),
(Some(0.05), Typs),
(Some(0.05), TypFamilies),
(Some(0.1), TypFamilies),
(Some(0.5), TypsAndFamilies),
(Some(0.6), Typs),
(Some(0.5), TypsAndFamilies)
)
In [21]:
val target = Expression.varVals(mpEqTerms(1)).tail.head
Out[21]:
target: VarVal[Any] = FinalVal(
Elem(
(@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
)
)
In [27]:
val teqs = eqs.filter(_.lhs == target)
Out[27]:
teqs: Set[Equation] = Set(
Equation(
FinalVal(
Elem(
(@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
)
),
Product(
Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
FinalVal(
InIsle(
Elem(
(@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
AtCoord(TermsWithTyp, ∏(B : 𝒰 ){ (@a → ((@a → B) → B)) } :: HNil)
),
@a,
Island(
AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
AddVar(𝒰 , 0.3),
Lambda,
InIsle
)
)
)
)
)
)
In [28]:
teqs.size
Out[28]:
res27: Int = 1
In [ ]:
In [ ]:
Content source: siddhartha-gadgil/ProvingGround
Similar notebooks: