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 learning._
import library._, MonoidSimple._
Out[2]:
import provingground._ , interface._, HoTT._
import learning._
import library._, MonoidSimple._
In [ ]:
In [3]:
repl.pprinter.bind(translation.FansiShow.fansiPrint)
In [4]:
val tg = TermGenParams()
tg.nodeCoeffSeq
Out[4]:
tg: TermGenParams = TermGenParams(0.1, 0.1, 0.1, 0.1, 0.1, 0.05, 0.05, 0.05, 0.3, 0.7, 0.5)
res3_1: NodeCoeffSeq[TermState, Term, Double] = Cons(
BaseCons(
BasePi(provingground.learning.RandomVarFamily$$Lambda$2292/368952730@30d6b608, FuncsWithDomain),
0.55,
BaseCons(
BasePi(provingground.learning.GeneratorNode$$Lambda$2295/1777621063@ff038da, FuncsWithDomain),
0.1,
BaseCons(
BasePi(
provingground.learning.GeneratorNode$$Lambda$2295/1777621063@3c109d59,
FuncsWithDomain
),
0.1,
BaseCons(
BasePi(
provingground.learning.GeneratorNode$$Lambda$2295/1777621063@55e999c2,
FuncsWithDomain
),
0.1,
BaseCons(
BasePi(
provingground.learning.TermGeneratorNodes$$Lambda$2281/168572575@7d28562a,
FuncsWithDomain
),
0.1,
Target(FuncsWithDomain)
)
)
)
)
),
Cons(
BaseCons(
Map(
provingground.learning.TermRandomVars$TargetTyps$$$Lambda$2298/413538804@619b999d,
Goals,
TargetTyps
),
0.7,
BaseCons(
Map(
provingground.learning.TermRandomVars$TargetTyps$$$Lambda$2299/1742855736@64d6a6f1,
Typs,
TargetTyps
),
0.30000000000000004,
Target(TargetTyps)
)
),
...
In [5]:
val mfd = MonixFiniteDistributionEq(tg.nodeCoeffSeq)
val ts = TermState(dist1, dist1.map(_.typ))
Out[5]:
mfd: MonixFiniteDistributionEq[TermState, Term] = MonixFiniteDistributionEq(
Cons(
BaseCons(
BasePi(
provingground.learning.RandomVarFamily$$Lambda$2292/368952730@30d6b608,
FuncsWithDomain
),
0.55,
BaseCons(
BasePi(
provingground.learning.GeneratorNode$$Lambda$2295/1777621063@ff038da,
FuncsWithDomain
),
0.1,
BaseCons(
BasePi(
provingground.learning.GeneratorNode$$Lambda$2295/1777621063@3c109d59,
FuncsWithDomain
),
0.1,
BaseCons(
BasePi(
provingground.learning.GeneratorNode$$Lambda$2295/1777621063@55e999c2,
FuncsWithDomain
),
0.1,
BaseCons(
BasePi(
provingground.learning.TermGeneratorNodes$$Lambda$2281/168572575@7d28562a,
FuncsWithDomain
),
0.1,
Target(FuncsWithDomain)
)
)
)
)
),
Cons(
BaseCons(
Map(
provingground.learning.TermRandomVars$TargetTyps$$$Lambda$2298/413538804@619b999d,
Goals,
TargetTyps
),
0.7,
BaseCons(
Map(
provingground.learning.TermRandomVars$TargetTyps$$$Lambda$2299/1742855736@64d6a6f1,
...
ts: TermState = TermState(
FiniteDistribution(
Vector(
Weighted(e_l, 0.047619047619047616),
Weighted(e_r, 0.047619047619047616),
Weighted(mul, 0.047619047619047616),
Weighted(eqM, 0.047619047619047616),
Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.047619047619047616),
Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
Weighted(eqM, 0.2857142857142857),
Weighted(mul, 0.2857142857142857)
)
),
FiniteDistribution(
Vector(
Weighted(M, 0.047619047619047616),
Weighted(M, 0.047619047619047616),
Weighted((M → (M → M)), 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.047619047619047616),
Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
Weighted(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.047619047619047616),
Weighted(
∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
0.047619047619047616
),
Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.2857142857142857),
Weighted((M → (M → M)), 0.2857142857142857)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
)
In [6]:
import TermRandomVars._
val tsk = mfd.varDist(ts)(Terms, 0.001)
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$2530/1333989368@294e856f
)
import monix.execution.Scheduler.Implicits.global
In [7]:
val rp = tsk.runSyncUnsafe()
val eqs = rp._2
Out[7]:
rp: (FiniteDistribution[Term], Set[GeneratorVariables.EquationTerm]) = (
FiniteDistribution(
Vector(
Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.029778252577854582),
Weighted(mul(e_r)(e_l), 0.0053934227946860315),
Weighted(eqM(e_r)(e_r), 0.0053934227946860315),
Weighted((_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ eqM, 0.0011761943024481748),
Weighted((_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)}, 0.0011761943024481746),
Weighted((_ : ∏(a : M){ eqM(a)(a) }) ↦ mul, 0.0011761943024481748),
Weighted(eqM(e_r)(e_l), 0.0053934227946860315),
Weighted((_ : (M → (M → 𝒰 ))) ↦ axiom_{eqM(mul(a)(e_r))(a)}, 0.0011761943024481746),
Weighted(mul(e_r), 0.02478994011666693),
Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.029778252577854582),
Weighted((_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ mul, 0.0011761943024481748),
Weighted((@a : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ @a, 0.0015122498174333678),
Weighted((@a : (M → (M → 𝒰 ))) ↦ @a(e_r), 0.0023589908047798197),
Weighted((_ : (M → (M → 𝒰 ))) ↦ e_l, 0.0011761943024481746),
Weighted(eqM(e_l)(e_l), 0.0053934227946860315),
Weighted(
(_ : (M → (M → 𝒰 ))) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
0.0011761943024481746
),
Weighted((@a : (M → (M → 𝒰 ))) ↦ @a(e_l), 0.0023589908047798197),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}(e_r), 0.003541420016666704),
Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.029778252577854582),
Weighted(
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ mul,
0.0011761943024481748
),
Weighted(mul, 0.24983231236562614),
Weighted(eqM(e_r), 0.02478994011666693),
Weighted(
(@a : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ @a,
0.0015122498174333675
),
Weighted((_ : (M → (M → 𝒰 ))) ↦ eqM, 0.008233360117137222),
Weighted(axiom_{eqM(a)(a)}(e_r), 0.003541420016666704),
Weighted(
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ eqM,
0.0011761943024481748
),
Weighted((@a : M) ↦ @a, 0.0030244996348667355),
Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l), 0.003541420016666704),
Weighted((@a : (M → (M → 𝒰 ))) ↦ @a, 0.010585748722033573),
Weighted((@a : ∏(a : M){ eqM(a)(a) }) ↦ @a, 0.0015122498174333678),
Weighted((_ : (M → (M → M))) ↦ axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.0011761943024481746),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.029778252577854582),
Weighted(e_l, 0.033331339533166776),
Weighted(axiom_{eqM(a)(a)}, 0.029778252577854582),
...
eqs: Set[GeneratorVariables.EquationTerm] = Set(
EquationTerm(
FinalVal(
Elem(
Wrap((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
)
),
Product(
Coeff(
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
)
)
)
)
),
EquationTerm(
FinalVal(Elem((@a : (M → (M → M))) ↦ @a, Terms)),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
FinalVal(
InIsle(
Elem(@a, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
)
)
),
EquationTerm(
FinalVal(
...
In [8]:
eqs
Out[8]:
res7: Set[GeneratorVariables.EquationTerm] = Set(
EquationTerm(
FinalVal(
Elem(
Wrap((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
)
),
Product(
Coeff(
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
)
)
)
)
),
EquationTerm(
FinalVal(Elem((@a : (M → (M → M))) ↦ @a, Terms)),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
FinalVal(
InIsle(
Elem(@a, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
)
)
),
EquationTerm(
FinalVal(
...
In [9]:
val lefts = eqs.map(_.lhs)
lefts.size
Out[9]:
lefts: Set[GeneratorVariables.Expression] = Set(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
),
FinalVal(
...
res8_1: Int = 585
In [10]:
import GeneratorVariables._, Expression._
val eqgs = Equation.group(eqs)
Out[10]:
import GeneratorVariables._
eqgs: Set[Equation] = Set(
Equation(
FinalVal(
Elem(
Wrap((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
)
),
Product(
Coeff(
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
)
)
)
)
),
Equation(
FinalVal(
InIsle(
Elem(mul, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }, 0.3),
Lambda,
InIsle
)
)
),
Product(
...
In [11]:
eqgs.size
eqs.size
Out[11]:
res10_0: Int = 585
res10_1: Int = 809
In [12]:
eqgs.head
Out[12]:
res11: Equation = Equation(
FinalVal(
Elem(
Wrap((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
)
),
Product(
Coeff(
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
)
)
)
)
)
In [13]:
eqgs.map(_.rhs)
Out[13]:
res12: Set[Expression] = Set(
Sum(
Sum(
Product(
Product(Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms), FinalVal(Elem((M → (M → M)), Typs))),
FinalVal(Elem((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}, Terms))
),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
)
)
),
Product(
Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
)
)
),
Product(
Coeff(
FlatMap(
Typs,
provingground.learning.TermGeneratorNodes$$Lambda$2283/1598454918@70bec38a,
Typs
),
Typs
),
FinalVal(
InIsle(
Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
@a,
Island(Typs, ConstRandVar(Typs), AddVar((M → (M → 𝒰 )), 0.3), Sigma, InIsle)
)
)
),
Product(
Coeff(Init(Terms), Terms),
...
In [14]:
val rights = eqgs.map(_.rhs).flatMap(GeneratorVariables.Expression.varVals)
Out[14]:
rights: Set[VarVal[_]] = Set(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
InitialVal(
InIsle(
Elem(e_l, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
ConstRandVar(Terms),
...
In [15]:
val extras = rights -- lefts.flatMap(GeneratorVariables.Expression.varVals)
Out[15]:
extras: Set[VarVal[_]] = Set(
InitialVal(Elem(mul, Terms)),
InitialVal(Elem(e_r, Terms)),
InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)),
InitialVal(
Elem(
Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}),
AtCoord(FuncsWithDomain, M :: HNil)
)
),
InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(eqM, AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil))),
InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), Funcs)),
InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)),
InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }, Typs)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem((M → (M → M)), Typs)),
InitialVal(Elem(eqM, Terms)),
InitialVal(Elem(∏(a : M){ eqM(mul(a)(e_r))(a) }, Typs)),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), Funcs)),
InitialVal(Elem(Wrap(eqM), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, Typs)),
InitialVal(Elem(M, Typs)),
InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(mul), Funcs)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
InitialVal(Elem(Wrap(mul), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(∏(a : M){ eqM(a)(a) }, Typs)),
InitialVal(Elem(e_r, AtCoord(TermsWithTyp, M :: HNil))),
InitialVal(Elem(mul, AtCoord(TermsWithTyp, (M → (M → M)) :: HNil))),
InitialVal(Elem((M → (M → 𝒰 )), Typs)),
InitialVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil))),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)),
...
In [16]:
extras.size
Out[16]:
res15: Int = 46
In [17]:
lefts.size
rights.size
Out[17]:
res16_0: Int = 585
res16_1: Int = 459
In [18]:
lefts.take(20)
Out[18]:
res17: Set[Expression] = Set(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
),
FinalVal(
...
In [19]:
import GeneratorVariables.Expression.varVals
val egEq = eqgs.find(eq => varVals(eq.rhs).intersect(extras).nonEmpty)
Out[19]:
import GeneratorVariables.Expression.varVals
egEq: Option[Equation] = Some(
Equation(
InitialVal(
InIsle(
Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
@a,
Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
)
),
Product(
IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
)
)
)
In [20]:
egEq.get.lhs
Out[20]:
res19: Expression = InitialVal(
InIsle(
Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
@a,
Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
)
)
In [21]:
egEq.get.toString
Out[21]:
res20: String = "(P\u2080(InIsle((a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs,@a,Island(Typs,Typs,AddVar,Sigma,InIsle)))) == ((IsleScale(@a,(a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs)) * (P\u2080((a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs)))"
In [22]:
varVals(egEq.get.rhs)
varVals(egEq.get.rhs).intersect(extras)
Out[22]:
res21_0: Set[VarVal[_]] = Set(InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)))
res21_1: Set[VarVal[_]] = Set(InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)))
Note: This may not be an error as we may simply have too low cutoff to get any terms on the rhs.
As we see below (which will change after a corrections), most of the extras are initial values in islands, which should be paired with those outside.
In [23]:
val initExtras = extras.filter(_.isInstanceOf[InitialVal[_]])
Out[23]:
initExtras: Set[VarVal[_]] = Set(
InitialVal(Elem(mul, Terms)),
InitialVal(Elem(e_r, Terms)),
InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)),
InitialVal(
Elem(
Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}),
AtCoord(FuncsWithDomain, M :: HNil)
)
),
InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(eqM, AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil))),
InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), Funcs)),
InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)),
InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }, Typs)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem((M → (M → M)), Typs)),
InitialVal(Elem(eqM, Terms)),
InitialVal(Elem(∏(a : M){ eqM(mul(a)(e_r))(a) }, Typs)),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), Funcs)),
InitialVal(Elem(Wrap(eqM), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, Typs)),
InitialVal(Elem(M, Typs)),
InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(mul), Funcs)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
InitialVal(Elem(Wrap(mul), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(∏(a : M){ eqM(a)(a) }, Typs)),
InitialVal(Elem(e_r, AtCoord(TermsWithTyp, M :: HNil))),
InitialVal(Elem(mul, AtCoord(TermsWithTyp, (M → (M → M)) :: HNil))),
InitialVal(Elem((M → (M → 𝒰 )), Typs)),
InitialVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil))),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)),
...
In [24]:
initExtras.size
Out[24]:
res23: Int = 46
In [25]:
extras.size
Out[25]:
res24: Int = 46
In [26]:
lefts.filter(_.isInstanceOf[InitialVal[_]])
Out[26]:
res25: Set[Expression] = Set(
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
InitialVal(
InIsle(
Elem(e_l, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → 𝒰 )), 0.3),
Lambda,
InIsle
)
)
),
InitialVal(
InIsle(
Elem(Wrap(@a), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
InitialVal(
InIsle(
Elem(e_r, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(a)(a) }, 0.3), Lambda, InIsle)
)
),
InitialVal(
...
In [27]:
val linits = eqgs.filter(_.lhs.isInstanceOf[InitialVal[_]])
Out[27]:
linits: Set[Equation] = Set(
Equation(
InitialVal(
InIsle(
Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
@a,
Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
)
),
Product(
IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
)
),
Equation(
InitialVal(
InIsle(
Elem(e_r, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
)
)
),
Product(IsleScale(@a, Elem(e_r, Terms)), InitialVal(Elem(e_r, Terms)))
),
Equation(
InitialVal(
InIsle(
Elem(mul, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
)
)
),
Product(IsleScale(@a, Elem(mul, Terms)), InitialVal(Elem(mul, Terms)))
),
Equation(
InitialVal(
InIsle(
...
In [28]:
linits.size
Out[28]:
res27: Int = 164
In [29]:
linits.head.toString
Out[29]:
res28: String = "(P\u2080(InIsle((a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs,@a,Island(Typs,Typs,AddVar,Sigma,InIsle)))) == ((IsleScale(@a,(a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs)) * (P\u2080((a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs)))"
In [30]:
linits.head.rhs
Out[30]:
res29: Expression = Product(
IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
)
In [31]:
linits.head.lhs
Out[31]:
res30: Expression = InitialVal(
InIsle(
Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
@a,
Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
)
)
In [32]:
val termEqs = eqgs.collect{case Equation(FinalVal(Elem(t : Term, Terms)), rhs) => t -> rhs}
Out[32]:
termEqs: Set[(Term, Expression)] = Set(
(
(_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ eqM,
Sum(
Product(
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
FinalVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
),
FinalVal(Elem((_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ eqM, Terms))
),
Product(
Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
FinalVal(
InIsle(
Elem(eqM, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.3), Lambda, InIsle)
)
)
)
)
),
(
mul(e_r)(e_r),
Sum(
Product(
Product(
Coeff(FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms), Terms),
FinalVal(Elem(Wrap(mul(e_r)), Funcs))
),
FinalVal(Elem(e_r, AtCoord(TermsWithTyp, M :: HNil)))
),
Product(
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
FinalVal(Elem(Wrap(mul(e_r)), Funcs))
),
FinalVal(Elem(e_r, Terms))
)
)
),
(
axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r)(e_r)(axiom_{eqM(a)(a)}(e_r)),
Product(
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs))
),
...
In [33]:
termEqs.size
Out[33]:
res32: Int = 127
In [34]:
termEqs.map(_._1)
Out[34]:
res33: Set[Term] = Set(
axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
axiom_{(eqM(a)(b) \to eqM(b)(a))},
mul(e_r)(e_l),
eqM(e_r)(e_r),
(_ : M) ↦ e_r,
(_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ eqM,
(_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)},
(_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ axiom_{eqM(mul(a)(e_r))(a)},
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ e_l,
(_ : ∏(a : M){ eqM(a)(a) }) ↦ mul,
(_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ axiom_{eqM(mul(a)(e_r))(a)},
(_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ e_l,
eqM(e_r)(e_l),
(_ : (M → (M → 𝒰 ))) ↦ axiom_{eqM(mul(a)(e_r))(a)},
mul(e_r),
axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
(_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ mul,
(@a : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ @a,
(@a : (M → (M → 𝒰 ))) ↦ @a(e_r),
(_ : (M → (M → 𝒰 ))) ↦ e_l,
eqM(e_l)(e_l),
(_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ axiom_{eqM(mul(e_l)(a))(a)},
(_ : (M → (M → 𝒰 ))) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ axiom_{eqM(mul(a)(e_r))(a)},
(@a : (M → (M → 𝒰 ))) ↦ @a(e_l),
(_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ axiom_{(eqM(a)(b) \to eqM(b)(a))},
(_ : ∏(a : M){ eqM(a)(a) }) ↦ axiom_{eqM(a)(a)},
axiom_{eqM(mul(a)(e_r))(a)}(e_r),
axiom_{eqM(mul(e_l)(a))(a)},
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ mul,
mul,
eqM(e_r),
(@a : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ @a,
(_ : ∏(a : M){ eqM(a)(a) }) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
(_ : (M → (M → 𝒰 ))) ↦ eqM,
axiom_{eqM(a)(a)}(e_r),
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ eqM,
($tia : M) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(mul(e_l)(e_r))(e_l)($tia)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
(@a : M) ↦ @a,
($sxc : M) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_r)(e_r)($sxc)(axiom_{eqM(a)(a)}(e_r)),
axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l),
(_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
...
In [35]:
termEqs.map(_._1.typ).filter(tp => !isUniv(tp))
Out[35]:
res34: Set[Typ[U] forSome { type U >: x$1._1.type <: Term with Subs[U]; val x$1: (Term, Expression) }] = Set(
∏($tcy : M){ (eqM(e_l)($tcy) → eqM(mul(e_l)(e_l))($tcy)) },
eqM(e_r)(e_r),
eqM(mul(e_l)(e_r))(e_l),
(∏(a : M){ eqM(mul(e_l)(a))(a) } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
(∏(a : M){ eqM(a)(a) } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
(M → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
(∏(a : M){ eqM(mul(a)(e_r))(a) } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
((M → (M → M)) → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
((M → (M → 𝒰 )) → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
eqM(e_l)(e_l),
∏(a : M){ eqM(mul(e_l)(a))(a) },
(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → M),
(M → M),
(∏(a : M){ eqM(mul(a)(e_r))(a) } → M),
(∏(a : M){ eqM(mul(e_l)(a))(a) } → M),
(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } } → M),
(∏(a : M){ eqM(a)(a) } → M),
((M → (M → M)) → M),
((M → (M → 𝒰 )) → M),
eqM(mul(e_l)(e_l))(e_l),
((M → (M → M)) → (M → (M → M))),
(∏(a : M){ eqM(mul(a)(e_r))(a) } → (M → (M → M))),
(M → (M → (M → M))),
(∏(a : M){ eqM(a)(a) } → (M → (M → M))),
((M → (M → 𝒰 )) → (M → (M → M))),
(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → (M → (M → M))),
(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } } → (M → (M → M))),
(∏(a : M){ eqM(mul(e_l)(a))(a) } → (M → (M → M))),
(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
(∏(a : M){ eqM(mul(a)(e_r))(a) } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
(∏(a : M){ eqM(a)(a) } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
((M → (M → M)) → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
((M → (M → 𝒰 )) → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
(M → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
(∏(a : M){ eqM(mul(e_l)(a))(a) } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
∏($szu : M){ (eqM(e_r)($szu) → eqM(mul(e_l)(e_r))($szu)) },
∏($tia : M){ (eqM(e_l)($tia) → eqM(mul(e_l)(e_r))($tia)) },
M,
eqM(e_l)(mul(e_l)(e_r)),
((M → (M → M)) → (M → M)),
(M → (M → M)),
∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
...
In [36]:
val eqid = termEqs.find(_._1.typ == eqM(l)(op(l)(r)))
Out[36]:
eqid: Option[(Term, Expression)] = Some(
(
axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
Product(
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs))
),
FinalVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}(e_l), Terms))
)
)
)
This is a case of symmetry being applied, and presumably the equation is passed on too.
In [37]:
val eqid0 = termEqs.find(_._1.typ == eqM(op(l)(r))(l))
Out[37]:
eqid0: Option[(Term, Expression)] = Some(
(
axiom_{eqM(mul(a)(e_r))(a)}(e_l),
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Product(
Product(
Coeff(
BaseThenCondition(
ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil),
Filter(WithTyp((M → (M → 𝒰 ))))
),
AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil)
),
FinalVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs))
),
FinalVal(Elem(e_l, Terms))
),
Product(
Product(
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
AtCoord(TermsWithTyp, M :: HNil),
Filter(WithTyp(M))
),
AtCoord(TermsWithTyp, M :: HNil)
),
FinalVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs))
),
FinalVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil)))
)
),
Product(
Product(
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
Funcs,
Restrict(FuncOpt)
...
In [38]:
eqgs.find(eq => varVals(eq.rhs).intersect(extras).nonEmpty)
Out[38]:
res37: Option[Equation] = Some(
Equation(
InitialVal(
InIsle(
Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
@a,
Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
)
),
Product(
IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
)
)
)
In [39]:
val finExtras = extras -- initExtras
Out[39]:
finExtras: Set[VarVal[_]] = Set()
In [40]:
finExtras.size
Out[40]:
res39: Int = 0
In [41]:
val ats = eqs.map(_.rhs).flatMap(Expression.atoms)
Out[41]:
ats: Set[Expression] = Set(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
InitialVal(
InIsle(
Elem(e_l, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
ConstRandVar(Terms),
...
In [42]:
val coeffs = ats.collect{case coeff @ Coeff(_, _) => coeff}
Out[42]:
coeffs: Set[Coeff[Any]] = Set(
Coeff(
BaseThenCondition(
ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
AtCoord(TermsWithTyp, (M → (M → M)) :: HNil),
Filter(WithTyp((M → (M → M))))
),
AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
),
Coeff(
BaseThenCondition(ZipMapOpt(UnifApplnOpt, TypFamilies, Terms, Terms), Typs, Restrict(TypOpt)),
Typs
),
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
AtCoord(TermsWithTyp, M :: HNil),
Filter(WithTyp(M))
),
AtCoord(TermsWithTyp, M :: HNil)
),
Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs),
Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
Coeff(
FlatMap(Typs, provingground.learning.TermGeneratorNodes$$Lambda$2282/1458646167@3b664a79, Typs),
Typs
),
Coeff(
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
),
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
Funcs,
Restrict(FuncOpt)
),
Funcs
),
Coeff(
Init(AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)),
AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
),
...
In [43]:
val cs = coeffs.toVector.map(c => c.get(tg.nodeCoeffSeq) -> c.rv)
Out[43]:
cs: Vector[(Option[Double], RandomVar[Any])] = Vector(
(Some(0.1), AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)),
(Some(0.1), Typs),
(Some(0.1), AtCoord(TermsWithTyp, M :: HNil)),
(Some(0.1), Funcs),
(Some(0.05), Terms),
(Some(0.1), Typs),
(Some(0.1), AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)),
(Some(0.1), Funcs),
(Some(0.16500000000000004), AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)),
(Some(0.1), AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil)),
(Some(0.30000000000000004), TargetTyps),
(Some(0.1), AtCoord(TermsWithTyp, M :: HNil)),
(Some(0.1), Terms),
(Some(0.1), Terms),
(Some(0.55), Terms),
(Some(0.16500000000000004), AtCoord(TermsWithTyp, M :: HNil)),
(Some(0.55), TypFamilies),
(Some(0.1), Terms),
(Some(0.1), AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil)),
(Some(0.1), Typs),
(Some(0.1), AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil)),
(Some(0.55), AtCoord(FuncsWithDomain, M :: HNil)),
(Some(0.1), Terms),
(Some(0.1), AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)),
(Some(0.1), Funcs),
(Some(0.55), Funcs),
(Some(0.6), Typs),
(Some(0.16500000000000004), AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil)),
(Some(0.05), Typs)
)
In [44]:
val initEls = extras.collect{case el @ InitialVal(Elem(_, _)) => el}
Out[44]:
initEls: Set[InitialVal[Any]] = Set(
InitialVal(Elem(mul, Terms)),
InitialVal(Elem(e_r, Terms)),
InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)),
InitialVal(
Elem(
Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}),
AtCoord(FuncsWithDomain, M :: HNil)
)
),
InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(eqM, AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil))),
InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), Funcs)),
InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)),
InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }, Typs)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem((M → (M → M)), Typs)),
InitialVal(Elem(eqM, Terms)),
InitialVal(Elem(∏(a : M){ eqM(mul(a)(e_r))(a) }, Typs)),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs)),
InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), Funcs)),
InitialVal(Elem(Wrap(eqM), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, Typs)),
InitialVal(Elem(M, Typs)),
InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(mul), Funcs)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
InitialVal(Elem(Wrap(mul), AtCoord(FuncsWithDomain, M :: HNil))),
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(∏(a : M){ eqM(a)(a) }, Typs)),
InitialVal(Elem(e_r, AtCoord(TermsWithTyp, M :: HNil))),
InitialVal(Elem(mul, AtCoord(TermsWithTyp, (M → (M → M)) :: HNil))),
InitialVal(Elem((M → (M → 𝒰 )), Typs)),
InitialVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil))),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)),
...
In [45]:
extras -- initEls
Out[45]:
res44: Set[VarVal[_]] = Set()
In [46]:
val sd = implicitly[StateDistribution[TermState, FiniteDistribution]]
Out[46]:
sd: StateDistribution[TermState, FiniteDistribution] = provingground.learning.TermState$$anon$1@5311ab99
In [47]:
val zeroVals = initEls.filter{case InitialVal(Elem(x, rv)) => sd.value(ts)(rv)(x) == 0}
Out[47]:
zeroVals: Set[InitialVal[Any]] = Set(
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms))
)
In [48]:
val withZero = eqs.filter(eq => varVals(eq.rhs).intersect(zeroVals.map(x => x : VarVal[_])).nonEmpty)
Out[48]:
withZero: Set[EquationTerm] = Set(
EquationTerm(
InitialVal(
InIsle(
Elem(@a, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
Product(IsleScale(@a, Elem(@a, Terms)), InitialVal(Elem(@a, Terms)))
),
EquationTerm(
InitialVal(
InIsle(Elem(@a, Terms), @a, Island(Terms, ConstRandVar(Terms), AddVar(M, 0.3), Lambda, InIsle))
),
Product(IsleScale(@a, Elem(@a, Terms)), InitialVal(Elem(@a, Terms)))
),
EquationTerm(
InitialVal(
InIsle(
Elem(@a, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
)
),
Product(IsleScale(@a, Elem(@a, Terms)), InitialVal(Elem(@a, Terms)))
),
EquationTerm(
InitialVal(
InIsle(
Elem(@a, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.3), Lambda, InIsle)
)
),
Product(IsleScale(@a, Elem(@a, Terms)), InitialVal(Elem(@a, Terms)))
),
EquationTerm(
InitialVal(
InIsle(
Elem(@a, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → 𝒰 )), 0.3),
Lambda,
InIsle
)
...
In [49]:
val atoms = ats.union(lefts)
Out[49]:
atoms: Set[Expression] = Set(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
),
FinalVal(
...
In [50]:
import ExpressionEval._
Out[50]:
import ExpressionEval._
In [51]:
val init = initMap(atoms, tg, ts)
Out[51]:
init: Map[Expression, Double] = Map(
IsleScale(@a, Elem(mul, Terms)) -> 0.7,
InitialVal(Elem(mul, Terms)) -> 0.3333333333333333,
InitialVal(Elem(e_r, Terms)) -> 0.047619047619047616,
IsleScale(@a, Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), Funcs)) -> 0.7,
Coeff(
BaseThenCondition(
ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
AtCoord(TermsWithTyp, (M → (M → M)) :: HNil),
Filter(WithTyp((M → (M → M))))
),
AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
) -> 0.1,
Coeff(
BaseThenCondition(ZipMapOpt(UnifApplnOpt, TypFamilies, Terms, Terms), Typs, Restrict(TypOpt)),
Typs
) -> 0.1,
InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)) -> 0.047619047619047616,
InitialVal(
Elem(
Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}),
AtCoord(FuncsWithDomain, M :: HNil)
)
) -> 0.052631578947368425,
IsleScale(@a, Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)) -> 0.7,
InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)) -> 0.047619047619047616,
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
AtCoord(TermsWithTyp, M :: HNil),
Filter(WithTyp(M))
),
AtCoord(TermsWithTyp, M :: HNil)
) -> 0.1,
Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs) -> 0.1,
IsleScale(@a, Elem(e_l, Terms)) -> 0.7,
IsleScale(@a, Elem(eqM, Terms)) -> 0.7,
IsleScale(@a, Elem(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, Typs)) -> 0.7,
IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)) -> 0.7,
IsleScale(@a, Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)) -> 0.7,
InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), AtCoord(FuncsWithDomain, M :: HNil))) -> 0.052631578947368425,
IsleScale(@a, Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)) -> 0.7,
InitialVal(Elem(eqM, AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil))) -> 1.0,
IsleScale(@a, Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)) -> 0.7,
InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), Funcs)) -> 0.05263157894736841,
InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)) -> 0.047619047619047616,
...
In [52]:
init.size
Out[52]:
res51: Int = 187
In [53]:
val m2 = nextMap(init, eqgs)
Out[53]:
m2: Map[Expression, Double] = Map(
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.036842105263157884,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
InitialVal(
InIsle(
Elem(e_l, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → 𝒰 )), 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
IsleScale(@a, Elem(mul, Terms)) -> 0.7,
InitialVal(Elem(mul, Terms)) -> 0.3333333333333333,
FinalVal(Elem(mul, Terms)) -> 0.18333333333333335,
InitialVal(
InIsle(
Elem(Wrap(@a), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.3,
InitialVal(
InIsle(
Elem(e_r, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(a)(a) }, 0.3), Lambda, InIsle)
...
In [54]:
m2.size
Out[54]:
res53: Int = 387
In [55]:
val m3 = nextMap(m2, eqgs)
Out[55]:
m3: Map[Expression, Double] = Map(
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.036842105263157884,
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.020263157894736837,
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.01833333333333333,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
FinalVal(
InIsle(
Elem(e_l, Terms),
@a,
Island(
AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → 𝒰 )), 0.3),
...
In [56]:
m3.size
Out[56]:
res55: Int = 573
In [57]:
atoms.size
Out[57]:
res56: Int = 772
In [58]:
atoms -- m3.keys
Out[58]:
res57: Set[Expression] = Set(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
),
FinalVal(
Elem(
((M → (M → M)) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
),
FinalVal(
Elem(
($stt : M) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(mul(e_r)(e_r))(e_r)($stt)(axiom_{eqM(mul(a)(e_r))(a)}(e_r)),
Terms
)
),
FinalVal(Elem((_ : ∏(a : M){ eqM(a)(a) }) ↦ axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
FinalVal(Elem((_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(e_l)(a))(a)}(e_l), Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
FinalVal(
Elem(Wrap((_ : (M → (M → 𝒰 ))) ↦ e_r), AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil))
),
FinalVal(
InIsle(
Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r), Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
)
),
FinalVal(Elem((_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ mul, Terms)),
FinalVal(Elem((M → (M → 𝒰 ))×(M → (M → M)), Typs)),
FinalVal(Elem((_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)),
FinalVal(Elem((_ : M) ↦ e_r, Terms)),
FinalVal(
Elem((_ : ∏(a : M){ eqM(a)(a) }) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)
),
FinalVal(
Elem(
...
In [59]:
m2.values.toSet
Out[59]:
res58: Set[Double] = Set(
0.057142857142857134,
0.028947368421052635,
0.16500000000000004,
0.3,
0.6,
0.028571428571428567,
1.0,
0.09523809523809523,
0.033333333333333326,
0.06666666666666665,
0.052631578947368425,
0.047619047619047616,
0.3333333333333333,
0.08250000000000002,
0.7,
0.05,
0.1,
0.5,
0.18333333333333335,
0.36842105263157887,
0.19999999999999998,
0.55,
0.028947368421052628,
0.05263157894736841,
0.20263157894736838,
0.2578947368421052,
0.036842105263157884,
0.2333333333333333,
0.4285714285714286,
0.3684210526315789,
0.2026315789473684,
0.02619047619047619,
0.30000000000000004
)
In [60]:
init.filter(_._1.isInstanceOf[Coeff[_]])
Out[60]:
res59: Map[Expression, Double] = Map(
Coeff(
BaseThenCondition(
ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
AtCoord(TermsWithTyp, (M → (M → M)) :: HNil),
Filter(WithTyp((M → (M → M))))
),
AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
) -> 0.1,
Coeff(
BaseThenCondition(ZipMapOpt(UnifApplnOpt, TypFamilies, Terms, Terms), Typs, Restrict(TypOpt)),
Typs
) -> 0.1,
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
AtCoord(TermsWithTyp, M :: HNil),
Filter(WithTyp(M))
),
AtCoord(TermsWithTyp, M :: HNil)
) -> 0.1,
Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs) -> 0.1,
Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms) -> 0.05,
Coeff(
FlatMap(Typs, provingground.learning.TermGeneratorNodes$$Lambda$2282/1458646167@3b664a79, Typs),
Typs
) -> 0.1,
Coeff(
Island(
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
ConstRandVar(Terms),
AddVar((M → (M → M)), 0.3),
Lambda,
InIsle
),
AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
) -> 0.1,
Coeff(
BaseThenCondition(
FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
Funcs,
Restrict(FuncOpt)
),
Funcs
) -> 0.1,
Coeff(
Init(AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)),
AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
...
In [61]:
val m4 = nextMap(m3, eqgs)
Out[61]:
m4: Map[Expression, Double] = Map(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.0165,
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.036842105263157884,
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.020263157894736837,
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.01833333333333333,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
) -> 0.0019999999999999996,
FinalVal(
...
In [62]:
m4.size
Out[62]:
res61: Int = 757
In [63]:
val m5 = nextMap(m4, eqgs)
Out[63]:
m5: Map[Expression, Double] = Map(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.01652355461584635,
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.036842105263157884,
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.020263157894736837,
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.01833333333333333,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
) -> 0.0019999999999999996,
FinalVal(
...
In [64]:
m5.size
Out[64]:
res63: Int = 768
In [65]:
atoms -- m5.keySet
Out[65]:
res64: Set[Expression] = Set(
FinalVal(Elem((@a : (M → (M → M))) ↦ @a(e_r), Terms)),
FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a(e_r), Terms)),
FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a(e_l), Terms)),
FinalVal(Elem((@a : (M → (M → M))) ↦ @a(e_l), Terms))
)
In [66]:
val zeroE = eqgs.filter(eq => !m5.keySet(eq.lhs))
Out[66]:
zeroE: Set[Equation] = Set(
Equation(
FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a(e_l), Terms)),
Product(
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
),
FinalVal(Elem(e_l, Terms))
)
),
Equation(
FinalVal(Elem((@a : (M → (M → M))) ↦ @a(e_l), Terms)),
Product(
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
FinalVal(Elem(Wrap((@a : (M → (M → M))) ↦ @a), Funcs))
),
FinalVal(Elem(e_l, Terms))
)
),
Equation(
FinalVal(Elem((@a : (M → (M → M))) ↦ @a(e_r), Terms)),
Product(
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
FinalVal(Elem(Wrap((@a : (M → (M → M))) ↦ @a), Funcs))
),
FinalVal(Elem(e_r, Terms))
)
),
Equation(
FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a(e_r), Terms)),
Product(
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
),
FinalVal(Elem(e_r, Terms))
)
)
)
In [67]:
zeroE.head.rhs
Out[67]:
res66: Expression = Product(
Product(
Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
),
FinalVal(Elem(e_l, Terms))
)
In [68]:
val x = Expression.atoms(zeroE.head.rhs).filter(exp => recExp(m4, exp) == 0).head
Out[68]:
x: Expression = FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
In [69]:
eqgs.find(_.lhs == x)
Out[69]:
res68: Option[Equation] = Some(
Equation(
FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs)),
Quotient(
FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a, Terms)),
FinalVal(Event(Terms, Restrict(FuncOpt)))
)
)
)
In [70]:
val ts = Expression.atoms(eqgs.find(_.lhs == x).get.rhs).toVector
Out[70]:
ts: Vector[Expression] = Vector(
FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a, Terms)),
FinalVal(Event(Terms, Restrict(FuncOpt)))
)
In [71]:
ts.map(m4.get(_))
Out[71]:
res70: Vector[Option[Double]] = Vector(Some(0.033), None)
In [72]:
val eventEq = eqgs.find(_.lhs == ts(1)).get
Out[72]:
eventEq: Equation = Equation(
FinalVal(Event(Terms, Restrict(FuncOpt))),
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r)), Funcs)),
FinalVal(Elem(Wrap(eqM(e_l)), Funcs))
),
FinalVal(Elem(Wrap(eqM(e_r)), Funcs))
),
FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_r)), Funcs))
),
FinalVal(Elem(Wrap(mul(e_l)), Funcs))
),
FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_l)), Funcs))
),
FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l)), Funcs))
),
FinalVal(Elem(Wrap(mul(e_r)), Funcs))
),
Sum(
FinalVal(Elem(Wrap((@a : (M → (M → M))) ↦ @a), Funcs)),
FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
)
),
Sum(
Sum(
Sum(FinalVal(Elem(Wrap(mul(e_l)), Funcs)), FinalVal(Elem(Wrap(eqM(e_l)), Funcs))),
FinalVal(Elem(Wrap(mul(e_r)), Funcs))
),
FinalVal(Elem(Wrap(eqM(e_r)), Funcs))
)
)
)
In [73]:
val m6 = nextMap(m5, eqgs)
Out[73]:
m6: Map[Expression, Double] = Map(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.016535378155739335,
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.036842105263157884,
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.020263157894736837,
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.01833333333333333,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
) -> 0.0019999999999999996,
FinalVal(
...
In [74]:
m6.size
Out[74]:
res73: Int = 772
In [75]:
atoms -- m6.keySet
Out[75]:
res74: Set[Expression] = Set()
In [76]:
val ms = stableSupportMap(init, eqgs)
Out[76]:
ms: Map[Expression, Double] = Map(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.016541309982685166,
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.036842105263157884,
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.020263157894736837,
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.01833333333333333,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
) -> 0.0019999999999999996,
FinalVal(
...
In [77]:
val m100 = iterateMap(ms, eqgs, 100)
Out[77]:
m100: Map[Expression, Double] = Map(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.016547277936962753,
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.036842105263157884,
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.020263157894736837,
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.01833333333333333,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
) -> 0.0019999999999999996,
FinalVal(
...
In [78]:
val m200 = iterateMap(m100, eqgs, 100)
Out[78]:
m200: Map[Expression, Double] = Map(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.016547277936962753,
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.036842105263157884,
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 0.020263157894736837,
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.01833333333333333,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> 0.033333333333333326,
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
) -> 0.0019999999999999996,
FinalVal(
...
In [79]:
mapRatio(m100, m200)
Out[79]:
res78: Double = 1.0000000000000009
In [80]:
mapRatio(ms, m100)
Out[80]:
res79: Double = 2.0112732240884026
In [81]:
zeroVals
Out[81]:
res80: Set[InitialVal[Any]] = Set(
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(Wrap(@a), Funcs)),
InitialVal(Elem(@a, Terms)),
InitialVal(Elem(@a, Terms))
)
In [82]:
zeroVals.map{case InitialVal(elem : Elem[_]) => isIsleVar(elem)}
Out[82]:
res81: Set[Boolean] = Set(true)
In [83]:
val ins = TermState(dist1, dist1.map(_.typ))
val fsT = tg.nextStateTask(ins, 0.001)
val fs = fsT.runSyncUnsafe()
Out[83]:
ins: TermState = TermState(
FiniteDistribution(
Vector(
Weighted(e_l, 0.047619047619047616),
Weighted(e_r, 0.047619047619047616),
Weighted(mul, 0.047619047619047616),
Weighted(eqM, 0.047619047619047616),
Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.047619047619047616),
Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
Weighted(eqM, 0.2857142857142857),
Weighted(mul, 0.2857142857142857)
)
),
FiniteDistribution(
Vector(
Weighted(M, 0.047619047619047616),
Weighted(M, 0.047619047619047616),
Weighted((M → (M → M)), 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.047619047619047616),
Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
Weighted(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.047619047619047616),
Weighted(
∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
0.047619047619047616
),
Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.2857142857142857),
Weighted((M → (M → M)), 0.2857142857142857)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
)
fsT: monix.eval.Task[TermState] = FlatMap(
FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$2530/1333989368@2030de41),
provingground.learning.TermGenParams$$Lambda$3341/1899735046@45f00ab8
)
fs: TermState = TermState(
FiniteDistribution(
Vector(
Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.029778252577854582),
Weighted(mul(e_r)(e_l), 0.0053934227946860315),
Weighted(eqM(e_r)(e_r), 0.0053934227946860315),
Weighted((_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ eqM, 0.0011761943024481748),
Weighted((_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)}, 0.0011761943024481746),
Weighted((_ : ∏(a : M){ eqM(a)(a) }) ↦ mul, 0.0011761943024481748),
Weighted(eqM(e_r)(e_l), 0.0053934227946860315),
Weighted((_ : (M → (M → 𝒰 ))) ↦ axiom_{eqM(mul(a)(e_r))(a)}, 0.0011761943024481746),
Weighted(mul(e_r), 0.02478994011666693),
Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.029778252577854582),
Weighted((_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ mul, 0.0011761943024481748),
Weighted((@a : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ @a, 0.0015122498174333678),
Weighted((@a : (M → (M → 𝒰 ))) ↦ @a(e_r), 0.0023589908047798197),
Weighted((_ : (M → (M → 𝒰 ))) ↦ e_l, 0.0011761943024481746),
Weighted(eqM(e_l)(e_l), 0.0053934227946860315),
Weighted(
(_ : (M → (M → 𝒰 ))) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
0.0011761943024481746
),
Weighted((@a : (M → (M → 𝒰 ))) ↦ @a(e_l), 0.0023589908047798197),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}(e_r), 0.003541420016666704),
Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.029778252577854582),
Weighted(
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ mul,
0.0011761943024481748
),
Weighted(mul, 0.24983231236562614),
Weighted(eqM(e_r), 0.02478994011666693),
Weighted(
(@a : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ @a,
0.0015122498174333675
),
Weighted((_ : (M → (M → 𝒰 ))) ↦ eqM, 0.008233360117137222),
Weighted(axiom_{eqM(a)(a)}(e_r), 0.003541420016666704),
Weighted(
(_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ eqM,
0.0011761943024481748
),
Weighted((@a : M) ↦ @a, 0.0030244996348667355),
Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l), 0.003541420016666704),
Weighted((@a : (M → (M → 𝒰 ))) ↦ @a, 0.010585748722033573),
Weighted((@a : ∏(a : M){ eqM(a)(a) }) ↦ @a, 0.0015122498174333678),
Weighted((_ : (M → (M → M))) ↦ axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.0011761943024481746),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.029778252577854582),
Weighted(e_l, 0.033331339533166776),
Weighted(axiom_{eqM(a)(a)}, 0.029778252577854582),
...
In [84]:
val expEv = ExpressionEval.fromStates(ins, fs, eqgs, tg)
Out[84]:
expEv: ExpressionEval = ExpressionEval(
TermState(
FiniteDistribution(
Vector(
Weighted(e_l, 0.047619047619047616),
Weighted(e_r, 0.047619047619047616),
Weighted(mul, 0.047619047619047616),
Weighted(eqM, 0.047619047619047616),
Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.047619047619047616),
Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
Weighted(eqM, 0.2857142857142857),
Weighted(mul, 0.2857142857142857)
)
),
FiniteDistribution(
Vector(
Weighted(M, 0.047619047619047616),
Weighted(M, 0.047619047619047616),
Weighted((M → (M → M)), 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.047619047619047616),
Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
Weighted(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.047619047619047616),
Weighted(
∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
0.047619047619047616
),
Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
Weighted((M → (M → 𝒰 )), 0.2857142857142857),
Weighted((M → (M → M)), 0.2857142857142857)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
),
TermState(
FiniteDistribution(
Vector(
Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.029778252577854582),
Weighted(mul(e_r)(e_l), 0.0053934227946860315),
Weighted(eqM(e_r)(e_r), 0.0053934227946860315),
Weighted((_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ eqM, 0.0011761943024481748),
Weighted((_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)}, 0.0011761943024481746),
...
In [85]:
expEv.hExp
Out[85]:
res84: Expression = Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Sum(
Product(
Product(InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)), Literal(-1.0)),
Log(InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)))
),
Product(
Product(
InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)),
Literal(-1.0)
),
Log(InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)))
)
),
Product(
Product(InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)), Literal(-1.0)),
Log(InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)))
)
),
Product(
Product(InitialVal(Elem(mul, Terms)), Literal(-1.0)),
Log(InitialVal(Elem(mul, Terms)))
)
),
Product(
Product(InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)), Literal(-1.0)),
Log(InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)))
)
),
Product(
Product(InitialVal(Elem(e_l, Terms)), Literal(-1.0)),
Log(InitialVal(Elem(e_l, Terms)))
)
),
Product(
Product(InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)), Literal(-1.0)),
Log(InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)))
)
),
Product(Product(InitialVal(Elem(eqM, Terms)), Literal(-1.0)), Log(InitialVal(Elem(eqM, Terms))))
),
Product(Product(InitialVal(Elem(e_r, Terms)), Literal(-1.0)), Log(InitialVal(Elem(e_r, Terms))))
)
In [86]:
val v = expEv.entropyProjection()(m200)
Out[86]:
v: Vector[Double] = Vector(
-4.9763786428984865E-8,
4.304068722953969E-4,
7.825579496279935E-4,
-0.007865854590058665,
-0.0043262200245322785,
-6.6252189744191E-8,
-6.625218974419076E-8,
-7.330142310666104E-5,
-0.0038753621373031275,
-0.007046112976914767,
-4.326220024532279E-4,
-9.225422040748262E-4,
-1.8508707244961254E-4,
-3.875362137303129E-4,
-0.01104766870010009,
-0.01935346292461547,
1.7524021516971672E-6,
3.1861857303584815E-6,
-0.007046112976914766,
-0.003875362137303117,
-1.7822492002662562E-4,
-7.843743637793382E-4,
-7.819762275242176E-6,
-0.005535136690582533,
-0.010065875681306813,
-4.3262200245322737E-4,
-3.875362137303143E-4,
-4.3262200245322764E-4,
-8.184021850128861E-5,
-0.0061803143207604045,
-0.011236935128655237,
-7.843743637793366E-4,
-0.004326220024532275,
-0.007865854590058684,
1.2054336828801602E-4,
2.1916976052367254E-4,
4.739556688640917E-10,
8.61737579752899E-10,
-0.004326220024532278,
-0.007865854590058676,
-3.46170946598965E-4,
-0.007865854590058667,
-0.004326220024532272,
-0.003196253246208674,
-0.001357545744697577,
-0.002468264990359229,
-9.225422040748282E-4,
-6.625218974419083E-7,
...
In [87]:
val grad = expEv.variableIndex.mapValues(j => v(j))
Out[87]:
grad: Map[Expression, Double] = Map(
FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> -4.9763786428984865E-8,
FinalVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 4.304068722953969E-4,
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
) -> 7.825579496279935E-4,
InitialVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> -0.007865854590058665,
FinalVal(
InIsle(
Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
) -> -0.0043262200245322785,
FinalVal(
Elem(
((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
Typs
)
) -> -6.6252189744191E-8,
FinalVal(
...
In [88]:
grad.toVector.sortBy{case (_, p) => - math.abs(p)}
Out[88]:
res87: Vector[(Expression, Double)] = Vector(
(InitialVal(Elem(eqM, Terms)), -0.019353462924615473),
(InitialVal(Elem(mul, Terms)), -0.01935346292461547),
(
InitialVal(
InIsle(Elem(eqM, Terms), @a, Island(Terms, ConstRandVar(Terms), AddVar(M, 0.3), Lambda, InIsle))
),
-0.013547424047230871
),
(
InitialVal(
InIsle(
Elem(mul, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.3), Lambda, InIsle)
)
),
-0.013547424047230843
),
(
InitialVal(
InIsle(
Elem(mul, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(a)(a) }, 0.3), Lambda, InIsle)
)
),
-0.013547424047230833
),
(
InitialVal(
InIsle(
Elem(mul, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
InIsle
)
)
),
-0.013547424047230833
),
(
InitialVal(
InIsle(
Elem(eqM, Terms),
...
In [89]:
expEv.jet(m200)(expEv.hExp)
Out[89]:
res88: spire.math.Jet[Double] = Jet(
3.119162312519754,
Array(
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.07671320486001368,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.07671320486001368,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.07671320486001368,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
-0.0,
...
In [90]:
expEv.jet(m200)(expEv.klExp)
Out[90]:
res89: spire.math.Jet[Double] = Jet(
-1.9624979394717363,
Array(
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
-9.191501396401179E-4,
0.0,
0.0,
-0.12439165223129593,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
-9.191501396401179E-4,
0.0,
-0.005923412011014092,
0.0,
0.0,
0.0,
0.0,
0.0,
-0.017770236033042276,
0.0,
-9.191501396401179E-4,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
0.0,
-0.018838158871566455,
0.0,
0.0,
...
In [91]:
import spire.algebra._
import spire.implicits._
v.norm
Out[91]:
import spire.algebra._
import spire.implicits._
res90_2: Double = 0.1112345315327967
In [92]:
val vv = expEv.entropyProjection()(expEv.finalDist)
Out[92]:
vv: Vector[Double] = Vector(
-4.9763786428984865E-8,
4.304068722953969E-4,
7.825579496279935E-4,
-0.007865854590058665,
-0.0043262200245322785,
-6.6252189744191E-8,
-6.625218974419076E-8,
-7.330142310666104E-5,
-0.0038753621373031275,
-0.007046112976914767,
-4.326220024532279E-4,
-9.225422040748262E-4,
-1.8508707244961254E-4,
-3.875362137303129E-4,
-0.01104766870010009,
-0.01935346292461547,
1.7524021516971672E-6,
3.1861857303584815E-6,
-0.007046112976914766,
-0.003875362137303117,
-1.7822492002662562E-4,
-7.843743637793382E-4,
-7.819762275242176E-6,
-0.005535136690582533,
-0.010065875681306813,
-4.3262200245322737E-4,
-3.875362137303143E-4,
-4.3262200245322764E-4,
-8.184021850128861E-5,
-0.0061803143207604045,
-0.011236935128655237,
-7.843743637793366E-4,
-0.004326220024532275,
-0.007865854590058684,
1.2054336828801602E-4,
2.1916976052367254E-4,
4.739556688640917E-10,
8.61737579752899E-10,
-0.004326220024532278,
-0.007865854590058676,
-3.46170946598965E-4,
-0.007865854590058667,
-0.004326220024532272,
-0.003196253246208674,
-0.001357545744697577,
-0.002468264990359229,
-9.225422040748282E-4,
-6.625218974419083E-7,
...
In [93]:
vv.norm
Out[93]:
res92: Double = 0.1112345315327967
In [94]:
val best = expEv.vars.zipWithIndex.sortBy{case (v, n) => -vv(n)}.map{case (v, n) => (v, vv(n))}
Out[94]:
best: Vector[(Expression, Double)] = Vector(
(FinalVal(Elem(Wrap((@a : (M → (M → M))) ↦ @a), Funcs)), 0.0030554265290708275),
(FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs)), 0.0030554265290708062),
(InitialVal(Elem(Wrap(eqM), Funcs)), 0.0016881778689094718),
(
InitialVal(
InIsle(
Elem(Wrap(eqM), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
0.0011817245082366306
),
(
InitialVal(
InIsle(
Elem(Wrap(eqM), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
)
),
0.001181724508236628
),
(
InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs)),
0.0011179399280399904
),
(InitialVal(Elem(Wrap(mul), Funcs)), 0.0011032460029815274),
(FinalVal(Elem(Wrap(eqM), Funcs)), 9.284978279002059E-4),
(InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)), 8.074382773262631E-4),
(
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
)
),
7.825579496279936E-4
),
(
InitialVal(
InIsle(
Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
)
),
...
In [95]:
best.reverse
Out[95]:
res94: Vector[(Expression, Double)] = Vector(
(InitialVal(Elem(eqM, Terms)), -0.019353462924615473),
(InitialVal(Elem(mul, Terms)), -0.01935346292461547),
(
InitialVal(
InIsle(Elem(eqM, Terms), @a, Island(Terms, ConstRandVar(Terms), AddVar(M, 0.3), Lambda, InIsle))
),
-0.013547424047230871
),
(
InitialVal(
InIsle(
Elem(mul, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.3), Lambda, InIsle)
)
),
-0.013547424047230843
),
(
InitialVal(
InIsle(
Elem(eqM, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
)
),
-0.013547424047230833
),
(
InitialVal(
InIsle(
Elem(eqM, Terms),
@a,
Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.3), Lambda, InIsle)
)
),
-0.013547424047230833
),
(
InitialVal(
InIsle(
Elem(mul, Terms),
@a,
Island(
Terms,
ConstRandVar(Terms),
AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
Lambda,
...
In [ ]:
Content source: siddhartha-gadgil/ProvingGround
Similar notebooks: